In a functional calculus, the so called omega-rule states that if two terms P and Q applied to any closed term N return the same value (i.e. PN = QN), then they are equal (i.e. P = Q holds). As it is well known, in the lambda beta-calculus the omega-rule does not hold, even when the eta-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 omega-rule when added to the lambda beta-calculus. In this paper we solve the problem, by showing that the resulting theory is Pi(1)(1)-Complete.
Intrigila, B., Statman, R. (2009). THE OMEGA RULE IS Pi(1)(1)-COMPLETE IN THE lambda beta-CALCULUS. LOGICAL METHODS IN COMPUTER SCIENCE, 5(2) [10.2168/LMCS-5(2:6)2009].
THE OMEGA RULE IS Pi(1)(1)-COMPLETE IN THE lambda beta-CALCULUS
INTRIGILA, BENEDETTO;
2009-01-01
Abstract
In a functional calculus, the so called omega-rule states that if two terms P and Q applied to any closed term N return the same value (i.e. PN = QN), then they are equal (i.e. P = Q holds). As it is well known, in the lambda beta-calculus the omega-rule does not hold, even when the eta-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 omega-rule when added to the lambda beta-calculus. In this paper we solve the problem, by showing that the resulting theory is Pi(1)(1)-Complete.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
