TY - JOUR
T1 - Cartesian Closed Dialectica Categories
AU - Biering, Bodil
N1 - Annals of Mathematical Logic continued as
Annals of Pure and Applied Logic
Paper id:: 0.1016/j.apal.2008.07.004
PY - 2008
Y1 - 2008
N2 - When Gödel developed his functional interpretation, also known as the Dialectica interpretation, his aim was to prove (relative) consistency of first order arithmetic by reducing it to a quantifier-free theory with finite types. Like other functional interpretations (e.g. Kleene’s realizability interpretation and Kreisel’s modified realizability) Gödel’s Dialectica interpretation gives rise to category theoretic constructions that serve both as new models for logic and semantics and as tools for analysing and understanding various aspects of the Dialectica interpretation itself. Gödel’s Dialectica interpretation gives rise to the Dialectica categories (described by V. de Paiva in [V.C.V. de Paiva, The Dialectica categories, in: Categories in Computer Science and Logic (Boulder, CO, 1987), in: Contemp. Math., vol. 92, Amer. Math. Soc., Providence, RI, 1989, pp. 47–62] and J.M.E. Hyland in [J.M.E. Hyland, Proof theory in the abstract, Ann. Pure Appl. Logic 114 (1–3) (2002) 43–78, Commemorative Symposium Dedicated to Anne S. Troelstra (Noordwijkerhout, 1999)]). These categories are symmetric monoidal closed and have finite products and weak coproducts, but they are not Cartesian closed in general. We give an analysis of how to obtain weakly Cartesian closed and Cartesian closed Dialectica categories, and we also reflect on what the analysis might tell us about the Dialectica interpretation.
AB - When Gödel developed his functional interpretation, also known as the Dialectica interpretation, his aim was to prove (relative) consistency of first order arithmetic by reducing it to a quantifier-free theory with finite types. Like other functional interpretations (e.g. Kleene’s realizability interpretation and Kreisel’s modified realizability) Gödel’s Dialectica interpretation gives rise to category theoretic constructions that serve both as new models for logic and semantics and as tools for analysing and understanding various aspects of the Dialectica interpretation itself. Gödel’s Dialectica interpretation gives rise to the Dialectica categories (described by V. de Paiva in [V.C.V. de Paiva, The Dialectica categories, in: Categories in Computer Science and Logic (Boulder, CO, 1987), in: Contemp. Math., vol. 92, Amer. Math. Soc., Providence, RI, 1989, pp. 47–62] and J.M.E. Hyland in [J.M.E. Hyland, Proof theory in the abstract, Ann. Pure Appl. Logic 114 (1–3) (2002) 43–78, Commemorative Symposium Dedicated to Anne S. Troelstra (Noordwijkerhout, 1999)]). These categories are symmetric monoidal closed and have finite products and weak coproducts, but they are not Cartesian closed in general. We give an analysis of how to obtain weakly Cartesian closed and Cartesian closed Dialectica categories, and we also reflect on what the analysis might tell us about the Dialectica interpretation.
KW - Dialectica categories
KW - Dialectica interpretation
KW - Functional interpretation
KW - Realizability
KW - Dialectica categories
KW - Dialectica interpretation
KW - Functional interpretation
KW - Realizability
U2 - doi:10.1016/j.apal.2008.07.004
DO - doi:10.1016/j.apal.2008.07.004
M3 - Journal article
SN - 0168-0072
VL - 156
SP - 290
EP - 307
JO - Annals of Pure and Applied Logic
JF - Annals of Pure and Applied Logic
ER -