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

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Beitragende

  • Tim Lyon - , Professur für Computational Logic (Autor:in)
  • Agata Ciabattoni - , Technische Universität Wien (Autor:in)
  • Didier Galmiche - , Université de Lorraine, LORIA (Autor:in)
  • Marianna Girlando - , Universiteit van Amsterdam (Autor:in)
  • Dominique Larchey-Wendling - , Université de Lorraine, LORIA (Autor:in)
  • Daniel Méry - , Université de Lorraine, LORIA (Autor:in)
  • Nicola Olivetti - , Aix-Marseille Université (Autor:in)
  • Revantha Ramanayake - , University of Groningen (Autor:in)

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.

Details

OriginalspracheEnglisch
Seiten (von - bis)59–151
FachzeitschriftBulletin of the Section of Logic
Jahrgang54
Ausgabenummer1
PublikationsstatusVeröffentlicht - Juni 2025
Peer-Review-StatusJa

Externe IDs

ORCID /0000-0003-3214-0828/work/199216618
Mendeley e779cdd2-6d78-3550-9faa-364192a79e26
Scopus 105027519462

Schlagworte

ASJC Scopus Sachgebiete

Schlagwörter

  • bunched implication, conditional logic, display calculus, external calculus, hypersequent, internal calculus, intuitionistic logic, labeled calculus, modal logic, nested calculus, proof theory, sequent, tense logic