Linear Logic via algebra I: Girard algebras

Paolo Agliano; Mitar Nedeljkovic

Home/Archive/arXiv

arXiv · 2610.16804

Linear Logic via algebra I: Girard algebras

Paolo Agliano·Mitar Nedeljkovic

View original source ↗Read source document ↗Export metadata ↓

Abstract

In this paper we develop several aspects of the algebraic theory of Girard algebras, regarded as the equivalent algebraic semantics of multiplicative additive Linear Logic $\mathsf{MALL}$. The main structural results concern the bottom of the subvariety lattice of the variety of Girard algebras: varieties generated by simple Girard algebras generated by the constants correspond exactly to the atoms of the lattice. Moreover the lattice itself is atomic, i.e. every nontrivial subvariety contains an atom. These atoms can be represented uniformly by the maximal filters of the free algebra generated by the constants. Moreover every congruence of this free algebra is realized by a subvariety, and the resulting atom-support topology records the behavior of arbitrary joins: the atoms below a join of atoms are precisely the points in the closure of the corresponding subset of the spectrum. The concrete constructions show that the bottom of the lattice is already quite rich. Besides determining the integral and degenerate boundary cases and exhibiting finite modular and nonmodular atoms and chains of covers, we constructed infinite families of atoms whose topology reflects genuinely infinitary behavior; thus finite and infinite joins behave essentially differently at the bottom of the subvariety lattice. On the logical side, these results yield $2^{\aleph_0}$ Post-complete extensions of $\mathsf{MALL}$.

Explore related subjects

math.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Paolo Agliano, Mitar Nedeljkovic. 2026-10-12. Linear Logic via algebra I: Girard algebras. https://arxiv.org/abs/2610.16804

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Extension of Lipschitz maps definable in Hensel minimal structures

In this paper, we establish a theorem on extension of Lipschitz maps $f$ definable in Hensel minimal fields $K$. This may be regarded as a definable, non-Archimedean, non-locally compact version of Kirszbraun's extension theorem. We proceed with double induction with respect to the dimensions of the ambient space and of the domain of $f$. To this end, we introduce the concept of a definable open cell package with a skeleton which, along with the concept of a risometry, plays a key role in our induction procedure.

math.LO↗

arXiv2026

Convex Team Logics

We prove expressive completeness results for convex propositional and modal team logics, where a logic is convex if, for each formula, if it is true in two teams $t$ and $u$ and $t\subseteq s\subseteq u$, then it is also true in $s$. We introduce propositional/modal team logics which are expressively complete for the class of all convex propositional/modal team properties. We also answer an open question concerning the expressive power of classical propositional logic extended with the nonemptiness atom NE: we show that it is expressively complete for the class of all convex and union-closed properties. A modal analogue of this result additionally yields an expressive completeness theorem for Aloni's (2022) Bilateral State-Based Modal Logic. There is a specific sense in which one of the propositional convex logics we introduce extends propositional dependence logic; this sense corresponds to the existence of a compositional translation between the two logics. Another of the convex logics extends propositional inquisitive logic in the same manner. We generalize the notion of uniform definability, as considered in the team semantics literature, to formalize this notion of compositional extension.

math.LO↗

arXiv2026

A definable matching theorem and approximate Grothendieck semigroups

For an arbitrary first-order structure, we introduce the notion of an approximate Grothendieck semigroup, which satisfies a Banach-Schröder-Bernstein Theorem, as well as a weak Cancellation Law (wCL). At the heart of the proof of the wCL lies a definable matching theorem, which vastly generalizes a related result in Maříková \cite{mat}, and is of independent interest.

math.LO↗