Open AccessNatural Number Objects in Dialectica Categories
Author(s) -
Valeria de Paiva,
Charles G. Morgan,
Samuel G. da Silva
Publication year - 2014
Publication title -
electronic notes in theoretical computer science
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.242
H-Index - 60
ISSN - 1571-0661
DOI - 10.1016/j.entcs.2014.06.005
Subject(s) - interpretation (philosophy) , consistency (knowledge bases) , natural (archaeology) , set (abstract data type) , categorical variable , natural number , linear logic , mathematics , epistemology , philosophy , computer science , discrete mathematics , linguistics , biology , paleontology , statistics , programming language
This note sets down some facts about natural number objects in the Dialectica category Dial2(Sets). Natural number objects allow us to model Gödel's System T in an intrinsically logical fashion. Gödel's Dialectica Interpretation is a powerful tool originally used to prove the consistency of arithmetic. It was surprising (but pleasing) to discover, in the late eighties, that studying the Dialectica Interpretation by means of categorical proof theory led to models of Girard's Linear Logic, in the shape of Dialectica categories. More recently Dialectica Interpretations of (by now established) Linear Logic systems have been studied, but not extended to System T. In this note we set out to to consider notions of natural number objects in the original Dialectica category models of the Interpretation. These should lead to intrinsic notions of linear recursitivity, we hope
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom