Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Surjective Pairing
Lambda Calculus and Surjective Pairing
Here is a formal proof that
extending the extensional lambda calculus
with surjective pairing is conservative. The proof is written using
version 1.5R1 of the Twelf system.
The proof is from the article:
Kristian Støvring. Extending the Extensional Lambda Calculus with Surjective
Pairing is Conservative. Logical Methods in Computer Science, 2(2:1):1-14,
March 2006.