nLab Dialectica interpretation




In proof theory, the Gödel’s Dialectica interpretation is a proof interpretation of intuitionistic arithmetic (Heyting arithmetic) into a finite type extension of primitive recursive arithmetic. It was reinterpreted by de Paiva as a construction (actually, multiple related constructions) on categories, related to (but distinct from) the Chu construction.


  • Kohlenbach’s Proof Mining Program: A systematic development of specially designed versions of functional interpretations (Dialectica is the prime example) and their use in numerical analysis, functional analysis, metric fixed point theory and geodesic geometry. See Gödel’s functional interpretation and its use in current mathematics.

  • Certain cardinal invariants of the continuum in ZFC set theory can be expressed and proven using Dialectica categories; see da Silva and de Paiva.


The original Dialectica construction in proof theory is due to:

  • Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica (1958), pp. 280–287.

Other work in proof theory:

  • Avigad and Feferman, Gödel’s Functional (“Dialectica”) Interpretation. Available from

The categorical construction originally appeared in

  • Valeria de Paiva, The Dialectica Categories. University of Cambridge, Computer Laboratory, PhD Thesis, Technical Report 213, 1991 (pdf).

and has been studied further by de Paiva and many others.

For comparisons to the Chu construction, see

  • Valeria de Paiva, Dialectica and Chu Constructions: Cousins?, Theory and Applications of Categories, Vol. 17, 2006, No. 7, pp 127-152., link

  • Mike Shulman, The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions, Theory and Applications of Categories, Vol. 35, 2020, No. 4, pp 89-136. link

Application to cardinal invariants in set theory is discussed in

Last revised on April 7, 2023 at 02:57:43. See the history of this page for a list of all contributions to it.