Universes in explicit mathematics

Authors
Jager, G Kahle, R Studer, T
Citation
G. Jager et al., Universes in explicit mathematics, ANN PUR APP, 109(3), 2001, pp. 141-162
Citations number
30
Categorie Soggetti
Mathematics
Journal title
ANNALS OF PURE AND APPLIED LOGIC
ISSN journal
01680072 → ACNP
Volume
109
Issue
3
Year of publication
2001
Pages
141 - 162
Database
ISI
SICI code
0168-0072(20010530)109:3<141:UIEM>2.0.ZU;2-0
Abstract
This paper deals with universes in explicit mathematics. After introducing some basic definitions, the limit axiom and possible ordering principles fo r universes are discussed. Later, we turn to least universes, strictness an d name induction. Special emphasis is put on theories for explicit mathemat ics with universes which are proof-theoretically equivalent to Feferman's T -0. (C) 2001 Elsevier Science B.V. All rights reserved.