{'fraction_non_alphanumeric': 0.054623102165141074, 'fraction_numerical': 0.014397638598860122, 'mean_word_length': 3.9837245696400627, 'pattern_counts': {'":': 0, '<': 4, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 41, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The polyhedral geometry of Wajsberg hoops

We show that the category of finitely presented Wajsberg hoops with homomorphisms is dually equivalent to a particular subcategory of rational polyhedra with Z-maps. We use the duality to provide a geometrical characterization of finitely generated projective and exact Wajsberg hoops. As applications, we study logical properties of the positive fragment of Lukasiewicz logic. We show that, while deducibility in the fragment is equivalent to deducibility among positive formulas in Lukasiewicz logic, the same is not true for admissibility of rules. Moreover, we show that the unification type of Wajsberg hoops is nullary, while the exact unification type is unitary, therefore showing decidability of admissible rules in the fragment.


Introduction
Residuated structures arise naturally in the study of various algebraic systems, such as ideals of rings [45] or lattice-ordered groups [8], and have acquired a particular relevance in algebraic logic. Most notably, they encompass the equivalent algebraic semantics in the sense of Blok-Pigozzi [13] of so-called substructural logics [25]. The latter are a large class of logical systems including classical logic and several of the most interesting non-classical logics, such as intuitionistic logic, fuzzy logics, and relevance logics to name a few. Algebraizabilityà la Blok-Pigozzi entails that the deducibility relation of an algebraizable logic can be characterized by means of the algebraic equational consequence of its equivalent algebraic semantics. Therefore, interesting properties of algebraizable logics can be studied via algebraic means (for details on algebraizability and a collection of general results on substructural logics see [25]).
Hoops are a particular variety of residuated monoids related to logic which were defined in an unpublished manuscript by Büchi and Owens, inspired by the work of Bosbach on partially ordered monoids [12]. Hoops indeed correspond to commutative monoids endowed with a partial order ≤ definable by means of the residuum → of the monoid operation as a ≤ b if and only if a → b = 1, and such an order is natural, in the sense that a ≤ b if and only if there exists c such that a = b · c. The first systematic study of hoops has been carried out by Ferreirim in her PhD thesis [21] and in her works with Blok [10,11], while in her work with Aglianò and Montagna [2] they investigate the connection between hoops and fuzzy logics.
Wajsberg hoops play a special role in this framework. From the algebraic point of view, they can be used to describe subdirectly irreducible hoops, and the whole variety of hoops can be obtained as the join of iterated powers of the variety of Wajsberg hoops, in the sense defined in [11]. Wajsberg hoops also have a peculiar connection with lattice-ordered abelian groups (abelian ℓ-groups for short). In fact, the variety WH of Wajsberg hoops is generated by its totally ordered members, that are, in loose terms, either negative cones of abelian ℓ-groups, or intervals of abelian ℓ-groups [4].
Besides their purely algebraic interest, Wajsberg hoops are relevant structures in the realm of algebraic logic. Indeed, they are term-equivalent to the 0-free subreducts of MV-algebras, the equivalent algebraic semantics of the infinite-valued Lukasiewicz logic, seen as residuated lattices. Therefore, WH is the equivalent algebraic semantics of the positive (i.e., 0-free) fragment of the infinite-valued Lukasiewicz logic L, the latter seen as an extension of the Full Lambek Calculus with exchange FL e , (thus in the language with constants 0, 1 and binary connectives ∧, ∨, ·, →, see [25]) . We could actually rephrase the representation of totally ordered Wajsberg hoops in terms possibly more familiar to the reader expert in many-valued logics. Namely, totally ordered Wajsberg hoops are either cancellative hoops, i.e. hoops where the monoidal operation satisfies the cancellativity law, or MV-algebras, whose representation in terms of intervals of abelian ℓgroups with strong unit actually lifts to a categorical equivalence via the well-known Mundici's functor [40].
In the context of the algebraic semantics of many-valued logics, the relevance of Wajsberg hoops is also related to the study of the equivalent algebraic semantics of Hájek Basic Logic and its positive subreducts (BL-algebras and basic hoops). Given the well-known decomposition result in terms of Wajsberg hoops for totally ordered BL-algebras given by Aglianò and Montagna [3], and the representation of free BL-algebras in [7] building on this result, the understanding of Wajsberg hoops is key to obtain interesting results in this framework.
The categorical approach in studying varieties connected to Wajsberg hoops and MValgebras has shown to be fruitful in finding interesting connections with categories of ℓ-groups [1,20,24,40]. Moreover, both abelian ℓ-groups and abelian ℓ-groups with strong order unit (equivalently, MV-algebras), enjoy a deep connection with geometrical objects. In particular, finitely presented structures are dually equivalent, respectively, to categories whose objects are closed polyhedral cones [9] and rational polyhedra [34]. In the case of MV-algebras, the geometrical approach has allowed the investigation of logical properties of Lukasiewicz logic (see for instance [42,34]).
In this contribution we will show that finitely presented Wajsberg hoops have an interesting geometrical dual as well, in particular, with what we will call pointed rational polyhedra. More precisely, we show how finitely presented Wajsberg hoops are dually equivalent to a (non-full) subcategory of rational polyhedra with Z-maps, given by rational polyhedra in unit cubes [0, 1] n that contain the lattice point 1 = (1, . . . , 1), and pointed Z-maps, that are Z-maps that respect the lattice point 1. In particular, we obtain this result by first demonstrating that Wajsberg hoops are equivalent to a subcategory of finitely presented MV-algebras, that we shall call in what follows positive, and then suitably restricting the Marra-Spada duality [34].
The first geometrical approach to the study of Wajsberg hoops is in [4], which contains a key step to understand the geometrical duality, that is, the description of the free n-generated Wajsberg hoop as a particular subreduct of the free MV-algebra over the same number of generators. We show how this result can be seen as a consequence of both general properties of varieties of positive subreducts and specific characteristics of MV-algebras.
The connection with the MV-algebraic duality with rational polyhedra will allow us to use the deep results obtained by Cabrer and Mundici about finitely generated projective MV-algebras [17,18,15] to describe finitely generated projective Wajsberg hoops. In particular, we show that no MV-algebra (or more precisely, its 0-free reduct) is projective in the variety of Wajsberg hoops, and actually that finitely generated (nontrivial) projective Wajsberg hoops are necessarily unbounded. Interestingly enough, this implies that, in particular, the (0-free reduct of the) two-element Boolean algebra 2 is not projective in the variety of residuated lattices, while 2 is projective in every variety of bounded commutative integral residuated lattices, and in the variety of all bounded commutative integral residuated lattices it is the only finite projective algebra [5].
The fact that Wajsberg hoops are the equivalent algebraic semantics of the positive fragment of Lukasiewicz logic will allow us to use our algebraic and geometric investigation to derive some analogies and differences between Lukasiewicz logic and its positive fragment, that we shall refer to as L + . In particular, we show that while deducibility in L + coincides with deducibility of positive terms in Lukasiewicz logic, the same is not true for admissibility of rules.
Moreover, via the algebraic approach to unification problems developed by Ghilardi [26], we will show that the unification type of the variety of Wajsberg hoops, and thus of the positive fragment of Lukasiewicz logic, is nullary. This is in close analogy with the case of MV-algebras, and indeed our proof adapts to pointed rational polyhedra the pathological example given in [34] for the case of Lukasiewicz logic. Moreover, via the algebraic approach to admissibility developed in [16], we show that while the exact unification type of Lukasiewicz logic is finitary, the one of its positive fragment is unitary. This in particular implies decidability of the admissibility of rules in Wajsberg hoops and the positive fragment of Lukasiewicz logic.

Preliminaries
We start by recalling the needed facts about hoops, for more details and further references the reader can consult [21,11,2]. A hoop is an algebra A = (A, ·, →, 1) such that (A, ·, 1) is a commutative monoid and: A Wajsberg hoop is a hoop satisfying the following identity: often called Tanaka's equation thanks to Tanaka's work in this framework [43], although this particular identity seems to appear later in [28]. Every hoop carries a natural order structure definable as: that is in general a meet-semilattice order, where ∧ is definable as: x ∧ y = x · (x → y).
In the case of Wajsberg hoops this order is actually a lattice order, where the join operation is definable as: By Tanaka's identity, the defined join operation is commutative, and in fact in the literature on BCK-algebras (T) is also called the commutativity law. Moreover, (·, →) form a residuated pair with respect to this lattice order, that is to say: In fact, Wajsberg hoops can be seen as particular commutative residuated lattices. A commutative residuated lattice is an algebra A = (A, ·, →, ∧, ∨, 1) where We call a commutative residuated lattice integral if 1 is the top element in the lattice order, and bounded if it is integral and there is also an extra element 0 that is the bottom element of the lattice. Commutative residuated lattices are a variety called CRL, and their version with an extra constant 0 (not necessarily being the lower bound) is a variety called FL e . The last name comes from logic, as FL e -algebras are the equivalent algebraic semantics of the Full Lambek calculus with exchange (for more details on residuated structures and substructural logics see [25]). The subvariety of FL e consisting of bounded residuated lattices is called FL ew (where w stands for weakening in the associated logical system).
With respect to their structure theory, all varieties of residuated lattices are ideal-determined in the sense of [6], and the role of ideals is played by congruence filters, that is, (non-empty) lattice filters closed under products. In particular, there is a lattice-isomorphism between the lattice of congruence filters and the congruence lattice. Given a commutative integral residuated lattice A, the isomorphism is given by the following two maps, where θ is any congruence of A and F is any congruence filter of A: Finitely generated (or, equivalently, compact) congruences are then in bijection with finitely generated congruence filters. Now, given A a commutative integral residuated lattice, and X ⊆ A, the congruence filter generated by X in A is the set Fil A (X) = {b ∈ A : a 1 · . . . · a n ≤ b, a 1 , . . . , a n ∈ X, n ∈ N}.
It then follows that finitely generated congruence filters correspond to principal congruence filters (it suffices to take the meet of the generators), and analogously finitely generated congruences are principally generated. Wajsberg hoops fit in the residuated lattice framework since they are term equivalent to the variety WH of commutative integral residuated lattices satisfying (T), and the divisibility condition: x which ensure that the order is natural. From now on, we shall see a Wajsberg hoop as an algebra in WH, with the signature of residuated lattices {·, →, ∧, ∨, 1}. Bounded Wajsberg hoops are term-equivalent to MV-algebras, the equivalent algebraic semantics of infinite-valued Lukasiewicz logic. MV-algebras are usually introduced (see [19]) in the signature {⊕, ¬, 0}, and can be defined as algebras A = (A, ⊕, ¬, 0) such that As mentioned in the introduction, both Wajsberg hoops and MV-algebras are closely related to lattice-ordered abelian groups, that we shall call abelian ℓ-groups for short. An abelian ℓ-group is an algebra G = (G, +, −, 0, ∧, ∨) where (G, +, −, 0) is an abelian group, (G, ∧, ∨) is a lattice, and the group operation distributes over the lattice operations.
Let G be an abelian ℓ-group with a strong unit u, i.e., an element u such that for all x ∈ G, there exists n ∈ N: x ≤ u+. . .+u (n times). Then Mundici's Γ functor constructs an MV-algebra Every MV-algebra can be obtained in this way [40].
Both MV-algebras and abelian ℓ-groups can be seen in the framework of residuated lattices. The latter are indeed term-equivalent to commutative residuated lattices that satisfy x · (x → 1) = 1, via the translation x · y := x + y, 1 := 0, and x → y := −x + y.
Thus, as it often happens in the literature, in what follows we refer to MV-algebras as algebras in MV, in the signature {·, →, ∧, ∨, 0, 1}.
Given any abelian ℓ-group G seen as a residuated lattice, we define its negative cone to be the algebra G − = (G − , ·, → 1 , ∧, ∨, 1) on the subset of negative elements G − = {x ∈ G : x ≤ 1} with x → 1 y = (x → y) ∧ 1. Negative cones of abelian ℓ-groups are a variety of residuated lattices [8], term equivalent to cancellative hoops, that is, hoops where the product satisfies the usual cancellativity law. Cancellative hoops are a subvariety of Wajsberg hoops, and moreover, a totally ordered Wajsberg hoop is either bounded (thus, equivalent to an MV-algebra) or cancellative [4, Proposition 2.1].
Since the algebras on [0, 1] are generic for MV and WH, i.e. they generate the two varieties, by a standard universal algebraic argument (see [36,Lemma 4.98]) the n-generated free algebras are algebras of functions from [0, 1] n to [0, 1] generated by the projections and with operations defined componentwise by the ones on the standard algebra. We point out that the understanding of finitely generated free algebras in this context is meaningful from the logical point of view, since the n-generated free algebra is isomorphic to the Lindenbaum algebra of n-variable formulas of the corresponding logic.
By the well-known McNaughton's Theorem, the free n-generated MV-algebra is shown to be (isomorphic to) the algebra of McNaughton functions, that is, piecewise linear continuous functions with integer coefficients [35,41]. Thus, to each McNaughton function corresponds an equivalence class of MV-terms in the appropriate free algebra (equivalently, logically equivalent Lukasiewicz formulas). From now on, we will see the free n-generated MV-algebra as its representative F MV (n) given by the McNaughton functions over [0, 1] n .
In [4] the authors show that the free Wajsberg hoop over n generators F WH (n) can be characterized in terms of the free MV-algebra F MV (n) in the following way. Let 1 be the point in the n-cube whose coordinates are all 1, then: In what follows we will refer to the McNaughton functions in F WH (n) as Wajsberg functions.
A key character of the rest of this paper is going to be played by finitely presented Wajsberg hoops. A finitely presented algebra is an algebra with a finite number of generators, satisfying finitely many identities. In a variety V, a finitely presented algebra is then (isomorphic to) a quotient of a finitely generated free algebra modulo a finitely generated congruence. In what follows, we will denote with F V (n)/f a finitely presented algebra that is the quotient of F V (n) with respect to a principal congruence filter generated by an element f ∈ F V (n). The core of the present manuscript is a representation of finitely presented Wajsberg hoops in terms of geometrical objects. This connection stems from the following observation, that allows to connect principal filters with polyhedra in unit cubes. Given any function f ∈ F MV (n), let O f be its one-set, i.e.
Similarly, given an MV-term t, we will write O t for the one-set of its associated McNaughton function. Then a particular instance of Lemma 4.1 in [4] yields the following.
We shall see in what follows that one-sets of Wajsberg functions correspond to particular rational polyhedra. By a (rational) convex polyhedron (or (rational) polytope) of R k we mean the convex hull of finitely many points of R k (Q k respectively), and a (rational) polyhedron is a finite union of (rational) polytopes.

Positive reducts
As it follows from (2.1), the free Wajsberg hoop on n generators F WH (n) is (isomorphic to) a particular subreduct of the free MV-algebra over the same number of generators. We shall see how this arises from both general considerations and properties more specific to the MValgebraic-theory.
Let us first consider a variety of FL e -algebras and the variety of their 0-free subreducts. This last sentence makes sense because of the following (known) fact, which we prove here for the sake of the reader. Proposition 3.1. Let V be a variety of FL e -algebras, then the class V 0 of its 0-free subreducts is a variety of commutative residuated lattices.
Proof. We show that V 0 is closed under homomorphic images, subalgebras, and direct products.
Suppose first that S ∈ V 0 is a subreduct of some A ∈ V, and that R = h(S) for an homomorphism h of residuated lattices. Let us call A 0 the 0-free reduct of A, then A 0 ∈ V 0 , and S is a subalgebra of A 0 , in symbols S ≤ A 0 . Since commutative residuated lattices have the congruence extension property ([25, Lemma 3.57], [22]), this means that, if we call θ = ker(h), there exists θ 0 congruence of A 0 such that θ 0 ∩ (S × S) = θ. Then it follows from the Third Isomorphism Theorem ([14, Theorem 6.18]) that S/θ ≤ A 0 /θ 0 . Finally, A 0 /θ 0 is necessarily bounded, because A 0 is, and thus it is the 0-free reduct of a quotient of A. Hence, R = h(S) is a subreduct of an algebra in V, and V 0 is closed under homomorphic images.
It is easy to see that V 0 is closed under subalgebras. Indeed, if R ≤ S and S is a residuated lattice that is the subreduct of some A ∈ V, it is clear that R is a subreduct of A as well.
Finally, we show that V 0 is closed under direct products. Let {S i } i∈I be a family of subreducts of algebras in V, more precisely say that S i ≤ A i,0 , where each A i,0 the 0-free reduct of some A i ∈ V. Then, denoting with P and S the algebraic operators denoting the class of direct products and subalgebras respectively, Thus, it follows that i∈I S i is a subalgebra of the 0-free reduct of i∈I A i and the proof is completed.
It is worth pointing out that the previous proof works in the very same way for varieties of bounded residuated lattices that are not necessarily commutative, but do have the congruence extension property. Notice also that, in general, the class of 0-free subreducts of a variety of FL-algebras is a quasivariety. In fact, the closure under subalgebras and direct products requires no special properties.
We will write T V0 (X) for the term algebra over X in the language of V 0 , and T V (X) for the term algebra over the same set of generators X in the language of V. Given any variety W and any set of variables X = {x 1 , . . . , x n }, an assignment of X into an algebra A ∈ W is a function h mapping each variable x i to an element of A, say h(x i ) = a i ∈ A, for i = 1, . . . , n. Then h extends to a homomorphism (that we shall also call h) from the term algebra T W (X) to A. Moreover, given terms t(x 1 , . . . , x n ), u(x 1 , . . . , x n ) over the language of W, we write that A |= t ≈ u if for any assignment h of the variables x 1 , . . . , x n to elements of A, Proposition 3.2. Let V be a variety of FL e -algebras and V 0 be the variety of its 0-free subreducts. Let X be any set, then F V0 (X) is isomorphic to the subalgebra of the 0-free reduct of F V (X) generated by X.
Proof. Clearly T V0 (X) is exactly the subalgebra of the 0-free reduct of T V (X) generated by X. Thus, the thesis follows from the fact that, given terms for some assignments to the variables in a, b to elements of A 0 . The same elements seen , also the 0-free reduct of A does not satisfy the identity, which means that V 0 |= a ≈ b.
We now focus on the case where V = MV and V 0 = WH, where the above proposition can be refined. We call an MV-term positive if it is written in the 0-free signature {·, →, ∧, ∨, 1}. We call an MV-term negative if it is the negation of a positive term, where as usual ¬x := x → 0. The following result also follows from [7, Lemma 1]. Lemma 3.3. Every MV-term t is either equivalent in MV to a positive term or to a negative term.
Proof. We prove this by induction on the construction of the term t. For the base case, obviously the constant 1 and the generators are positive terms, while MV |= 0 ≈ ¬1.
Let now f, g be positive terms, we show that f * g, f * ¬g, ¬f * g, ¬f * ¬g for * ∈ {·, →} are either equivalent to positive terms themselves or their negation is, which implies the claim.
Let us start with * = ·. Clearly f · g is positive.
The negation of f · ¬g is equivalent to a positive term, indeed in MV, [4], but it can also be easily checked in the standard MV-algebra), which is positive.
, thus its negation is equivalent to a positive term. Finally, Notice that a term cannot be equivalent to both a positive and a negative MV-term. Indeed, if we evaluate on any MV-algebra all variables to 1, such an evaluation of a positive term gives 1, while it would give 0 on a negative term.
Notice that in the proof of the lemma we used both involutivity and the identity ¬(¬f ·¬g) = (f → (f · g)) → g that does not hold in all involutive structures, thus the lemma cannot be generalized outside of MV in a straightforward way.
Let us then call a function f ∈ F MV (n) positive if it corresponds to the equivalence class of a positive term. Then the previous lemma also gives us a different point of view on the description of the finitely generated free Wajsberg hoops in [4], indeed we can show that positive McNaughton functions are exactly those that are 1 in 1. Proof. If a function f is positive, then the statement can be easily seen by induction on the construction of a positive term f corresponds to, given that the operations are defined pointwise. Vice versa, since positive terms are 1 in 1, negative terms are clearly 0 and the claim follows from Proposition 3.3.
Thus we get an alternative proof of Theorem 3.1 in [4], as a consequence of Propositions 3.2 and 3.4. A similar line of thought to show Agliano and Panti's result has been followed in [1], however what we presented here is in higher generality and contains more details, as they are relevant for what follows.
We will see that the connection described in the last corollary lifts to a categorical equivalence between finitely presented Wajsberg hoops and a subcategory of finitely presented MV-algebras, given by quotients of free MV-algebras with respect to positive McNaughton functions.
As shown in [42], finitely presented MV-algebras are isomorphic to algebras of McNaughton functions restricted to rational polyhedra. In particular, given P ⊆ [0, 1] n , we write M(P), for the algebra of functions in F MV (n) restricted to P: Moreover, a finitely presented MV-algebra of the kind F MV (n)/f is isomorphic to M(O f ) [42]. We shall then now see how one can characterize one-sets of positive McNaughton functions. Proof. Since P is pointed, it contains the point 1. Thus if two functions g and h in F MV (n) coincide over P, they have the same value at 1 and the claim follows.
The previous lemma justifies the following definition. For all unexplained notions of category theory we refer the reader to [32].
We call MV + the category of positive MV-algebras with positive homomorphisms.
Notice that MV + is a category since the identity maps are positive homomorphisms and a composition of positive homomorphisms is still positive. Moreover, MV + is a (non-full) subcategory of finitely presented MV-algebras.
Let now n ∈ N, and P ⊆ [0, 1] n be a pointed rational polyhedron. We define the Wajsberg hoop relative to P, W(P), to be the algebra of functions in F WH (n) restricted to P: Notice that this is a well-defined Wajsberg hoop since the operations of the free algebra are defined pointwise. We show that, analogously to the MV-algebraic case, all finitely presented Wajsberg hoops are of this kind (up to isomorphism).
It is easy to see that ω is an homomorphism. Indeed, clearly ω(1 ↾O f ) = 1/f . Moreover, given g, h ∈ F WH (n) and * ∈ {·, →}, since operations are defined pointwise, We now prove that ω is injective.
∈ Fil(f ). We conclude that g/f = h/f , and thus ω is injective. Surjectivity is easily checked, since given g/f ∈ F WH (n)/f , ω(g ↾O f ) = g/f . Therefore we obtain the following.
Theorem 3.11. Let A be a Wajsberg hoop, then the following are equivalent.

1.
A is finitely presented.
Proof. Directly follows from Lemma 3.10 and Lemma 3.7.
Let WH fp be the category of finitely presented Wajsberg hoops with homomorphisms, that is a full subcategory of the algebraic category of Wajsberg hoops. We now define a map Φ : Theorem 3.12. Finitely presented Wajsberg hoops with homomorphisms and positive finitely presented MV-algebras with positive homomorphisms are categorically equivalent.
Proof. The fact that Φ is a functor from MV + to WH fp is easy to check and essentially follows from Lemmas 3.7, 3.8 and 3.10.
It suffices to show that Φ is full, faithful and essentially surjective ([32, Theorem 1, p. 91]). Let us first show the latter. Let A be a finitely presented Wajsberg hoop, then by what we recalled in the preliminaries in Section 2, A is isomorphic to a quotient of the kind F WH (n)/f , which by Lemma 3.10, is isomorphic to We now show that Φ is faithful. Consider two positive homomorphisms α 1 , α 2 from M(P) to M(Q), that differ on some f ↾P ∈ M(P). Since either f is positive or ¬f is, it follows from the definition and involutivity (¬¬x = x in MV) that Φ(α 1 ) and Φ(α 2 ) either differ on f ↾P or on ¬f ↾P . Thus Φ is faithful.
It is left to prove that the functor is full. Let β : W(P) → W(Q) be a homomorphism of Wajsberg hoops. Consider the homomorphism β + : M(P) → M(Q) defined as follows.
Suppose β(f ↾P ) = g ↾Q , then define β + (f ↾P ) = g ↾Q and β + (¬f ↾P ) = ¬g ↾Q . β + is well defined since given f, h ∈ F MV (n) that coincide over P, they are either both positive or both negative (Lemma 3.8). We show that β + is a homomorphism. It suffices to check that it preserves a constant, product and negation. The fact that it preserves constants and negation follows directly from the definition. For the product, we show one of the cases, the other ones being similar. Let h, k ∈ F WH (n), and suppose β(h ↾P ) = x ↾Q and β(k ↾P ) = y ↾Q , then Finally, clearly Φ(β + ) = β. Thus the functor is full and the proof is complete.
We point out that there always is an adjunction between an algebraic category and the subcategory of the reducts given by the forgetful functor (see [1] for the case of WH and [39] for a general approach). The connection we highlighted here is meant to provide a clear understanding of the geometrical duality in the following section.

Duality with pointed rational polyhedra
In this section we present the duality between finitely presented Wajsberg hoops and pointed rational polyhedra, which follows from the categorical equivalence shown in the previous section, and the restriction to positive MV-algebras of the well-known duality between finitely presented MV-algebras and rational polyhedra in [34].
In more details, in [34] the authors show that finitely presented MV-algebras with homomorphisms are dual to a category whose objects are rational polyhedra P ⊆ R n for some n ∈ N, and the morphisms are Z-maps between them. We recall that given a rational polyhedron P ⊆ R n and a continuous map z = (z 1 , . . . , z m ) : P → R m , with m, n ∈ Z + , z is a Z-map (of P) if for each j = 1, . . . , m, z j is piecewise linear with integer coefficients. For details on rational polyhedra and Z-maps the reader is referred to [42].
Since any rational polyhedron in R n is Z-homeomorphic to a rational polyhedron in [0, 1] n (Claim 3.5 in Theorem 3.4 in [34]), the category of rational polyhedra in the duality with finitely presented MV-algebras can be restricted to account only for polyhedra in [0, 1] n for some n ∈ N.
Here we choose to use this version of the duality since, although less general from the geometrical point of view, it has a clearer algebraic meaning that will be useful in the following sections: the polyhedra are the one-sets of McNaughton functions generating the principal filter associated to a finitely presented algebra. Another choice that we make here is that, given a finitely presented MV-algebra of the kind F MV (n)/f , we consider the associated polyhedron to be O f , the one-set of the function f , instead of (equivalently, in the case of MV-algebras, see [42, Corollary 2.10 ]) picking the zero-set of the function f . By Lemma 3.7, pointed polyhedra are mapped to positive MV-algebras by the Marra-Spada duality in [34]. We will now show what positive homomorphisms correspond to on the geometrical side. In the full duality in [34], homomorphisms between finitely presented MValgebras are exactly those obtainable in the following way via the functor M from the category of rational polyhedra to finitely presented MV-algebras that established the duality. Let P ⊆ [0, 1] n , Q ⊆ [0, 1] m be rational polyhedra, and λ : P → Q a Z-map. Then the map dual to λ, M(λ), is such that: and all homomorphisms between M(Q) and M(P) can be obtained in this way. Therefore we obtain the following characterization.   Let P + Z be the category of pointed rational polyhedra with pointed Z-maps. Let M be the previously described functor in the duality for MV-algebras, from rational polyhedra to finitely presented MV-algebras. Composing the restriction of M to the category of P + Z with the functor Φ (notice that the composition is well defined thanks to Lemmas 4.1 and 3.7), we obtain a functor W from P + Z to the category of finitely presented Wajsberg hoops. In particular, given pointed rational polyhedra P ⊆ [0, 1] n and Q ⊆ [0, 1] m , and ζ : P → Q a pointed Z-map: • W(P) is the algebra of restricted Wajsberg function as in 3.2.
We then obtain the following result.
Theorem 4.4 (Duality for finitely presented Wajsberg hoops). The functor W yields a duality between the category of pointed rational polyhedra P + Z and the category of finitely presented Wajsberg hoops WH fp .
Proof. It follows from Lemmas 4.1 and 3.7 that the duality in [34,Theorem 3.4] restricts to a duality between the categories P + Z and positive finitely presented MV-algebras with positive homomorphisms. The claim then follows by the categorical equivalence in Theorem 3.12.
The duality we obtained has the very same essence of the one about finitely presented MV-algebras, indeed it could have been shown by adapting the proofs in [34]. Here however, we decided to highlight the connection between finitely presented Wajsberg hoops and the subcategory of positive finitely presented MV-algebras which we believe has interest of its own.
We point out the following description of monomorphisms and epimorphisms in the category of pointed polyhedra, that is, left and right cancellable morphisms respectively. Following [15], let us call strict a pointed Z-map that is a Z-homeomorphism (a homeomorphism via a Z-map whose inverse is also a Z-map) onto its image. Proof. (1) and (2) can be shown analogously to [15,Theorems 3.2], we point out the necessary modifications. Recall that in concrete categories injective morphisms are monomorphisms, and surjective morphisms are epimorphisms.
Let us end this section with some relevant examples of finitely presented Wajsberg hoops and their associated polyhedra. Let us call W n the Wajsberg chain with n-elements. Example 4.6. W 1 is isomorphic to W({1}), and for all n ∈ N, n ≥ 2, W n is isomorphic to W({ 1 n−1 , 1}) . Indeed, since all Wajsberg functions have value 1 in 1, F WH (1) restricted to {1} is the trivial algebra with one element W 1 . The 0-free reduct of the 2-elements Boolean algebra W 2 is isomorphic the free algebra of Wajsberg functions with one variable restricted to {0, 1}, since Wajsberg functions are either 0 or 1 in 0 and can only have value 1 in 1.
The cases of W n , n ≥ 3, can be shown by induction on the construction of the elements of the free algebra. F WH (1) is generated by the projection function π 1 (that is the identity map), and since the operations are defined pointwise, this generates an algebra isomorphic to a Wajsberg subhoop of [0, 1] generated by 1 n−1 and 1, which is W n . Notice that in MV-algebras instead, the finite MV-chain of n elements is isomorphic to M({ 1 n−1 }). We point out that the algebras W n from the previous example are, up to isomorphisms, all the finite subdirectly irreducible Wajsberg hoops. The next proposition shows properties of finitely presented subdirectly irreducible Wajsberg hoops. Proof. By Theorem 3.11, a finitely presented Wajsberg hoop is an algebra isomorphic to W(P), for some n ∈ N and some pointed rational polyhedron P ⊆ [0, 1] n . Suppose that P contains two different points x = y of [0, 1] n , with x, y = 1. Then one can construct two piecewise linear functions with integer coefficients that map 1 to 1, and that restricted to P are incomparable with respect to the pointwise order. Such McNaughton functions can be constructed using Schauder's hats, we omit the technical details here (for details on Schauder's hats the reader can check [19]). Thus, if P contains two points different from each other and from 1, W(P) is not totally ordered, and thus it is not subdirectly irreducible. Indeed, in WH it holds the prelinearity equation (x → y)∨(y → x) ≈ 1 (see [4]), that characterizes varieties of commutative and integral residuated lattices whose subdirectly irreducible algebras are totally ordered (see [25]).
Aside from the algebras W n , other relevant subdirectly irreducible Wajsberg hoops can be defined as follows. Let Z be the abelian ℓ-group of the integers naturally ordered, then we call Z × lex Z the totally ordered abelian group that has as domain the cartesian product of Z × Z, the group operations are defined componentwise, and the ordering is the lexicographic ordering. Let C ω n be the 0-free reduct of Γ(Z × lex Z, (n, 0)). Let C ω be the cancellative hoop defined as the free monoid over one generator C ω = {1 = a 0 , a 1 , a 2 , a 3 , . . .} ordered by 1 = a 0 > a 1 > a 2 > a 3 > . . ., and with operations defined as a m · a n = a m+n , a m → a n = a max(n−m,0) . Then C ω , C ω n are subdirectly irreducible Wajsberg hoops that are not finitely presented, since the former is unbounded and the latter is not simple.
One can obtain other examples of finitely presented Wajsberg hoops using the analogue of [42, Lemma 3.6], which can be proved in a completely analogous way.

Projective and exact Wajsberg hoops
In this section we specialize the duality to two interesting classes of finitely presented Wajsberg hoops, that is, finitely generated projective algebras and exact algebras in WH. An algebra P is projective in a class of algebras K if whenever there are A, B ∈ K, a homomorphism f : P → A and a surjective homomorphism g : B → A, then there exists h : P → B such that f = g • h. This algebraic notion of projectivity corresponds to a categorical notion (where surjective homomorphisms correspond to regular epimorphisms). Equivalently, in a variety of algebras V, P is projective if and only if it is a retract of some free algebra F V (X). We recall that A is a retract of F if there are homomorphisms i : A → F and j : F → A such that j • i = id A . Notice that, necessarily, i is injective and j is surjective.
An algebra E in a variety V is called exact if it is (isomorphic to) a finitely generated subalgebra of a finitely generated free algebra. It follows that finitely generated projective algebras in a variety are a subclass of exact algebras.
We start by showing that we can indeed use the duality for finitely presented Wajsberg hoops to study exact algebras, and therefore projective algebras, in WH. The following is the analogue of [42, Corollary 6.6], we write the proof here in reference to our previous results for the sake of the reader.
Lemma 5.1. Let B be a finitely generated subalgebra of a finitely presented Wajsberg hoop A. Then B is finitely presented.
Proof. Suppose A ∼ = W(P), for P some pointed polyhedron P ⊆ [0, 1] n . Suppose B is generated by g 1 . . . g k ∈ W(P). Then g = (g 1 . . . g k ) is a pointed Z-map by Lemma 4.3, and its image g(P) ⊆ [0, 1] k is a rational polyhedron ( [42,Lemma 3.4]) and it is pointed because it is the image of a pointed Z-map. By Lemma 4.8, B ∼ = W(Q), thus by Theorem 3.11 B is finitely presented.
As an immediate consequence we get the next proposition.
Proposition 5.2. If a n-generated Wajsberg hoop is exact (or projective), then it is finitely presented, i.e. isomorphic to W(P) for some pointed rational polyhedron P ⊆ [0, 1] n .
The fact that in a variety being projective is equivalent to being a retract of a free algebra (see [26]), applying the duality of The geometrical study of Z-retracts has been carried out in the papers [17,18,15]. In particular, necessary conditions for a polyhedron are obtained, that yield a full characterization for the 1-dimensional case.
In order to study the analogue of such characterization we need to introduce the notions of contractibility and strong regularity. We say that a polyhedron is contractible if it is homotopically equivalent to a point. Strong regularity is usually defined as a property of triangulations (see [42]), however Cabrer shows an intrinsic characterization ( [15,Theorem 4.4]) that we follow here: a polyhedron P is strongly regular if and only if for each rational vector v ∈ P and each 0 < δ ∈ R, there exists a rational vector w ∈ P such that the Euclidean distance dist(v, w) < δ, and, calling den(x) the least common denominator of the coordinates of a point x, den(v) and den(w) are coprime (in the sense that gcd(den(v), den(w)) = 1).
Following [18,Corollary 4.4,Theorem 3.5], if a rational polyhedron P ⊆ [0, 1] n is a Z-retract then it is: contractible, strongly regular, and it contains a point with integer coordinates. In the one-dimensional case the converse also holds. Since pointed polyhedra always include a vertex of [0, 1] n , we get the following. If P is one-dimensional, the converse also holds.
Proof. The proof is a direct consequence of [18,Theorem 3.5].
We can then see geometrically that the trivial algebra is projective, which is not surprising since it is the free algebra over the empty set of generators. Other projective Wajsberg hoops are the algebras in Example 4.9.
Notice that contractibility implies connectedness, and the polyhedra associated to the algebras W n for n ≥ 2 are not connected as seen in Example 4.6. Since we recall that C ω , C ω n are not finitely presented, we obtain the following consequences.
Corollary 5.5. The subdirectly irreducible Wajsberg hoops C ω , C ω n , W n for n ≥ 2 are not projective in WH, nor in any variety of residuated lattices that contains WH.
In particular then the 2-element residuated lattice W 2 is not projective in RL, while its bounded version, the 2-element Boolean algebra, is projective in every subvariety of FL. Indeed, it corresponds to the free algebra on the empty set of generators.
We can actually obtain stronger negative results. Let us call a Wajsberg hoop A weakly projective if whenever it is a homomorphic image of another Wajsberg hoop B, it is also isomorphic to one if its subalgebras. This notion of weak projectivity is studied in relation to the study of the lattices of subquasivarieties [27]. Clearly, being projective implies being weakly projective, but the opposite is in general not true. Notice that a weakly projective Wajsberg hoop is finitely presented by Lemma 5.1.
Proof. Let A be n-generated and weakly projective in WH. Then A is a homomorphic image of F WH (n), and thus isomorphic to a subalgebra of F WH (n). Since the operations in the free algebra are defined pointwise, and all functions in F WH (n) are continuous, it follows that the only idempotent element in F WH (n) is the function constantly equal to 1. Thus a bounded algebra with more than one element cannot be embedded in F WH (n), since there is no element in which to map its (necessarily idempotent) lower bound. Thus A is either trivial or unbounded.
Thus no finitely generated positive reduct of an MV-algebra is projective in the variety of Wajsberg hoops.
We now turn our attention to the larger class of exact algebras, that can be characterized geometrically via the results in [15] and the duality of Theorem 4.4.
Theorem 5.8. A finitely generated Wajsberg hoop is exact if and only if it is isomorphic to W(P), for a pointed rational polyhedron P ⊆ [0, 1] n , for some n ∈ N, such that: • P is connected; • P is strongly regular.
Proof. Suppose A is a finitely generated exact Wajsberg hoop. Then by definition, A is isomorphic to a finitely generated subalgebra of a (finitely generated) free algebra. By Lemma 5.1 A is finitely presented, thus it is isomorphic to W(P) for some pointed rational polyhedron P ⊆ [0, 1] n (Theorem 3.11). Via Theorem 4.4 and Proposition 4.5, since A embeds into a finitely generated free algebra, there is an onto pointed Z-map from [0, 1] n to P, for some n ∈ N. By [15,Lemma 4.12], this implies that P is connected and strongly regular.
Vice versa, suppose A is isomorphic to W(P), and P ⊆ [0, 1] n is connected and strongly regular. By [15,Lemma 4.12], there is an onto Z-map ζ : [0, 1] l → P for some l ∈ N. This implies that there is also a pointed Z-map from [0, 1] l to P. Indeed either ζ(1) = 1, and therefore ζ is a pointed Z-map, or it suffices to consider ρ • ζ, where ρ is the Z-map that rotates the cube and maps 1 to the vertex v ∈ [0, 1] l such that ζ(v) = 1 ∈ P, thus ρ • ζ is a pointed Z-map. For instance, considering the onto Z-map arising from [15,Lemma 4.12], such v would be e 1 = (1, 0, . . . , 0) ∈ [0, 1] l . Therefore, by the duality in Theorem 4.4 and Proposition 4.5, there is an embedding from A to F WH (l), and thus A is an exact Wajsberg hoop.
As a consequence of algebraizability, we recall that a quasiequation of the kind (t ≈ 1) ⇒ (u ≈ 1) is valid in MV (WH) if and only if t deduces u in L ( L + ). Thus, we have also shown that deducibility in L + corresponds to deducibility of positive terms in Lukasiewicz logic.
In what follows, given a variety V and two sets of identities Σ, ∆ in its language, we will write Σ |= V ∆ to mean that if V |= Σ, then V |= ∆.
Another direct consequence of the geometrical representation, and another analogy between Wajsberg hoops and MV-algebras, is that the variety WH is coherent in the sense of [46]: any finitely generated subalgebra of a finitely presented member is finitely presented (Lemma 5.1). This entails the fact that L + , as Lukasiewicz logic, has right uniform (Maehara) interpolation in the sense of [44]: a variety V admits right uniform Maehara interpolation if for any finite sets of variables X, Y and finite set of equations Γ over variables in X ∪ Y , there exists a finite set of equations Π over variables in Y such that for any finite sets of equations Σ and ∆ over variables in Y ∪ Z, Γ, Σ |= V ∆ if and only if Π, Σ |= V ∆. Proposition 6.2. WH admits right uniform Maehara interpolation. [31,Proposition 2.4]. WH is coherent for Lemma 5.1, while deductive interpolation has been shown in [38]. Moreover, by [44,Theorem 3.13], a variety with right uniform deductive interpolation and the congruence extension property admits Maehara right uniform interpolation, and every commutative variety of residuated lattices has the congruence extension property [25, Lemma 3.57].

Proof. A variety admits right uniform deductive interpolation if and only if it is coherent and admits deductive interpolation
As it is clear from the above proof, right uniform Maehara interpolation implies right uniform deductive interpolation (in the sense of [44, Definition 3.1]). We recall that the Maehara interpolation property for Wajsberg hoops holds for the results in [38,37]. However, as ℓ-groups, but unlike MV-algebras, WH does not admit left uniform deductive interpolation. A variety V admits left uniform deductive interpolation if for any finite sets Y, Z and finite set of equations ∆ with variables in Y ∪ Z, there exists a finite set of equations Π over variables in Y such that Π |= V ∆ and for any set of equations Σ over X ∪ Y , Σ |= V ∆ implies Σ |= V Π. This property indeed fails trivially, as in ℓ-groups ([44, Remark 4.2]), since there is no set of equations Π(y) such that Π |= WH y ≈ z.
We shall now move to the main applications of the geometrical interpretation of finitely presented Wajsberg hoops, that involve the two related logical problems of unification and admissibility, via the algebraic approaches developed respectively in [26] and [16].

Unification
Finitely generated projective algebras in a variety that is the equivalent algebraic semantics of a logic are connected to unification problems for their corresponding logics via Ghilardi's algebraic approach to unification [26].
The usual notion of unification problem for a logic consists in a finite set of identities, and a solution or unifier is a substitution that makes the identities provable in the logic.
Ghilardi shows that in an algebraizable logic L with equivalent algebraic semantics V L , one can instead consider the following, equivalent, notion. An algebraic unification problem is a finitely presented algebra A in the variety, and a unifier is a homomorphism u : A → P, where P is a projective algebra in V L . The underlying idea is that, given a symbolic unification problem given by the set of identities {s i ≈ t i : i = 1 . . . n}, where s i , t i for i = 1 . . . n are terms in the appropriate language over a set of variables X, the corresponding finitely presented algebra is F VL (X)/θ, where θ is the congruence (finitely) generated by the pairs {(s i , t i ) : i = 1 . . . n}. The algebraic unifiers can be ordered by generality in the following way: given two unifiers for a problem A, say u 1 : A → P 1 and u 2 : A → P 2 , we say that u 1 is more general than u 2 if there exists an homomorphism h : P 1 → P 2 such that h • u 1 = u 2 . This gives a preorder on the set of unifiers, thus one can consider the associated partial order of unifiers that are "equally general".
Then the unification type of the problem is said to be: unitary, if there is a maximum in the partial order of unifiers; finitary, if there are instead finitely many maximal elements; infinitary, if instead there are infinitely many maximal elements; nullary, otherwise. The unification type of the variety, and via Ghilardi's results of the corresponding logic, is the worst unification type occurring for the unification problems in the variety.
In [34] the authors show that the unification type of MV-algebras, and hence of Lukasiewicz logic, is nullary. Indeed, using the duality with polyhedra, they show a unification problem with a co-final chain of order-type ω of unifiers.
Let us turn our attention to the positive fragment L + , or equivalently, to unification problems in Wajsberg hoops. First, notice that every unification problem in WH has a solution, that is, there is always an homomorphism to the projective trivial Wajsberg hoop. Equivalently, the substitution mapping all variables to 1 unifies every identity. Whereas in Lukasiewicz logic, an identity is unifiable if and only if it is classically satisfiable ([29, Lemma 3.3]), or, from the algebraic point of view, if and only if there is a homomorphism to the 2-element Boolean algebra, since 2 is projective and a retract of every projective MV-algebra [5].
Moreover, while clearly if an identity is unifiable in L + it is unifiable in Lukasiewicz as well via the same substitution, unification in L + does not reduce to unification of positive identities in Lukasiewicz logic, since substitutions in Lukasiewicz logic may also make use of the constant 0. Example 6.3. Let us define in the language of Wajsberg hoops x ⊕ y := (x → (x · y)) → y, which in MV coincides with Lukasiewicz sum, and we write 2x for x ⊕ x. Consider now the identity 2x → x ≈ 1. Since MV |= 2x → x ≈ x ∨ ¬x, the one-set of 2x → x in [0, 1] is given by {0, 1}. Thus the identity algebraically corresponds to the finitely presented algebra W 2 . A unifier for W 2 would be a homomorphism to a (finitely generated) projective algebra, that is, a retract of a finitely generated free algebra. Since W 2 is bounded, and the only idempotent element of a free finitely generated Wajsberg hoop is the top element, the only possible unifier is the homomorphism to W 1 .
Equivalently, the identity only has as a solution in WH, (the equivalence class of) the substitution σ(x) = 1. Whereas in MV, τ (x) = 0 is also a solution, and σ and τ are incomparable in the poset of unifiers.
Nonetheless, we show that we can suitably adapt the pathological example in [34] to our case, and conclude that the unification type of Wajsberg hoops, and thus of the positive fragment of Lukasiewicz logic, is nullary as well.
The unification problem we consider is equivalent to the one in [34], with its corresponding polyhedron being the boundary of the unit square in [0, 1] 2 , which is a pointed rational polyhedron. In the MV-algebraic case, this corresponds to the identity x ∨ ¬x ∨ y ∨ ¬y ≈ 1, which is equivalent to the (more cumbersome) identity in the negation-free language of Wajsberg hoops: Direct computation indeed shows that the one-set of ((x → x 2 ) → x) → x] ∨ [((y → y 2 ) → y) → y is the border of the unit square, which we will denote by B in analogy to [34]. Notice that this is not a Z-retract of a unit cube, since it is clearly not contractible. The unification problem we are considering is then A = F WH (2)/B.
We will now find a co-final chain of order-type ω of unifiers, i.e. projective Wajsberg hoops {P i } i≥1 , i ∈ N, and corresponding homomorphisms u i : A → P i . It will suffice to obtain a slight modification of the key lemma 6.2 in [34]. Lemma 6.4. For each integer i ∈ N, i ≥ 1, there is an integer n i ∈ N, n i ≥ 1, and a pointed rational polyhedron P i ⊆ [0, 1] ni that is a pointed Z-retract of [0, 1] ni such that: 1. for each i ≥ 1 there are onto pointed Z-maps µ i : P i → B, and injective pointed Z-maps ν i such that the following diagram commutes: For any two i > j > 0, there is no pointed Z-map ν : P i → P j making the following diagram commute.
Proof. In order to find the pointed polyhedra P i , we make use of [ We further compose with the Z-homeomorphism β that maps B onto itself mapping: (1, 0) → (1, 1), (1, 1) → (0, 1), (0, 1) → (0, 0), (0, 0) → (1, 0). Let us denote with η i the map from t i to t i+1 in [34,Lemma 6.2]. We claim that then the wanted maps are Indeed, for (1), ν i is injective as it is a composition of injective maps, and µ i is onto since it is a composition of surjective maps. The diagram commutes since ζ i = ζ i+1 • η i by [34, Lemma 6.2 (i)]. For (2), if there were such a ν, this would lead to a contradiction of [34,Lemma 6.2 (ii)]. In the very same way, since a pointed rational polyhedron is in particular a rational polyhedron, the last point follows from [34, Lemma 6.2 (iii)] and the above Z-homeomorphism between each T i and P i .
Theorem 6.5. The unification type of Wajsberg hoops, and therefore of the positive fragment of Lukasiewicz logic, is nullary.
Proof. The proof follows from Lemma 6.4 and the duality in Theorem 4.4. Indeed, consider the unification problem described by the identity 6.1 and represented by the polyhedron B. Then, consider each rational polyhedron P i , for i ≥ 1, from Lemma 6.4. Each P i is a Z-retract of [0, 1] ni , since it is Z-homeomorphic to T i , and therefore also to t i in [34,Lemma 6.2]. Since each P i is pointed, the family {P i } i≥1 corresponds to a countable family of projective Wajsberg hoops. Taking the dual of each map µ i gives a unifier for the unification problem represented by B. By Lemma 6.4 (1) and (2), the maps µ i for i ∈ N, i ≥ 1 are a strictly increasing chain of order type ω with respect to the partial order of generality. By Lemma 6.4 (3) the chain is co-final. Thus we have a unification problem with nullary type, and therefore the unification type of Wajsberg hoops, and of the positive reduct of Lukasiewicz logic, is nullary.

Admissibility
Checking the admissibility of rules is a problem closely connected to unification. Given two sets of formulas Σ, Γ in the language of a variety V, we say that Σ ⇒ Γ is V-admissible if every substitution that unifies all formulas of Σ in V, it unifies at least one formula of Γ in V. This is equivalent to the universal formula Σ ⇒ Γ being valid in the free algebra over ω generators in V [16, Lemma 2.4]. For details on the algebraic approach to admissibility we refer to [16], where the authors show that admissibility is related to what they call exact unification. More precisely, they define a notion of exact unification type, based on a preorder on the set of unifiers for a unification problem that is weaker than the generality preorder. Then the authors prove that, given a rule Σ ⇒ Γ, it suffices to check admissibility with respect to substitutions in a set S which includes all the maximal unifiers in the new preorder [16,Corollary 3.2]. Here we are interested in the algebraic counterpart of this preorder.
Algebraically, studying the exact unification type corresponds to considering the set of coaxact unifiers. Given a finitely presented algebra A ∈ V, a coexact unifier is a homomorphism onto an exact algebra E ∈ V. Coexact unifiers are ordered as algebraic unifiers, that is, given two coexact unifiers for a problem A, say u 1 : A → E 1 and u 2 : A → E 2 , we say that u 1 is more general than u 2 if there exists an homomorphism h : The study of the exact unification type is relevant since if a variety V has unitary or finitary exact type, and there exists an algorithm for finding a finite complete set of unifiers, then checking admissibility in V is decidable whenever the equational theory of V is decidable.
While in [16] the authors prove that Lukasiewicz logic has finitary exact type, we will show that Wajsberg hoops, and therefore the positive fragment of Lukasiewicz logic, have instead unitary type.
The following useful fact is the analogue of [29, Theorem 4.1, Corollary 4.2], we sketch the proof in our language for the sake of the reader. Lemma 6.6. All free Wajsberg hoops F WH (n), for n ∈ N, n ≥ 1, have the same universal theory.
Proof. The statement is equivalent to showing that all free Wajsberg hoops satisfy the same rules Σ ⇒ ∆. Indeed, every such rule is a universal formula, and vice versa, the validity of a universal formula is equivalent to the validity of a set of such rules (see the discussion in [29]).
We can show that a rule Σ ⇒ ∆ is valid in F WH (n), for any n ≥ 2, if and only if it is valid in F WH (1). The left-to-right direction follows from the fact that F WH (1) is a subalgebra of all F WH (n), for any n ≥ 2.
We now sketch the right-to-left direction. First, one can restrict to considering Σ to be one identity t(x 1 , . . . , x n ) ≈ 1 ([23, Lemma 3.1]). Let ∆ = {u i (x 1 , . . . , x n ) ≈ 1, i = 1 . . . m}. Suppose Σ ⇒ ∆ is not valid in F WH (k) for some k ≥ 2. Then there is an assignment h to F WH (k) such that h(t) = ⊤, where ⊤ is the function constantly equal to 1, but h(u i ) < ⊤ for all i = 1 . . . m. In particular, there are some rational points y 1 , . . . y m ∈ [0, 1] k where the Wajsberg functions h(u i ) are such that h(u i )(y i ) < 1. The idea is to now define a pointed Z-map f : [0, 1] → [0, 1] k such that, if we define a new assignment k of {x 1 , . . . , x n } to F WH (1) mapping each x i to h(x i ) • f , k validates Σ, but it does not validate any of the identities in ∆.
Thus k is an assignment of {x 1 , . . . , x n } in F WH (1) which testifies the failure of the validity of Σ ⇒ ∆ in F WH (1), and the proof is completed.
For the following lemma and theorem we adapt some ideas in [29,30,16]. In particular, we use the fact that by [15,Theorem 4.17], a rational polyhedron is strongly regular if and only if it is a finite union of anchored sets, where a set X ⊆ R n is called anchored if for some v 1 , . . . , v m ∈ R n , X = conv(v 1 , . . . , v m ) and the affine hull of X intersects Z n .
Given a set of identities Σ = {s i ≈ t i , i = 1 . . . n}, where s i , t i are n-variable Wajsberg terms, we will write F WH (n)/Σ for the quotient of F WH (n) with respect to the congruence generated by {(s i , t i ), i = 1 . . . n}. Lemma 6.7. Let Σ = {t(x 1 , . . . , x n ) ≈ 1} be an identity in the language of Wajsberg hoops. Then there exists a term u(x 1 , . . . , x n ) over the same variables such that, considering ∆ = {u(x 1 , . . . , x n ) ≈ 1}: Proof. Let O t ⊆ [0, 1] n be the one-set of the Wajsberg function corresponding to t.
Then O t can be written as a finite union of polytopes P i for i = 1 . . . m, m ∈ N: Intuitively, we want a connected component of O t that is strongly regular and as large as possible. Thus, we restrict to connected unions of strongly regular polytopes, which means by [15,Theorem 4.17], finite unions of anchored polytopes. Let then I = {i ∈ {1, . . . , m} : P i is anchored}, P = i∈I P i .
Let C 1 . . . C k be the connected components of P, and let C i0 be the connected component that contains 1, for some i 0 ∈ {1 . . . k}. Notice that i 0 exists, with the limit case being the singleton {1}. Say that I 0 ⊆ I is such that Since C i0 is a pointed rational polyhedron by construction, consider a Wajsberg function f ∈ F WH (n) whose one-set is C i0 , and let u(x 1 , . . . , x n ) be a Wajsberg term associated to f . We now show (1) -(3).
(1) By definition, C i0 is connected and it is strongly regular (since it is a finite union of anchored polytopes, [15,Theorem 4.17]). Thus F WH (n)/∆ is an exact Wajsberg hoop by Theorem 5.8.
(2) By Proposition 6.1, WH |= ∆ ⇒ Σ if and only if O u ⊆ O t , which holds by construction.
(3) By Lemma 6.6 we can restrict to consider substitutions to terms with 1 variable, say y. Let then σ : T WH (x 1 , . . . , x n ) → T WH (y) be a WH-unifier of Σ. Letσ : F WH (n) → F WH (y) be the homomorphism induced by σ, that closes the following diagram, where µ, µ ′ are the natural epimorphisms: Since the image ofσ is a finitely generated subalgebra of F WH (y),σ(F WH (n)) is an exact Wajsberg hoop, isomorphic to a quotient of the kind F WH (y)/Q, where Q ⊆ [0, 1] is a pointed polyhedron that is connected and strongly regular, that is, it is a segment of the kind Since each S j is anchored, so is each P ij . Thus, ζ[q, 1] ⊆ P, and since it is connected (being the image of a connected interval via a continuous map), and since ζ is pointed, this implies that ζ[q, 1] ⊆ C i0 = O u . Since ζ is the dual of the substitution map acting on the free algebra F WH (n), this implies that ∆ ⊆ kerσ, and thus σ also unifies u. Therefore, Σ ⇒ ∆ is admissible in WH. Proof. Without loss of generality, let us consider a finitely presented Wajsberg hoop of the kind A = F WH (n)/Σ, where Σ = {t(x 1 , . . . , x n ) ≈ 1}. Let then B = F WH (n)/∆ be the exact Wajsberg hoop given by Lemma 6.7, and let e : A → B be the dual of the inclusion map from the polyhedron associated to B to the polyhedron associated to A (following the notation of Lemma 6.7, from C i0 to O t ). Then e is a coexact unifier, since it is an homomorphism onto an exact Wajsberg hoop by Lemma 6.7 via the duality and Proposition 4.5. We claim that e is maximal in the set of coexact unifiers for A. This follows from the admissibility of Σ ⇒ ∆, Lemma 6.7(3). Indeed, suppose there is a coexact unifier u : A → C, for some exact Wajsberg hoop C that embeds in F WH (ω) via a homomorphism i. This, as outlined in the proof of [16, Theorem 3.6]), gives a unifier for Σ. Indeed, consider the natural epimorphisms µ 1 : F WH (n) → A = F WH (n)/Σ, µ 2 : F WH (n) → B = F WH (n)/∆, µ : T WH (n) → F WH (n), µ ω : T WH (ω) → F WH (ω), and letσ = i • u • µ 1 . The substitution is then defined as σ(x i ) = t if µ ω (t) =σ • µ(x i ), thus σ unifies Σ by construction. Hence, it also unifies ∆, and then ∆ ⊆ kerσ = ker(u • µ 1 ) since i is injective. Thus there exists an homomorphism w : B → C that closes the following diagram: That is to say, such that w • µ 2 = u • µ 1 . Moreover, since e is the dual of the inclusion map, e • µ 1 = µ 2 , thus w • e = u, that is, u ≤ e in the preorder of coexact unifiers. Therefore, e is maximal, and since A was an arbitrary finitely presented Wajsberg hoop, the exact type of WH is unitary.
Since the proof of Lemma 6.7 also shows a procedure to find the maximal coexact unifier of a finitely presented Wajsberg hoop, we get the following consequence. Corollary 6.9. The set of admissible rules is decidable in WH (and in the positive fragment of Lukasiewicz logic).
We stress that, while deducibility of Wajsberg hoops reduces to deducibility in MV-algebras (Proposition 6.1), this is not true for admissibility. If we consider a rule Σ ⇒ ∆ in the language of the positive reduct that is admissible in MV, this is also admissible in WH, as a consequence of Proposition 6.1. However, the opposite does not hold, as shown by the following example of a rule that is admissible in WH but not in MV.  Figure 2. Moreover, it is not admissible in MV. Indeed, consider the substitution σ(x) = 0. Clearly σ unifies x ∨ ¬x ≈ 1, since MV |= 0 ∨ ¬0 ≈ 1, but it does not unify 2x ≈ 1, since MV |= 0 ⊕ 0 ≈ 0. However, (2x → x ≈ 1) ⇒ (2x ≈ 1) is admissible in WH. Indeed, as shown by Figure 2, the maximal coexact unifier for 2x → x ≈ 1 is represented geometrically by the singleton {1}, which represents the homomorphism onto the trivial algebra. In fact, the only one-variable unifier for 2x → x ≈ 1 in WH is (the equivalence class of) the substitution σ(x) = 1, which unifies any identity written with positive terms. g f Figure 2: The functions f (x) = 2x → x, g(x) = 2x in F WH (1).

Conclusions and future work
The duality in terms of rational polyhedra we presented in this manuscript shows to be fruitful to study logical properties of the positive fragment of Lukasiewicz logic, in the same fashion as in the MV-algebraic case. Via this representation, we derived some analogies and differences between Lukasiewicz logic and its positive fragment.
The duality we presented here is meant to have a clear algebraic interpretation, i.e., the pointed polyhedra are exactly the one-sets of the functions in the free Wajsberg hoop, and finitely presented Wajsberg hoops are the algebras of Wajsberg functions restricted to pointed polyhedra. However, a more general approach could be developed, in the lines of [33,34]. Moreover, the connections with the categorical equivalence in [24] in the more general setting shall be investigated.
Given the representation of free BL-algebras (and basic hoops) in [7], the insight given by this work could also be useful to study finitely presented BL-algebras and basic hoops from a geometrical point of view.