Concept

Double-negation translation

Overview

In proof theory, a discipline within mathematical logic, double-negation translation, sometimes called negative translation, is a general approach for embedding classical logic into intuitionistic logic. Typically it is done by translating formulas to formulas that are classically equivalent but intuitionistically inequivalent. Particular instances of double-negation translations include Glivenko's translation for propositional logic, and the Gödel–Gentzen translation and Kuroda's translation for first-order logic.

Overview adapted from Wikipedia (CC BY-SA 4.0; see the article history for authors).

Related ideas

• First-order logic
• If and only if
• Kurt Gödel
• Intuitionistic logic
• Propositional logic
• Proof theory
• Mathematical logic
• Peano axioms
• Curry–Howard correspondence
• Minimal logic
• Double negation
• Atomic formula
• Tautology (logic)
• Classical logic
• Logic translation
• Universal quantification
• Existential quantification
• Heyting arithmetic

Place in the tradition

Part of Linear logic.

Explore Double-negation translation in the interactive graph →