 Gödel’s so-called double negation interpretation extends Theorem 9 to a reduction of classical first order logic to intuitionistic predicate logic. The translation in this case can be taken to map A′ to A for atomic A. Moreover, we let ∀xA(x)′ = ∀xA′(x) :