Double-negation translation

From Wikipedia for FEVERv2
Revision as of 05:12, 7 January 2021 by imported>Unknown user
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search

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 by translating formulas to formulas which are classically equivalent but intuitionistically inequivalent. Double-negation translation_sentence_0

Particular instances of double-negation translation include Glivenko's translation for propositional logic, and the Gödel–Gentzen translation and Kuroda's translation for first-order logic. Double-negation translation_sentence_1

Propositional logic Double-negation translation_section_0

The easiest double-negation translation to describe comes from Glivenko's theorem, proved by Valery Glivenko in 1929. Double-negation translation_sentence_2

It maps each classical formula φ to its double negation ¬¬φ. Double-negation translation_sentence_3

Glivenko's theorem states: Double-negation translation_sentence_4

Double-negation translation_description_list_0

  • If φ is a propositional formula, then φ is a classical tautology if and only if ¬¬φ is an intuitionistic tautology.Double-negation translation_item_0_0

Glivenko's theorem implies the more general statement: Double-negation translation_sentence_5

Double-negation translation_description_list_1

  • If T is a set of propositional formulas, T* a set consisting of the doubly negated formulas of T, and φ a propositional formula, then T ⊢ φ in classical logic if and only if T* ⊢ ¬¬φ in intuitionistic logic.Double-negation translation_item_1_1

In particular, a set of propositional formulas is intuitionistically consistent if and only if it is classically satisfiable. Double-negation translation_sentence_6

First-order logic Double-negation translation_section_1

The Gödel–Gentzen translation (named after Kurt Gödel and Gerhard Gentzen) associates with each formula φ in a first-order language another formula φ, which is defined inductively: Double-negation translation_sentence_7

Double-negation translation_unordered_list_2

  • If φ is atomic, then φ is ¬¬φDouble-negation translation_item_2_2
  • (φ ∧ θ) is φ ∧ θDouble-negation translation_item_2_3
  • (φ ∨ θ) is ¬(¬φ ∧ ¬θ)Double-negation translation_item_2_4
  • (φ → θ) is φ → θDouble-negation translation_item_2_5
  • (¬φ) is ¬φDouble-negation translation_item_2_6
  • (∀x φ) is ∀x φDouble-negation translation_item_2_7
  • (∃x φ) is ¬∀x ¬φDouble-negation translation_item_2_8

This translation has the property that φ is classically equivalent to φ. Double-negation translation_sentence_8

The fundamental soundness theorem (Avigad and Feferman 1998, p. 342; Buss 1998 p. 66) states: Double-negation translation_sentence_9

Double-negation translation_description_list_3

  • If T is a set of axioms and φ is a formula, then T proves φ using classical logic if and only if T proves φ using intuitionistic logic.Double-negation translation_item_3_9

Here T consists of the double-negation translations of the formulas in T. Double-negation translation_sentence_10

A sentence φ may not imply its negative translation φ in intuitionistic first-order logic. Double-negation translation_sentence_11

Troelstra and Van Dalen (1988, Ch. Double-negation translation_sentence_12

2, Sec. Double-negation translation_sentence_13

3) give a description (due to Leivant) of formulas that do imply their Gödel–Gentzen translation. Double-negation translation_sentence_14

Variants Double-negation translation_section_2

There are several alternative definitions of the negative translation. Double-negation translation_sentence_15

They are all provably equivalent in intuitionistic logic, but may be easier to apply in particular contexts. Double-negation translation_sentence_16

One possibility is to change the clauses for disjunction and existential quantifier to Double-negation translation_sentence_17

Double-negation translation_unordered_list_4

  • (φ ∨ θ) is ¬¬(φ ∨ θ)Double-negation translation_item_4_10
  • (∃x φ) is ¬¬∃x φDouble-negation translation_item_4_11

Then the translation can be succinctly described as: prefix ¬¬ to every atomic formula, disjunction, and existential quantifier. Double-negation translation_sentence_18

Another possibility (known as Kuroda's translation) is to construct φ from φ by putting ¬¬ before the whole formula and after every universal quantifier. Double-negation translation_sentence_19

Notice that this reduces to the simple ¬¬φ translation if φ is propositional. Double-negation translation_sentence_20

It is also possible to define φ by prefixing ¬¬ before every subformula of φ, as done by Kolmogorov. Double-negation translation_sentence_21

Such a translation is the logical counterpart to the call-by-name continuation-passing style translation of functional programming languages along the lines of the Curry–Howard correspondence between proofs and programs. Double-negation translation_sentence_22

Results Double-negation translation_section_3

The double-negation translation was used by Gödel (1933) to study the relationship between classical and intuitionistic theories of the natural numbers ("arithmetic"). Double-negation translation_sentence_23

He obtains the following result: Double-negation translation_sentence_24

Double-negation translation_description_list_5

  • If a formula φ is provable from the axioms of Peano arithmetic then φ is provable from the axioms of intuitionistic Heyting arithmetic.Double-negation translation_item_5_12

This result shows that if Heyting arithmetic is consistent then so is Peano arithmetic. Double-negation translation_sentence_25

This is because a contradictory formula θ ∧ ¬θ is interpreted as θ ∧ ¬θ, which is still contradictory. Double-negation translation_sentence_26

Moreover, the proof of the relationship is entirely constructive, giving a way to transform a proof of θ ∧ ¬θ in Peano arithmetic into a proof of θ ∧ ¬θ in Heyting arithmetic. Double-negation translation_sentence_27

(By combining the double-negation translation with the Friedman translation, it is in fact possible to prove that Peano arithmetic is Π2-conservative over Heyting arithmetic.) Double-negation translation_sentence_28

The propositional mapping of φ to ¬¬φ does not extend to a sound translation of first-order logic, because ∀x ¬¬φ(x) → ¬¬∀x φ(x) is not a theorem of intuitionistic predicate logic. Double-negation translation_sentence_29

This explains why φ has to be defined in a more complicated way in the first-order case. Double-negation translation_sentence_30

See also Double-negation translation_section_4

Double-negation translation_unordered_list_6

Credits to the contents of this page go to the authors of the corresponding Wikipedia page: translation.