In proof theory, the Dialectica interpretation 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.
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
Proof translation (soundness)
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 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).
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.
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.
In 1962 Spector 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
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 Shirahata's work 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.
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 , and .
Credits to the contents of this page go to the authors of the corresponding Wikipedia page: en.wikipedia.org/wiki/Dialectica interpretation.