key: cord-0044860-gqjsuqid
authors: Abbadini, Marco; Di Stefano, Federica; Spada, Luca
title: Unification in Łukasiewicz Logic with a Finite Number of Variables
date: 2020-05-16
journal: Information Processing and Management of Uncertainty in Knowledge-Based Systems
DOI: 10.1007/978-3-030-50153-2_46
sha: e6268f9a263ea45608bbb506b25050aa6fcdcdae
doc_id: 44860
cord_uid: gqjsuqid

We prove that the unification type of Łukasiewicz logic with a finite number of variables is either infinitary or nullary. To achieve this result we use Ghilardi’s categorical characterisation of unification types in terms of projective objects, the categorical duality between finitely presented MV-algebras and rational polyhedra, and a homotopy-theoretic argument.

The classical, syntactic unification problem is: given two terms s, t in a purely functional language, find a uniform replacement of the variables occurring in s and t by other terms that makes s and t identical. The substitution is then called unifier. When the latter syntactical identity is replaced by equality modulo a given equational theory E, one speaks of E-unification. The study of unification modulo an equational theory has acquired increasing significance in recent years (see e.g. [2, 3] ). The most basic piece of information one would like to have about E in connection with unification issues is its unification type. In order to define it precisely, let us recall some standard notions.

We consider a set F of function symbols along with a further set V = {X 1 , X 2 , . . .} of variables. We then let Term V (F ) be the term algebra built from F and V in the usual manner [5, Definition 10.1] . A substitution is a mapping σ : V → Term V (F ) that acts identically but for a finite number of exceptions, i.e. is such that {X ∈ V | σ(X) = X} is a finite set. Any substitution extends in a unique way to the whole Term V (F ) by requiring that it commutes with operations; hence it makes sense to speak of composition between substitutions.

Let E be a set of equations in the language F . A unification problem modulo E is a finite set of pairs for some finite index set J. A unifier for E is a substitution σ such that E |= σ(s j ) ≈ σ(t j ) , for each j ∈ J, i.e. such that the equality σ(s j ) = σ(t j ) holds in every algebra of the variety V E in the usual universal-algebraic sense [5, p. 78 ]. The problem E is unifiable if it admits at least one unifier. The set U (E ) of unifiers for E can be partially ordered as follows. If σ and τ are substitutions we say that σ is more general than τ (with respect to E), written τ E σ, if there exists a substitution ρ such that

holds for every X ∈ V . This amounts to saying that τ is an instantiation of σ, up to E-equivalence. We endow U (E ) with the relation E . The relation E is a pre-order. Let ∼ be the equivalence relation: u ∼ w if and only if both u E w and w E u hold. Then the quotient U (E ) ∼ carries a canonical partial order given by:

The unification type of the unification problem E is: The unification types above are listed in order of desirability, with nullary being the worst possible case. The unification type of the equational theory E is now defined to be the worst unification type occurring among the unifiable problems E modulo E.

Unification has also found applications in the study of non classical logics for its connections with admissible rules [10, 11, 13, 14] . For a propositional logic L, a unification problem is simply a formula of L and a unifier is a substitution that makes that formula into a theorem. When a logic has an equivalent algebraic semantics, in the sense of [4] , given by a class of algebras axiomatised by a set E of equations, the unification type of the logic and the unification type of E are the same. This paper is devoted to an investigation of the unification type of fragments of Lukasiewicz (infinite-valued propositional) logic where only a finite number of variables are available. The standard references for Lukasiewicz logic are [7, 18] .

The unification type of Lukasiewicz logic is known to be the worst possible:

). The unification type of Lukasiewicz logic is nullary. Specifically, consider the unification problem

where p 1 and p 2 are distinct propositional variables. Then the partially ordered set of unifiers for E contains a co-final chain of order-type ω.

By a chain of order-type ω we mean, as usual, a totally ordered set that is orderisomorphic to the natural numbers with their natural order. Recall also that a subset C of a partially ordered set (P, ) is co-final if for every p ∈ P there is c ∈ C with p c. In particular, Theorem 1 implies that no unifier for the unifiable problem E is maximally general -a condition that is strictly stronger than nullarity.

The proof of Theorem 1 requires an infinite amount of distinct propositional variables to be carried out-see Remark 4 for more details. Therefore the problem of establishing the unification type of fragments of Lukasiewicz logic with a finite number of variables was left open. The only case for which the unifications type was settled is the fragment of Lukasiewicz logic with only one variable. In this case the unification type is finitary (in a sense almost unitary): We shall see that when at least two variables are allowed the unification type becomes again non-finitary. The main result of this paper, Theorem 5, asserts that for every n 2 the unification type of the fragment of Lukasiewicz logic with n distinct variables has unification type either infinitary of nullary. To establish such a result we first move to the equivalent algebraic semantics of Lukasiewicz logic, called MV-algebras; we then use Ghilardi's characterisation of the unification type in terms of projective and finitely presented objects [9] ; as next step we use the duality between finitely presented MV-algebras and rational polyhedra [16] . In this latter category we build an infinite family of (dual) unifiers for the (dual of the) unification problem ( ) with the property that any infinite subfamily does not admit an upper bound in the order E . The proof of this last result rests upon the lifting property of the universal cover of the polyhedron associated with ( ).

We briefly discuss all these diverse tools used in the proof. More specifically, in Sect. 2 we spell out some preliminaries: in Subsect. 2.1 we summarise Ghilardi's approach to E-unification through projectivity; Subsect. 2.2 contains some basic information about MV-algebras and the background on polyhedral geometry required to state the duality theorem for finitely presented MV-algebras; in Subsect. 2.3 we give the needed background in algebraic topology. Finally, in Sect. 3 we prove the main theorem.

An object P in a category is called projective with respect to a class E of morphisms if for any f : A → B in E and any arrow g : P → B, there exists an arrow h : P → A such that the following diagram commutes.

The class E may consist of all epimorphisms, regular epimorphisms, strong epimorphisms, etc. In this paper, the main objects are algebras in a variety, and the arrow f : A → B is always taken to be a surjection. It is well known that surjections in a variety are the same thing as regular epimorphisms, see e.g. [1, (vi) on p. 135].

An object A in a category is said to be a retract of an object B if there are arrows s : A → B and r : B → A such that r • s is the identity on A. When this is the case, r is called a retraction (of s) and s a section (of r). If the category in question is a variety, it follows at once that r is surjective, and s is injective. One checks that on these definitions projective objects in any variety of algebras are stable under retractions, and they are precisely the retracts of free objects. In particular, free objects are projective.

Let us fix a variety V of algebras, and let us write F I for the free object in V generated by a set I. Recall that an algebra A of V is finitely presented if it is a quotient of the form A = F I /θ, with I finite and θ a finitely generated congruence. The elements of I are the generators of A, while any given set of pairs (s, t) ∈ θ that generates the congruence θ is traditionally called a set of relators for A.

Following [9] , by an algebraic unification problem we mean a finitely presented algebra A of V. An algebraic unifier for A is a homomorphism u : A → P with P a finitely presented projective algebra in V; and A is algebraically unifiable if such an algebraic unifier exists.

Given another algebraic unifier w : A → Q, we say that u is more general than w, written w V u, if there is a homomorphism g : P → Q making the following diagram commute.

The relation V is a pre-order on the set U (A) of algebraic unifiers for A and can be canonically quotiented into a partial order U (A) ∼ , V . The algebraic unification type of an algebraically unifiable finitely presented algebra A in the variety V is now defined exactly as in the symbolic case (see the Introduction), using the partially ordered set U (A) ∼ , V in place of U (E ) ∼ , E . One also defines the algebraic unification type of the variety V in the same fashion. 

Then E is unifiable if and only if A is algebraically unifiable. Further, the partially ordered sets U (A) ∼ , VE of algebraic unifiers for A, and U (E ) ∼ , E of unifiers for E , are isomorphic. In particular, the unification type of E and the algebraic unification type of V E coincide. Remark 1. Ghilardi's approach to unification goes far beyond the universalalgebraic contexts. Indeed, one readily sees that projectivity can be stated in any category, while thanks to the work of Gabriel and Ulmer [8] we know that the concept of 'finitely-presented' object makes sense in any locally small category. In particular this shows that the unification type is preserved under categorical equivalences.

The equivalent algebraic semantics of Lukasiewicz logic, in the precise sense of Blok and Pigozzi [4] , is given by MV-algebras. An MV-algebra is an algebraic structure (M, ⊕, ¬, 0), where 0 ∈ M is a constant, ¬ is a unary operation satisfying ¬¬x = x, ⊕ is a binary operation making (M, ⊕, 0) a commutative monoid, the element 1 defined as ¬0 satisfies x ⊕ 1 = 1, and the law

holds. Any MV-algebra has an underlying structure of distributive lattice bounded below by 0 and above by 1. Joins are defined as x ∨ y = ¬(¬x ⊕ y) ⊕ y. Thus, the characteristic law (1) states that x ∨ y = y ∨ x. Meets are defined by the de Morgan condition x ∧ y = ¬(¬x ∨ ¬y). Boolean algebras are precisely those MV-algebras that are idempotent, meaning that x ⊕ x = x holds, or equivalently, that satisfy the tertium non datur law x ∨ ¬x = 1. The interval [0, 1] ⊆ R can be made into an MV-algebra with neutral element 0 by defining x ⊕ y = min {x + y, 1} and ¬x = 1 − x. The underlying lattice order of this MV-algebra coincides with the natural order that [0, 1] inherits from the real numbers. This MV-algebra is often referred as the standard MV-algebra. Let us fix an integer d 0 as the dimension of the real vector space R d . A convex combination of a finite set of vectors v 1 , . . . , v u ∈ R d is any vector of the form λ 1 v 1 +· · ·+λ u v u , for non-negative real numbers λ i 0 satisfying u i=1 λ i = 1. If S ⊆ R d is any subset, we let conv S denote the convex hull of S, i.e. the collection of all convex combinations of finite sets of vectors v 1 , . . . , v u ∈ S. A polytope is any subset of R d of the form conv S, for some finite S ⊆ R d , and a (compact ) polyhedron is a union of finitely many polytopes in R d . A polytope is rational if it may be written in the form conv S for some finite set S ⊆ Q d ⊆ R d of vectors with rational coordinates. Similarly, a polyhedron is rational if it may be written as a union of finitely many rational polytopes.

Throughout, the adjective 'linear' is to be understood as 'affine linear'. A function f : R d → R is piecewise linear if it is continuous (with respect to the Euclidean topology on R d and R), and there is a finite set of linear functions l 1 , . . . , l u such that for each x ∈ R d one has f (x) = l i (x) for some choice of i = 1, . . . , u. If, moreover, each l i can be written as a linear polynomial with integer coefficients, then f is called Z-map. For an integer d 0, a function λ = (λ 1 , . . . , λ d ): R d → R d is a piecewise linear map (respectively, a Z-map) if each one of its scalar components λ j : R d → R is a piecewise linear function (respectively, Z-map). We now define piecewise linear maps (Z-maps) A → B for arbitrary subsets A ⊆ R d , B ⊆ R d as the restriction and co-restriction of piecewise linear maps (Z-maps) R d → R d .

When the spaces at issue are rational polyhedra, a useful equivalent to the preceding definition of Z-map is available.

Let P ⊆ R d be a rational polyhedron, and let f : P → R be a continuous function. Then the following are equivalent.

2. There exist finitely many linear polynomials with integer coefficients l 1 , . . . , l u : R d → R such that, for each p ∈ P , f (p) = l ip (p) for some i p ∈ {1, . . . , u}.

Notice that in item 2 the result of gluing the linear polynomials l 1 , . . . , l u is only required to be continuous on P and not on the whole R n . For example, consider a polyhedron P which is a disjoint union of two polytopes A and B, and consider the map f : P → R defined by f (x) = 0 for x ∈ A and f (x) = 1 for x ∈ B. By lemma 1, f is automatically a Z-map; we do not need to interpolate the two maps constantly equal to 0 and 1. To see that the hypothesis that P be a polyhedron is crucial, see [16, Remark 4.10] . It is not hard to show that the composition of Z-maps between rational polyhedra is again a Z-map. A Z-map λ : A → B between rational polyhedra A ⊆ R d and B ⊆ R d is a Z-homeomorphism if there exists a Z-map λ : B → A such that λ • λ = 1 B and λ • λ = 1 A . In other words, a Z-map is a Zhomeomorphism if it is a homeomorphism whose inverse is a Z-map, too. With these definitions, rational polyhedra and Z-maps form a category.

The following result is a particular case of a larger duality for semisimple MV-algebras (see [6, 16] for more details).

Remark 2. Theorem 4 provides a back-and-forth translation of algebraic concepts into geometric ones. Free n-generated MV-algebras correspond to [0, 1] n , an algebraic unification problem (=finitely presented MV-algebra) A becomes a rational polyhedron Q and an algebraic unifier for A (=finitely presented projective MV-algebra B with a homomorphism f : A → B) becomes a polyhedron P , which is a retract by Z-maps of [0, 1] n for some n ∈ N, together with a Z-map g : P → Q (because the equivalence is contravariant). We shall call co-unifier such a pair (P, g).

Let us recall some standard notions from algebraic topology; we refer to [12] for details.

A path in a space X is a continuous map f : [0, 1] → X; the endpoints of f are f (0) and f (1). A space X is path-connected if for any x 0 , x 1 ∈ X there is a path in X with endpoints x 0 , x 1 . On the other hand, X is locally path-connected if each point has arbitrarily small open neighbourhoods that are path-connected; that is, for each y ∈ X and each neighbourhood U of y there is a path-connected open neighbourhood of y contained in U . It is not hard to prove that polyhedra are locally path-connected (in fact, locally contractible by [12, Proposition A.1]), and therefore that a polyhedron is connected if and only if it is path-connected.

A loop in X is a path p in X such that p(0) = p (1) . A space X is simplyconnected if it is path-connected and, for every loop p in X, letting If p :X → X is a covering map of the space X, and if Y is any space, a continuous map f : Y → X is said to lift to p (or, more informally, toX, when p is understood), if there is a continuous mapf : Y →X such that p •f = f . Any suchf is then called a lift of f . In the next lemma we recall two important properties of covering maps with respect to lifts that we will use in Sect. 3. Proposition 1.33 and 1.34]) . Given topological spaces X andX, suppose that p :X → X is a covering map. Further, let Y be a topological space, and let f : Y → X be a continuous map. Then the following hold. It is not hard to prove that polyhedra are locally path-connected (in fact, locally contractible by [12, Proposition A.1]), so item 2 applies to any simply-connected polyhedron Y . Given a path-connected, locally path-connected space X, a covering map p :X → X is called a universal covering map ifX is simply-connected. In this caseX is called the universal cover of X. This name is due to the fact that, among the covering maps t : Y → X with Y connected, a universal covering map p :X → X is characterised by a certain universal property-namely, p factors through every such a t. A universal covering map (of a path-connected, locally path-connected space) is essentially unique. Under suitable conditions, a space X admits a universal cover (see [12, Theorem 1.38] ). The following is an example of universal covering map.

be the unit circle in the Euclidean plane R 2 , and let χ : R → S 1 be the continuous function given by t → (cos 2πt, sin 2πt).

Upon embedding R into R 3 as a helix H via t → (cos 2πt, sin 2πt, t), χ acts on H as the orthogonal projection onto S 1 along the z-axis. The surjective map χ : R → S 1 is the universal covering map of the circle, and R is the universal cover of S 1 .

Having set up all necessary background we turn to the main question of the paper: what is the unification type of the fragments of Lukasiewicz logic with at most n variables, with n 2? So, we are interested in unification problems and unifiers that involve at most n variables. More precisely, using the algebraic notation introduced at the beginning of the paper, for any fixed n 2, we let V n := {X 1 . . . , X n } and F be the set of basic operations in the language of MValgebras. We consider only unification problems whose terms range in Term V (F ) and unifiers going from V into Term V (F ). In terms of the framework presented in Sect. 2.1 this corresponds to restricting to finitely presented and projective algebras with up to n-generators, which we call n-generated.

Let us call a polyhedron n-generated if it is Z-homeomorphic to a polyhedron inside [0, 1] n . An easy inspection of [16] shows that the duality of Theorem 4 restricts as follows.

We will concentrate on the co-unifiers of the rational polyhedron given by the border of the unit square:

Consider the map ζ : R → B which wraps R around B, counter-clockwise, at constant speed 1, sending 0 to (0, 0). More precisely,

where x is the greatest integer below x.

Remark 3. Upon embedding R into R 3 as a squared helix H, as depicted in Fig. 1 , ζ acts on H as the orthogonal projection onto B along the z-axis. Proof. This is obvious as B is homeomorphic to S 1 and up to homeomorphism ζ maps R on B as χ does on S 1 in Example 1.

Notice that ζ is continuous but is not a Z-map; however, the following holds. Proof. This can be seen using Lemma 1. Indeed, ζ a,b is defined on every interval [a + i, a + i + 1], with 0 i < |b − a|, by one of the four cases of Eq. (3); each of those functions is linear with integer coefficients on [a + i, a + i + 1] because x − x can be written on such an interval as x − (a + i).

Remark 4. The co-final chain of Theorem 1 is obtained by taking increasingly larger parts of the piece-wise linear spiral depicted in Fig. 1 , together with their projections onto B. An easy argument shows that Z-homeomorphisms preserve the number of points with integer coordinates. As a consequence, it can be seen that there can be no finite bound on the dimensions of the unital cubes that embed the rational polyhedra in the above mentioned increasing sequence. Hence the proof strategy of Theorem 1 cannot be adopted for fragments of Lukasiewicz logic with a finite amounts of variables.

Let Y be a connected space and f, g : Y → R be a pair of continuous functions. If ζ • f = ζ • g then there exists k ∈ Z such that, for every y ∈ Y ,

Proof. Let y 0 be any point of Y . By inspection of the definition (3) one easily sees that ζ(f (y 0 )) = ζ(g(y 0 )) entails the existence of some k ∈ Z such that g(y 0 ) − f (y 0 ) = 4k. Since by definition ζ has period 4, ζ • g = ζ • f = ζ • (f + 4k), so the maps g : Y → R and f +4k : Y → R are both lifts to R of ζ•g. By the choice of y 0 , both g and f + 4k attain the same value at y 0 , because g(y 0 ) = f (y 0 ) + 4k. Thus, by item 1 in Lemma 2, g = f + 4k.

Let Y be a connected space and f : Y → B be a continuous map which admits a lift to ζ. Every liftf : Y → R has a connected image, whose length 1 , by Lemma 5, is independent of the choice off . We denote the length of f [Y ] with d(Y, f ) and we call it the degree of (Y, f ). Proof. It is straightforward to verify that, if A is a retract of B in the category of topological spaces and continuous functions, and B is simply-connected, then A is simply-connected. As a consequence, if (P, f ) is a co-unifier, then P is simplyconnected. So by item 2 in Lemma 2, f admits a lift. Moreover, d(P, f ) is finite because P is compact. Proof. The polyhedron [0, 1] is obviously a retract of itself. Furthermore, notice that v n is a Z-map whose image is [0, 4n] and, by Lemma 4, the restriction of ζ to [0, 4n] is a Z-map. Since composition of Z-maps is a Z-map, we have that each f n is indeed a Z-map. Proof. Let F be such a subset. Since F is infinite, by Lemma 9, it must contain co-unifiers of arbitrarily large degree. Thus, by Lemma 7 an upper bound of such a family of co-unifiers cannot have finite degree and this contradicts Lemma 6.

Theorem 5. For every n 2 the fragments of Lukasiewicz logic with n distinct variables have unification type either infinitary or nullary.

Proof. By way of contradiction, let us suppose that the fragment of Lukasiewicz logic with n distinct variables has finitary unification type. Then, by coupling Theorem 3 with Corollary 1, we get the the co-unification type of B must be finitary. Let (Q 1 , g 1 ), . . . , (Q k , g k ) be the maximal co-unifiers of B. So each counifier ([0, 1], f m ) must be less general than some (Q i , g i ) for i k. Since k is finite there must be at least an infinite family {([0, 1], f mj ) | j ∈ N} of co-unifiers that are all less general than some (Q i , g i ). This contradicts Lemma 11.

Locally Presentable and Accessible Categories

Unification in modal and description logics

Unification theory

Algebraizable logics

A Course in Universal Algebra

MV-algebras, infinite dimensional polyhedra, and natural dualities

Algebraic Foundations of Many-Valued Reasoning

Lokal präsentierbare Kategorien. LNM

Unification through projectivity

Unification in intuitionistic logic

Best solving modal equations

Algebraic Topology

On the admissible rules of intuitionistic propositional logic

Admissible rules of modal logics

Categories for the Working Mathematician. GTM

The dual adjunction between MV-algebras and Tychonoff spaces

Duality, projectivity, and unification in Lukasiewicz logic and MV-algebras

Advanced Lukasiewicz Calculus and MV-algebras