Always Look on Both Sides of Proof: Syntax and Semantics as the Yin and Yang of Structural Proof Theory

Abstract

Proof theory provides a purely syntactic way of reasoning, without the need to resort to semantics. This is especially true of internal proof calculi where proof objects are interpreted as formulas, as opposed to external calculi that also exploit semantic elements. On the other hand, tableau formalisms suggest that the distinction between pure and “impure” syntax, between internal and external calculi is, perhaps, more superficial than commonly believed. Indeed, tableaus are typically isomorphic to some internal sequent-like calculus, despite themselves being described in largely semantic terms. I argue that the choice between embracing and avoiding semantic elements is a false one, that the two sides of proof formalisms mutually enrich rather than oppose each other. As an illustration of such successful interplay, I will discuss how semantic intuitions have been instrumental in developing several proof formalisms, including those used for solving two open problems: (1) the Lyndon interpolation property for Gödel–Dummett Logic and (2) decidability for the intuitionistic modal logic S4.