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

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.