PROOF-THEORETIC STRENGTHS OF WEAK THEORIES FOR POSITIVE INDUCTIVE DEFINITIONS
Keyword(s):
AbstractIn this article the lightface ${\rm{\Pi }}_1^1$-Comprehension axiom is shown to be proof-theoretically strong even over ${\rm{RCA}}_0^{\rm{*}}$, and we calibrate the proof-theoretic ordinals of weak fragments of the theory ${\rm{I}}{{\rm{D}}_1}$ of positive inductive definitions over natural numbers. Conjunctions of negative and positive formulas in the transfinite induction axiom of ${\rm{I}}{{\rm{D}}_1}$ are shown to be weak, and disjunctions are strong. Thus we draw a boundary line between predicatively reducible and impredicative fragments of ${\rm{I}}{{\rm{D}}_1}$.
Keyword(s):
1975 ◽
Vol 20
(3)
◽
pp. 301-304
1970 ◽
Vol 22
(5)
◽
pp. 1082-1096
◽
Keyword(s):
1976 ◽
Vol 41
(1)
◽
pp. 188-198
◽
Keyword(s):