Motivation[edit]
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).
Linear logic[edit]
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.[3] 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[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.
Variants[edit]
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,[5][6] and.[7]