[Prev][Next][Index][Thread]

Conservative extension by surjective pairing



I hae a question related to your LICS '89 paper which we just had
the pleasure of presenting in our research seminar.

You establish that surjective pairing axioms conservatively extend
lambda-beta conversion, and mention that this question is open for
lambda-beta-eta conversion.

Of course there are lots of other lambda-beta, indeed lambda-beta-eta,
theories where conservative extension HOLDS simply because the theory
consists of the valid equations in some lambda model in which surjective
pairing functions exist, e.g,, D_infinity.  Also, I have no doubt there
are other theories besides lambda-beta-eta where conservativity is OPEN.
Is there any theory for which conservative extension by surjective pairing
is know to FAIL?  If not, would you conjecture that surjective pairing
axioms yield a conservative extension of EVERY lambda-beta-theory?

Regards, A.