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:
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 24, 2020 at 20:20:49. See the history of this page for a list of all contributions to it.