In proof theory, the Dialectica interpretation[1] is a proof interpretation of intuitionistic logic (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 1958 special issue dedicated to Paul Bernays on his 70th birthday.
Gödel's motivation for developing the dialectica interpretation was to obtain a relative consistency proof for Heyting arithmetic (and hence for Peano arithmetic).
of Heyting arithmetic is mapped to a quantifier-free formula
are tuples of fresh variables (not appearing free in
is provable in Heyting arithmetic then there exists a sequence of closed terms
which requires the assumption that quantifier-free formulas are decidable.
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.
[citation needed] 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.
The basic dialectica interpretation of intuitionistic logic has been extended to various stronger systems.
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.
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.
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.
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.
Although the linear interpretation in Shirahata's work[4] validates the weakening rule (it is actually an interpretation of affine logic), de Paiva's dialectica spaces interpretation does not validate weakening for arbitrary formulas.
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).