SYSTEMS OF EXPLICIT MATHEMATICS WITH NONCONSTRUCTIVE MU-OPERATOR .1

Authors
FEFERMAN S JAGER G
Citation
S. Feferman et G. Jager, SYSTEMS OF EXPLICIT MATHEMATICS WITH NONCONSTRUCTIVE MU-OPERATOR .1, Annals of pure and applied Logic, 65(3), 1993, pp. 243-263
Citations number
20
Categorie Soggetti
Mathematics, Pure",Mathematics,Mathematics,Mathematics
Journal title
Annals of pure and applied Logic → ACNP
ISSN journal
01680072
Volume
65
Issue
3
Year of publication
1993
Pages
243 - 263
Database
ISI
SICI code
0168-0072(1993)65:3<243:SOEMWN>2.0.ZU;2-9
Abstract
This paper is mainly concerned with the proof-theoretic analysis of sy stems of explicit mathematics with a non-constructive minimum operator . We start off from a basic theory BON of operators and numbers and ad d some principles of set and formula induction on the natural numbers as well as axioms for mu. The principal results then state: (i) BON(mu ) plus set induction is proof-theoretically equivalent to Peano arithm etic PA; (ii) BON(mu) plus formula induction is proof-theoretically eq uivalent to the system (IIinfinity0-CA)(<epsilon 0) of second-order ar ithmetic.