English

Proof-theoretic strengths of weak theories for positive inductive definitions

Logic 2018-02-21 v7

Abstract

In this paper the lightface Π11\Pi^{1}_{1}-Comprehension axiom is shown to be proof-theoretically strong even over \mboxRCA0\mbox{RCA}_{0}^{*}, and we calibrate the proof-theoretic ordinals of weak fragments of the theory \mboxID1\mbox{ID}_{1} of positive inductive definitions over natural numbers. Conjunctions of negative and positive formulas in the transfinite induction axiom of \mboxID1\mbox{ID}_{1} are shown to be weak, and disjunctions are strong. Thus we draw a boundary line between predicatively reducible and impredicative fragments of \mboxID1\mbox{ID}_{1}.

Keywords

Cite

@article{arxiv.1603.01342,
  title  = {Proof-theoretic strengths of weak theories for positive inductive definitions},
  author = {Toshiyasu Arai},
  journal= {arXiv preprint arXiv:1603.01342},
  year   = {2018}
}