Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative
AbstractWe answer Klop and de Vrijer's question whether adding surjective-pairing axioms to the extensional lambda calculus yields a conservative extension. The answer is positive. As a byproduct we obtain the first ``syntactic'' proof that the extensional lambda calculus with surjective pairing is consistent.
How to Cite
Støvring, K. (2005). Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative. BRICS Report Series, 12(35). https://doi.org/10.7146/brics.v12i35.21902
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.