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
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