No label defined (Q4934566)

In proof theory, most approaches to develop stronger notation systems for ordinals beyond the Bachmann-Howard ordinal use cardinals to denote small ordinals. Thus denotations for ordinals may be built up from denotations denoting larger ordinals: The term may be smaller in the resulting ordering than some of its subterms (components). In the paper under review the author extends his previous approach [in G. Sambin et al. (eds.), Twenty-five years of constructive type theory, Oxf. Logic Guides 36, 245-263 (1998; Zbl 0930.03092)] where he defines ordinal systems ``from below''. He explores three types of (iterated) ordinal systems: ordinal systems, \(n\)-ordinal systems, and \(\sigma\)-ordinal systems, and presents what he calls an intuitive well-ordering proof. After this he gives constructive well-ordering proofs, which can be formalized in constructive theories. The main idea is to equip a notation system with a termination ordering \(\prec'\) which satisfies \[ s\prec t \rightarrow s \preceq k(t) \vee s\prec't: \] ``if \(s\) is smaller than \(t\), then \(s\) is smaller than one of the components \(k(t)\) of \(t\) or \(s\) must have been introduced before \(t\) with respect to the termination ordering \(\prec'\)''. An ordinal system OS on a set \(T\) of terms additionally satisfies the conditions that the components of a term are smaller than the term, have a shorter length (which is a natural number) and, if a set of terms \(A\) is well-ordered, then the set of terms \(T \upharpoonright A\), which can be built using components from \(A\), is well-ordered with respect to the termination ordering \(\prec'\). An ordinal system is \textsl{elementary} if all sets and functions that appear are provably primitive recursive in PRA. A well-ordering proof for this kind of notation systems can be carried out in \(KP\omega\), and the given constructive well-ordering proof can be formulated in intuitionistic \(ID_1\) or in type theory ``having the accessible part or one unnested W-type''. Since all these theories have Bachmann-Howard as their proof-theoretic ordinal, it follows that the order type of elementary ordinal systems is less than the Bachmann-Howard ordinal. In order to show that this bound is sharp, and to compare his approach with other ones, Setzer defines the notion of ordinal function generators. The example of the extended Schütte Klammer symbols exhausts the strength of this concept. It is not difficult to extend this concept to \(n\)-times iterated ordinal systems (\(n\)-ordinal systems) which are essentially families of \(n\) ordinal systems, where a term may have components from one of the other ordinal systems. It is shown that this concept has the strength of \(|ID_n|\) or \(|KP\omega\) \(+\) ``there are \(n-1\) admissible sets \(x_1 \in \ldots \in x_{n-1}\text{''}|\). The transition from \(n\) to a transfinite ordinal \(\sigma\) is more tedious. Here the key idea is to introduce a level function. It is shown that the supremum of the strength of \(\sigma\)-OS is \(|ID_\sigma|\). Originally the author's motivation for his work was a pedagogical one. He realized a lot of difficulties in the audience, teaching denotation systems above the Bachmann-Howard ordinal, whereas he had the impression that he succeeded in teaching typical ordinal denotation systems below Bachmann-Howard like the Schütte Klammer symbols. Looking closer to the problem, he found that behind the pedagogical problems the real problem was on foundations and the notion of ``natural well-ordering''. He suggests to replace the notion ``natural well-ordering'' by ``ordering with an intuitive well-ordering proof''. Thus he seems to replace one unprecise notion by another one. But closer inspection shows that the concept of intuitive well-ordering proof is less vague than that of natural well-ordering. A technical advantage of Setzer's approach is that the well-ordering proofs become easier and we get simultanously well-ordering proofs in the formal theories considered for a complete family of notation systems. Further the proofs focus on the structural properties crucial for achieving that strength. For the entire collection see [Zbl 0919.00040].