Dialectica interpretation

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. 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.

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).

The interpretation has two components: a formula translation and a proof translation. The formula translation describes how each formula ${\displaystyle A}$ of Heyting arithmetic is mapped to a quantifier-free formula ${\displaystyle A_{D}(x;y)}$ of the system T, where ${\displaystyle x}$ and ${\displaystyle y}$ are tuples of fresh variables (not appearing free in ${\displaystyle A}$). Intuitively, ${\displaystyle A}$ is interpreted as ${\displaystyle \exists x\forall yA_{D}(x;y)}$. The proof translation shows how a proof of ${\displaystyle A}$ has enough information to witness the interpretation of ${\displaystyle A}$, i.e. the proof of ${\displaystyle A}$ can be converted into a closed term ${\displaystyle t}$ and a proof of ${\displaystyle A_{D}(t;y)}$ in the system T.

...
Wikipedia