Proof Theory and Algebra

The interaction between proof theory and algebra has long played an important role in the development of modern logic. Algebraic perspectives provide powerful tools for understanding formal proofs, while proof-theoretic methods offer new insights into algebraic structures.
The workshop "Proof Theory and Algebra" aims to bring together distinguished experts from both fields in order to foster new connections and stimulate further research at their interface. It will also serve as the 2026 Annual Meeting of the Swiss Society for Logic and Philosophy of Sciences (SSLPS), sponsored by the Swiss Academy of Sciences (SCNAT).

The workshop will take place at Hostellerie am Schwarzsee, Schwarzsee, Switzerland. The nearest train station is Fribourg/Freiburg from where you can take Bus no. 123 in direction Schwarzsee for 50 minutes. The bus stops directly in front of the hotel at the stop "Schwarzsee, Hostellerie". Timetables for the bus can be found here.

A conucleus on a residuated lattice is a generalization of an S4 modal operator on a Boolean algebra. Its interest stems from extending the relation between S4 modal algebras and Heyting algebras given by the Gödel translation to other varieties of residuated lattices. We consider the problem of deciding the validity of universal sentences (or equivalently, quasi-equations) in varieties of integral conuclear residuated lattices and show that among other varieties, MV-algebras with a conucleus and Abelian l-group cones with a conucleus have decidable universal theories. As a corollary, this settles positively the long-standing open problem of whether integral cancellative commutative residuated lattices have a decidable universal theory.

We show that there exists an algorithm that, on input a finite boolean combination of inequalities such as u^2*v < w, decides whether the formula holds in every commutative monoid equipped with a total order satisfying v \leq w \Rightarrow uv \leq uw. In other words, the universal theory of monoids with such an order is decidable.

The algorithm exploits the structure of the topological space of total preorders on monomials in n variables in a crucial manner. This is an irreducible spectral space, and we cover it by countably many “affine real spaces”. This generalises Robbiano's celebrated classification of monomial orders via weight matrices. We then show that the negation of the input formula yields a semialgebraic set in each of these affine spaces. For the output “no” we have to find one of these sets that is nonempty, and in parallel a separate algorithm is searching for a “yes” certificate.

(Based on joint work with George Metcalfe and Simon Santschi.)

Substructural logics are resource-sensitive generalizations of classical and intuitionistic logic. In particular, they may lack the (structural) properties of exchange, weakening and contraction, so the order and multiplicity of assumptions is important in a derivation. As a result, they are useful in studying degrees of truth and settings where various information tokens are received or where the order of formulas is important (non-Abelian groups, sentence structure in linguistics).

Knotted axioms reinstate some (controlled and specified) degree of the structural properties of contraction and weakening back in the logic, which may be suitable for certain settings. The deductibility of knotted substructural logics is known to be undecidable when exchange is fully absent and decidable when exchange (or weaker versions of it) is present. We establish the exact computation complexity of these logics, in cases when they are decidable and in this talk we present the methods used to obtain the lower complexity bounds.

In particular, we prove that this complexity class is exactly Ackermanian (the first non-elementary complexity class). We show hardness with respect to this complexity class by encoding the termination problem for and-branching counter machines that have an Ackermanian memory limit. Actually, our results apply to more general axioms than knotted ones (joinand-incresing and joinand decreasing) and to specific weaker versions of exchange. Finally, we show that for knotted rules of contractive type provability has the same complexity as deducibility.

(Joint work with V. Greati, R. Ramanayake and G. St. John.)

Hypersequent calculi provide cut-free presentations for a wide range of substructural logics and are therefore a central tool for studying the computational properties of such logics. However, the intricate manipulation of multisets of sequents by hypersequent rules poses many challenges for controlling the complexity of proof search in these calculi. This talk presents recent advances in the complexity study of substructural logics admitting cut-free hypersequent calculi, using methods that combine structural proof theory and well-quasi-orders (wqos). We start by discussing prior work [1], where a hyper-Ackermannian upper bound was obtained for many families of logics through the analysis of hypersequent proof search using a length theorem for wqos over sets of sequents. We then present novel algorithms [2] that instead control proof search via a simpler wqo defined over sequents, thus permitting the use of a simpler length theorem that yields improved Ackermannian upper bounds. In particular, we obtain a new Ackermannian upper bound for the fundamental fuzzy logic MTL, whose exact complexity is a longstanding open problem.

[1] Nikolaos Galatos, Vitor Greati, Revantha Ramanayake, Gavin St. John. “Complexities of Well-Quasi-Ordered Substructural Logics”. 2025. Preprint: https://arxiv.org/abs/2504.21674
[2] A.R. Balasubramanian, Vitor Greati, Revantha Ramanayake. “Hypersequent Calculi Have Ackermannian Complexity”. Accepted in LICS’26. 2026. Preprint: https://arxiv.org/abs/2602.19229

In this talk, I will describe global transformations of sequent-style derivations that preserve provability while recovering analyticity, reducing some of the bureaucracy of the formalism in which derivations are defined, or establishing semantic results syntactically. In particular, I will show how arbitrary cuts can be restricted to analytic cuts (cut restriction), recovering the essential proof-theoretic benefits usually associated with cut elimination without requiring full elimination. These methods apply uniformly across broad classes of non-classical logics, including substructural, intermediate, and modal logics. The overall message is that when local proof transformations are unavailable, carefully designed proof surgeries can still recover many of their most important proof-theoretic and semantic consequences.

A simple candidate for a Glivenko master theorem applies not only to the customary generalisations, such as Kuroda’s to predicate logic, but always when an extension by axioms of a suitable consequence relation is to be conservative over the Kleisli extension with respect to a given nucleus. The conservation criterion amounts to the nuclear shift for implication---a variant of Kuroda's double negation shift---whenever the additional axioms express stability, i.e. that the nucleus be identified with identity, as is the case not only for Glivenko's original theorem.

(Based on joint work with Giulio Fellin, and with Sara Negri and Giulio Fellin.)

Proving non-trivial lower bounds on proof size in the classical sequent calculus remains a longstanding open problem in proof complexity. In this work, we revisit this problem through the lens of substructural and linear logics. By considering calculi that restrict contraction or weakening, we obtain systems in which derivations are subject to resource-sensitive constraints. Within these frameworks, we exhibit formulas that, while admitting short classical proofs, require substantially larger derivations. These results provide a proof-theoretic explanation of why classical systems are difficult to analyze: their efficiency stems from the interaction of structural rules, a feature that becomes visible only when examined against substructural baselines.

TBA

In recent years, there has been considerable progress in developing a repertoire of techniques for studying interpolation properties in novel logical contexts. These techniques have, among other things, been successfully applied to give exhaustive classifications of the logics having deductive or Craig interpolation within various families. The kinds of logical families for which these techniques have succeeded are, however, limited in a number of respects: Chiefly, these successes have been confined to logics having an equivalent algebraic semantics comprising a quite well-behaved variety.

In the present work, we offer a case study illustrating the extension of our existing techniques to deductive systems which are not even substitution invariant. In particular, we give a complete classification of extensions of inquisitive logic having the Craig Interpolation family.

(This is joint work with Josef von Hoffmann Doyle.)

PDF

We describe the structure of some models of the Lambek Calculus, focusing on residuated partially ordered semigroups where the poset has several connected components. In this setting, the components are congruence classes and the quotient algebra for this congruence is a group with an antichain order. We show that the components are up and down-directed, and if one of the components has a lower bound, then all components are bounded. For residuated po-monoids, the connected component that contains the unit is called the unital component. We consider special cases when the unital component is an integral involutive po-monoid, a Boolean algebra or a Sugihara monoid. For the Boolean case we prove that the algebras are conuclear images of the direct product of a group and a Boolean algebra, hence all connected components are order-isomorphic to Boolean algebras with cardinality at most that of the unital component. In the case of Sugihara monoids we use partially ordered Plonka sums to decompose finite algebras into fibers that have Boolean unital components. We also discuss a general construction of Plonka sums for residuated po-algebras. The research reported here is based on joint work with Marta Bilkova, Melissa Sugimoto, José Gil-Férez and Giuseppe Zecchini.

The 3-valued logics of Kleene and McCarthy are among the most widely used frameworks for reasoning about partial recursive predicates in theoretical computer science. From the perspective of algebraic logic, these logics correspond to the varieties of Kleene lattices and McCarthy algebras, respectively. However, the relationships between these algebraic structures have remained relatively underexplored. In this paper, we provide constructions that yield (partial) mappings from Kleene lattices to McCarthy algebras, and back -- viewing both the former and the latter either as varieties of algebras or as classes of ordered structures. In particular, we show that the algebraic category of Kleene lattices is equivalent to a subcategory of the algebraic category of McCarthy algebras, and that a category of ordered algebras based on Kleene lattices can be densely embedded into a corresponding category based on McCarthy algebras.

(Joint work with Davide Fazio, Gavin St. John.)

PDF