Induction Is Not Derivable in Second Order Dependent Type Theory Export

@incollection{citeulike:6081478, abstract = {This paper proves the non-derivability of induction in second order dependent type theory (λP2). This is done by providing a model construction for λP2, based on a saturated sets like interpretation of types as sets of terms of a weakly extensional combinatory algebra. We give counter-models in which the induction principle over natural numbers is not valid. The proof does not depend on the specific encoding for natural numbers that has been chosen (like e.g. polymorphic Church numerals), so in fact we prove that there can not be an encoding of natural numbers in λP2 such that the induction principle is satisfied. The method extends immediately to other data types, like booleans, lists, trees, etc. In the process of the proof we establish some general properties of the models, which we think are of independent interest. Moreover, we show that the Axiom of Choice is not derivable in λP2.}, author = {Geuvers, Herman}, citeulike-article-id = {6081478}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-45413-6_16}, citeulike-linkout-1 = {http://www.springerlink.com/content/uqw3xcbtyh6a2cle}, doi = {10.1007/3-540-45413-6_16}, journal = {Typed Lambda Calculi and Applications}, keywords = {lambda-calculus, system-f}, pages = {166--181}, posted-at = {2009-11-06 20:00:33}, priority = {2}, title = {Induction Is Not Derivable in Second Order Dependent Type Theory}, url = {http://dx.doi.org/10.1007/3-540-45413-6_16}, year = {2001} }

TY - CHAP ID - citeulike:6081478 L3 - citeulike-article-id:6081478 N2 - This paper proves the non-derivability of induction in second order dependent type theory (λP2). This is done by providing a model construction for λP2, based on a saturated sets like interpretation of types as sets of terms of a weakly extensional combinatory algebra. We give counter-models in which the induction principle over natural numbers is not valid. The proof does not depend on the specific encoding for natural numbers that has been chosen (like e.g. polymorphic Church numerals), so in fact we prove that there can not be an encoding of natural numbers in λP2 such that the induction principle is satisfied. The method extends immediately to other data types, like booleans, lists, trees, etc. In the process of the proof we establish some general properties of the models, which we think are of independent interest. Moreover, we show that the Axiom of Choice is not derivable in λP2. JF - Typed Lambda Calculi and Applications EP - 181 TI - Induction Is Not Derivable in Second Order Dependent Type Theory SP - 166 KW - lambda-calculus KW - system-f AU - Geuvers, Herman PY - 2001/// UR - http://dx.doi.org/10.1007/3-540-45413-6_16 ER -