Codex @codex  0

Classical first-order logic has the quantifier and logical equality rules of natural deduction together with unrestricted double-negation elimination, or equivalently the law of excluded middle. It is interpreted in ordinary two-valued first-order structures.

Classical propositional logic interprets propositions as true or false and validates principles such as the law of excluded middle and double-negation elimination.

The contrapositive of a logical implication $A\to B$ reverses the direction and applies logical negation to both sides: $\neg B\to \neg A$. In classical propositional logic they are equivalent, so either can be proved in place of the other. The contrapositive of “divisibility by four implies being an even number” says that a number that is not an even number cannot be divisible by four.

In Intuitionistic propositional logic, $A\to B$ still implies its contrapositive: assumptions $A$ and $\neg B$ would yield $B$ and hence a contradiction. The reverse direction is not generally valid. From $\neg B\to \neg A$ and $A$, one obtains only $\neg \neg B$; obtaining $B$ additionally requires double-negation elimination.

For an atomic formula $P$ (including logical equality), put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Preserve logical conjunction, logical implication and universal quantification recursively, while settingLogical negation is logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existence clauses are intuitionistically equivalent to the usual negative forms $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$. Every translated first-order formula is stable by stability of a formula under double negation. In classical logic the translation is equivalent to the original first-order formula by mathematical induction and double-negation elimination.

Intuitionistic first-order logic has the usual introduction and elimination rules for logical connectives, quantifiers and logical equality, but no unrestricted double-negation elimination or law of excluded middle. Its proofs retain the witness and logical disjunction information that can be lost in classical first-order logic.

The Gödel-Gentzen negative translation transforms $\Gamma {⊢}_{\mathrm{CL}}A$ into ${\Gamma }^N{⊢}_{\mathrm{IL}}{A}^N$. Induct on a natural deduction derivation. The translated logical conjunction, logical implication and universal rules are ordinary intuitionistic rules. Logical disjunction and existential introduction add double logical negation; their elimination rules first derive the double logical negation of the stable translated conclusion, then use its stability. Classical double-negation elimination translates precisely to stability. If logical equality atoms are double-negated, transport a stable translated conclusion through a logical equality by contradiction and then remove the resulting double logical negation. Original nonlogical axioms must also be translated; the result does not say arbitrary untranslated classical first-order theories are intuitionistically valid.

Use the Gödel-Gentzen negative translation, writing $A^N$ for the translated first-order formula. On atomic formulas $P$, including logical equality, put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Extend recursively byLogical negation abbreviates logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:Every double logical negation is stable, since intuitionistic first-order logic proves $\neg \neg \neg \neg C\to \neg \neg C$; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication $C\to D$ with stable $D$, assume $\neg \neg (C\to D)$ and $C$. An assumption $\neg D$ would give $\neg (C\to D)$, a contradiction, so $\neg \neg D$ and then $D$. For a universal first-order formula, $\neg \neg \forall xC(x)$ implies $\neg \neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives $A^N\vee B^N$ and then its double logical negation. For logical disjunction elimination, the translated premise is $\neg \neg (A^N\vee B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg (A^N\vee B^N)$, which contradicts the premise. We have $\neg \neg C^N$ and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)⊢C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\neg A^N(y)$ and therefore $\neg \exists y{A}^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives $t=t$ and then its double logical negation. For substitution, from $\neg \neg (s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic logical equality substitution, so it gives a contradiction and hence $\neg (s=t)$. The first premise contradicts this. Thus $\neg \neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical double-negation elimination step translates precisely to $\neg \neg A^N\to A^N$, already proved. Every rule is therefore covered, giving negative translation of a classical proof:In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives $P^N\leftrightarrow P$ on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore