Provable wellorderings of formal theories for transfinitely iterated inductive definitions

Publisher Website
Google Scholar
Abstract
By [12] we know that transfinite induction up to ΘεΩN+10 is not provable in IDN, the theory of N-times iterated inductive definitions. In this paper we will show that conversely transfinite induction up to any ordinal less than ΘεΩN+10 is provable in IDNi, the intuitionistic version of IDN, and extend this result to theories for transfinitely iterated inductive definitions.In [14] Schütte proves the wellordering of his notational systems using predicates is wellordered) with Mκ ≔ {x ∈ and 0 ≤ κ ≤ N. Obviously the predicates are definable in IDNi with the defining axioms: where Prog [Mκ, X] means that X is progressive with respect to Mκ, i.e. The crucial point in Schütte's wellordering proof is Lemma 19 [14, p. 130] which can be modified to where TI[Mκ + 1, a] is the scheme of transfinite induction over Mκ + 1 up to a.

This publication has 8 references indexed in Scilit: