
AbstractThis 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.
linear logic, natural numbers object, categorical logic, dialectica categories, Theoretical Computer Science, Computer Science(all)
linear logic, natural numbers object, categorical logic, dialectica categories, Theoretical Computer Science, Computer Science(all)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
