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. https://www2.mathematik.tu-darmstadt.de/~kohlenbach/centenary.pdf
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:
Other work in proof theory:
The categorical construction originally appeared in
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.