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

Tim LyonTim Lyon, Agata CiabattoniAgata Ciabattoni, Didier GalmicheDidier Galmiche, Marianna GirlandoMarianna Girlando, Dominique Larchey-WendlingDominique Larchey-Wendling, Daniel MéryDaniel Méry, Nicola OlivettiNicola Olivetti, Revantha RamanayakeRevantha Ramanayake

Tim Lyon, Agata Ciabattoni, Didier Galmiche, Marianna Girlando, Dominique Larchey-Wendling, Daniel Méry, Nicola Olivetti, Revantha Ramanayake
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
Bulletin of the Section of Logic, 2025

Details
Bibtex

KurzfassungAbstract
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 easy 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'. It is observed that these classes resist a rigorous separation, and we critically assess the properties that (calculi from) these classes are purported to possess.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{LCGGLMOR2025,
  author  = {Tim Lyon and Agata Ciabattoni and Didier Galmiche and Marianna
             Girlando and Dominique Larchey-Wendling and Daniel M{\'{e}}ry and
             Nicola Olivetti and Revantha Ramanayake},
  title   = {Internal and External Calculi: Ordering the Jungle without Being
             Lost in Translations},
  journal = {Bulletin of the Section of Logic},
  year    = {2025}
}