Argument

Dialectica interpretation

Overview

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.

Overview adapted from Wikipedia (CC BY-SA 4.0; see the article history for authors).

Related ideas

• Finitism
• Kurt Gödel
• Intuitionistic logic
• Proof theory
• Peano axioms
• Solomon Feferman
• Linear logic
• Gödel's incompleteness theorems
• Consistency
• Heyting arithmetic
• Jean-Yves Girard
• Double-negation translation
• Dialectica
• Affine logic
• Jeremy Avigad
• Markov's principle

Place in the tradition

Part of Intuitionistic logic.

Explore Dialectica interpretation in the interactive graph →