Bounds for cut elimination in intuitionistic propositional logic
Bounds for cut elimination in intuitionistic propositional logic
复制标题
直觉命题逻辑中割消去的界
DOI：
10.1007/bf01627506
复制
发表时间：
1992
影响因子：
0.3
通讯作者：
J. Hudelmaier
中科院分区：
文献类型：
--
作者：
J. Hudelmaier
根岑证明理论的中心定理指出，每个演绎d（在经典或直觉主义，命题或量词逻辑中）都可以转化为不使用切割规则的演绎G（d）。显然，避免使用特定的证明规则会导致G（d）变得比d长，而根森的割消算法建立了G（d）的长度l（G（d））的上限。在这篇文章中，我将为直觉主义命题逻辑构造一个（不同的）无割演绎J（d），并推导出l（J（d））的更精确的上界。此外，我将使用为此目的开发的方法，以建立一个有效的决策方法。l（G（d））的Gentzen上限取决于长度l（d）和d的截度g（d），即d中使用的截公式的次数的最大值，增加1;它具有以下形式：
The central theorem of Gentzen's theory of proofs states that every deduction d (in classical or intuitionistic, propositional or quantifier logic) can be transformed into a deduction G(d) which does not make use of the cut rule. Avoiding the use of a particular proof rule will, obviously, have the effect that G(d) becomes longer than d, and Gentzen's algorithm for cut elimination establishes an upper bound for the length l(G(d)) of G(d). In this article, I shall construct a (different) cut free deduction J(d) for the case of intuitionistic propositional logic and derive considerably sharper upper bounds for l(J(d)). Also, I shall use the methods developed for this purpose in order to set up an effective decision method. Gentzen's upper bound for l(G(d)) depends on both the length l(d) and the cut degree g(d) of d, viz. the maximum of the degrees, increased by 1, of cut formulas used in d; it has the form