 The proof of this version of de Jongh’s Theorem does not need realizability; cf. Smorynski [1973]. As an example, Rosser’s form of Gödel’s Incompleteness Theorem provides a sentence \(C\) of \(L(\mathbf{HA})\) such that \(\mathbf{PA}\) proves neither \(C\) nor \(\neg C,\) so by the disjunction property \(\mathbf{HA}\) cannot prove \((C \vee \neg C).\) But de Jongh’s semantical proof also established that every intuitionistically unprovable predicate formula of a restricted kind has an arithmetical substitution instance which is unprovable in \(\mathbf{HA}.\) Using a syntactic method, Daniel Leivant [1979] extended de Jongh’s Theorem to all intuitionistically unprovable predicate formulas, proving that \(\mathbf{IQC}\) is arithmetically complete for \(\bf{HA}.\) See van Oosten [1991] for a historical exposition and a simpler proof of the full theorem, using abstract realizability with Beth models instead of Kripke models.