 De Jongh’s Theorem (for IPC) [1970]  If a propositional formula \(A\) of the language \(L\) is not provable in \(\mathbf{IPC},\) then some arithmetical substitution instance of \(A\) is not provable in \(\mathbf{HA}.\)