 It is not generally true that a formula \(A\) is a theorem of pure quantificational logic if, and only if, \(\neg \neg A\) is a theorem of intuitionistic quantificational logic, but there is a more sophisticated double-negation interpretation of theorems of pure quantificational logic. In particular, we have that a formula \(A\) is a theorem of quantificational logic if, and only if, it is a theorem of intuitionistic quantificational logic supplemented with a double negation schema: