[Prev][Next][Index][Thread]
Is extensionality equational in the absence of xi?
The theory (lambda) has the following derivation rules:
(I) (\x.M)N = M[x:=N] (beta)
(II.1) M = M (reflexivity)
(II.2) M = N => N = M (symmetry)
(II.3) L = M, M = N => L = N (transitivity)
(II.4) M = N => ML = NL (congruence)
(II.5) M = N => LM = ZL (congruence)
(II.6) M = N => \x.M = \x.N (xi)
In the presence of these rules, then extensionality
Mx = Nx => M = N (ext)
is equivalent to (eta)
\x.Mx = M (eta)
Define (lambda-) to be (lambda) without rule (xi). It is easy
to check that (lambda-)+(ext) is closed under (xi).
Question: Is it possible to extend (lambda-) by a finite set of
equations A such that (lambda-)+A is closed under (ext)?
We cannot solve this trivially by taking A=(ext) or A=(eta)+(xi),
because A must be a set of equations of the form M=N, which rules
out conditional equations like (ext) and (xi).
For combinatory logic CL there is such a set of equations, called
A_beta_eta, see Barendregt 7.3.15. Further, CL+A_beta_eta is provably
equivalent to (lambda)+(ext), but this proof relies on (xi).
Cheers, -- P