Omega规则是$\mathbf{Π_{1}^{1}}$ -在$λβ$ -微积分中完成
The Omega Rule is $\mathbf{Π_{1}^{1}}$-Complete in the $λβ$-Calculus
摘要：
在函数演算中，所谓的Ω-规则指出，如果两个项P和Q应用于任何闭项<i>N</i>返回相同的值（即PN = QN），则它们相等（即P = Q成立）。众所周知，在λβ-演算中，Ω-规则不成立，即使在演算中加入η-规则（弱扩张性）。H. Barendregt（1975）关注的是当把Ω-规则加到λβ-演算中时，确定Ω-规则的逻辑幂。在本文中，我们解决了这个问题，证明了所得到的理论是<$1 ^{1}-完备的.
英文摘要：
In a functional calculus, the so called Ω-rule states that if two terms P and Q applied to any closed term <i>N</i> return the same value (i.e. PN = QN), then they are equal (i.e. P = Q holds). As it is well known, in the λβ-calculus the Ω-rule does not hold, even when the η-rule (weak extensionality) is added to the calculus. A long-standing problem of H. Barendregt (1975) concerns the determination of the logical power of the Ω-rule when added to the λβ-calculus. In this paper we solve the problem, by showing that the resulting theory is Π\_{1}^{1}-complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
