Induction is not derivable in second order dependent type theory

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    16 Citations (Scopus)
    3 Downloads (Pure)

    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.
    Original languageEnglish
    Title of host publicationTyped Lambda Calculi and Applications : 5th International Conference, TLCA 2001, Kraków, Poland, May 2-5, 2001: proceedings
    EditorsS. Abramsky
    PublisherSpringer
    Pages166-181
    ISBN (Print)3-540-41960-8
    DOIs
    Publication statusPublished - 2001

    Publication series

    NameLecture Notes in Computer Science
    Volume2044
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'Induction is not derivable in second order dependent type theory'. Together they form a unique fingerprint.

    Cite this