 The more sophisticated negative translation of classical into intuitionistic theories, due independently to Gödel and Gentzen, associates with each formula \(A\) of the language \(L\) another formula \(g(A)\) (with no \(\vee\) or \(\exists),\) such that: