[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

```