ABSTRACT. This tutorial explores the landscape of sequent-based proof formalisms for modal logics, using Gödel-Löb provability logic (GL) as a running example. We survey four major paradigms--labeled sequents, nested (or tree) sequents, linear nested sequents, and Gentzen sequents--and discuss the various trade-offs of choosing one formalism over another, including sequent size, proof size, and suitability for counter-model extraction. The central theme of the tutorial is understanding how these formalisms relate by means of proof transformations, explaining how one can systematically "transition" between them: from graphs, to trees, to lines, and to points (i.e., standard Gentzen sequents). Along the way, we highlight what is lost or gained in each transition, such as invertibility of rules or proof compactness. We also touch on how the choice of formalism affects proof-search algorithms.

ABSTRACT. As is very well known, System F admits (strong) normalization, and it can be proved by combination of Tait's computability predicates and Girard's reducibility candidates. But this approach is not satisfactory for proof theorists who are interested in proof-theoretic ordinals of (fragments of) second-order arithmetic. A more satisfactory approach would be to prove normalization by employing inductive definitions, as it seems to give us some ordinal information on the complexity of normalization. Although it is currently limited to some parameter-free fragments of System F, it is here, we believe, that one finds a small link between lambda calculus and ordinal analysis. In this talk, we revisit some brilliant ideas in the development of lambda caluclus and ordinal analysis (up to 1980's) from a modern perspective. 1. The Joachimski-Matthes method (2003) for proving normalization theorems for the simply typed lambda calculus and its extensions based on inductive definitions instead of computability predicates. 2. The Buchholz method using the Omega rule (1981), which was originally proposed for ordinal analysis, but can also be combined with 1 to obtain a concise proof of normalization for parameter-free fragments of System F. 3. The Altenkirch-Coquand method for proving normalization of a parameter-free fragment (2001), which is based on computability predicates but avoids use of reducibility candidates. Interestingly, this can be construed as a semantic analogue of 2. By reviewing these ideas and extending them, we address the question of how and to what extent one can replace computability predicates and reducibility candidates by inductive definitions when proving normalization.

ABSTRACT. We study the non-constructivity of checking the most common soundness condition for cyclic proofs over a constructive foundation. In light of our results, we argue that the constructively favourable formulation of proofhood restricts to periodic branches rather than arbitrary branches.

ABSTRACT. Formal languages with term-forming operators (tfos) are very useful in several fields. However, a syntactical analysis of such devices requires significant changes in the toolkit of proof theory. In this paper we discuss the problems connected with construction of cut-free sequent calculi for languages with tfos. As a case study we are analysing Quine’s Virtual Theory of Classes (VTC), a neutral basis for proof theoretic development of theories of sets like ZFC or NBG, based on the application of set abstracts.

ABSTRACT. Cut elimination procedures for deep inference calculi such as BV and its extensions have traditionally required intricate reasoning about rewriting proofs into normal form. I will present another way, based on ideas from the rewriting-free Normalisation by Evaluation (NbE) technique for lambda-calculi. NbE works by constructing a model from the syntax of normal (or cut free) proofs and evaluating proofs containing cut into that model. A reification procedure then reads out the normalised (cut free) proof from the interpretation. I will show that this technique works for BV and its extensions with additives and exponential. This is joint work with Wen Kokke.

ABSTRACT. We introduce a new formalism for representing proofs in propositional logic called ``scroll nets''. Its fundamental construct is the scroll, a topological notation for implication proposed by C. S. Peirce at the end of the 19th century as the basis for his diagrammatic system of existential graphs (EGs). Scroll nets are derived from EGs by following the Curry-Howard methodology of internalizing inference rules inside judgments, just as terms in type theory internalize natural deduction rules. We focus on the intuitionistic implicative fragment of EGs, starting from an intuitive diagrammatic notation for scroll nets, and then distilling their combinatorial essence into an inductive definition. We also identify a notion of detour, as well as an equational theory inspired by cartesian monoidal categories that can be oriented to perform detour elimination. We illustrate how to simulate normalization in the simply typed $\lambda$-calculus, demonstrating both the logical and computational expressivity of our framework.

ABSTRACT. The logical principles of focalisation and polarisation can be used to design well-behaved term syntaxes for sequent calculus, which play a role as meta-languages for describing effectful computation. On the semantics side, this corresponds to an axiomatic and polarised notion of model of computation stated in terms of non-associative categories as well as adjunctions between “bare” functors (reflexive graph morphisms) over such non-associative categories. In this paper, we study the special and delicate cases of resource and effect modalities in a general intuitionistic and linear setting: an exponential comonad ! (refining the necessity modality □) and a strong monad (written ◊). The starting point of our contribution is noti- cing that the completeness for a polarised syntax for ! and ◊ with respect to (co)monads in linear call-by-push-value models can be achieved if we move to relative (co)monads (Alten- kirch, Chapman and Uustalu, 2015; Arkor and McDermott, 2024): more precisely, comonads relative to ↓ (the positive shift functor) for ! and monads relative to ↑ (the negative shift functor) for ◊. These specialisations of the concept of relative (co)monad to call-by-push-value adjunctions recently appeared in Jiang, Xue and New (2025) and Melliès (2025, 2026). Yet the syntax we present arose from proof-theoretic consideration in Munch-Maccagnoni (2009) and Curien, Fiore and Munch-Maccagnoni (CFMM 2016), without the link with relative (co)monads being noticed at the time. Our first remark and explanation is thus that (co)monads relative to a call-by-push-value adjunction have been motivated previously from a proof-theoretic perspective in the context of focalisation, which also provides a meta-language for these concepts in an effectful setting. We carry out the study of these modalities from the axiomatic, non-associative point of view. We recall the definition of adjunction between bare functors in this context, and estab- lish correspondence results between this notion of adjunction and that of relative adjunction. This correspondence is then extended to linear-non-linear and strong versions of adjunctions as needed to model ! and ◊.

ABSTRACT. The traditional single-conclusion restriction in intuitionistic logic is often regarded as an external structural constraint that distinguishes it from classical multiple-conclusion systems. We explore here an alternative approach to capturing intuitionistic provability within a classical, multiple-conclusion framework by employing subexponentials. By extending Multiplicative-Additive Linear Logic (\mall) and full Linear Logic (\LL) with a linear subexponential ($!_l$), which does not allow for contraction and weakening, the systems \malll and \LLl are developed. A translation that systematically prepends the subexponential to subformulas enables hosting intuitionistic (single-conclusion) variants of MALL and LL in (multiple-conclusion) versions of \malll and \LLl. Specifically, a sequent is provable in the single-conclusion intuitionistic system if and only if its translation is provable in the corresponding multiple-conclusion subexponential system. This development demonstrates that the single-conclusion nature of intuitionistic logic can be viewed as an emergent property of specific logical connectives and subexponential constraints rather than an explicitly imposed constraint on the structure of sequents.