Dialectica interpretation
Arithmetical concept
title: "Dialectica interpretation" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["proof-theory", "intuitionism", "1958-introductions"] description: "Arithmetical concept" topic_path: "general/proof-theory" source: "https://en.wikipedia.org/wiki/Dialectica_interpretation" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0
::summary Arithmetical concept ::
In proof theory, the Dialectica interpretation{{cite book | title = Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes | author = Kurt Gödel | publisher = Dialectica | year = 1958 | pages = 280–287
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).
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 A_D(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 A_D(t; y) in the system T.
Formula translation
The quantifier-free formula A_D(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 A_D(t; y) is provable in the system T. The sequence of terms t and the proof of A_D(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
- Axiom of choice
- Markov's principle
- Independence of premise for universal formulas is necessary and sufficient for characterising the formulas of HA which are interpretable by the Dialectica interpretation. The choice axiom here is formulated for any 2-ary predicate in the premise and an existence claim with a variable of function type in its conclusion.
Extensions
The basic dialectica interpretation of intuitionistic logic has been extended to various stronger systems. Intuitively, the dialectica interpretation can be applied to a 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 by 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{{cite book | title = Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics | author = Clifford Spector | publisher = Recursive Function Theory: Proc. Symposia in Pure Mathematics | year = 1962 | pages = 1–27
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.{{cite book | title = The Dialectica Categories | author = Valeria de Paiva | url = http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-213.pdf | publisher = University of Cambridge, Computer Laboratory, PhD Thesis, Technical Report 213 | year = 1991
Although the linear interpretation in Shirahata's work{{cite book | title = The Dialectica interpretation of first-order classical affine logic | author = Masaru Shirahata | url = http://www.tac.mta.ca/tac/volumes/17/4/17-04abs.html | publisher = Theory and Applications of Categories, Vol. 17, No. 4 | year = 2006 | pages = 49–79
Variants
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,{{cite book | title = Gödel's functional ("Dialectica") interpretation | url = http://math.stanford.edu/~feferman/papers/dialectica.pdf | author = Jeremy Avigad and Solomon Feferman | publisher = in S. Buss ed., The Handbook of Proof Theory, North-Holland | year = 1999 | pages = 337–405 | title = Applied Proof Theory: Proof Interpretations and Their Use in Mathematics | url = https://archive.org/details/appliedprooftheo00ukoh | url-access = limited | author = Ulrich Kohlenbach | publisher = Springer Verlag, Berlin | year = 2008 | pages = 1–536 | title = Metamathematical Investigation of Intuitionistic Arithmetic and Analysis | author = Anne S. Troelstra (with C.A. Smoryński, J.I. Zucker, W.A.Howard) | publisher = Springer Verlag, Berlin | year = 1973 | pages = 1–323
References
::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::