Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

Kristian Stoevring

doi:10.2168/LMCS-2(2:1)2006

Kristian Stoevring - Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative

lmcs:2249 - Logical Methods in Computer Science, March 16, 2006, Volume 2, Issue 2 - https://doi.org/10.2168/LMCS-2(2:1)2006

Extending the Extensional Lambda Calculus with Surjective Pairing is ConservativeArticle

Authors: Kristian Stoevring

We 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 a "syntactic" proof that the extensional lambda calculus with surjective pairing is consistent.

Comment: To appear in Logical Methods in Computer Science

https://doi.org/10.2168/LMCS-2(2:1)2006

Source: arXiv.org:math/0602544

Volume: Volume 2, Issue 2

Published on: March 16, 2006

Imported on: November 23, 2005

Keywords: Mathematics - Logic, F.4.1

Licence: arXiv.org - Assumed non-exclusive license to distribute