2
$\begingroup$

QUESTIONS.

(a) What is the formal system $(\Pi^1_1$-CA)${}+{}$BI?

(b) And what is ID${}_\omega$, the formal theory of $\omega$-times iterated inductive definitions?

They are both mentioned in the following paper without any further explanations:

W. Buchholz, An independence result for $(\Pi^1_1$-CA)+$BI$, Annals of Pure and Applied Logic 33, 131-155, 1987.

I asked this question at math.stackexchange, but no one knows the answer there.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ I couldn't find a freely accessible document defining the $ID_\nu$ systems, so I put a definition on the nLab here. See also the references recorded therein. $\endgroup$
    – Ulrik Buchholtz
    Commented Oct 21, 2016 at 16:57
  • $\begingroup$ Hi Ulrik, thanks for writing that explanation. I left you a question over there at the nLab forum. $\endgroup$
    – Gabriel Nivasch
    Commented Oct 25, 2016 at 3:39

1 Answer 1

Reset to default
2
$\begingroup$

BI = Bar Induction.

See https://www.jstor.org/stable/2270902 for the abbreviation

and

https://en.wikipedia.org/wiki/Bar_induction for the definition.

Improve this answer
$\endgroup$
1
  • $\begingroup$ This, together with Ulrik's writeup on ID_nu systems that he mentions in his comment, answers my question. $\endgroup$
    – Gabriel Nivasch
    Commented Oct 27, 2016 at 13:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .