We explain in detail why the notion of list-arithmetic pretopos should be taken as the general categorical definition for the construction of arithmetic universes introduced by Andre Joyal to give a categorical proof of Godel's incompleteness results. We motivate this definition for three reasons: first, Joyal's arithmetic universes are list-arithmetic pretopoi; second, the initial arithmetic universe among Joyal's constructions is equivalent to the initial list-arithmetic pretopos; third, any list-arithmetic pretopos enjoys the existence of free internal categories and diagrams as required to prove Godel's incompleteness. In doing our proofs we make an extensive use of the internal type theory of the categorical structures involved in Joyal's constructions. The definition of list-arithmetic pretopos is equivalent to the general one that I came to know in a recent talk by Andre Joyal.

Joyal's arithmetic universe as list-arithmetic pretopos

MAIETTI, MARIA EMILIA
2010

Abstract

We explain in detail why the notion of list-arithmetic pretopos should be taken as the general categorical definition for the construction of arithmetic universes introduced by Andre Joyal to give a categorical proof of Godel's incompleteness results. We motivate this definition for three reasons: first, Joyal's arithmetic universes are list-arithmetic pretopoi; second, the initial arithmetic universe among Joyal's constructions is equivalent to the initial list-arithmetic pretopos; third, any list-arithmetic pretopos enjoys the existence of free internal categories and diagrams as required to prove Godel's incompleteness. In doing our proofs we make an extensive use of the internal type theory of the categorical structures involved in Joyal's constructions. The definition of list-arithmetic pretopos is equivalent to the general one that I came to know in a recent talk by Andre Joyal.
2010
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11577/2426137
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 17
  • OpenAlex ND
social impact