Joyal's arithmetic universe as list-arithmetic pretopos

Maria Emilia Maietti

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 André Joyal to give a categorical proof of Gödel's incompleteness results.

Keywords: Pretopoi, dependent type theory, categorical logic

2000 MSC: 03G30, 03B15, 18C50, 03B20, 03F55

Theory and Applications of Categories, Vol. 24, 2010, No. 3, pp 39-83.

http://www.tac.mta.ca/tac/volumes/24/3/24-03.dvi
http://www.tac.mta.ca/tac/volumes/24/3/24-03.ps
http://www.tac.mta.ca/tac/volumes/24/3/24-03.pdf
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/24/3/24-03.dvi
ftp://ftp.tac.mta.ca/pub/tac/html/volumes/24/3/24-03.ps

TAC Home