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 -