Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
Tim S. Lyon, Agata Ciabattoni, Didier Galmiche, Marianna Girlando, Dominique Larchey-Wendling, Daniel M\'ery, Nicola Olivetti, Revantha Ramanayake

TL;DR
This paper surveys sequent-based proof formalisms across various logics, organizes them hierarchically by data structure, and analyzes the complexities of translating proofs within this hierarchy, especially between internal and external calculi.
Contribution
It provides a comprehensive hierarchy of sequent calculi for multiple logics and critically examines the translation processes and distinctions between internal and external calculi.
Findings
Proof translations are straightforward upwards in the hierarchy.
Downward translations are significantly more complex.
Ambiguities exist in the definitions of internal and external calculi.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Logic, programming, and type systems · Philosophy and Theoretical Science
