Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative Export

@article{citeulike:6037061, abstract = {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.}, archivePrefix = {arXiv}, author = {Stoevring, Kristian}, citeulike-article-id = {6037061}, citeulike-linkout-0 = {http://arxiv.org/abs/math/0602544}, citeulike-linkout-1 = {http://arxiv.org/pdf/math/0602544}, citeulike-linkout-2 = {http://dx.doi.org/10.2168/LMCS-2(2:1)2006}, day = {17}, doi = {10.2168/LMCS-2(2:1)2006}, eprint = {math/0602544}, issn = {18605974}, journal = {Logical Methods in Computer Science}, keywords = {lambda-calculus, surjective-pairing}, month = {Mar}, number = {2}, posted-at = {2009-10-29 20:54:42}, priority = {0}, title = {Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative}, url = {http://dx.doi.org/10.2168/LMCS-2(2:1)2006}, volume = {2}, year = {2006} }

TY - JOUR ID - citeulike:6037061 L3 - citeulike-article-id:6037061 N2 - 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. IS - 2 JF - Logical Methods in Computer Science SN - 18605974 TI - Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative VL - 2 KW - lambda-calculus KW - surjective-pairing AU - Stoevring, Kristian PY - 2006/Mar/17/ UR - http://dx.doi.org/10.2168/LMCS-2(2:1)2006 ER -