A semantical proof of De Jongh's theorem (Q1812961)

From MaRDI portal
scientific article
Language Label Description Also known as
English
A semantical proof of De Jongh's theorem
scientific article

    Statements

    A semantical proof of De Jongh's theorem (English)
    0 references
    0 references
    25 June 1992
    0 references
    The author gives a proof of De Jongh's maximality theorem (intuitionistic first-order predicate logic proves a formula A iff intuitionistic first- order arithmetic HA proves all arithmetical substitution instances of A), using sheaf models of realizability. A corollary of the proof is the maximality of the intuitionistic first-order predicate calculus with respect to a notion of realizability, defined in an expansion of HA containing combinators; one might view this as evidence for the conjecture that, in an intuitionistic metatheory, Kleene's realizability gives a faithful interpretation of the intuitionistic connectives.
    0 references
    De Jongh's maximality theorem
    0 references
    intuitionistic first-order predicate logic
    0 references
    intuitionistic first-order arithmetic HA
    0 references
    sheaf models of realizability
    0 references
    Kleene's realizability
    0 references

    Identifiers