Dialectica interpretation




In proof theory, the 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.



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.

The categorical construction originally appeared in

  • Valeria de Paiva, The Dialectica Categories. University of Cambridge, Computer Laboratory, PhD Thesis, Technical Report 213, (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 24, 2020 at 20:20:49. See the history of this page for a list of all contributions to it.