Math 2.0

Mathematical logic and foundations Proof theory Concept

Dialectica interpretation

Builds on Heyting arithmeticPrimitive recursive function

Summary

The Dialectica interpretation translates Heyting arithmetic into Gödel's system T. This is a quantifier-free theory of computable functionals of finite type. Gödel published it in 1958 in the journal Dialectica. Each formula becomes a formula of the form ∃x ∀y AD(x,y)\exists x\, \forall y\, A_D(x, y), and a proof yields a term of system T that gives the witness xx. It gives a relative consistency proof of arithmetic and is the main tool for extracting bounds from proofs.

Reading path

To understand this page from the ground up, read these 5 pages in order. The foundations come first.

Show the path as a graph
Intuitionistic logic, concept, no evidence levelIntuitionistic logicconceptPeano axioms, concept, no evidence levelPeano axiomsconceptPrimitive recursive function, concept, no evidence levelPrimitive recursive f…conceptHeyting arithmetic, concept, no evidence levelHeyting arithmeticconceptDialectica interpretation, concept, no evidence levelDialectica interpreta…concept
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Intuitionistic logic concept
  2. Peano axioms concept
  3. Primitive recursive function concept
  4. Heyting arithmetic concept
  5. Dialectica interpretation concept

Further reading

  1. Web https://en.wikipedia.org/wiki/Dialectica_interpretation
About this page
TagHZ17ES9PDY
URIm2://HZ17ES9PDY
Kindconcept
WritingW0 stub
MSC03F10, 03F25, 03F50
UsesHeyting arithmetic, Primitive recursive function
Same as
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

Definitions