切割限制理论：第一步
A theory of cut-restriction: first steps
摘要：
割消是证明理论的基础。正是这种算法消除了微积分证明中的切割，导致了无切割微积分和应用。割消适用于许多逻辑，而与它们的语义无关。这是它的影响，每当削减消除是不可证明的微积分不变的反应一直是一个移动到一个更丰富的证明系统，以恢复it.In本文中，我们调查了一个根本不同的方法，后者：适应古老的削减消除限制的形状时，消除是不可能的削减公式。我们解决了无割以上的“第一级”：分析割。我们的方法被应用到双直觉逻辑和S5的分析削减已经知道是必需的微积分。这标志着切割限制理论的第一步。
英文摘要：
Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-elimination applies to many logics irrespective of their semantics. Such is its influence that whenever cut-elimination is not provable in a sequent calculus the invariable response has been a move to a richer proof system to regain it. In this paper we investigate a radically different approach to the latter: adapting age-old cut-elimination to restrict the shape of the cut-formulas when elimination is not possible. We tackle the "first level" above cut-free: analytic cuts. Our methodology is applied to the sequent calculi for bi-intuitionistic logic and S5 where analytic cuts are already known to be required. This marks the first steps in a theory of cut-restriction.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
