Universal Proof Theory, TACL 2022 Lecture Notes

TL;DR

These notes survey Universal Proof Theory, focusing on the existence problem: when do logics admit good proof systems with properties like cut elimination and termination? They develop and apply a general method based on interpolation and uniform interpolation to derive both positive and negative existence results across broad families of logics (intermediate, modal, non-normal, conditional, and substructural) and their sequent calculi. The work highlights terminating calculi (e.g., G3cp, G3KD, G4ip) and demonstrates UIP/ULIP for several logics (K, KD, iKBox, CE, CK, LL), while identifying negative results for others (S4, K4 with certain calculi) and extending results to substructural logics. It also connects proof-theoretic methods to admissible rules and Visser-Harrop properties, offering constructive procedures and a unified framework for evaluating proof systems across diverse logics. Overall, the notes chart a principled pathway for assessing and constructing general, terminating, and analyzable proof systems in a wide logical landscape, with concrete implications for automated reasoning and formal verification.

Abstract

These lecture notes survey the emerging area of Universal Proof Theory, which investigates general questions about the existence, equivalence, and characterization of good proof systems for broad classes of logics. In particular, the notes concentrate on the existence problem: for which logics do there exist proof systems satisfying desirable meta-properties (e.g. cut elimination, analyticity, termination)? After a brief historical and conceptual introduction, we survey different flavours of proof theory (Hilbert systems, natural deduction, sequent calculi) in the context of classical, intuitionistic, modal, and substructural logics. We then develop a general method for obtaining positive and negative existence results, based on interpolation and uniform interpolation techniques, and apply it to a range of logics (intermediate, modal, non-normal, conditional, and substructural). We also discuss variations of the method. As these are lecture notes, proofs are often sketched or omitted, with pointers to papers containing the full proofs. The survey thus aims to chart the scope and challenges of Universal Proof Theory for future work.

Figures (8)

• Figure 1: Some conditional logics
• Figure 1: The natural deduction system ND for CQC (resp. NDi for IQC) consists of the above rules (resp. the above rules except for $E_c\bot$). In $E\exists$ and $I\forall$, either $y=x$ or $y$ is not free in $\raisebox{.4ex}{$\chi$}$ and not free in $\varphi$ and not free in any open assumption of ${\EuScript D}$ except in the indicated one, $[\varphi(y)]^a$. The variable $y$ is called an eigenvariable. In $E\vee$, $I\!\rightarrow$ and $E\exists$ the assumptions labelled $a$ and $b$ are closed in a derivation once the conclusion of the inference is reached.
• Figure 2: ${\sf G4LL}$ is ${\sf G4ip}$ plus all four rules.
• Figure 2: The sequent calculus ${\sf G1cp}$ for CPC.
• Figure 3: The sequent calculus ${\sf G1ip}$ for IPC. $\Delta$ contains at most one formula.

Theorems & Definitions (50)

• Example 4.1
• Theorem 5.1
• Theorem 5.2
• Theorem 6.1
• Theorem 6.2
• Lemma 6.1
• Lemma 6.2
• Remark 6.1
• Theorem 6.3
• Theorem 6.4