Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Dialectica interpretation
Résumé
In proof theory, the Dialectica interpretation is a proof interpretation of intuitionistic logic (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).
Logic translation
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 (not appearing free in ). 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.
The quantifier-free formula is defined inductively on the logical structure of as follows, where is an atomic formula:
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.
It has also been shown that Heyting arithmetic extended with the following principles
Axiom of choice
Markov's principle
Independence of premise for universal formulas
is necessary and sufficient for characterising the formulas of HA which are interpretable by the Dialectica interpretation.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.