内部与外部演算：在翻译中有序地梳理丛林
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
AI总结：
本文探讨了基于序列的证明形式化方法的层级结构，分析了内部与外部演算的区别及其翻译难度。
摘要：
本文对证明论文献中各种基于序列的证明形式化方法进行了全面概述。我们考虑了各种模态和时态逻辑、直觉逻辑、条件逻辑和束逻辑的形式化方法。在提供所考虑逻辑和证明形式化方法的概览后，我们展示了如何根据序列的底层数据结构将这些基于序列的形式化方法置于一个层级中。然后讨论如何通过翻译来遍历这一层级。将证明向上这个层级翻译相对简单，而向下翻译则更加困难。最后，我们审视了结构证明论中'内部演算'和'外部演算'之间的普遍区分。我们讨论了这些类别非正式定义中的模糊性，并批判性地评估了这些类别（形式化方法）所声称具备的性质。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
