Linear Logic via algebra I: Girard algebras
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 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ℵ0 Post-complete extensions of MALL.
Related
- Extending structures for the linear framework of Universal Algebra with applications to transposed Poisson algebras
- On the sphere spectrum from the viewpoint of linear logic
- Quantization of Preprojective Algebras and the Type A Rational Cherednik Algebra
- Freeness and divisibility for right H-simple left H-comodule algebras over a pointed Hopf algebra H
- Invariants of Nilpotent Lie Algebras via Geometry and Algebra with a Focus on Computation
BibTeX
@misc{agliano2026linear,
title = {{Linear Logic via algebra I: Girard algebras}},
author = {Paolo Agliano and Mitar Nedeljkovic},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.16804},
eprint = {2610.16804},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.16804},
}
RIS
TY - UNPB
TI - Linear Logic via algebra I: Girard algebras
AU - Paolo Agliano
AU - Mitar Nedeljkovic
PY - 2026
DA - 2026/10/12
PB - arXiv
DO - 10.48550/arxiv.2610.16804
UR - https://arxiv.org/abs/2610.16804
AB - 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 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^ℵ_0 Post-complete extensions of MALL.
ER -