Internal and External Calculi: Ordering the Jungle without Being Lost in Translations

Abstract

This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively straightforward while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi.' We discuss the ambiguities involved in the informal definitions of these categories, and we critically assess the properties that (calculi from) these classes are purported to possess.

Published in the Bulletin of the Section of Logic

References in corpus (10)

• A System of Interaction and Structure
• On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics
• On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
• Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
• Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
• Cut-free Calculi and Relational Semantics for Temporal STIT Logics
• Display to Labeled Proofs and Back Again for Tense Logics
• Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi
• Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
• Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents