In this paper we consider the problem (due to A. Cantini) of the existence of a λ-theory T such that: –T is recursive enumerable; –the ω-rule holds in T (that is: if two terms M, N are such that for every closed term Q, MQ=NQ holds in T, then M=N holds in T). We solve affirmatively this problem. Some related questions are also discussed.
Intrigila, B., Statman, R. (2005). Some results on extensionality in lambda calculus. ANNALS OF PURE AND APPLIED LOGIC [10.1016/j.apal.2003.05.001].
Some results on extensionality in lambda calculus
INTRIGILA, BENEDETTO;
2005-01-01
Abstract
In this paper we consider the problem (due to A. Cantini) of the existence of a λ-theory T such that: –T is recursive enumerable; –the ω-rule holds in T (that is: if two terms M, N are such that for every closed term Q, MQ=NQ holds in T, then M=N holds in T). We solve affirmatively this problem. Some related questions are also discussed.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.
