The Gödel–Gentzen translation (named after Kurt Gödel and Gerhard Gentzen) associates with each formula φ in a first-order language another formula φN, which is defined inductively: as above, but furthermore and otherwise This translation has the property that φN is classically equivalent to φ. Troelstra and Van Dalen (1988, Ch.
3) give a description, due to Leivant, of formulas that do imply their Gödel–Gentzen translation in intuitionistic first-order logic also.
One possibility can thus succinctly be described as follows: Prefix "¬¬" before every atomic formula, but also to every disjunction and existential quantifier, Another procedure, known as Kuroda's translation, is to construct a translated φ by putting "¬¬" before the whole formula and after every universal quantifier.
The Gödel-Gentzen- and Kuroda-translated formulas of each φ are provenly equivalent to one another, and this result holds already in minimal propositional logic.
Let TN consist of the double-negation translations of the formulas in T. The fundamental soundness theorem (Avigad and Feferman 1998, p. 342; Buss 1998 p. 66) states: The double-negation translation was used by Gödel (1933) to study the relationship between classical and intuitionistic theories of the natural numbers ("arithmetic").