Editing Intuitionistic logic (section)

====Formula translation====
Weakening statements by adding two negations before existential quantifiers (and atoms) is also the core step in the [[Gödel-Gentzen translation|double-negation translation]]. It constitutes an [[embedding]] of classical first-order logic into intuitionistic logic: a first-order formula is provable in classical logic if and only if its Gödel–Gentzen translation is provable intuitionistically. For example, any theorem of classical propositional logic of the form  <math>\psi\to\phi</math> has a proof consisting of an intuitionistic proof of <math>\psi\to\neg\neg\phi</math> followed by one application of double-negation elimination. Intuitionistic logic can thus be seen as a means of extending classical logic with constructive semantics.