arXiv subjects

Peter Jipsen

Publications and source records attributed to Peter Jipsen.

At least 19 recordsLinked to original sources

arXiv2026

Dialectica Categories over Heyting Algebras

Categorification---the process of constructing a categorical model of a piece of mathematics---often identifies a common abstraction that connects formerly unrelated but known structures. In the case of de Paiva's categorification of G\"odel's Dialectica interpretation, we find that its specialization to partial orders produces (functorial) embeddings of Heyting algebras into residuated lattices that appear to have been overlooked. For the non-categorical audience, we present this specialization and take care to reproduce the original proofs in the algebraic setting. Along the way we obtain results particular to this algebraic setting: an embedding lacking an evident adjoint in de Paiva's general construction acquires a definable one here; a single Dialectica tensor validates contraction in the intuitionistic construction D yet refutes it in the classical variant G; and, over ZF, the poset reflection PD(Set) collapses onto the four-element algebra PD(2) exactly when the Axiom of Choice holds.

math.LO↗

arXiv2026

The logic of bunched implications is undecidable

The logic of bunched implications (BI), introduced by O'Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the {and, or, not, --*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then --* splits into two divisions \, /). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.

math.LO↗

arXiv2025

Balanced residuated partially ordered semigroups

A residuated semigroup is a structure $\langle A,\le,\cdot,\backslash,/ \rangle$ where $\langle A,\le \rangle$ is a poset and $\langle A,\cdot \rangle$ is a semigroup such that the residuation law $x\cdot y\le z\iff x\le z/y\iff y\le x \backslash z$ holds. An element $p$ is positive if $a\le pa$ and $a \le ap$ for all $a$. A residuated semigroup is called balanced if it satisfies the equation $x \backslash x \approx x / x$ and moreover each element of the form $a \backslash a = a / a$ is positive, and it is called integrally closed if it satisfies the same equation and moreover each element of this form is a global identity. We show how a wide class of balanced residuated semigroups (so-called steady residuated semigroups) can be decomposed into integrally closed pieces, using a generalization of the classical Plonka sum construction. This generalization involves gluing a disjoint family of ordered algebras together using multiple families of maps, rather than a single family as in ordinary Plonka sums.

cs.LO↗

arXiv2025

Duality theory and representations for distributive quasi relation algebras and DInFL-algebras

We develop dualities for complete perfect distributive quasi relation algebras and complete perfect distributive involutive FL-algebras. The duals are partially ordered frames with additional structure. These frames are analogous to the atom structures used to study relation algebras. We also extend the duality from complete perfect algebras to all algebras, using so-called doubly-pointed frames with a Priestley topology. We then turn to the representability of these algebras as lattices of binary relations. Some algebras can be realised as term subreducts of representable relation algebras and are hence representable. We provide a detailed account of known representations for all algebras up to size six.

cs.LO↗

arXiv2025

Residuated lattices do not have the amalgamation property

We show that the variety of residuated lattices does not have the amalgamation property, thereby settling a long-standing open problem. In addition, we show that the amalgamation property fails for several subvarieties, including idempotent residuated lattices, involutive residuated lattices, and (integral) distributive residuated lattices.

math.RA↗

arXiv2024

On the structure of balanced residuated partially ordered monoids

A residuated poset is a structure $\langle A,\le,\cdot,\backslash,/,1 \rangle$ where $\langle A,\le \rangle$ is a poset and $\langle A,\cdot,1 \rangle$ is a monoid such that the residuation law $x\cdot y\le z\iff x\le z/y\iff y\le x\backslash z$ holds. A residuated poset is balanced if it satisfies the identity $x\backslash x \approx x/x$. By generalizing the well-known construction of Plonka sums, we show that a specific class of balanced residuated posets can be decomposed into such a sum indexed by the set of positive idempotent elements. Conversely, given a semilattice directed system of residuated posets equipped with two families of maps (instead of one, as in the usual case), we construct a residuated poset based on the disjoint union of their domains. We apply this approach to provide a structural description of some varieties of residuated lattices and relation algebras.

math.LO↗

arXiv2023

Locally Integral Involutive PO-Semigroups

We show that every locally integral involutive partially ordered semigroup (ipo-semigroup) $\mathbf A = (A,\le, \cdot, \sim,-)$, and in particular every locally integral involutive semiring, decomposes in a unique way into a family $\{\mathbf A_p : p\in A^+\}$ of integral ipo-monoids, which we call its integral components. In the semiring case, the integral components are unital semirings. Moreover, we show that there is a family of monoid homomorphisms $\Phi = \{\varphi_{pq}: \mathbf A_p\to \mathbf A_q : p\le q\}$, indexed over the positive cone $(A^+,\le)$, so that the structure of $\mathbf A$ can be recovered as a glueing $\int_\Phi \mathbf A_p$ of its integral components along $\Phi$. Reciprocally, we give necessary and sufficient conditions so that the P{\l}onka sum of any family of integral ipo-monoids $\{\mathbf A_p : p\in D\}$, indexed over a join-semilattice $(D,\lor)$ along a family of monoid homomorphisms $\Phi$ is an ipo-semigroup.

math.LO↗

arXiv2023

$S$-preclones and the Galois connection ${}^S\mathrm{Pol}$-${}^S\mathrm{Inv}$, Part I

We consider $S$-operations $f \colon A^{n} \to A$ in which each argument is assigned a signum $s \in S$ representing a "property" such as being order-preserving or order-reversing with respect to a fixed partial order on $A$. The set $S$ of such properties is assumed to have a monoid structure reflecting the behaviour of these properties under the composition of $S$-operations (e.g., order-reversing composed with order-reversing is order-preserving). The collection of all $S$-operations with prescribed properties for their signed arguments is not a clone (since it is not closed under arbitrary identification of arguments), but it is a preclone with special properties, which leads to the notion of $S$-preclone. We introduce $S$-relations $\varrho = (\varrho_{s})_{s \in S}$, $S$-relational clones, and a preservation property ($f \mathrel{\stackrel{S}{\triangleright}} \varrho$), and we consider the induced Galois connection ${}^S\mathrm{Pol}$-${}^S\mathrm{Inv}$. The $S$-preclones and $S$-relational clones turn out to be exactly the closed sets of this Galois connection. We also establish some basic facts about the structure of the lattice of all $S$-preclones on $A$.

math.RA↗

arXiv2023

Representable and diagonally representable weakening relation algebras

A binary relation defined on a poset is a weakening relation if the partial order acts as a both-sided compositional identity. This is motivated by the weakening rule in sequent calculi and closely related to models of relevance logic. For a fixed poset the collection of weakening relations is a subreduct of the full relation algebra on the underlying set of the poset. We present a two-player game for the class of representable weakening relation algebras akin to that for the class of representable relation algebras. This enables us to define classes of abstract weakening relation algebras that approximate the quasivariety of representable weakening relation algebras. We give explicit finite axiomatisations for some of these classes. We define the class of diagonally representable weakening relation algebras and prove that it is a discriminator variety. We also provide explicit representations for several small weakening relation algebras.

cs.LO↗

arXiv2022

Varieties of unary-determined distributive $\ell$-magmas and bunched implication algebras

A distributive lattice-ordered magma ($d\ell$-magma) $(A,\wedge,\vee,\cdot)$ is a distributive lattice with a binary operation $\cdot$ that preserves joins in both arguments, and when $\cdot$ is associative then $(A,\vee,\cdot)$ is an idempotent semiring. A $d\ell$-magma with a top $\top$ is unary-determined if $x{\cdot} y=(x{\cdot}\!\top\wedge y)$ $\vee(x\wedge \top\!{\cdot}y)$. These algebras are term-equivalent to a subvariety of distributive lattices with $\top$ and two join-preserving unary operations $\mathsf p,\mathsf q$. We obtain simple conditions on $\mathsf p,\mathsf q$ such that $x{\cdot} y=(\mathsf px\wedge y)\vee(x\wedge \mathsf qy)$ is associative, commutative, idempotent and/or has an identity element. This generalizes previous results on the structure of doubly idempotent semirings and, in the case when the distributive lattice is a Heyting algebra, it provides structural insight into unary-determined algebraic models of bunched implication logic. We also provide Kripke semantics for the algebras under consideration, which leads to more efficient algorithms for constructing finite models. We find all subdirectly irreducible algebras up to cardinality eight in which $\mathsf p=\mathsf q$ is a closure operator, as well as all finite unary-determined bunched implication chains and map out the poset of join-irreducible varieties generated by them.

math.LO↗

arXiv2021

A finite axiomatization of positive MV-algebras

Positive MV-algebras are the subreducts of MV-algebras with respect to the signature $\{\oplus, \odot, \lor, \land, 0, 1\}$. We provide a finite quasi-equational axiomatization for the class of such algebras.

math.LO↗

arXiv2021

Algorithmic correspondence for relevance logics, bunched implication logics, and relation algebras: the algorithm PEARL and its implementation (Technical Report)

The non-deterministic algorithmic procedure PEARL (an acronym for `Propositional variables Elimination Algorithm for Relevance Logic') has been recently developed for computing first-order equivalents of formulas of the language of relevance logics RL in terms of the standard Routley-Meyer relational semantics. It succeeds on a large class of axioms of relevance logics, including all so-called inductive formulas. In the present work we re-interpret PEARL from an algebraic perspective, with its rewrite rules seen as manipulating quasi-inequalities interpreted over Urquhart's relevant algebras, and report on its recent Python implementation. We also show that all formulae on which PEARL succeeds are canonical, i.e., preserved under canonical extensions of relevant algebras. This generalizes the "canonicity via correspondence" result in Urquhart's 1996 paper. We also indicate that, with minor modifications, PEARL can be applied to bunched implication algebras and relation algebras.

cs.LO↗

arXiv2020

The structure of finite commutative idempotent involutive residuated lattices

We characterize commutative idempotent involutive residuated lattices as disjoint unions of Boolean algebras arranged over a distributive lattice. We use this description to introduce a new construction, called gluing, that allows us to build new members of this variety from other ones. In particular, all finite members can be constructed in this way from Boolean algebras. Finally, we apply our construction to prove that the fusion reduct of any finite member is a distributive semilattice, and to show that this variety is not locally finite.

math.LO↗

arXiv2020

Injective and projective semimodules over involutive semirings

We show that the term equivalence between MV-algebras and MV-semirings lifts to involutive residuated lattices and a class of semirings called \textit{involutive semirings}. The semiring perspective helps us find a necessary and sufficient condition for the interval $[0,1]$ to be a subalgebra of an involutive residuated lattice. We also import some results and techniques of semimodule theory in the study of this class of semirings, generalizing results about injective and projective MV-semimodules. Indeed, we note that the involution plays a crucial role and that the results for MV-semirings are still true for involutive semirings whenever the Mundici functor is not involved. In particular, we prove that involution is a necessary and sufficient condition in order for projective and injective semimodules to coincide.

math.RA↗

arXiv2020

Structure theorems for idempotent residuated lattices

In this paper we study structural properties of residuated lattices that are idempotent as monoids. We provide descriptions of the totally ordered members of this class and obtain counting theorems for the number of finite algebras in various subclasses. We also establish the finite embeddability property for certain varieties generated by classes of residuated lattices that are conservative in the sense that monoid multiplication always yields one of its arguments. We then make use of a more symmetric version of Raftery's characterization theorem for totally ordered commutative idempotent residuated lattices to prove that the variety generated by this class has the amalgamation property. Finally, we address an open problem in the literature by giving an example of a noncommutative variety of idempotent residuated lattices that has the amalgamation property.

math.LO↗

arXiv2019

Distributive laws in residuated binars

In residuated binars there are six non-obvious distributivity identities of $\cdot$,$/$,$\backslash$ over $\wedge, \vee$. We show that in residuated binars with distributive lattice reducts there are some dependencies among these identities; specifically, there are six pairs of identities that imply another one of these identities, and we provide counterexamples to show that no other dependencies exist among these.

math.LO↗

arXiv2018

Logics for Rough Concept Analysis

Taking an algebraic perspective on the basic structures of Rough Concept Analysis as the starting point, in this paper we introduce some varieties of lattices expanded with normal modal operators which can be regarded as the natural rough algebra counterparts of certain subclasses of rough formal contexts, and introduce proper display calculi for the logics associated with these varieties which are sound, complete, conservative and with uniform cut elimination and subformula property. These calculi modularly extend the multi-type calculi for rough algebras to a `nondistributive' (i.e. general lattice-based) setting.

math.LO↗

arXiv2018

Nonassociative right hoops

The class of nonassociative right hoops, or narhoops for short, is defined as a subclass of right-residuated magmas, and is shown to be a variety. These algebras generalize both right quasigroups and right hoops, and we characterize the subvarieties in which the operation $x\sqcap y=(x / y)y$ is associative and/or commutative. Narhoops with a left unit are proved to have a top element if and only if $\sqcap$ is commutative, and their congruences are determined by the equivalence class of the left unit. We also show that the four identities defining narhoops are independent.

math.RA↗