Dialectica interpretation


In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic 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.

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.

Dialectica interpretation of intuitionistic logic

The interpretation has two components: a formula translation and a proof translation. The formula translation describes how each formula of Heyting arithmetic is mapped to a quantifier-free formula of the system T, where and are tuples of fresh variables. Intuitively, is interpreted as. The proof translation shows how a proof of has enough information to witness the interpretation of, i.e. the proof of can be converted into a closed term and a proof of in the system T.

Formula translation

The quantifier-free formula is defined inductively on the logical structure of as follows, where is an atomic formula:

Proof translation (soundness)

The formula interpretation is such that whenever is provable in Heyting arithmetic then there exists a sequence of closed terms such that is provable in the system T. The sequence of terms and the proof of are constructed from the given proof of in Heyting arithmetic. The construction of is quite straightforward, except for the contraction axiom 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 a stronger system, as long as the dialectica interpretation of the extra principle can be witnessed by terms in the system T.

Induction

Given Gödel's incompleteness theorem 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
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 Shirahata's work validates the weakening rule , 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 and Kohlenbach's monotone and Ferreira-Oliva bounded interpretations.
Comprehensive treatments of the interpretation can be found at
,
and