内部和外部演算：在不迷失于翻译中整理丛林

本文广泛论述了证明论文献中各种基于相继式的证明形式体系。我们考虑了各种模态逻辑、时态逻辑、直觉主义逻辑、条件逻辑以及束逻辑的形式体系。在概述了所考察的逻辑和证明形式体系之后，我们展示了这些基于相继式的形式体系如何根据相继式的底层数据结构被置于一个层次结构中。然后我们讨论了如何通过翻译来遍历这个层次结构。向上翻译证明相对直接，而向下翻译证明则困难得多。最后，我们审视了结构证明论中“内部演算”与“外部演算”之间的流行区分。我们讨论了这些类别非正式定义中的模糊之处，并批判性地评估了这些类别（中的演算）据称应具备的性质。