Workshop on definability, algebra and duality in non-classical logic

In (1,2), we extended the logical categories framework to first order modal logic. In our modal categories, modal operators are applied directly to subobjects and interact with the background factorization system. We prove a Joyal-style representation theorem into relational structures formalizing a ‘counterpart’ semantics. We investigate saturation conditions related to definability questions and we enrich our framework with quotients and disjoint sums, thus leading to the notion of a modal (quasi) pretopos.

Joint work with J. Marques.

(1): S. Ghilardi and J. Marques. A completeness theorem for topological doctrines, July 2025. link.

(2): S. Ghilardi and J. Marques. First order modal logic via logical categories. J. of Symbolic Logic, November 2025. link

This talk explores proof-theoretic decision procedures for intuitionistic and modal logics, taking intuitionistic modal logic IS4 as case study. This logic is the intuitionistic variant of S4, as axiomatised by Fischer Servi. Decidability of the logic was left open in Simpson’s PhD thesis (1994).

We first review the standard proof-theoretic algorithm to establish decidability of classical modal logic S4. Using a labelled calculus for the logic, we define a proof-search strategy, whose termination is ensured by a loopcheck. The algorithm produces either a proof or a countermodel for the input formula. This naïve approach fails in the case of IS4, due to the difficulty of producing a correct countermodel. To overcome this issue, we define a new decision algorithm, which incorporates repeating behaviour into the calculus by means of loop rules. In this setting, a failed search easily produces a countermodel, while a successful search yields a derivation from which the loop rules can be eliminated. We thus establish decidability of IS4.

This talk is based on joint work with R. Kuznets, S. Marin, M. Morales and L. Strassburger. Refer to here and here

The theory of rational choice and stable contracts originated in the famous note by D. Gale and L.S. Shapley (1962). In later years, in particular, in the work of C.R. Plott (1973), it led to the study of the so-called choice functions given by an operation C on the powerset of X satisfying certain natural conditions. Intuitively, C(A) represents the preferred choices of an agent if it is given a ‘menu’ A. This theory has a long tradition represented, in particular, by the more recent works of V.I. Danilov and G. Koshevoy. We will argue that Plottian choice functions happen to be exactly the neigborhood frames of a subnormal (monotone) version of Gödel—Löb logic GL, denoted mGL. The emerging connections show a lot of interesting parallel features of the provability logic and Plottian choice function theory, including the role of fixed points.

The results obtained so far include neighborhood completeness theorem for mGL, failure of de Jongh theorem (definability of fixed points) in mGL, a ‘distributed provability’ interpretation of mGL.

Joint work with V. Danilov, D. Shamkanov, D. Trofimov.

Which lattices can arise as the lattice of sentences, modulo provable equivalence, of an intuitionistic higher-order theory? Categorically, this asks which Heyting algebras are topos-admissible: isomorphic to the lattice of subobjects of the terminal object of an elementary topos, also called its lattice of truth values. The question whether every Heyting algebra is topos-admissible appeared in print in a 1992 paper by Pitts, but dates back at least to 1980, when Pitts learned it from Freyd.

Recently, Xu and Ye answered this question negatively, showing that the free Heyting algebra on two generators is not topos-admissible. This leaves open the problem of finding an intrinsic characterisation of the Heyting algebras that can occur as lattices of truth values. Known positive cases include complete Heyting algebras (frames), via sheaf toposes, and Boolean algebras, via a construction due to Freyd. In joint work with Rodrigo Almeida and Igor Arrieta, we extend Freyd’s construction to all étale-finite Heyting algebras, a class introduced by E. Kuznetsov. These algebras satisfy a generalisation of the law of excluded middle relative to a finite Heyting subalgebra, and include examples that are neither Boolean nor complete. Using Esakia duality, we construct, for each such algebra, an elementary topos of compact étale spaces whose lattice of truth values is isomorphic to the given algebra.

Joint work with R. N. Almeida and I. Arrieta.

A superintuitionistic logic is locally tabular if, up to logical equivalence, there are finitely many formulas in any fixed finite number of variables. It is prelocally tabular if it is not locally tabular but all its proper extensions are. A celebrated result of Mardaev states that there are continuum many prelocally tabular propositional superintuitionistic logics of width 3.

In this talk, we will revisit Mardaev’s proof from a duality-theoretic perspective, with the aim of shedding light on the machinery he employed. Our approach is based on an analysis of the behavior of endomorphisms on certain points of the Esakia duals of free finitely generated Heyting algebras. Using tools from automata theory and symbolic dynamics, we will also answer some additional questions concerning the finite axiomatizability and the structure of the canonical frames of the logics considered by Mardaev.

Joint work with R. N. Almeida.

This talk investigates a form of syntactic duality arising in essentially algebraic theories. It is well known that the category of models of an essentially algebraic theory T is equivalent to the category of Set-valued lex functors defined on the opposite category of finitely presented T-models. In this sense, lex categories classify essentially algebraic theories and can be regarded as invariant syntax. When T is the equational theory of a locally finite variety (i.e., one in which every finitely generated algebra is finite) in a finite signature, the category of finitely presented T-models itself also classify an essentially algebraic theory, which we call the dual theory of T. We focus on the case of monadic Boolean algebras, or S5-modal algebras. Exploiting a categorical duality for finite S5-algebras, we relate the dual theory of S5-algebras to Kan extensions and symmetric group actions.

Joint work with S. Ghilardi.

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, among other things, 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. In our work, we establish the exact computational complexity of these logics in cases when they are decidable: we prove that this complexity class is exactly Ackermaniann (the first non-elementary complexity class). We establish the upper bound by a detailed proof-theoretic analysis, employing sequent and hypersequent systems for these logics. In particular, we control the complexity of formulas in upward-growing branches of derivations via a norm function on a well-quasi-ordered set that emerges, after proving a Curry-type lemma for a suitable auxiliary calculus. On the other hand, we show hardness with respect to this complexity class by encoding the termination problem for and-branching counter machines that have an Ackermaniann memory limit. Actually, our lower-bound 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.