Dialectica interpretation

Dialectica interpretation

In proof theory, the Dialectica interpretation [1] is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic, the so-called System T. It was developed by Kurt Gödel to provide a consistency proof of arithmetic. The name of the interpretation comes from the journal Dialectica, where Gödel's paper was published in a special issue dedicated to Paul Bernays on his 70th birthday.

Contents

Motivation

Via the Gödel–Gentzen negative translation, the consistency of classical Peano arithmetic had already been reduced to the consistency of intuitionistic 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).

Dialectica interpretation of intuitionistic logic

The interpretation has two components: a formula translation and a proof translation. The formula translation describes how each formula A of Heyting arithmetic is mapped to 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). Intuitively, A is interpreted as \exists x \forall y A_D(x; y). The proof translation shows how a proof of A has enough information to witness the interpretation of A, i.e. the proof of A can be converted into a closed term t and a proof of AD(t;y) in the system T.

Formula translation

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) \rightarrow 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}

Proof translation (soundness)

The formula interpretation is such that whenever A is provable in Heyting 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. The construction of t is quite straightforward, except for the contraction axiom A \rightarrow A \wedge A which requires the assumption that quantifier-free formulas are decidable.

Characterisation principles

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.

Extensions of basic interpretation

The basic dialectica interpretation of intuitionistic logic has been extended to various stronger systems. Intuitively, the dialectica interpretation can be applied to stronger system, as long as the dialectica interpretation of the extra principle can be witnessed by terms in the system T (or an extension of system T).

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. To give a Dialectica interpretation of induction, Gödel makes use of what is nowadays called Gödel's primitive recursive functionals, which are higher order functions with primitive recursive descriptions.

Classical logic

Formulas and proofs in classical arithmetic can also be given a dialectica interpretation via an initial embedding into Heyting arithmetic followed the dialectica interpretation of Heyting arithmetic. Shoenfield, in his book, combines the negative translation and the dialectica interpretation into a single interpretation of classical arithmetic.

Comprehension

In 1962 Spector [2] 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.

Dialectica interpretation of linear 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. Since linear logic is a refinement of intuitionistic logic, the dialectica interpretation of linear logic can also be viewed as a refinement of the dialectica interpretation of intuitionistic logic.

Although the linear interpretation in [3] validates the weakening rule (it is actually an interpretation of affine logic), the dialectica spaces interpretation does not validate weakening for arbitrary formulas.

Variants of the dialectica interpretation

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

References

  1. ^ Kurt Gödel (1958). Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica. pp. 280–287. 
  2. ^ Clifford 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. pp. 1–27. 
  3. ^ Masaru Shirahata (2006). The Dialectica interpretation of first-order classical affine logic. Theory and Applications of Categories, Vol. 17, No. 4. pp. 49–79. 
  4. ^ Jeremy Avigad and Solomon Feferman (1999). Gödel's functional ("Dialectica") interpretation. in S. Buss ed., The Handbook of Proof Theory, North-Holland. pp. 337–405. http://math.stanford.edu/~feferman/papers/dialectica.pdf. 
  5. ^ Ulrich Kohlenbach (2008). Applied Proof Theory: Proof Interpretations and Their Use in Mathematics. Springer Verlag, Berlin. pp. 1–536. 
  6. ^ Anne S. Troelstra (with C.A. Smoryński, J.I. Zucker, W.A.Howard) (1973). Metamathematical Investigation of intuitionistic Arithmetic and Analysis. Springer Verlag, Berlin. pp. 1–323. 

Wikimedia Foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Look at other dictionaries:

  • Dialectica space — Dialectica spaces are a categorical way of constructing models of linear logic. They were introduced by Valeria de Paiva, Martin Hyland s student, in her doctoral thesis, as a way of modeling both linear logic and Gödel s dialectica… …   Wikipedia

  • Dialectica — is a quarterly philosophy journal published by Blackwell. The journal was founded in 1947 by Gaston Bachelard, Paul Bernays and Ferdinand Gonseth. Dialectica is edited in Switzerland and has a focus on analytical philosophy. The journal is the… …   Wikipedia

  • Radical interpretation — is interpretation of a speaker, including attributing beliefs and desires to them and meanings to their words, from scratch that is, without relying on translators, dictionaries, or specific prior knowledge of their mental states. The term was… …   Wikipedia

  • Curry–Howard correspondence — A proof written as a functional program: the proof of commutativity of addition on natural numbers in the proof assistant Coq. nat ind stands for mathematical induction, eq ind for substitution of equals and f equal for taking the same function… …   Wikipedia

  • List of mathematics articles (D) — NOTOC D D distribution D module D D Agostino s K squared test D Alembert Euler condition D Alembert operator D Alembert s formula D Alembert s paradox D Alembert s principle Dagger category Dagger compact category Dagger symmetric monoidal… …   Wikipedia

  • Gödel–Gentzen negative translation — In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first order logic into intuitionistic first order logic. It is one of a number of double negation translations that are of importance to the metatheory of …   Wikipedia

  • Système T — À l instar de la récursion primitive ou le lambda calcul, le Système T est un langage de programmation théorique. Il a été inventé par le logicien Kurt Gödel. Ce système consiste en une fusion de la récursion primitive et du lambda calcul… …   Wikipédia en Français

  • History of logic — Philosophy ( …   Wikipedia

  • Twelfth century (The) — The twelfth century John Marenbon INTRODUCTION The twelfth century began and ended with events which mark it off, at least symbolically, as a discrete period in the history of Western philosophy. It was in about 1100 that Abelard the most wide… …   History of philosophy

  • DIALECTIQUE — Le terme «dialectique» dérive du mot composé grec 嗀晴見凞﨎塚﨎晴益 (dialegein ), qui indique dès le départ que son sens n’est pas simple. La signification la plus courante de﨎塚﨎晴益, c’est «parler» et le préfixe 嗀晴見 indique l’idée d’un rapport ou d’un… …   Encyclopédie Universelle

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”