论文标题
削减透明真理系统的消除，并以限制的初始序列
Cut elimination for systems of transparent truth with restricted initial sequents
论文作者
论文摘要
本文研究了基于初始序列的限制，以完全失去词汇的真理研究。与众所周知的替代方法不同，这种系统既展示了简单和直观的模型理论，又显示出了显着的证明理论特性。我们首先表明，由于真相规则的强烈形式的可逆性形式，可以在系统中通过一种标准策略在系统中消除，该标准策略以适当的量度衡量真实规则在派生中的公式的应用数量。接下来，我们注意到将合适的算术公理添加到系统中时，切割仍然可以消除。最后，我们在所考虑系统的无限制制剂和定点语义的无限制制剂中建立了直接联系。明显地，与其他背景逻辑发生的情况不同，这种链接是在不限制真实规则前提的情况下建立的。
The paper studies a cluster of systems for fully disquotational truth based on the restriction of initial sequents. Unlike well-known alternative approaches, such systems display both a simple and intuitive model theory and remarkable proof-theoretic properties. We start by showing that, due to a strong form of invertibility of the truth rules, cut is eliminable in the systems via a standard strategy supplemented by a suitable measure of the number of applications of truth rules to formulas in derivations. Next, we notice that cut remains eliminable when suitable arithmetical axioms are added to the system. Finally, we establish a direct link between cut-free derivability in infinitary formulations of the systems considered and fixed-point semantics. Noticeably, unlike what happens with other background logics, such links are established without imposing any restriction to the premisses of the truth rules.
