-
Complexities of Well-Quasi-Ordered Substructural Logics
Authors:
Nikolaos Galatos,
Vitor Greati,
Revantha Ramanayake,
Gavin St. John
Abstract:
Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity), and associativity. This leads to a resource-sensitive logical framework that has proven influential beyond mathematical logic and its algebraic semantics, across theoretical computer science, linguistics, and philosophic…
▽ More
Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity), and associativity. This leads to a resource-sensitive logical framework that has proven influential beyond mathematical logic and its algebraic semantics, across theoretical computer science, linguistics, and philosophical logic. The set of theorems of a substructural logic is recursively enumerable and, in many cases, recursive. These logics also possess an intricate mathematical structure that has been the subject of research for over six decades.
We undertake a comprehensive study of substructural logics possessing an underlying well-quasi-order (wqo), using established ordinal-indexed fast-growing complexity classes to classify the complexity of their deducibility (quasiequational) and provability (equational) problems. This includes substructural logics with weak variants of contraction and weakening, and logics with weak or even no exchange. We further consider infinitely many axiomatic extensions over the base systems.
We establish a host of decidability and complexity bounds, many of them tight, by developing new techniques in proof theory, well-quasi-order theory (contributing new length theorems), the algebraic semantics of substructural logics via residuated lattices, algebraic proof theory, and novel encodings of counter machines. Classifying the computational complexity of substructural logics (and the complexity of the word problem and of the equational theory of their algebraic semantics) reveals how subtle variations in their design influence their algorithmic behavior, with the decision problems often reaching Ackermannian or even hyper-Ackermannian complexity.
△ Less
Submitted 30 April, 2025;
originally announced April 2025.
-
Axiomatizing small varieties of periodic l-pregroups
Authors:
Nikolaos Galatos,
Simon Santschi
Abstract:
We provide an axiomatization for the variety generated by the $n$-periodic l-pregroup $\mathbf{F}_n(\mathbb{Z})$, for every $n \in \mathbb{Z}^+$, as well as for all possible joins of such varieties; the finite joins form an ideal in the subvariety lattice of l-pregroups and we describe fully its lattice structure. On the way, we characterize all finitely subdirectly irreducible (FSI) algebras in t…
▽ More
We provide an axiomatization for the variety generated by the $n$-periodic l-pregroup $\mathbf{F}_n(\mathbb{Z})$, for every $n \in \mathbb{Z}^+$, as well as for all possible joins of such varieties; the finite joins form an ideal in the subvariety lattice of l-pregroups and we describe fully its lattice structure. On the way, we characterize all finitely subdirectly irreducible (FSI) algebras in the variety generated by $\mathbf{F}_n(\mathbb{Z})$ as the $n$-periodic l-pregroups that have a totally ordered group skeleton (and are not trivial). The finitely generated FSIs that are not l-groups are further characterized as lexicographic products of a (finitely generated) totally ordered abelian l-group and $\mathbf{F}_k(\mathbb{Z})$, where $k \mid n$.
△ Less
Submitted 24 March, 2025;
originally announced March 2025.
-
Generation and decidability for periodic l-pregroups
Authors:
Nikolaos Galatos,
Isis A. Gallardo
Abstract:
In [11] it is shown that the variety $\mathsf{DLP}$ of distributive l-pregroups is generated by a single algebra, the functional algebra $\mathbf{F}(Z)$ over the integers. Here, we show that $\mathsf{DLP}$ is equal to the join of its subvarieties $\mathsf{LPn}$, for $n\in\mathbb{Z}$, consisting of n-periodic l-pregroups. We also prove that every algebra in $\mathsf{LPn}$ embeds into the subalgebra…
▽ More
In [11] it is shown that the variety $\mathsf{DLP}$ of distributive l-pregroups is generated by a single algebra, the functional algebra $\mathbf{F}(Z)$ over the integers. Here, we show that $\mathsf{DLP}$ is equal to the join of its subvarieties $\mathsf{LPn}$, for $n\in\mathbb{Z}$, consisting of n-periodic l-pregroups. We also prove that every algebra in $\mathsf{LPn}$ embeds into the subalgebra $\mathbf{F}_n(Ω)$ of n-periodic elements of $\mathbf{F}(Ω)$, for some integral chain $Ω$; we use this representation to show that for every n, the variety $\mathsf{LPn}$ is generated by the single algebra $\mathbf{F}_n(\mathbb{Q}\overrightarrow{\times}\mathbb{Z})$, noting that the chain $\mathbb{Q}\overrightarrow{\times}\mathbb{Z}$ is independent of n. We further establish a second representation theorem: every algebra in $\mathsf{LPn}$ embeds into the wreath product of an l-group and $\mathbf{F}_n(\mathbb{Z})$, showcasing the prominent role of the simple n-periodic l-pregroup $\mathbf{F}_n(\mathbb{Z})$. Moreover, we prove that the join of the varieties $V(\mathbf{F}_n(\mathbb{Z}))$ is also equal to $\mathsf{DLP}$, hence equal to the join of the varieties $\mathsf{LPn}$, even though $\mathsf{V}(\mathbf{F}_n(\mathbb{Z}))$ is not equal to \mathsf{LPn} for every single n. In this sense, $\mathsf{DLP}$ has two different well-behaved approximations. We further prove that, for every n, the equational theory of $\mathbf{F}_n(\mathbb{Z})$ is decidable and, using the wreath product decomposition, we show that the equational theory of $\mathsf{LPn}$ is decidable, as well.
△ Less
Submitted 8 March, 2024;
originally announced March 2024.
-
Decidability of distributive l-pregroups
Authors:
Nikolaos Galatos,
Isis A. Gallardo
Abstract:
We show that every distributive lattice-ordered pregroup can be embedded into a functional algebra over an integral chain, thus improving the existing Cayley/Holland-style embedding theorem. We use this to show that the variety of all distributive lattice-ordered pregroups is generated by the single functional algebra on the integers. Finally, we show that the equational theory of the variety is d…
▽ More
We show that every distributive lattice-ordered pregroup can be embedded into a functional algebra over an integral chain, thus improving the existing Cayley/Holland-style embedding theorem. We use this to show that the variety of all distributive lattice-ordered pregroups is generated by the single functional algebra on the integers. Finally, we show that the equational theory of the variety is decidable.
△ Less
Submitted 19 October, 2023;
originally announced October 2023.
-
Gluing residuated lattices
Authors:
Nick Galatos,
Sara Ugolini
Abstract:
We introduce and characterize various gluing constructions for residuated lattices that intersect on a common subreduct, and which are subalgebras, or appropriate subreducts, of the resulting structure. Starting from the 1-sum construction (also known as ordinal sum for residuated structures), where algebras that intersect only in the top element are glued together, we first consider the gluing on…
▽ More
We introduce and characterize various gluing constructions for residuated lattices that intersect on a common subreduct, and which are subalgebras, or appropriate subreducts, of the resulting structure. Starting from the 1-sum construction (also known as ordinal sum for residuated structures), where algebras that intersect only in the top element are glued together, we first consider the gluing on a congruence filter, and then add a lattice ideal as well. We characterize such constructions in terms of (possibly partial) operators acting on (possibly partial) residuated structures. As particular examples of gluing constructions, we obtain the non-commutative version of some rotation constructions, and an interesting variety of semilinear residuated lattices that are 2-potent. This study also serves as a first attempt toward the study of amalgamation of non-commutative residuated lattices, by constructing an amalgam in the special case where the common subalgebra in the V-formation is either a special (congruence) filter or the union of a filter and an ideal.
△ Less
Submitted 31 May, 2023;
originally announced June 2023.
-
Unilinear residuated lattices: axiomatization, varieties and FEP
Authors:
Nick Galatos,
Xiao Zhuang
Abstract:
We characterize all residuated lattices that have height equal to $3$ and show that the variety they generate has continuum-many subvarieties. More generally, we study unilinear residuated lattices: their lattice is a union of disjoint incomparable chains, with bounds added. We we give two general constructions of unilinear residuated lattices, provide an axiomatization and a proof-theoretic calcu…
▽ More
We characterize all residuated lattices that have height equal to $3$ and show that the variety they generate has continuum-many subvarieties. More generally, we study unilinear residuated lattices: their lattice is a union of disjoint incomparable chains, with bounds added. We we give two general constructions of unilinear residuated lattices, provide an axiomatization and a proof-theoretic calculus for the variety they generate, and prove the finite model property for various subvarieties.
△ Less
Submitted 11 April, 2023;
originally announced April 2023.
-
Semiconic Idempotent Logic II: Beth Definability and Deductive Interpolation
Authors:
Wesley Fussner,
Nick Galatos
Abstract:
Semiconic idempotent logic sCI is a common generalization of intuitionistic logic, semilinear idempotent logic sLI, and in particular relevance logic with mingle. We establish the projective Beth definability property and the deductive interpolation property for many extensions of sCI, and identify extensions where these properties fail. We achieve these results by studying the (strong) amalgamati…
▽ More
Semiconic idempotent logic sCI is a common generalization of intuitionistic logic, semilinear idempotent logic sLI, and in particular relevance logic with mingle. We establish the projective Beth definability property and the deductive interpolation property for many extensions of sCI, and identify extensions where these properties fail. We achieve these results by studying the (strong) amalgamation property and the epimorphism-surjectivity property for the corresponding algebraic semantics, viz. semiconic idempotent residuated lattices. Our study is made possible by the structural decomposition of conic idempotent models achieved in the prequel, as well as a detailed analysis of the structure of idempotent residuated chains serving as index sets in this decomposition. Here we study the latter on two levels: as certain enriched Galois connections and as enhanced monoidal preorders. Using this, we show that although conic idempotent residuated lattices do not have the amalgamation property, the natural class of rigid and conjunctive conic idempotent residuated lattices has the strong amalgamation property, and thus has surjective epimorphisms. This extends to the variety generated by rigid and conjunctive conic idempotent residuated lattices, and we establish the (strong) amalgamation and epimorphism-surjectivity properties for several important subvarieties. Using the algebraizability of sCI, this yields the deductive interpolation property and the projective Beth definability property for the corresponding substructural logics extending sCI.
△ Less
Submitted 20 July, 2023; v1 submitted 20 August, 2022;
originally announced August 2022.
-
Complemented MacNeille completions and algebras of fractions
Authors:
Nick Galatos,
Adam Přenosil
Abstract:
We introduce ($\ell$-)bimonoids as ordered algebras consisting of two compatible monoidal structures on a partially ordered (lattice-ordered) set. Bimonoids form an appropriate framework for the study of a general notion of complementation, which subsumes both Boolean complements in bounded distributive lattices and multiplicative inverses in monoids. The central question of the paper is whether a…
▽ More
We introduce ($\ell$-)bimonoids as ordered algebras consisting of two compatible monoidal structures on a partially ordered (lattice-ordered) set. Bimonoids form an appropriate framework for the study of a general notion of complementation, which subsumes both Boolean complements in bounded distributive lattices and multiplicative inverses in monoids. The central question of the paper is whether and how bimonoids can be embedded into complemented bimonoids, generalizing the embedding of cancellative commutative monoids into their groups of fractions and of bounded distributive lattices into their free Boolean extensions. We prove that each commutative ($\ell$-)bimonoid indeed embeds into a complete complemented commutative $\ell$-bimonoid in a doubly dense way reminiscent of the Dedekind--MacNeille completion. Moreover, this complemented completion, which is term equivalent to a commutative involutive residuated lattice, sometimes contains a tighter complemented envelope analogous to the group of fractions. In the case of cancellative commutative monoids this algebra of fractions is precisely the familiar group of fractions, while in the case of Brouwerian (Heyting) algebras it is a (bounded) idempotent involutive commutative residuated lattice. This construction of the algebra of fractions in fact yields a categorical equivalence between varieties of integral and of involutive residuated structures which subsumes as special cases the known equivalences between Abelian $\ell$-groups and their negative cones, and between Sugihara monoids and their negative cones.
△ Less
Submitted 1 February, 2023; v1 submitted 18 November, 2021;
originally announced November 2021.
-
Twist structures and Nelson conuclei
Authors:
Manuela Busaniche,
Nikolaos Galatos,
Miguel Andrés Marcos
Abstract:
Motivated by Kalman residuated lattices, Nelson residuated lattices and Nelson paraconsistent residuated lattices, we provide a natural common generalization of them. Nelson conucleus algebras unify these examples and further extend them to the non-commutative setting. We study their structure, establish a representation theorem for them in terms of twist structures and conuclei that results in a…
▽ More
Motivated by Kalman residuated lattices, Nelson residuated lattices and Nelson paraconsistent residuated lattices, we provide a natural common generalization of them. Nelson conucleus algebras unify these examples and further extend them to the non-commutative setting. We study their structure, establish a representation theorem for them in terms of twist structures and conuclei that results in a categorical adjunction, and explore situations where the representation is actually an isomorphism. In the latter case, the adjunction is elevated to a categorical equivalence. By applying this representation to the original motivating special cases we bring to the surface their underlying similarities.
△ Less
Submitted 18 June, 2021;
originally announced July 2021.
-
From distributive l-monoids to l-groups, and back again
Authors:
Almudena Colacito,
Nikolaos Galatos,
George Metcalfe,
Simon Santschi
Abstract:
We prove that an inverse-free equation is valid in the variety LG of lattice-ordered groups (l-groups) if and only if it is valid in the variety DLM of distributive lattice-ordered monoids (distributive l-monoids). This contrasts with the fact that, as proved by Repnitskii, there exist inverse-free equations that are valid in all Abelian l-groups but not in all commutative distributive l-monoids,…
▽ More
We prove that an inverse-free equation is valid in the variety LG of lattice-ordered groups (l-groups) if and only if it is valid in the variety DLM of distributive lattice-ordered monoids (distributive l-monoids). This contrasts with the fact that, as proved by Repnitskii, there exist inverse-free equations that are valid in all Abelian l-groups but not in all commutative distributive l-monoids, and, as we prove here, there exist inverse-free equations that hold in all totally ordered groups but not in all totally ordered monoids. We also prove that DLM has the finite model property and a decidable equational theory, establish a correspondence between the validity of equations in DLM and the existence of certain right orders on free monoids, and provide an effective method for reducing the validity of equations in LG to the validity of equations in DLM.
△ Less
Submitted 6 March, 2022; v1 submitted 27 February, 2021;
originally announced March 2021.
-
Most simple extensions of $\mathsf{FL_e}$ are undecidable
Authors:
Nikolaos Galatos,
Gavin St. John
Abstract:
All known structural extensions of the substructural logic $\mathsf{FL_e}$, Full Lambek calculus with exchange/commutativity, (corresponding to subvarieties of commutative residuated lattices axiomatized by $\{\vee, \cdot, 1\}$-equations) have decidable theoremhood; in particular all the ones defined by knotted axioms enjoy strong decidability properties (such as the finite embeddability property)…
▽ More
All known structural extensions of the substructural logic $\mathsf{FL_e}$, Full Lambek calculus with exchange/commutativity, (corresponding to subvarieties of commutative residuated lattices axiomatized by $\{\vee, \cdot, 1\}$-equations) have decidable theoremhood; in particular all the ones defined by knotted axioms enjoy strong decidability properties (such as the finite embeddability property). We provide infinitely many such extensions that have undecidable theoremhood, by encoding machines with undecidable halting problem. An even bigger class of extensions is shown to have undecidable deducibility problem (the corresponding varieties of residuated lattices have undecidable word problem); actually with very few exceptions, such as the knotted axioms and the other prespinal axioms, we prove that undecidability is ubiquitous. Known undecidability results for non-commutative extensions use an encoding that fails in the presence of commutativity, so and-branching counter machines are employed. Even these machines provide encodings that fail to capture proper extensions of commutativity, therefore we introduce a new variant that works on an exponential scale. The correctness of the encoding is established by employing the theory of residuated frames.
△ Less
Submitted 1 May, 2020;
originally announced May 2020.
-
Theorems of Alternatives for Substructural Logics
Authors:
Almudena Colacito,
Nikolaos Galatos,
George Metcalfe
Abstract:
A theorem of alternatives provides a reduction of validity in a substructural logic to validity in its multiplicative fragment. Notable examples include a theorem of Arnon Avron that reduces the validity of a disjunction of multiplicative formulas in the R-mingle logic RM to the validity of a linear combination of these formulas, and Gordan's theorem for solutions of linear systems over the real n…
▽ More
A theorem of alternatives provides a reduction of validity in a substructural logic to validity in its multiplicative fragment. Notable examples include a theorem of Arnon Avron that reduces the validity of a disjunction of multiplicative formulas in the R-mingle logic RM to the validity of a linear combination of these formulas, and Gordan's theorem for solutions of linear systems over the real numbers, that yields an analogous reduction for validity in Abelian logic A. In this paper, general conditions are provided for axiomatic extensions of involutive uninorm logic without additive constants to admit a theorem of alternatives. It is also shown that a theorem of alternatives for a logic can be used to establish (uniform) deductive interpolation and completeness with respect to a class of dense totally ordered residuated lattices.
△ Less
Submitted 26 February, 2020;
originally announced February 2020.
-
Categories of Models of R-Mingle
Authors:
Wesley Fussner,
Nick Galatos
Abstract:
We give a new Esakia-style duality for the category of Sugihara monoids based on the Davey-Werner natural duality for lattices with involution, and use this duality to greatly simplify a construction due to Galatos-Raftery of Sugihara monoids from certain enrichments of their negative cones. Our method of obtaining this simplification is to transport the functors of the Galatos-Raftery constructio…
▽ More
We give a new Esakia-style duality for the category of Sugihara monoids based on the Davey-Werner natural duality for lattices with involution, and use this duality to greatly simplify a construction due to Galatos-Raftery of Sugihara monoids from certain enrichments of their negative cones. Our method of obtaining this simplification is to transport the functors of the Galatos-Raftery construction across our duality, obtaining a vastly more transparent presentation on duals. Because our duality extends Dunn's relational semantics for the logic R-mingle to a categorical equivalence, this also explains the Dunn semantics and its relationship with the more usual Routley-Meyer semantics for relevant logics.
△ Less
Submitted 24 October, 2017; v1 submitted 11 October, 2017;
originally announced October 2017.
-
Canonical formulas for k-potent commutative, integral, residuated lattices
Authors:
Nick Bezhanishvili,
Nick Galatos,
Luca Spada
Abstract:
Canonical formulas are a powerful tool for studying intuitionistic and modal logics. Actually, they provide a uniform and semantic way to axiomatise all extensions of intuitionistic logic and all modal logics above K4. Although the method originally hinged on the relational semantics of those logics, recently it has been completely recast in algebraic terms. In this new perspective canonical formu…
▽ More
Canonical formulas are a powerful tool for studying intuitionistic and modal logics. Actually, they provide a uniform and semantic way to axiomatise all extensions of intuitionistic logic and all modal logics above K4. Although the method originally hinged on the relational semantics of those logics, recently it has been completely recast in algebraic terms. In this new perspective canonical formulas are built from a finite subdirectly irreducible algebra by describing completely the behaviour of some operations and only partially the behaviour of some others. In this paper we export the machinery of canonical formulas to substructural logics by introducing canonical formulas for $k$-potent, commutative, integral, residuated lattices ($k$-$\mathsf{CIRL}$). We show that any subvariety of $k$-$\mathsf{CIRL}$ is axiomatised by canonical formulas. The paper ends with some applications and examples.
△ Less
Submitted 22 June, 2016; v1 submitted 26 September, 2015;
originally announced September 2015.
