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

#### 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.
##### Scheda breve Scheda completa Scheda completa (DC)
2009
Pubblicato
Rilevanza internazionale
Articolo
Sì, ma tipo non specificato
Settore INF/01 - INFORMATICA
English
lambda calculus; omega rule; lambda theories
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].
Intrigila, B; Statman, R
Articolo su rivista
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: `https://hdl.handle.net/2108/33110`
• ND
• ND
• 2