---
tag: FXVTE32FPN
kind: statement
role: proposition
name: Formula translation
sources:
  - wikipedia: en:169262@r1372008844
    locator: Intuitionistic logic, section Theorems > Double negations > Formula translation
    note: adopted
    mention: wikipedia://en/169262#PBP8
    sections: [Statement]
inventory: [WPD41Z66W7]
---

## Statement

Weakening statements by adding two negations before existential quantifiers (and atoms) is also the core step in the 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 $\psi\to\phi$ has a proof consisting of an intuitionistic proof of $\psi\to\neg\neg\phi$ followed by one application of double-negation elimination. Intuitionistic logic can thus be seen as a means of extending classical logic with constructive semantics.