Dialectica interpretation

From Wikipedia, the free encyclopedia

The Dialectica interpretation [1], developed by Kurt Gödel, is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic, the so-called System T.

Contents

[edit] Motivation

Via the Gödel/Gentzen negative translation, the consistency of Peano arithmetic had already been reduced to the consistency of Heyting arithmetic. Gödel's motivation for developing the Dialectica interpretation was to obtain a relative consistency proof for Heyting arithmetic (and hence for Peano arithmetic).

[edit] Interpretation (formula translation)

Formula interpretation. To each formula A of Heyting arithmetic a quantifier-free formula AD(x;y) of the system T, where x and y are tuples of fresh variables (not appearing free in A). The quantifier-free formula AD(x;y) is defined inductively on the logical structure of A as follows, where P is an atomic formula:

\begin{array}{lcl} (P)_D & \equiv & P \\ (A \wedge B)_D(x, v; y, w) & \equiv & A_D(x; y) \wedge B_D(v; w) \\ (A \vee B)_D(x, v, z; y, w) & \equiv & (z = 0 \rightarrow A_D(x; y)) \wedge (z \neq 0 \to B_D(v; w)) \\ (A \rightarrow B)_D(f, g; x, w) & \equiv & A_D(x; f x w) \wedge B_D(g x; w) \\ (\exists z A)_D(x, z; y) & \equiv & A_D(x; y) \\ (\forall z A)_D(f; y, z) & \equiv & A_D(f z; y) \end{array}

[edit] Soundness theorem (proof translation)

The formula interpretation is such that whenever A is provable in Heything arithmetic then there exists a sequence of closed terms t such that AD(t;y) is provable in the system T. The sequence of terms t and the proof of AD(t;y) are constructed from the given proof of A in Heyting arithmetic. It has also been shown that Heyting arithmetic extended with the following principles

is necessary and sufficient for characterising the formulas of HA which are interpretable by the Dialectica interpretation.

[edit] Interpretation of affine logic

The Dialectica interpretation has been used to build a model of Girard's refinement of intuitionistic logic known as linear logic, via the so-called Dialectica spaces. Because the linear interpretation[2] validates the weakening rule for arbitrary formulas it is actually an interpretation of affine logic.

[edit] Interpretation of induction

Given Gödel's incompleteness theorem (which implies that the consistency of PA cannot be proven by finitistic means) it is reasonable to expect that system T must contain non-finitistic constructions. Indeed this is the case. The non-finitistic constructions show up in the interpretation of mathematical induction. In order to give a Dialectica interpretation of induction, Gödel makes use of what is nowadays called Gödel's primitive recursive functionals.

[edit] Interpretation of comprehension

In 1962 Spector [3] extended Gödel's Dialectica interpretation of arithmetic to full mathematical analysis, by showing how the schema of countable choice can be given a Dialectica interpretation by extending system T with bar recursion.

[edit] Variants of the dialectica interpretation

Several variants of the Dialectica interpretation have been proposed since. Most notably the Diller-Nahm variant (in order to avoid the contraction problem) and Kohlenbach's monotone and Ferreira-Oliva bounded interpretations (in order to interpret weak König's lemma). Comprehensive treatments of the interpretation can be found at [4], [5] and [6].

[edit] References

  1. ^ Kurt Gödel (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica, 280--287. 
  2. ^ Masaru Shirahata (2006). The Dialectica interpretation of first-order classical affine logic. Theory and Applications of Categories, Vol. 17, No. 4, 49--79. 
  3. ^ Cliford Spector (1962). Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. Recursive Function Theory: Proc. Symposia in Pure Mathematics, 1--27. 
  4. ^ Jeremy Avigad and Solomon Feferman (1999). Gödel's functional ("Dialectica") interpretation. in S. Buss ed., The Handbook of Proof Theory, North-Holland, 337--405. 
  5. ^ Ulrich Kohlenbach (2008). Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer Verlag, Berlin, 1--536. 
  6. ^ Anne S. Troelstra (with C.A. Smorynski, J.I. Zucker, W.A.Howard) (1973). Metamathematical Investigationof intuitionistic Arithmetic and Analysis. Springer Verlag, Berlin, 1--323.