Mathematical logic and foundations Definition

Double-negation translation

Builds on Intuitionistic logic Negation Peano axioms Heyting arithmetic Law of excluded middle

Definition

Fix a first-order language, and read $\neg A$ as $A \to \bot$ . The Gödel–Gentzen negative translation is the map $A \mapsto A^N$ on formulas defined by these clauses.

$\bot^N = \bot$ , and $P^N = \neg \neg P$ for every other atomic formula $P$ .
$(A \wedge B)^N = A^N \wedge B^N$ .
$(A \vee B)^N = \neg (\neg A^N \wedge \neg B^N)$ .
$(A \to B)^N = A^N \to B^N$ .
$(\forall x\, A)^N = \forall x\, A^N$ .
$(\exists x\, A)^N = \neg \forall x\, \neg A^N$ .

For a set of formulas $\Gamma$ , let $\Gamma^N = \set{A^N : A \in \Gamma}$ . Its main property is this: $\Gamma \vdash A$ in classical logic if and only if $\Gamma^N \vdash A^N$ in intuitionistic logic. A double-negation translation is any map with this property obtained by inserting double negations, such as the translations of Kolmogorov and Kuroda.

Remarks

Example: for the law of excluded middle with $P$ atomic, $(P \vee \neg P)^N = \neg (\neg \neg \neg P \wedge \neg \neg \neg \neg P)$ . Since $\neg \neg \neg P$ is equivalent to $\neg P$ in intuitionistic logic, this is equivalent to $\neg (\neg P \wedge \neg \neg P)$ , which is intuitionistically provable. Non-example: the identity map $A \mapsto A$ is not a double-negation translation, because $P \vee \neg P$ is classically provable but not intuitionistically provable. For arithmetic, Peano arithmetic proves $A$ if and only if Heyting arithmetic proves $A^N$ . In particular, if HA is consistent, then PA is consistent, because $\bot^N = \bot$ . In arithmetic, atomic formulas are equations, which are decidable in HA, so one may take $P^N = P$ .

Reading path

To understand this page from the ground up, read these 8 pages in order. The foundations come first.

Show the path as a graph

Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.

no evidence level

Intuitionistic logic concept
Peano axioms concept
Proposition concept
Disjunction definition
Negation definition
Law of excluded middle statement
Heyting arithmetic definition
Double-negation translation definition

Tag	`QEZR7PZ2DD`
URI	`m2://QEZR7PZ2DD`
Kind	definition
Writing	W0 stub
MSC	03F25, 03F55, 03B20
Defines	Double-negation translation
Uses	Intuitionistic logic, Negation, Peano axioms, Heyting arithmetic, Law of excluded middle
Changed	2 November 2026

Double-negation translation

Definition

Remarks

Reading path

Further reading

What this page needs for W1

What links here