 Glivenko’s Theorem does not extend to predicate logic, although an arbitrary predicate formula \(A\) is classically provable if and only if \(\neg \neg A\) is provable in intuitionistic predicate logic plus the “double negation shift” schema.