Dialectica interpretation

From Wikipedia for FEVERv2
Jump to navigation Jump to search

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

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

Motivation Dialectica interpretation_section_0

Via the Gödel–Gentzen negative translation, the consistency of classical Peano arithmetic had already been reduced to the consistency of intuitionistic Heyting arithmetic. Dialectica interpretation_sentence_2

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_sentence_3

Dialectica interpretation of intuitionistic logic Dialectica interpretation_section_1

Formula translation Dialectica interpretation_section_2

Proof translation (soundness) Dialectica interpretation_section_3

Characterisation principles Dialectica interpretation_section_4

It has also been shown that Heyting arithmetic extended with the following principles Dialectica interpretation_sentence_4

Dialectica interpretation_unordered_list_0

is necessary and sufficient for characterising the formulas of HA which are interpretable by the Dialectica interpretation. Dialectica interpretation_sentence_5

Extensions of basic interpretation Dialectica interpretation_section_5

The basic dialectica interpretation of intuitionistic logic has been extended to various stronger systems. Dialectica interpretation_sentence_6

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

Induction Dialectica interpretation_section_6

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

Indeed this is the case. Dialectica interpretation_sentence_9

The non-finitistic constructions show up in the interpretation of mathematical induction. Dialectica interpretation_sentence_10

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

Classical logic Dialectica interpretation_section_7

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

Shoenfield, in his book, combines the negative translation and the Dialectica interpretation into a single interpretation of classical arithmetic. Dialectica interpretation_sentence_13

Comprehension Dialectica interpretation_section_8

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_sentence_14

Dialectica interpretation of linear logic Dialectica interpretation_section_9

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

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

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

Variants of the Dialectica interpretation Dialectica interpretation_section_10

Several variants of the Dialectica interpretation have been proposed since. Dialectica interpretation_sentence_18

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

Comprehensive treatments of the interpretation can be found at , and . Dialectica interpretation_sentence_20

Credits to the contents of this page go to the authors of the corresponding Wikipedia page: en.wikipedia.org/wiki/Dialectica interpretation.