Arithmetic Universes

Introduction

Following Lawvere's categorical treatment of algebraic theories, which abstracts so successfully from syntax based presentations, many mathematicians felt that much of mathematical logic would be better formulated categorically. In 1973, André Joyal proposed a categorical formulation of Gödel's incompleteness theorem for theories of arithmetic. As with Lawvere's treatment of algebraic theories, Joyal's proposal uses categorical structure to abstract from the details of the syntax of arithmetic theories. In particular, Joyal's proof includes an abstract account of Gödel numbering. This sort of high level formulation should make it easier to apply and extend Gödel's result and related results.

It has been suggested by Vickers (1999) that, quite independently from incompleteness results, Joyal's notion of Arithmetic Universe may provide a good strength of logic for specifying computations. Maietti (1999) has identified a dependently typed internal language for Arithmetic Universes and exploits this to demonstrate the existence of some useful constructions in Arithmetic Universes. Taylor observes that every Arithmetic Universe may be represtented as the category of overt discrete spaces in a model of ASD.

References

• A. Joyal. Theorem d'Incomplétitude de Gödel et Univers Arithmétiques. Unpublished talk, Amiens Colloquium, 9 July 1973.
• A. Joyal. On the Incompleteness Theorem of Gödel from the Point of View of the Theory of Categories. Unpublished talk, Milano, 28 June 1978.
• A. Joyal. `The Gödel Incompleteness Theorem', Section 4 (26 November) in Categories and Logic, Topos Theory/Category Theory Seminar, mimeographed notes, 1979. 16 pages.
• M. E. Maietti. The Typed Calculus of Arithmetic Universes. Technical report CSR-99-14, School of computer Science, University of Birmingham, December 1999.
• M. Maietti. Modular Correspondence Between Dependent Type Theories and Categorical Universes. Report No. 44, 2000/2001, Institute Mittag-Leffler, the Royal Swedish Academy of Sciences. ISSN 1103-467X, ISRN IML-R-44-00/01-SE. 39 pages.
• M. E. Maietti. Joyal's Arithmetic Universes via Type Theory. Category Theory in Computer Scinece, August 2002, Ottawa, Canada (R. Blute and P. Selinger, editors), Electronic Notes in theoretical Computer Science, vol. 69, Elsevier, 2003.
• A. Morrison. Reasoning in Arithmetic Universes. MSc Thesis, Imperial College, University of London, 1996.
• P. Taylor. `Universes', Section 9.6 in Practical Foundations of Mathematics. Cambridge University Press, 1999.
• P. Taylor, Computably based locally compact spaces. May 2003. 51 pages.
• P. Taylor, Geometric and higher order logic using abstract Stone duality. Theory and Applications of Categories, 7(15):284-338, 2000.
• S. J. Vickers. `Arithmetic universes: some speculations', Section 6.1 in Topical Categories of Domains, Mathematical Structures in Computer Science 9 569-616, 1999.
• G. Wraith. Arithmetic Universes (work of A. Joyal, Amiens Colloquium, 9 July 1973). Unpublished talk, undated.
• G. Wraith. Arithmetic universe notes. Unpublished notes, 24 February 1984, September 1985, others undated.

People

• André Joyal
• Milly Maietti
• Alan Morrison
• Paul Taylor
• Steve Vickers
• Gavin Wraith