\documentclass[10pt]{article} \usepackage{amsfonts} \usepackage{amsmath} \usepackage{amssymb} \usepackage{dina4} \usepackage{pictex} % Here are the formatting declarations as required by CUP \usepackage{fancyheadings} \setlength{\headrulewidth}{0pt} \lhead[\textnormal\thepage]{} \rhead[]{\textnormal\thepage} \chead[\textit{The Author}]% {\textit{Ordinal Systems}} \lfoot{}\cfoot{}\rfoot{} \addtolength{\headheight}{2.5pt} \setlength{\textheight}{215mm} \setlength{\textwidth}{138mm} \setlength{\parskip}{0pt} \setlength{\parindent}{16pt} \pagestyle{fancy} % % % \bibliographystyle{/opt/tex/lib/tex/macros/alpha} % % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % Verwaltungsmakros % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % \def\j#1#2{\setcounter{section}{#2}\input{#1}} \def\n#1#2{{ }} % % %%%%% \laprint is \label and defines \actlabel to be %%%%% pointing to the label introduced %%%%% allows to use \refact{a} for \ref{\actlabel{newlabelused}} %%%% to refer to part a), b), c) ... of a Lemma % % % \laprint erzeugt ein Label, und notiert erzeugt ein % commando \sublabel das ein label aus dem Hauptlabel und % dem jeweiligen Label erzeugt (\laprint {label}) \begin{enumerate} % \item\sublabel{c} erzeugt dann ein Label {labelc} % das auch ein macro \myreflabelc erzeugt das zu a expandiert % % Mit \subref{labelc} wird dann (a) erzeugt, mit % \subrefcom{label}{c} die Nummer des Lemmas + (a) % Beispiel f\"ur die Anwendung % % %\begin{lemma} %\laprint{lemma1rhd} %\begin{enumerate} %\item\sublabel{a}Text %\item\sublabel{b}Text %\end{enumerate} %\end{lemma} %\begin{lemma} %\laprint{ee} %\begin{enumerate} %\subitem a Text2 %\subitem {b} Text2 %\end{enumerate} %\end{lemma} %Text: \ref{lemma1rhda} \par %Lemma \ref{lemma1rhdb}, \ref{eea}, \ref{eeb}, Lemma % % % \def \laprint#1{{ \label {#1}} \expandafter \global \def \actlabel{#1}} \def \ssubitem#1{\item \label{\actlabel#1} } %creates a labeled item % the label is composed of % the label of the lemma % and the parameter \def \refsub#1#2{\ref{#1#2}} % forms the subitems of a %Lemma like (a), (b) \def \refact#1{\ref{\actlabel#1}} %like \refsub but %refers to the last defined %lemma so %\refact b means (b) % if in the last lemma % subitem b was the second \def \refcom#1#2{\ref{#1}\ \ref{#1#2}}% forms the subitems % together with the number of the % Lemma like 1.2 (a), 1.3 (b) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % Gr"o"sere Macros % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \def \fornum#1#2{{\renewcommand{\theequation}{#2}% \begin{equation} #1 \end{equation}% \renewcommand{\theequation}{\arabic{equation}}}} %%%%%%%%%%%%%%%%%%%% Macht Formeln mit eigener Nummerierung %%%%%%%%%%%%%%%%%%%% Bsp \fornum{a+b=c}\ast \def \fornumeqnarray#1#2{{\renewcommand{\theequation}{#2} \begin{eqnarray} #1 \end{eqnarray} \renewcommand{\theequation}{\arabic{equation}}}} %%%%%%%%%%%%% fornumeqnarray wie fornum, nur mit eqnarray % % % \def\mycases#1{\begin{cases}#1\end{cases}} \def\picture#1{\bigskip \bigskip \bigskip \bigskip \par \centerline{!!!! Bild wurde hier ausgelassen} \bigskip \bigskip \bigskip \bigskip\par } %\def\picture#1{\noindent\input{#1}\par} % % % % %%%%% Boxes % % % \def\condition#1{\indent \hbox to 2.0cm{$(#1)$\hfill}} \def\conditionbox#1{\indent \hbox to 2.0cm{#1\hfill}} % % %%%% Environments % % % \newtheorem {lemma}{Lemma} [section] \newtheorem {definition} [lemma]{Definition} \newtheorem {deflemma} [lemma]{Definition and Lemma} \newtheorem {lemdef} [lemma]{Lemma and Definition} \newtheorem {corollary} [lemma]{Corollary} \newtheorem {theorem} [lemma]{Theorem} \newtheorem {remark} [lemma] {Remark} \newtheorem {notation}[lemma]{Notation} \newtheorem {assumption}[lemma]{Assumption} \newtheorem {example}[lemma]{Example} %\newtheorem{assumption}[theorem]{Assumption}{\bfseries}{\rm} %\newtheorem{deflemma}[theorem]{Assumption}{\bfseries}{\rm} %\newtheorem{notation}[theorem]{Assumption}{\bfseries}{\rm} % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % To allow enumerate in the form (a) % % erm\"oglichen % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % \renewcommand{\labelenumi}{(\alph{enumi})} \renewcommand{\theenumi}{(\alph{enumi})} % % % % %%%% Connectives and similar mathematical symbols %%%% General ones % % % \def\Andd{\bigwedge} \def \prove{\vdash} \def\all{\forall} \def\ar{\rightarrow} \def\longar{\longrightarrow} \def \Ar{\Rightarrow} \def \iff{\leftrightarrow} \def \Iff{\Leftrightarrow} \def \cross{\times} %%% calligraphic \def \powset {{\mathcal P}} %%%%% Potenzmenge \def \calA{{\mathcal A}} \def \calL{{\mathcal L}} \def \calC{{\mathcal C}} \def \calO{{\mathcal O}} \def \calS{{\mathcal S}} \def \calW{{\mathcal W}} % % % % % %%%% Special symbols % % \def\qedsquare{\hbox{\rlap{$\sqcap$}$\sqcup$}} \def\QED{\relax\ifmmode\hskip2em \Box\else\unskip\nobreak\hskip1em $\qedsquare$\fi} % % % %%%%% Natural numbers % % \def\nat{\mathbb{N}} \def\nathat{\widehat{\mathbb{N}}} \def\length{\mathrm{length}} \def\lengthvec{\vec{\mathrm{length}}} \def\seqlength{\mathrm{seqlength}} \def\seq#1{\mathopen{<}#1\mathclose{>}} % % %%%% Other basic data structures % % % \def\potsetfin{{\mathcal{P}^\mathrm{fin}}} \def\potset{{\mathcal{P}}} % % % %%%% Ordinal systems % % % \def\Arg{\mathrm{Arg}} \def\k{\mathrm{k}} \def\lrm{\mathrm{l}} \def\krmhat{\widehat{\mathrm{k}}} \def\krmhattil{\widehat{\widetilde{\mathrm{k}}}} \def\lrmhat{\widehat{\mathrm{l}}} \def\Lhat{\widehat{\mathrm{L}}} \def\krmtil{\widetilde{\mathrm{k}}} \def\krmcheck{\check{\mathrm{k}}} \def\krmvec{\vec{\mathrm{k}}} \def\OS{{\mathrm{OS}}} \def\Cl{{\mathcal{C}l}} \def\lex{\mathrm{lex}} \def\des{\mathrm{des}} \def\weakdes{\mathrm{weakdes}} \def\alle{\mathrm{all}} \def\Mbb{\mathbb{M}} \def\calGvec{\vec{\mathcal G}} \def\calFvec{\vec{\mathcal F}} \def\eval{\mathrm{eval}} \def\plusbar{\underline{+}} \def\alphabar{\underline{\alpha}} \def\cdotbar{\underline{\cdot}} \def\omegabar{{\underline{\omega}}} \def\phibar{{\underline{\varphi}}} \def\psibar{{\underline{\psi}}} \def\thetabar{{\underline{\theta}}} \def\schuette{\mathrm{Sch\ddot{u}tte}} \def\APN{\mathbb{A}} \def\CNF{\mathrm{CNF}} \def\wrm{\mathrm{w}} \def\zero{\mathrm{zero}} \def\lesstil{\widetilde{<}} \def\leqtil{\widetilde{\leq}} \def\lengthhat{\widehat{\mathrm{length}}} \def\levelhat{\widehat{\mathrm{level}}} % %%%% Orderings % % % %%%%\def\preccirc{\mathrel{\bigcirc \kern-15.5pt \prec}} %% works for 12pt \def\preccirc{\mathrel{\bigcirc \kern-12pt \prec}} %% works for 10pt % %%%% Ordinal notations % \def\C{\mathrm{C}} \def\NF{\mathrm{NF}} \def\T{\mathrm{T}} \def\OT{\mathrm{OT}} \def\calOT{{\mathcal{OT}}} \def\Ord{\mathrm{Ord}} \def\TI{\mathrm{TI}} \def\Acc{\mathrm{Acc}} \def\ordinal{{\mathrm{o}}} \def\M{\mathrm{M}} \def\Succ{\mathrm{S}} \def\L{\mathrm{L}} \def\Lvec{\vec{\mathrm{L}}} \def\level{\mathrm{level}} \def\levelvec{\vec{\mathrm{level}}} \def\B{\mathrm{B}} \def\I{\mathrm{I}} \def \segment{\sqsubseteq} \def \Ag{\mathrm{Ag}} \def\Car{\mathrm{Car}} \def\p{\mathrm{p}} \def\S{\mathrm{S}} \def\Sigmabar{\underline{\Sigma}} % % % %%%% Theories % % \def\PRA{\mathrm{PRA}} \def\ID{\mathrm{ID}} \def\BI{\mathrm{BI}} \def\CA{\mathrm{CA}} \def\KPI{\mathrm{KPI}} \def\kpomega{\mathrm{KP\omega}} \def\HA{\mathrm{HA}} % %%%% tilde % % % \def \atil{{\widetilde {a}}} \def \btil{{\widetilde {b}}} \def \ctil{{\widetilde {c}}} \def \dtil{{\widetilde {d}}} \def \itil{{\widetilde {i}}} \def \xtil{{\widetilde {x}}} \def \ytil{{\widetilde {y}}} \def \ztil{{\widetilde {z}}} % % Some objects in \rm % % \def\Below{\mathrm{Below}} % % % % caligraphic % % \def\calF{\mathcal{F}} \def\calG{\mathcal{G}} % % % % vector % % \def \avec{{\vec a}} \def \bvec{{\vec b}} \def \cvec{{\vec c}} \def \svec{{\vec s}} \def \tvec{{\vec t}} \def \xvec{{\vec x}} \def \yvec{{\vec y}} \def \zvec{{\vec z}} \def \Avec{{\vec A}} \def \Bvec{{\vec B}} \def \Cvec{{\vec C}} \def \Dvec{{\vec D}} \def \Evec{{\vec E}} \def\gammavec{{\vec \gamma}} % % %%%%% \mathrm \def\ck{\mathrm{ck}} \def\rec{\mathrm{rec}} % % \def\underlinedef#1{{\it #1}} % % % % % % \begin{document} \title{Ordinal Systems} \author{Anton Setzer \thanks{Department of Mathematics, Uppsala University, P.O. Box 480, S-751 06 Uppsala, Sweden, email: {\tt setzer@math.uu.se}}} \maketitle \begin{abstract} Ordinal systems are structures for describing ordinal notation systems, which extend the more predicative approaches to ordinal notation systems, like the Cantor normal form, the Veblen function and the Sch{\"u}tte Klammer symbols, up to the Bachmann-Howard ordinal. $\sigma$-ordinal systems, which are natural extensions of this approach, reach without the use of cardinals the strength of the theories for transfinitely iterated inductive definitions $\ID_{\sigma}$ in an essentially predicative way. We explore the relationship with the traditional approach to ordinal notation systems via cardinals and determine, using ``extended Sch{\"u}tte Klammer symbols'', the exact strength of $\sigma$-ordinal systems. \end{abstract} \begin{tabbing} \cite{buchholzanewsys}\cite{buchholzschuettebook} \cite{buchholzasimplified}\cite{pohlersbook}\cite{rathjenweiermann} \cite{schuettebook}\cite{Schuette54}\cite{seisenbdipl} \cite{setz93}\cite{setz95a}\cite{setzvenedig}\cite{girardinductivepub} \cite{girardpionepartone} \cite{girardbooktwo}\kill \end{tabbing} \setcounter{section}{0} \section{Introduction} \laprint{sectintro} \subsection{Motivation} The original problem, which motivated the research in this article, seemed to be a {\em pedagogical} one. We have been trying to teach ordinal notation systems above the Bachmann-Howard ordinal several times. The impression we had was that we were able to teach the technical development of these ordinal notation systems, but there always remained some doubts in the audience. It remained unclear, why one could get a well-ordered notation system by denoting small ordinals by big cardinals.\par %The audience was able to understand %the formal verification, but this formal proof was not satisfactory. %And we had these problems not only when teaching others but we felt ourselves %uncomfortable as well.\par The situation was completely different with typical ordinal notation systems below the Bachmann-Howard ordinal. We had the impression we always succeeded in teaching it after the audience had overcome some technical problems. And this included the Sch{\"u}tte Klammer symbols (an ordinal notation system extending the Veblen hierarchy --- they will essentially be defined in this article): Although they are technically more complicated than the systems using one uncountable cardinal, they seem to be far more acceptable. Therefore the reason behind our pedagogical problems was not a technical one. The real problem was about {\em foundations}.\par The original task of proof theory as understood by Hilbert was to show the consistency of systems in which mathematical reasoning can be formalized. After the proof of G{\"o}del's incompleteness theorem, one had to modify this and demand the reduction of the consistency of a theory to some principles, for which we have good reasons to believe that they are correct. One reason, why Gentzen's result was so much appreciated, when it was presented, was that he reduced the consistency of Peano Arithmetic to the principle of well-ordering up to $\epsilon_0$, of which we believe intuitively that it is correct. The argument presented in Lemma \ref{lemintuitos} is an attempt to formalize what we believe is the reason for our confidence with this principle: the usual notation system for $\epsilon_0$ is built from below and has therefore an intuitive well-ordering proof.\par For the Veblen function and for the Sch{\"u}tte Klammer symbols the same holds. So, when analyzing a theory using these systems we have really gained more than only the reduction of the consistency of theory to a primitive recursive well-ordering: the reduction to the well-foundedness of an ordering, of which we intuitively believe that it is correct.\par This leads to another aspect: the relationship to the notion of ``natural well-ordering''. There exists a trivial ordinal analysis for any consistent theory. Take as elements of a well-ordering essentially pairs consisting of a well-ordering proof in the theory and elements of the corresponding well-ordering and order them lexicographically by the G{\"o}del-number of the proof and the ordering we are referring to. (A slight refinement is necessary in order to make it primitive recursive: replace the elements of the well-ordering by triples $\seq{a,b,c}$ where $a$ is an element of the well-ordering, $b$ a calculation that determines that $a$ is an element of this ordering and $c$ is a calculation that determines for all $x_B \cdots >_B b_m \} $. Note that we have reversed the order relative to \cite{Schuette54}. Further we define $\schuette(A,B) $\\ $:=((A ,B))_\des \cap \{(a_1,b_1 ,\ldots, a_m,b_m)\mid m \in \omega, a_i \in A, b_i \in B, a_1 >_A \cdots >_A a_m \} $. Both are elementary constructions from $A$, $B$. \ssubitem e If $A_1 ,\ldots, A_m$ are orderings and $|A_i|$ are disjoint, then $B:= $\underlinedef{$A_1 \preccirc A_2 \preccirc \cdots \preccirc A_m$} is the ordering with $|B|$ being the union of the $A_i$ and $\prec_B$ being the union of the $\prec_{A_i}$ together with the pairs $(a,b)$ for $a \in |A_i|$, $b \in |A_j|$, $1 \leq i < j \leq n$. This is an elementary construction from the orderings $A_i$. \ssubitem f We identify the one element set $A$ with the ordering $(A,\emptyset)$. \ssubitem g If $A$ is an ordering, $B$ a set, let $A \cap B := (|A| \cap B,\prec_A \cap ((|A|\cap B) \cross (|A|\cap B)))$ and $A \setminus B:= A \cap (|A| \setminus B)$. Note that this is an elementary construction from $A$, if $B$ is primitive recursive. \ssubitem h If $A$ is an ordering, let $\Acc(A)$ be the accessible part of $|A|$ with respect to $\prec_A$, i.e. the largest well-founded part of $A$, $\bigcup \{ X \subseteq |A| \mid (X,\prec)$ well-ordered $\} $. $\Acc_\prec(B):= \Acc(B,\prec)$. \ssubitem i If $A$ is an ordering, $a,b \in |A|$, $B \subseteq |A|$, let $B \cap a:= \{ c \in B \mid c \prec_A a \} $, and $[a,b]:= \{ c \in |A| \mid a \preceq_A c \preceq_A b \}$. The half open and open intervals $[a,b[$, $]a,b]$ and $]a,b[$ are defined similarly. Again we obtain elementary constructions from $A$, if $B$ is primitive recursive. \ssubitem j If $A$ is an ordering, $B,C \subseteq |A|$, then $B \segment C$ ({\em $B$ is an initial segment of $C$}) $:\Iff B \subseteq C \land \all x \in B. B \cap x = C \cap x$. \ssubitem k $\Ord$ is the class of ordinals, $\APN$ the class of additive principal numbers $>0$.\\ We identify classes of ordinals $A$ with the ordering $(A,<)$, where $<$ is the usual ordering on $\Ord$. \end{enumerate} } \end{definition} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% %% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% %\begin{definition}{\rm %\laprint{notations} %\begin{enumerate} %\ssubitem a %If $A$ is a set, let %\underlinedef{$A^\ast$} be the set of finite (possible empty) %sequences of elements of $A$ %coded, if $A \subseteq \nat$ %as natural numbers such that the usual properties, especially %primitive recursiveness hold.\\ %\underlinedef{$\seqlength(\avec)$} %is the length of an element of $\avec$, \underlinedef{$(\avec)_i$} the %$i$-th element of $\avec$.\\ %An extension $\PRA^+$ of $\PRA$ by \underlinedef{free predicate} is the %result of adding new predicates to the language and logic %of $\PRA$ without adding induction over formulas involving such %predicates.\\ %An \underlinedef{ordering} is a pair $(A, \prec)$ where $A$ is a %set and $\prec$ is a binary relation on $A$. It is %\underlinedef{primitive recursive}, if $A$ is a primitive %recursive subset of $\nat$ and $\prec$ is primitive recursive, %and \underlinedef{linear} %if $\prec$ is a linear ordering on $A$.\\ %If $A = (B, \prec)$, %then \underlinedef{$|A|$}$:= B$, %\underlinedef{$\prec_A$}$:= \prec$. %If $C \subseteq |A|$, %we will write $(C,\prec)$ instead of $(C, \prec \cap (B \cross B))$.\\ %\underlinedef{$\TI_{(A,\prec)}$} is transfinite %induction over the linear ordering $(A,\prec)$, %\underlinedef{$\TI_{(A,\prec)}(\phi(x))$} the special instance of it %for the formula $\phi$ (with respect to the variable $x$.\\ %Transfinite induction over $(B,\prec)$ is $\PRA$-reducible to %transfinite induction over $(A_i,\prec_i)$ ($i=1 ,\ldots, n$), %if in an extension $\PRA^+$ %of $\PRA$ by a free predicate $R$ %if there exist formulas $phi_{i,j}(x,\zvec)$ such that %$$\PRA^+ \prove %(\Andd_{i=1}^n \Andd_{j=1}^{n_i} \all \zvec (\TI_{(A_i,\prec_i)}(\phi_{i,j}(x, %\zvec)))) \ar \TI_{(B,\prec)}\enspace .$$ %\ssubitem {ab} If $(B,\prec)$ is an ordering, construced from orderings %$(A_1,\prec_1)$ ,\ldots, $(A_m,\prec_m)$, this is an %\underlinedef{elementary %construction}, if $B,\prec$ is primitive recursive, linear, %linear provable in $\PRA$, provided this property holds for %$(A_i,\prec_i)$ and %if, under the condition that $(A_i,\prec_i)$ are primitive recursive %and linear provably in $\PRA$, transfinite induction over %$(A,\prec)$ reduces to transfinite induciton over $(A_i,\prec_i)$. %\ssubitem b %If $f:A \ar B$, $M \subseteq A$, then %\underlinedef{$f[M]$}$:= \{ f(x) \mid x \in M \} $.\\ %\underlinedef{$\potsetfin(A)$} is %the set of finite sets of elements of $A$ %coded, if $A \subseteq \nat$, %as natural numbers, such that the usual properties, especially %primitive recursiveness, decidable subset-relation hold.\\ %In case $B \in \potsetfin(A)$, we write $t \in B$ for the %statement expressing $t$ is an element of $B$ expressed in %the language of $\PRA$.\\ %If $B \in \potsetfin(A)$, $a \in A$, $\prec$ is %a binary relation of $A$, then %\underlinedef{$B \prec a$}$\Iff \all x \in B.x \prec a$, %\underlinedef{$a \prec B$}$\Iff \exists x \in B.a \prec x$.\\ %If %$\prec$ is a binary relation on $A$, define \underlinedef{$a \preceq b$}$\Iff %a \prec b \lor a = b$, similarly for $\prec '$ etc.\\ %If $k: A \ar \potsetfin(B)$ and $C \subseteq B$, then %\underlinedef{$k^{-1}(C)$}$:= \{ x \in A \mid k(x) \subseteq C \} $.\\ %We write \underlinedef{$f: A \ar_\omega B$} for $f: A \ar \potsetfin(B)$. %If $f: A \ar_\omega B$, $f': A \ar_\omega B$, $g:B \ar_\omega C$, %then \underlinedef{$g \circ f$}$:A \ar_\omega C$, $(g \circ f)(a):= g[f(a)]$, %and $f \subseteq f' \Iff \all x \in A.f(x) \subseteq f'(x)$. %\ssubitem c %If $A_1 ,\ldots, A_m$ are orderings, %$f: (|A_1| \cross \cdots \cross |A_m|) \ar M$, %then $f[A_1 ,\ldots, A_m]$ denotes the ordering %$(f[A_1 ,\ldots, A_m],\prec)$ where %$f(a_1 ,\ldots, a_m) \prec f(b_1 ,\ldots, b_m)$ if %$(a_1 ,\ldots, a_m)$ lexicographically less then %$(b_1 ,\ldots, b_m)$ with respect to the orderings %$A_1 ,\ldots, A_m$. \par %We will use this definition only in case $f(a_1 ,\ldots, a_m) %= t[x_1:= a_1 ,\ldots, x_m:= a_m]$ for some term $t$ %(like $\varphi_xy$, $\psi(x)$, $(x,y,z)$, $x+y$, $x \choose y$) %and will write in this case the result of replacing in $t$ %the variable $x_i$ by $A_i$ instead of $f[A_1 ,\ldots, A_m]$ %(i.e. $\varphi_{A_1}A_2$, $\psi(A_1)$ ,\ldots). %The convention is here that the variables $x_i$ are ordered from %left to right and in case of $x \choose y$ from bottom to top %(i.e. $\varphi_{A_1}A_2$ is ordered by lexicographic ordering %on $(A_1,A_2)$, $A_1 \choose A_2$ by lexicographic ordering %on $(A_2,A_1)$). %Note that, after some standard G{\"o}delization, %the new ordering is an elementary construction from the %orderings $A_i$. %\ssubitem d %If $A$ is an ordering, $A^\ast_\des$ is the set of %(possibly empty) strictly descending sequences of $A$ ordered %lexicographically, which is an elementary construction from $A$. %In case of $({B \choose A})^\ast_\des$, %we write $\left(\begin{array}{ccc}b_1& \cdots& b_m \\ %a_1 &\cdots &a_m \end{array} \right)$ %instead of the element$\left ({b_1 \choose a_1} \cdots {b_m \choose %a_m}\right )$ of this ordering. %\ssubitem e %If $A_1 ,\ldots, A_m$ are orderings and $|A_i|$ are disjoint, then\\ %$B:= $\underlinedef{$A_1 \preccirc A_2 \preccirc \cdots \preccirc A_m$} %is the ordering with %$|B|$ being the union of the $A_i$ and %$\prec_B$ being the union of the $\prec_{A_i}$ %together with the pairs $(a,b)$ for $a \in |A_i|$, $b \in |A_j|$, %$1 \leq i < j \leq n$. %This is again an elementary construction from the orderings %$A_i$. %\ssubitem f We indentify the one element set $A$ with the %ordering $(A,\emptyset)$. %\ssubitem g If $A$ is an ordering, %$B$ a set, let\\ %$A \restriction B %:= (|A| \cap B,\prec_A \cap ((|A|\cap B) \cross (|A|\cap B)))$. %Note again that this is an elementary construction from $A$, %if $B$ is primitive recursive. %\ssubitem h If $A$ is an ordering, let $\Acc(A)$ be the %accessible part of $|A|$ with respect to $\prec_A$, %i.e. the largest well-founded part of $A$, %$\bigcap \{ X \subseteq |A| \mid (X,\prec)$ well-ordered $\} $. %$\Acc_\prec(B):= \Acc(B,\prec)$. %\ssubitem i If $A$ is an ordering, $a,b \in |A|$, %$B \subseteq |A|$, let $B \cap a:= \{ c \in |A| \mid %c \prec_A a \} $, %and $[a,b]:= \{ c \in |A| \mid a \preceq_A c \preceq_A b \}$. %$[a,b[$, $]a,b]$ and $]a,b[$ are defined similarly. %Again we get elementary constructions from $A$, if %$B$ is primitive recursive. %\ssubitem j If $A$ is an ordering, $B,C \subseteq |A|$, then %$B \segment C$ ($B$ is an initial segment of $C$) $:\Iff B \subseteq C \land %\all x \in B. B \cap x = C \cap x$. %\end{enumerate} } %\end{definition} % % %% %The essential definition in \cite{setzvenedig} was now: %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% %% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% %\begin{definition}{\rm %\laprint{defordfrombelow} %Let $\T$ be a subset of the natural numbers, %$\NF$ be a subset of $\T^\ast$, the set of finite sequences of elements in %$\T$, $\prec$, $\prec'$ be binary relations on %$\T$ and $\NF$, respectively and $f:\NF \ar \T$ injective %such that $\T$ is the closure under $f$, i.e. %the least set $M$ such that if $\avec \in \NF \cap M^\ast$, then %$f(\avec) \in M$. %Assume that $\T$, $\prec$, $\NF$, $\prec '$ %and $f$ are primitive recursive, and that %$\PRA$ proves, that $\prec$ is linear and %$\T$ is the closure under $f$ (i.e. the corresponding induction principle %can be proved for all formulas in extensions of $\PRA^+$ by %free predicates. %Then $(\T,\prec, \NF,\prec',f)$ %is an \underlinedef{ordinal notation system from below}, iff the %following holds:\\ %% %% %% %\condition{\Below\ 1} %${\PRA} \prove \all \avec \in \NF.\all i < \seqlength(\avec). %(\avec)_i \prec f(\avec)$.\\ %% %% %\condition{\Below\ 2} %${\PRA} \prove \all \avec \in \NF.\forall b \in \T. %b \prec f(\avec) \ar \exists i < \seqlength(\avec).$\\ %\conditionbox{}$b \preceq \avec_i \lor %\exists \cvec \prec ' \avec .b = f(\cvec)$.\\ %% %% %% %\condition{\Below\ 3} %$\TI_{(\NF\cap R^\ast,\prec')}$ is %$\PRA$-reducible to $\TI_{(\T \cap R,\prec)}$ for %a unary\\ %\conditionbox{} free predicate $R$.} %% %% %% %% %% %\end{definition} % % % %The intuition was that notations for ordinals refer only to smaller %ordinals (Below 1), that if we introduce a new ordinal, all %ordinals are introduced previously, i.e. they are either below one %of the ordinals from which the new ordinal is defined %($b \preceq a_i$) or it is smaller with respect to the %ordering $\prec '$, which determines the order in which new ordinals %are introduced. $\prec '$ should be always a well-ordering for the %set of ordinals we can built from the ones which were %already introduced, and this reduction was supposed to be provable %in an elementary way, which is expressed by condition (Below 3). %In all the examples we needed only a combination of %lexicographic ordering on pairs, lexicographic ordering on descending %sequences, selection of subsets of orderings and renaming, in %order to introduce $\prec$ from $\prec '$, which guaranteed %property (Below). We will give examples after having revised the %definition slightly.\par % % % \section{Elementary Ordinal Systems} \laprint{sectelem} % % \subsection{Definition of Ordinal Systems} We will in the following develop first the notation of ordinal systems from that of ordinal notation systems from below as defined in the first four chapters of \cite{setzvenedig}. However, it is not necessary to read this article, since for the reader who doesn't know the previous approach we will then repeat the motivation given there, adapted to the new setting.\par In \cite{setzvenedig}, the underlying structure of ordinal notation systems from below consisted of the set of notations $\T$, a subset $\NF$ of $\T^\ast$, linear orderings $\prec$ on $\T$ and $\prec '$ on $\NF$ and a function $f: \NF \ar \T$. In order to deal with stronger systems, which extend the notion of ordinal notation system from below and allow to define ordinals beyond the Bachmann-Howard ordinal, one needs to deal with arguments that have more structure. Even in the case of ordinals below the Bachmann-Howard ordinal some more structure on the argument is needed. For instance in case of extended Sch{\"u}tte Klammer symbols (in English: ``parenthesis symbols'' or better ``matrix symbols''), which will be defined in Example \refcom{exmplordfun}i below, we need the information about the size of each of the sub-matrices and which ordinal notations belong to which sub-matrix. We could handle this by using some coding (see Subsection \ref{equivonsfb}). However, the more elegant approach is to replace the set $\NF \subseteq \T^\ast$ by an arbitrary set $\Arg$ together with a function $\k: \Arg \ar_\omega \T$. The intuition is, that $a \in \Arg$ is an argument for the function $f$ which is built from ordinal notations $\k(a)$, but has some additional structural information. An ordinal notation system from below can be translated into the new structure by defining $\Arg:= \NF$ and $\k(a_1 ,\ldots, a_m):= \{ a_1 ,\ldots, a_m \}$.\par Now $f$ was always a bijection, and therefore we can identify $\Arg$ with $\T$, define $f:= \lambda x.x$ and omit $f$ completely. We have therefore two orderings on $\T$, $\prec$ and $\prec '$, $\prec$ being the ordering on the ordinal notation system and $\prec '$ being the ordering which determines the order, in which new ordinal notations are introduced.\par In order to express that $\T$ is the closure under the above process, we add a function $\length: \T \ar \nat$ and require $\length(a) < \length(b)$ for $a \in \k(b)$. We replace the long name ``ordinal notation system from below'' by ``ordinal system''.\par The motivation for the resulting structure is now as follows: Ordinal notations $t$ are built from a finite set of notations $\k(t)$. We want that the system is built from below: First, an ordinal should be denoted using smaller ones, i.e. $\k(t) \prec t$. Second, whenever we introduce a new notation $t$, we want to have constructed all smaller notations $s$ before $t$. Either $s$ could be below one of the components of $t$, i. e. $s \preceq \k(t)$, since, whenever we introduce an ordinal, we assume that we have constructed its components and therefore all ordinals below them as well. Or $s$ must have been introduced before $t$ with respect to the termination ordering $\prec'$, i. e. $s \prec ' t$. In \cite{setzvenedig} we showed that in case of simple systems like the standard system up to $\Gamma_0$ or the Sch{\"u}tte Klammer symbols, we can construct $\prec'$ from $\prec$ by using the lexicographic ordering on pairs and on strictly descending sequences together with some simple operations. For instance we ordered terms for the Cantor normal form by the lexicographic ordering on strictly descending sequences and terms $\varphi_ab$ by the lexicographic ordering on pairs $(a,b)$. Orderings $\prec'$ constructed like this have the property that, whenever a set of notations is $\prec$-well-ordered, the set of notations built from it is $\prec'$-well-ordered, and in the definition of ordinal systems we will demand this condition. However, in the above examples it is possible to show this reduction in $\PRA$, i.e. essentially in logic, and we define elementary ordinal systems by demanding additionally this stronger requirement. Elementary ordinal systems will have strength below the Bachmann-Howard ordinal, whereas with ordinal systems we will have no upper bound (choose for an arbitrary well-ordering $(\T,\prec)$, $\k(a) := \emptyset$, $\length(a):= 0$, $\prec':= \prec$). % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{definition}{\rm \laprint{defordinalsystem} \begin{enumerate} \ssubitem a An \underlinedef{Ordinal System Structure}, in short \underlinedef{OS-structure}, is a quintuple $\calF = (\T, \prec,\prec',\k,\length)$ where $\T$ is a set, $\prec '$, $\prec$ are linear orderings on $\T$, $\k:\T \ar_\omega \T$ and $\length: \T \ar \nat$.\\ We will sometimes regard the first two or three elements of this quintuple as a unity, so when writing $\calF$ is an OS-structure of the form $\calF=(A,\prec',\k,\length)$ or $(\calG,\k,\length)$ we mean that $A$ is of the form $(\T,\prec)$ and $\calG$ is of the form $(\T,\prec,\prec ')$ with $\T$, $\prec$ and $\prec '$ as above. \ssubitem b In the following, if not mentioned otherwise, let $\calF$ be as in \refact a, and for any index $i$ $\calF_i = (\T_i,\prec_i,\prec'_i,\k_i,\length_i)$. \ssubitem {ba} If $\calF$ is an ordinal system structure as above, $A,B \subseteq \T$, then $B \restriction A := B \cap \k^{-1}(A)$, the {\it restriction of $B$ to arguments built from $A$} or shorter {\it restriction of $B$ to $A$}. \ssubitem c An \underlinedef{Ordinal System}, in short \underlinedef{OS}, is an OS-structure $\calF$, such that the following holds:\\ \condition{\OS\ 1} $\all t \in \T.\k(t) \prec t$.\\ \condition{\OS\ 2} $\length[\k(t)] < \length(t)$.\\ \condition{\OS\ 3} $\all t \in \T.\all s \in \T (s \prec t \ar (s \preceq \k(t) \lor s \prec ' t))$.\\ \condition{\OS\ 4} If $A \subseteq \T$, $A$ is $\prec$-well-ordered, then $\T \restriction A$ is $\prec'$-well-ordered. \ssubitem e An OS $\calF$ is \underlinedef{primitive recursively represented}, if $\T$ is a primitive recursive subset of $\nat$, $\prec$, $\prec '$, $\k$, $\length$ are primitive recursive, and all the properties of an OS, including linearity of $\prec$, $\prec '$, but except of (OS\ 4), can be shown in $\PRA$.\par \ssubitem f A primitive recursively represented OS $\calF$ is \underlinedef{elementary}, if additionally $(\OS\ 4)$ can be shown in $\PRA$, i.e. for a free predicate $R$ $\TI_{(\T \restriction R,\prec ')}$ is $\PRA$-reducible to $\TI_{(\T \cap R,\prec)}$. \ssubitem g An OS-structure is \underlinedef{well-ordered}, if $\T$ is well-ordered. The \underlinedef{order type} of a well-ordered OS-structure $\calF$ is the order type of $\T$. \ssubitem h Two OS-structures are isomorphic, if there exists a bijection between the underlying sets, which respects $\prec$, $\prec'$, $\k$, $\length$. \end{enumerate}} \end{definition} We illustrate an ordinal system by the following picture:\\ %%% begin pic3.pictex %% pic3.fig \font\thinlinefont=cmr5 % \begingroup\makeatletter\ifx\SetFigFont\undefined % extract first six characters in \fmtname \def\x#1#2#3#4#5#6#7\relax{\def\x{#1#2#3#4#5#6}}% \expandafter\x\fmtname xxxxxx\relax \def\y{splain}% \ifx\x\y % LaTeX or SliTeX? \gdef\SetFigFont#1#2#3{% \ifnum #1<17\tiny\else \ifnum #1<20\small\else \ifnum #1<24\normalsize\else \ifnum #1<29\large\else \ifnum #1<34\Large\else \ifnum #1<41\LARGE\else \huge\fi\fi\fi\fi\fi\fi \csname #3\endcsname}% \else \gdef\SetFigFont#1#2#3{\begingroup \count@#1\relax \ifnum 25<\count@\count@25\fi \def\x{\endgroup\@setsize\SetFigFont{#2pt}}% \expandafter\x \csname \romannumeral\the\count@ pt\expandafter\endcsname \csname @\romannumeral\the\count@ pt\endcsname \csname #3\endcsname}% \fi \fi\endgroup \mbox{\beginpicture \setcoordinatesystem units <1.00000cm,1.00000cm> \unitlength=1.00000cm \linethickness=1pt \setplotsymbol ({\makebox(0,0)[l]{\tencirc\symbol{'160}}}) \setshadesymbol ({\thinlinefont .}) \setlinear % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 3.553 21.288 3.334 21.431 3.460 21.202 / % \circulararc 39.308 degrees from 3.810 20.320 center at 2.016 20.209 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 2.795 22.006 2.540 22.066 2.736 21.893 / % \circulararc 22.620 degrees from 3.334 21.431 center at 1.349 19.764 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 4.353 21.984 4.604 21.907 4.419 22.093 / % \circulararc 53.130 degrees from 4.604 21.907 center at 3.413 19.923 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 5.629 20.567 5.715 20.320 5.756 20.579 / % \circulararc 59.863 degrees from 5.715 20.320 center at 3.781 20.149 % % Fig POLYLINE object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) \putrule from 2.540 23.530 to 2.540 20.320 \putrule from 2.540 20.320 to 6.350 20.320 \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % Fig INTERPOLATED PT SPLINE % \plot 4.445 20.320 4.432 20.387 4.421 20.449 4.398 20.561 4.378 20.656 4.359 20.737 4.323 20.863 4.286 20.955 4.228 21.059 4.187 21.121 4.136 21.190 4.075 21.270 4.001 21.362 3.913 21.468 3.810 21.590 / % % arrow head % \plot 4.023 21.438 3.810 21.590 3.926 21.355 / % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % Fig INTERPOLATED PT SPLINE % \plot 3.810 21.590 3.718 21.659 3.638 21.718 3.569 21.768 3.509 21.809 3.411 21.869 3.334 21.907 3.218 21.947 3.146 21.965 3.060 21.984 2.959 22.003 2.840 22.022 2.773 22.033 2.701 22.043 2.624 22.055 2.540 22.066 / % % arrow head % \plot 2.800 22.094 2.540 22.066 2.783 21.969 / % % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 2.064 22.066 \put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 2.264 21.966 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$r$} [lB] at 3.810 20.003 \put{\SetFigFont{12}{14.4}{rm}$r$} [lB] at 3.710 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$s$} [lB] at 4.445 20.003 \put{\SetFigFont{12}{14.4}{rm}$s$} [lB] at 4.345 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 5.715 20.003 \put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 5.615 20.003 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k$} [lB] at 3.810 20.955 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k(t)=$} [lB] at 1.287 21.273 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$\{r,s\}$} [lB] at 1.287 20.765 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T,\prec')$} [lB] at 2.657 22.895 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T,\prec)$} [lB] at 6.032 20.637 \linethickness=0pt \putrectangle corners at 1.587 23.555 and 6.375 19.952 \endpicture} %%% end pic3.pictex % % % \noindent (The arrow from $t$ in $(\T,\prec ')$ to $t$ in $(\T,\prec)$ represents the function $f$ in the original definition, which is now the identity).\par % % % % \subsection{Equivalence of Elementary Ordinal Systems and Ordinal Notation Systems from below.} \laprint{equivonsfb} Let $\prec''$ be the ordering on $\NF$ in an ordinal notation system from below, $f$ the function used there, define $\prec'$ on $f[\NF]$ by $f(\avec) \prec' f(\bvec) :\Iff \avec \prec '' \bvec$, $\k(f(\avec)):= \{ a_1 ,\ldots, a_n \}$ and $\length$ in the obvious way. Then, if we started with an ordinal notation system from below in which $\prec ''$ is linear, provably in $\PRA$, we obtain an elementary OS.\par In the other direction, assume an elementary OS, together with an explicit enumeration of the natural numbers, i. e. there exists a primitive recursive function $g: \omega \ar \T$, where we write $\underbar{n}$ for $g(n)$, such that $\all n.n \leq \underbar{n}$ and $\all n \in \nat.\underbar{n} =$ $n$th element of $\T$ provable in $\PRA$ (more precisely the formula $\all n \in \nat(n \leq \underline{n} \land \all x \in \T(x \prec \underline{n} \iff \exists l0$, then $\varphi_{a_1}a_2 \in \T $ provided $m=2$ and $a_2$ is not of the form $\varphi_{b_1}b_2$ with $a_1 \prec b_1$, and $\omega^{a_1} \cdot n_1 +\cdots+ \omega^{a_m} \cdot n_m \in \T$ provided $a_m \prec \cdots \prec a_1$ and if $m=1$, then $a_1 \not = 0$ and $a_1$ is not of the form $\varphi_{b_1}b_2$. $\S^k(0) \prec \S^l(0): \Iff k < l$, $\S^k(0) \prec \omega^{a_1}\cdot n_1 +\cdots+ \omega^{a_m}\cdot n_m$, $\S^k(0) \prec \varphi_ab$, $\omega^{a_1} \cdot n_1 +\cdots+ \omega^{a_m}\cdot n_m \prec \omega^{b_1} \cdot l_1 +\cdots+ \omega^{b_k}\cdot l_k :\Iff (a_1,n_1 ,\ldots, a_m,n_m)$ is lexicographically smaller than $(b_1,l_1 ,\ldots, b_k,l_k)$, $c:= \omega^{a_1} \cdot n_1 +\cdots+ \omega^{a_m}\cdot n_m \prec \varphi_ab :\Iff a_1 ,\ldots, a_m,n_1 ,\ldots, n_m \prec \varphi_ab$ and, if this condition does not hold, then $\varphi_ab \prec c$, and $\varphi_ab \prec \varphi_{a'}b' :\Iff (a \prec a' \land b \prec \varphi_{a'}b') \lor (a = a' \land b \prec b') \lor (a' \prec a \land \varphi_ab \prec b')$. The termination ordering $\prec'$ on $\T$ is now defined by $\S^k(0) \prec' \omega^{a_1}\cdot n_1 +\cdots+ \omega^{a_m}\cdot n_m \prec' \varphi_ab$, $\S^k(0) \prec ' \S^l(0)$ iff $k1$,}\\ \emptyset&\text{otherwise.}}$ Let $\calO_{+,\wrm}$ be the resulting OFG. Then one easily verifies $\eval(\Sigmabar()) = 0$ (similar cases occurring in future examples will not be mentioned below) $\eval(\Sigmabar(\alpha_1 ,\ldots, \alpha_m)) = \alpha_1 +\cdots + \alpha_m$ for $m>0$. The fixed point free version of it, i.e. $\lrm(t) := \k(t)$ yields the same result, except $\eval(\Sigmabar(\alpha,\underbrace{1 ,\ldots, 1}_{l}))= \alpha + l+1$ \ssubitem c Let $(\Arg,<):= \Sigmabar'(\schuette(\APN,\omega \setminus \{ 0 \} ))$,\\ $\k(\Sigmabar'(\alpha_1,n_1 ,\ldots, \alpha_m,n_m)):= \{ \alpha_1 ,\ldots, \alpha_m,n_1,\ldots, n_{m-1},n_m-1 \}$,\\ $\lrm(\Sigmabar'(\alpha_1,n_1 ,\ldots, \alpha_m,n_m)):= \mycases{\{ \alpha_1,n_m-1\} & \text{if $m>1$ or $n_m> 1$,}\\ \emptyset&\text{otherwise.}}$\\ Let $\calO_+$ be the resulting OFG. $\eval_{\calO_+}(\Sigmabar'(\alpha_1,n_1 ,\ldots, \alpha_m,n_m)) = (\alpha_1 \cdot n_1) +\cdots+ (\alpha_m \cdot n_m)$. \ssubitem d If we replace in \refact b, \refact c $\APN$ by $\Ord$ and $\Sigmabar$ by $\CNF$, we obtain ordinal function generators $\calO_{\CNF,\wrm}$, $\calO_{\CNF}$ for the Cantor normal form, i.e. $\eval_{\calO_{\CNF,\wrm}} (\CNF(\alpha_1 ,\ldots, \alpha_m)) = \omega^{\alpha_1} +\cdots+ \omega^{\alpha_m}$ and $\eval_{\calO_{\CNF}} (\CNF'(\alpha_1 ,n_1,\ldots, \alpha_m,n_m)) = \omega^{\alpha_1}\cdot n_1 +\cdots+ \omega^{\alpha_m} \cdot n_m$ \ssubitem e Let $\calO_0$ be $\calO_{+,\wrm}$ or $\calO_+$, $\calO_1:= (\omegabar^\Ord,\k,\lrm)$ with $\k(\omegabar^\alpha):= \{ \alpha \}$, $\lrm(\omegabar^\alpha):= \emptyset$, $\calO:= \calO_0 \preccirc \calO_1$, then $\eval(\omegabar^\alpha)= \omega^\alpha$. The fixed point free version ($\lrm(\omegabar^\alpha):= \{ \alpha \}$) yields the same result, except $\eval(\omegabar^{\alpha +n})= \omega^{\alpha+n+1}$ for epsilon numbers $\alpha$. \ssubitem f Let $\calO_0$ be $\calO_{+,\wrm}$ or $\calO_+$, $\calO_1:= (\phibar_\Ord\Ord,\k,\lrm)$, $\k(\phibar_\alpha \beta):= \{ \alpha,\beta \}$,\\ $\lrm(\phibar_\alpha \beta):= \mycases{\{ \alpha \} &\text{if $\beta > 0 $,} \\ \emptyset&\text{otherwise,}}$ $\calO:= \calO_0 \preccirc \calO_1$. Then $\eval(\phibar_\alpha \beta) = \varphi_\alpha \beta$, where $\varphi$ is the Veblen function with $\varphi_0 \beta:= \omega^\beta$. If we use the OFG from \refact d or \refact e instead for $\calO_0$ we obtain the $\varphi$-function starting with $\varphi_0 \alpha:= \epsilon_\alpha$, and defining $\lrm(t):= \k(t)$ yields the fixed point free version of the Veblen function.\par \ssubitem g Let $\calO_0$ be $\calO_{+,\wrm}$ or $\calO_+$, $\calO_1:= \phibar(\schuette{\Ord \setminus \{ 0 \} \choose \Ord})$. If $A= {\beta_1 \cdots \beta_m \choose \alpha_1 \cdots \alpha_m}$, define\\ %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m \\ %\alpha_1 &\cdots &\alpha_m \end{array} \right)$, $\k(\phibar(A)):= \{ \beta_1 ,\ldots, \beta_m,\alpha_1 ,\ldots, \alpha_m \}$ and\\ $\lrm(\phibar(A)):= \{ \beta_1 ,\ldots, \beta_{m-1},\alpha_1 ,\ldots, \alpha_{m-1}\} \cup \mycases{ \{ \alpha_m \} &\text{if $\beta_m>1$,}\\ \emptyset&\text{otherwise,}}$\\ $\calO:= \calO_0 \preccirc \calO_1$.\\ As in \cite{Schuette54} we allow addition of columns $0 \choose \alpha$ and identify matrices which differ in such columns only. If $A= {\beta_1 \cdots \beta_m \choose \alpha_1 \cdots \alpha_m}$, %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m \\ %\alpha_1 &\cdots &\alpha_m\end{array} \right)$, $(A,\beta_{m+1},\alpha_{m+1}): = {\beta_1 \cdots \beta_m \beta_{m+1} \choose \alpha_1 \cdots \alpha_m \alpha_{m+1}}$,\\ %\left(\begin{array}{cccc}\beta_1& \cdots&\beta_m&\beta_{m+1} \\ %\alpha_1 &\cdots &\alpha_m&\alpha_{m+1}\end{array} \right)$,\\ $(A,\beta_{m+1},\alpha_{m+1},\beta_{m+2},\alpha_{m+2})$ etc. are defined similarly.\\ %If $A = \left(\begin{array}{cccc}\beta_1& \cdots&\beta_m&\beta_{m+1}\\ %\alpha_1 &\cdots &\alpha_m&0 \end{array} \right)$, %$A':= \left(\begin{array}{cccc}1+\beta_1& \cdots&1+\beta_m&\beta_{m+1}\\ %\alpha_1 &\cdots &\alpha_m&0 \end{array} \right)$.\\ Then $\eval(\phibar(A)) = \varphi(A)$, where $\varphi(A)$ is defined as in \cite{Schuette54}, based on $\varphi(\alpha):= \omega^\alpha$, but with reversed order of the columns. We prove this by induction on $<'_\calO$:\\ If $A = \phibar(\alpha,0)$, then we can easily show $\eval(A) = \omega^\alpha= \varphi(\alpha,0)$.\\ If $A= \phibar(B,\alpha,\beta,\gamma,0)$, then it follows that $\C(\phibar(A))$ is closed under $+$,\\ $\lambda \delta.\eval(\phibar(B,\alpha^\ast,\beta,\delta,\beta^\ast))$ for $\alpha^\ast<\alpha$, $\beta^\ast<\beta$ and contains further\\ $\eval(\phibar(B,\alpha,\beta,\gamma^\ast,0))$ for $\gamma^\ast<\gamma$, therefore using the IH $\eval(\phibar(B,\alpha,\beta,\gamma,0))\geq \varphi(B,\alpha,\beta,\gamma,0)$. On the other hand, $\varphi(A) \geq \k(\phibar(A))$, $\varphi(A)> \lrm(\phibar(A))$, and, if $B <' A$, $\k(\phibar(B))< \varphi(A)$, by the calculations in \cite{Schuette54} $\varphi(B) < \varphi(A)$, therefore using the IH $\all \gamma \in \C(\phibar(A))(\gamma < \varphi(A))$, $\varphi(A) \geq \eval(\phibar(A))$. \ssubitem h If we define in \refact g $\lrm(\phibar(A)):= \k(\phibar(A))$, we obtain a fixed point free version of the Klammer symbols or equivalently $\eval(\phibar {\beta_1 \cdots \beta_m \choose \alpha_1 \cdots \alpha_m})= %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m\\ %\alpha_1 &\cdots &\alpha_m\end{array} \right) = \vartheta(\Omega^{\alpha_1}\beta_1 +\cdots+ \Omega^{\alpha_m}\beta_m)$, where $\vartheta$ is defined as in \cite{rathjenweiermann}, but without closing $\C(\alpha,\beta)$ under $\lambda \gamma.\omega^\gamma$. (We obtain the original $\vartheta$ function, if we take as $\calO_0$ the OFG for $\CNF$). See \cite{seisenbdipl} for details. If we restricting the definition to those $\alpha_i,\beta_i$ such that for $\gamma:= \Omega^{\alpha_1}\beta_1 +\cdots+ \Omega^{\alpha_m}\beta_m$ $\gamma \in \C(\gamma)$, where $\C(\gamma)$ is defined as for the ordinary $\psi$-function, then we will get the same result, but with $\vartheta$ replaced by the $\psi$-function ($\psi = \psi_0$ as in \cite{buchholzanewsys} or $\psi= \psi_{\Omega_1}$ as in \cite{buchholzasimplified}, however with $\C(\alpha,\beta)$ not closed under $\varphi$). Note that this restriction has the effect that $\prec'$ and $\prec$ coincide in the corresponding OS for terms of the form $\phibar(a)$. \ssubitem i Let $\calS_0:= \Ord$, $\calS_{n+1}:= \schuette{\Ord \setminus \{ 0 \} \choose \calS_n}$,\\ $\k^i_0: \calS_i \ar_\omega \Ord$, $\k^0_0(\alpha):= \{ \alpha \}$, $\k^{i+1}_0 {\beta_1 \cdots \beta_m \choose A_1 \cdots A_m}:= %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m\\ %A_1 &\cdots &A_m\end{array} \right):= \{ \beta_1 ,\ldots, \beta_m \} \cup \bigcup_{j=1}^m \k^i_0(A_j)$.\\ Let $\k^i(\phibar(A)):= \k^i_0(A)$,\\ $\calO^i_1:= (\phibar(\calS_i),\k^i,\k^i)$, $\calO^i:=\calO_0 \preccirc \calO_1$ ($\calO_0$ as before). We obtain, what we can call the ``fixed point free version of extended Sch{\"u}tte Klammer symbols''. Let $f_i: \calS_i \ar \Ord$, $f_0(\alpha):= \alpha$, $f_{i+1} {\beta_1 \cdots \beta_m \choose A_1 \cdots A_m}:= %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m\\ %A_1 &\cdots &A_m\end{array} \right):= \Omega^{f_i(A_1)}\beta_1 +\cdots+ \Omega^{f_i(A_m)} \beta_m$, then one can easily see $\eval_{\calO^i}(\phibar(A))= \vartheta(f_i(A))$, $\vartheta$ as in \refact h. Applying a similar restriction as in \refact h yields the $\psi$-function restricted to ordinals $<\underbrace{\Omega^{\Omega^{\cdots^{\Omega}}}}_{i \text{ times}}$.\par \ssubitem j As in \refact g and \refact h, we can define a version of the extended Sch{\"u}tte Klammer symbols with fixed points. The verifications takes more space than is available here. In some sense we believe however that in the context of OS, the fixed point free versions are at least as natural or even more natural than the versions with fixed points. \ssubitem k Let $\calO^i$ be as in \refact i. The union of $\calO^i$ can be described as follows: Let $\calS'_{-1}:= \{ 0 \}$, $\calS'_0:= \Ord$, $\calS'_{n+1} := \calS'_n \preccirc (\schuette{\Ord \setminus \{ 0 \} \choose \calS'_n} \setminus |\schuette{\Ord \setminus \{ 0 \} \choose \calS'_{n-1}}|)$, $\k^i_0: \calS'_i \ar_\omega \Ord$, $\k^0_0(\alpha):= \{ \alpha \} $, $\k^{i+1}_0(A)= \k^i_0(A)$ for $A \in \calS'_i$, $\k^{i+1}_0(A)$ is defined as in \refact i for $A \in \calS'_{i+1} \setminus \calS'_i$. Let $|\calS'|:= \bigcup_{i< \omega }|\calS'_i|$, $\prec_{\calS'} := \bigcup_{i<\omega}\prec_{\calS'_i}$, $\k^i(\phibar(A)):= \k^i_0(A)$, $\k:= \bigcup \k^i$, $\calO:= \calO_0 \preccirc (\phibar(\calS'),\k,\k)$, which is an OFG.\\ Define $\iota_i:|\phibar(\calS_i)| \ar |\phibar(\calS'_i)|$ by $\iota_0(\phibar(\alpha)):= \alpha$, $\iota_1(\phibar{\choose}):= \phibar(0)$, $\iota_1(\phibar{\alpha \choose 0}):= \phibar(\alpha)$, $\iota_1(a):= a$ otherwise, $\iota_{i+2}(a):= \iota_{i+1}(a)$ for $a \in \phibar(\calS_{i+1})$, $\iota_{i+2}(\phibar{\beta_1 \cdots \beta_m \choose A_1 \cdots A_m}):= %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m\\ %A_1 &\cdots &A_m\end{array} \right):= \phibar{\beta_1 \cdots \beta_m \choose \iota_{i+1} (A_1)\cdots\iota_{i+1} (A_m)}$ otherwise. %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m\\ %\iota_i(A_1) &\cdots &\iota_i(A_m)\end{array} \right)$, %if $m>1$ or $m=1 \land A_m \not = 0,{\hbox{\quad}\choose \hbox{\quad}}$, %$\iota_i{\hbox{\quad}\choose \hbox{\quad}}:= 0$, %$\iota_1 {\alpha \choose 0}:= \alpha$, %$\iota_i+2{\alpha \choose {\hbox{\quad}\choose \hbox{\quad}}} %:= \alpha$. Then $\iota_i$ is an isomorphism from $\phibar(\calS_i)$ to $\phibar(\calS_i')$, $\phibar(\calS_0') \segment \phibar(\calS_1') \segment \cdots$, the isomorphism can be extended to an isomorphism from $\Arg_{\calO^i}$ to an initial segment of $\Arg_{\calO}$ which preserves the component sets $\k_i$. In this sense $\calO$ is the union of the $\calO_i$. \end{enumerate}} \end{example} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% The following lemma, which will be used in the proof of \ref{theoexampleos}, helps to derive from an OFG an OS based on it, which is primitive recursive: One introduces a set of terms $\T''$, which have the syntactical form of being arguments, if we replace its components by ordinals. From these terms we select now a set $\T$ of terms and $\T'$ of arguments based on $\T$ such that $\T$ represents all elements of $\Cl$ and $\T'$ all elements of $\Arg[\Cl]$. Whether an element belongs to $\T'$ or $\T$ depends now on the ordering of its components, which need to be in $\T$ and then one can show that under the assumptions formulated in the next lemma, $\T$, $\T'$, $\prec$ and $\prec'$ will be primitive recursive. Especially condition \refsub{defprimreksys}e will have some flavor of $\Pi_1^2$-logic, however, the ordering of the elements of $\T$ and whether and element of $\T ''$ belongs to $\T$ will depend not only on the order of its components, which allows some more generality. % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{lemma} \laprint{defprimreksys} Let $\calO$ be an OFG as usual, and let $\T''$ be a primitive recursive set, $\T \subseteq \T' \subseteq \T ''$, $f: \T' \ar \Arg$, $\krmhat: \T'' \ar_\omega \T''$, $\lrmhat: \T'' \ar_\omega \T''$, $\length': \T'' \ar \nat$, all primitive recursive. Let for $a,b \in \T'$, $a \prec' b: \Iff f(a) <' f(b)$, $a \prec b: \Iff \eval(f(a)) < \eval(f(b))$. Assume the following conditions: \begin{enumerate} \ssubitem a $\all a \in \T '. \lrmhat(a) \subseteq \krmhat(a) \subseteq \T$. \ssubitem b $\all a \in \T'(f[\krmhat(a)] = \k^0(f(a)) \land f[\lrmhat(a)] = \lrm(f(a)))$.\\ $\all a \in \T''.\length'[\krmhat(a)]< \length'(a)$. \ssubitem c For every subset $A$ of $\T$ $f[\{ t \in \T ' \mid \krmhat(t) \subseteq A \}] = \{ a \in \Arg \mid \k(a) \subseteq \eval[f[A]] \} $. \ssubitem d If $A \subseteq \T'$, $f \restriction A$ is injective, then $f \restriction \{ t \in \T ' \mid \krmhat(t) \subseteq A \} $ is injective. \ssubitem e For $a,b \in \T''$ such that $\krmhat(a) \cup \krmhat(b) \subseteq \T$ we can determine from $\prec$ restricted to $\krmhat(a) \cup \krmhat(b)$ (coded as a finite list which is coded as a natural number) in a primitive recursive way, whether $a,b \in \T '$ and, if this is the case, whether $a \prec ' b$. \ssubitem f $a \in \T \Iff a \in \T ' \land f(a) \in \NF \land \krmhat(a) \subseteq \T$. \end{enumerate} Then $\T$, $\T'$, $\prec'$, $\prec$, are primitive recursive, we can define $\lengthhat: \T' \ar_\omega \T$ such that $\lengthhat(a) = \length(f(a))$ for $a \in \T'$, and $(\T,\prec,\prec ',\krmhat,\lengthhat)$ is an OS based on $\calO$. \end{lemma} % % % {\bf Proof:} We determine for $t \in \T ''$ whether $t \in \T '$, $t \in \T$ and for $r,s \in \T'$ such that $\length'(r)$, $\length'(s)\leq \length'(t)$ whether $r \prec' s$ and whether $r \prec s$ holds by recursion on $\length'(t)$ and side-recursion on $\length'(r)+\length'(s)$: If $\krmhat(t) \not \subseteq \T$, $t \not \in \T '$. Otherwise we can decide whether $t \in \T '$. Assume now $r,s$ as above. Whether $r \prec ' s$ follows from the induction hypothesis and then using Lemma \refcom{lemordgen}{eb} we can determine whether $r \prec s$ holds. Now $t \in \T :\Iff t \in \T' \land \krmhat(t) \prec t$.\\ $f: \T \ar \Arg$ is injective by condition \refact d. $f[\T] \subseteq \NF$, $f[\T] \subseteq \Cl$. We show $f[\T] = \Cl$. It suffices to show $\all a \in \Cl.\exists b \in \T. f(b) = a$. Induction on $a$. $\krmhat(a) \subseteq f[\T]$. Therefore there exists a $t \in \T '$, $\krmhat(t) \subseteq \T$, such that $f(t) = a$. Since $\NF(a)$, follows $t \in \T$.\\ $\lengthhat(t)$ is defined now by $\lengthhat(t):= \max(\lengthhat[\krmhat(t)] \cup \{ -1 \})+1$.\QED % % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% %% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% %\begin{remark} %\laprint{remofgdil} %The conditions of Lemma \ref{defprimreksys} are almost like the %definition of ordinal denotations as studied by Girard in the area %of $\Pi^1_2$-logic. However, we want to keep a little bit more flexibility %in the sense, that whether an element belongs to the set $\T '$ might %not only depend on the ordering of its components but as well %on some syntactical properties of it. For instance, when using later %ordinary sum of $n$ additive principal numbers, the notation %$(a_1 ,\ldots, a_n)$ for the sum of $a_1 ,\ldots, a_n$ will not %only depend on the ordering of the $a_i$, but as well %on, whether they are represent additive principal numbers (which %one can see %\end{remark} %% % % %{\bf Important note:} The development of the ordinal systems corresponding %to the examples above can be done purely syntactically, %i.e. without using the %OFG and therefore without referring to ordinals, and this is as easy %as the above approach. The advantage of developing as OFG is that %we get a generalization of the functions for arbitrary ordinals and %not only for notations. % % % \begin{lemma} \laprint{theoexampleos} For all the OFG in the Example \refcom{exmplordfun}a - \refsub{exmplordfun}i, except for those examples involving the lexicographic ordering on weakly descending sequences (\refsub{exmplordfun}b and the examples referring to it) there exists an elementary OS represented by them. \end{lemma} % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{remark} \laprint{remnoteordinals} Note that the development of the OS can be done without having to refer to ordinals. \end{remark} % % % % % {\bf Proof of Lemma \ref{theoexampleos}:} First, using Lemma \ref{defprimreksys} we can define a primitive recursively represented OS based on the OFG. We look only at the example \refsub{exmplordfun}g in detail: Let $\underline{0}:= \Sigmabar'()$, $\underline{l+1}:= \Sigmabar'(\underline{0},\underline{l}\plusbar 1)$, $\underline{\nat}:= \{ \underline{l} \mid l \in \omega \}$. Define $\T''$ together with $\krmhat:\T'' \ar_\omega \T''$, $\lrmhat:\T'' \ar_\omega \T''$, $\length(\T'') \ar \nat$ recursively by:\\ If $m \in \omega$, $a_i \in \T ''$, $b_i \in \underline{\nat}$, $b_i \not = \underline{0}$ for $i1$ or $b_m \not = \underbar{0}$,}\\ \emptyset&\text{otherwise,}}$\\ $\length(t_0):= \max \{ \length(a_1) ,\ldots, \length(a_m), \length(b_1) ,\ldots, \length(b_m) \} +1$.\\ If $a_1 ,\ldots, a_m,b_1 ,\ldots, b_m \in \T''$, $a_1 ,\ldots, a_m \not = \underline{0}$, $t_1:= \phibar{a_1 \cdots a_m \choose b_1 \cdots b_m}\in \T''$, and we define $\krmhat(t_1)$, $\lrmhat(t_1)$ by translating the conditions from Example \refcom{exmplordfun}g and $\length(t_1)$ as before. $\T''$, $\length$, $\krmhat$, $\lrmhat$ are primitive recursive.\\ Define $\T \subseteq \T''$, $\T' \subseteq \T ''$, together with $f: \T' \ar \Arg$ inductively by: If $t_0$ is as above, $\krmhat(t_0) \subseteq \T$, $\eval(f(a_1)) > \cdots > \eval(f(a_m))$, then $t_0 \in \T'$,\\ $f(t_0):= \Sigmabar'(\eval(f(a_1)),\eval(f(b_1)) ,\ldots, \eval(f(a_{m-1})), \eval(f(b_{m-1})),$\\ \hbox{\qquad \qquad}$\eval(f(a_m)),\eval(f(b_m))+ 1)$.\\ If $t_1$ is as above, $\eval(f(b_1))> \cdots > \eval(f(b_m)) $, then $t_1 \in \T'$,\\ $f(t_1):= \phibar{\eval(f(a_1)) \cdots \eval(f(a_m)) \choose \eval(f(b_1)) \cdots \eval(f(b_m))}$.\\ Further $t \in \T :\Iff t \in \T ' \land \NF(f(t) )$.\\ The conditions of Lemma \ref{defprimreksys} are now fulfilled and therefore most conditions of a primitive recursively represented OS are fulfilled, what is missing is verified easily.\par The other OS are treated similarly. The constructions of new orderings considered in \cite{setzvenedig} Lemma 3.5 (especially the lexicographic ordering on pairs and and strictly descending sequences) yield orderings such that transfinite induction over it reduces to transfinite induction over the underlying orderings in $\PRA$ and therefore we get actually get in all cases elementary OS.\QED \par However, transfinite induction over weakly descending sequences reduces only in $\HA$ to the underlying ordering, so the examples where we used weakly descending sequences do not yield elementary OS.\par % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{theorem} \laprint{theostrengthordsyslow} \begin{enumerate} \ssubitem a The bound in Theorem \ref{theostrengthordsys} is sharp: The supremum of the order types of elementary OS is exactly the Bachmann-Howard ordinal. \ssubitem b The limit of the order type of ordinal systems from below as introduced in \cite{setzvenedig} is the Bachmann-Howard ordinal. \end{enumerate} \end{theorem} % % % {\bf Proof:} \refact a: Example \refcom{exmplordfun}i yields OS of strength $\vartheta(\underbrace{\Omega^{\Omega^{\cdots^\Omega}}}_{i \text{ times}})$, which in the limit reaches the Bachmann-Howard ordinal.\\ \refact b: by subsection \ref{equivonsfb}, \refact a and the upper bound developed in the last two sections of \cite{setzvenedig}.\QED \par Note that the construction in the example used in \refact a really exhausts the full strength of elementary OS: In the OS related to $\calO_i$ $\prec '$ is built from $\prec$ using $i$-times nested lexicographic ordering on descending sequences, $\TI$ over which reduces to the underlying ordering by using formulas of increasing length. The union of the $\calO_i$, $\calO '$ yields an OFG, such that in the OS belonging to it $\TI$ over $\prec '$ does no longer reduce to $\TI$ over $\prec$ in $\PRA$, so it is no longer elementary. What is required are twice iterated ordinal systems. % % % %{\bf Introducing ordinals via closure sets.} The usual ordinal notation %systems below the Bachmann-Howard ordinal, which lead to the definition %of ordinal notation systems from below, are always based on %ordinal functions, which can be defined using closure sets. %Consider as an example %$\lambda \alpha.\omega^\alpha$. Then we can define $\omega^\alpha$ %simultaneously with sets $\C_\omega(\alpha)$ for $\alpha \in \Ord$ %(where $\Ord$ is the class of ordinals) by induction on $\alpha$:\\ %$\C_\omega (\alpha) =$ closure of $\{ 0 \} \cup \{ \omega^\gamma \mid \gamma<\alpha \} $ under $+$; %$\omega^\alpha = \min \{ \gamma \in \Ord \mid \gamma \not \in \C_\omega (\alpha)$.\par %We can modify this definition slightly and define\\ %$\C_\omega (\alpha) = $ closure of $\beta \cup \{ 0 \} $ under %$\lambda \gamma< \alpha.\omega^\gamma$ and $+$, %$\omega^\alpha$ is definded as before.\\ %In the same spirit we can define addition by \\ %$\C_+(\alpha,\beta):= $ closure of $\alpha \cup \beta$ under %$\lambda \rho<\beta.\alpha + \rho \} $, %$\alpha + \beta = \min \{ \gamma \in \Ord \mid \gamma \not \in \C_+(\alpha,\beta) \}$,\\ %and\\ %$\phi_\alpha \beta := \min \{ \gamma \in \Ord \mid %\gamma \not \in \C_\phi(\alpha,\beta)$ with %$\C_\phi(\alpha,\beta):= $ closure of %$\alpha \cup \beta \cup \{ 0 \} $ under $+$, %$\lambda \gamma<\alpha .\lambda \rho.\phi_\gamma \rho$, %$\lambda \gamma<\beta.\phi_\alpha \gamma$.\\ %We can define Sch{\"u}tte's Klammer symbols as follows: %for a Klammer symbol $A$ let $\Ord(A)$ be the set of ordinals contained %in it, and $<_\lex$ the usual twice nested lexicographic ordering. %Then define:\\ %$\C(A):= $ closure of $\bigcup \Ord(A) \cup \{ 0 \} $ under %$\lambda \Ord(B).\phi(B)$ restricted to $B <_\lex A$\\ %(more formally the least set $M$ containing $\bigcup \Ord(A)$, %$0$ such that $\Ord(B) \subseteq M$, $B <_\lex A$, then $\phi(B) \in M$).\\ %$\varphi(A):= \min \{ \gamma \mid \gamma \not \in \C(A) \}$.\par %All these definitions can be generalized in the following sense: %Assume some set of terms $\T$ built from ordinals. So every %term $t$ has a set $\k(t)$ of ordinals, it is built from. Define an %partial ordering $<'$ on these terms. Assume $<'$ is well-founded. %Define by induction on $<'$ sets %$\C(t) \subseteq \Ord$ and $\eval: \C(t) \ar \Ord$ by %$\C(t):=$ least set containing $\bigcup \k(t)$, such that %if $s <'t$, $\k(s) \subseteq \C(t)$, then $\eval(s) \in \C(t)$, %$\eval(t):= \min \{ \gamma \in \Ord \mid \gamma \not \in \C(t)$.\\ %So for the definition of $+$, we define %as set of terms $\T_+:= \{\underbar{0} \} \cup %\{ \alpha \underbar{+} \beta \mid %\alpha,\beta \in \Ord \} $, %and as ordering on $\T_+$, %$<_+$ defined by %$0 <_+ \alpha \underbar{+} \beta $, and %$\alpha \underbar{+} \beta <_+ \alpha ' \underbar{+} \beta '$ %iff $\alpha = \alpha ' \land \beta < \beta '$, %$\eval(\alpha \underbar{+} \beta) = \alpha + \beta $.\\ %In case of $\lambda \rho .\omega^\rho$, %let $\T_\omega:= \T_+ \cup \{ \underlinedef{\omega}^\alpha \mid %\alpha \in \Ord \} $,\\ %and the ordering $<_\omega$ on $\T_\omega$ contains %$<_+$, has $t <_\omega \underlinedef{\omega}^\gamma$ for $t \in \T_+$ and %$\underlinedef{\omega}^\alpha <_\omega \underlinedef{\omega}^\beta$ iff %$\alpha < \beta$. %Similarly one can define orderings for all other functions mentioned before.\\ %If we select now normal forms, which means for each ordinal $\alpha$ we have %at most one term $t$ such that $\eval(t) = \alpha$, which %implies typically, that we do not only have %$\k(t) \leq \eval(t)$ as we had before, but %$\k(t) < \eval(t)$ (because if $\alpha \in \k(t)$, $\alpha = \eval(t)$, %then $\alpha$ would be ``a shorter'' notation than $t$, %then the ordering $<'$ can be defined as a linear ordering, %since $\C(t)$ will be linearly ordered (define %for $t,t'$ uncomparable $t <' t'$ iff $\eval(t) < \eval(t')$.\\ %If we have a set of terms $\T$ in normal forms as before, then %we can define a set of ordinal notations $\OT$ together %an interpretation $\ordinal:\OT \ar \Ord$ by: %if $t \in \T$, $\k(t) \subseteq \ordinal[\OT]$, %then we add a notation $t'$ for $t$ to $\OT$ and %define $\ordinal(t'):= \eval(t)$. If we define now for %$r,s \in \OT$, %$r \prec s \Iff \ordinal(r) < \ordinal(s)$, %$r \prec ' s \Iff r' <' s'$, $\k(r):= \ordinal^{-1}[\k(r')]$, %where in the last two definitions $\eval(r') = \ordinal(r)$, %$\eval(s') = \ordinal(s)$, then %we get an OS-structure, which fulfills (OS 1) (OS 2) and (OS 3).\\ %Now (OS 4) expresses that the ordering $<'$ is not just an %arbitrary one, but a good one %and this means that well-foundedness of $\k^{-1}(A)$ for %$A \subseteq \Ord$ reduces to well-foundedness of $A$. However, this %last definition is not a good one, since we have already that %all of $A$ is well-ordered. Girard gave some definition in his %$\Pi_1^2$-logic.????? We have to make an exact comparision yet --- %Definition of Ordinal system based on ordinals only possible ????? %In our approach we have made this precise only for the set of %notations, and (OS 4) expresses what we mean %by a good ordering $\prec '$. \par %We will give the following definition and lemma, in order %to sharpen our intuition. It will not be needed later. %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% %% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% %\begin{deflemma} %\laprint{lemclosureos} %Let $\calF$ be a OS.\\ %For $s \in \T$, let %$\C(s)$ be the least set, such that %for all $t \preceq \k(s)$, $t \in \C(s)$ and %for all $t \in \T$, if $\k(t) \subseteq \C(s)$ and %$t \prec ' s$, then $t \in \C(s)$.\\ %Then $\C(s)= \{ t \in \T \mid t \prec s \} $. %\end{deflemma} %% %% %% %{\bf Proof:} ``$\subseteq$'' Induction on the definition %of $\C(s)$. Assume $t \in \C(s)$ according to induction. %If $t \preceq \k(s)$, %$t \preceq \k(s) \prec s$. %Otherwise $t \prec 's$, by IH $\k(t) \prec s$. If %$s \preceq t$, then $s \preceq' t$ or %$s \preceq \k(t)$ contradicting the linearity of $\prec '$ %and $\prec$. ``$\supseteq$'': We show %$\all t \in \Cl_\calF.t \prec s \ar t \in \C(s)$ by induction %on $t \in \Cl_\calF$. Assume $t$ according to induction. %If $t \preceq \k(s)$, $t \in \Cl(s)$. Otherwise %$t \prec ' s$, by IH and $\k(t) \prec t \prec s$ follows %$\k(t) \subseteq \Cl(s)$, $t \in \Cl(s)$.\par %% %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% %% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% %\begin{remark} %\laprint{remcsprimrek} %$\C(s)$ as defined in \ref{lemclosureos} can be defined primitive-recursively. %\end{remark} %% %% %% %{\bf Proof:} Let a sequence $$ %a proof of $t_m \in \C(s)$, iff we can infer $t_i \in \C(s)$ %from knowing only that $t_i \in \C(s)$. One verifies, %that the set of such proofs is primitive recursive and %one can show that the set of terms, for which %such proofs exist, is $\C(s)$ (i.e. fulfills the %same closure and induction principles as $\C(s)$). % % % % % % % %\refact c Let $(\OT,\prec)$ be the usual ordinal notation %system built from $0$, $\Omega$,\break %$\lambda \alpha,\beta.\omega^\alpha+\beta$ and %$\psi$ (see for instance \cite{buchholzschuettebook}, but %omitting $\lambda \alpha.\Omega_\alpha$ except %of the constant $\Omega_1$, written as $\Omega$, and %of $\psi \alpha$ for $\alpha \not = 0$, and writing %$\psi$ instead of $\psi_0$, or, alternatively, replacing %the basic functions in %\cite{buchholzanewsys} or \cite{pohlersbook} by %our $0$ and $\lambda \alpha,\beta.\omega^\alpha+\beta$). %Let $\omega_0(x):= x$, $\omega_{n+1}(x):= %\omega^{\omega_m(x)}$. %Let $\calOT_m:= (\OT_m ,\prec_m):= %(\OT,\prec) \cap \{ c \in \OT_m \mid c \prec \psi(\omega_{n+1}(\Omega+1)) \} $. %\begin{definition}{\rm %\laprint{defOmegapower} %Assume $A$, $B$ are orderings, %$0$ is the minimal element of $B$. %\begin{enumerate} %\ssubitem a $\Omega^A \cdot B$ %is the ordering\\ %$(\{ \Omega^{a_1} \cdot b_1 +\cdots+ \Omega^{a_m} \cdot b_m %\mid n \in \omega, a_i \in |A|, %b_i \in |B|\setminus \{ 0 \} , a_m \prec_A \cdots \prec_A a_1 \}, %\prec')$,\\ %where elements %$\Omega^{a_1} \cdot b_1 +\cdots+ \Omega^{a_m} \cdot b_m $ are %ordered as %$\left (\begin{array}{ccc}a_1&\cdots&a_m \\ %b_1&\cdots &c_m \end{array}\right)$ in %$\left({B \choose A}\right)^\ast_\des$. %(Here, if $\Omega^a \cdot b$ is a defined function, this %definition has to be evaluated). %Note that, if $A$, $B$ are primitive recursive, transfinite induction over %$\Omega^A \cdot B$ reduces in $\PRA$ %to transfinite induction over $A$ and $B$. %$\Omega_c^A \cdot B$, %$\omega^A \cdot B$ are defined similarly. %\ssubitem b $\Omega \uparrow_0(A):= A$, %$\Omega\uparrow_{n+1}(A):= \Omega^{\Omega\uparrow_m(A)} \cdot A$. %Note that, if $A$, $B$ are primitive recursive, transfinite induction over %$\Omega^A \cdot B$ reduces in $\PRA$ %to transfinite induction over $A$ and $B$. %$\Omega_c \uparrow_m(A)$ %$\omega \uparrow_m(A)$ is defined similarly. %The set of components $\krmhat_m(a)$ for $a \in |\Omega_c \uparrow_m(A)|$ %is defined by: $\krmhat_m(a):= \{ a \} $, %and $\krmhat_{n+1}( \Omega^{a_1} \cdot b_1 +\cdots+ %\Omega^{a_m}\cdot b_m):= \{ b_1 ,\ldots, b_m \} \cup %\krmhat_m[\{ a_1 ,\ldots, a_m \} ]$. %\end{enumerate}} %\end{definition} %% %% %% %Let now $\prec_m$ be the ordering on $\OT_m$. %Let $\prec_m'$ be the ordering on %$\{ 0 \} \preccirc %(\omega^{\calOT_m} + \calOT_m)\preccirc \psi(\M_m) \cap \OT_m$, %where %$\M_m:= \Omega \uparrow_m(\calOT_m))$. %Define $\k:\OT_m \ar_\omega \OT_m$, %$\k(0):= \emptyset$, %$\k(\omega^a + b):= \{ a,b \} $ (if in normal form), %$\k(\psi(c)):= \krmhat_m(c)$ (if in normal form), where %$\krmhat_m(c)$ is the set of components of %$\M_m$.\\ %Then $(\OT_m,\prec_m,\prec_m ',\k$ is an elementary OS:\\ %$\prec_m$, $\prec_m '$ are %linear orderings provable in $\PRA$ is clear. %$(\OS\ 1)$: For $0$ and $\omega^a +b $ this is clear %and for $\psi(c)$ this follows by definition (we add %$\psi(c)$ to $\OT$ only, if $c \in C(c)$ which means just %$\k^n(c) \prec_m c$). $(\OS\ 2)$, $(\OS\ 3)$: easy. $(\OS\ 4)$: %$\prec_m '$ was defined using constructions, for which always %holds, that $\TI$ over the resulting construction reduces in %$\PRA$ to its underlying orderings (the proofs can be found %in \cite{setzvenedig}).\\ %Since the ordertype of $(\OT_m,\prec_m)$ is %$\psi(\omega_m(\Omega+1))$ and %$\sup_{n \in \omega}\psi(\omega_m(\Omega+1))$ %is the BHO we are done.\QED %\medskip %It seems to be more intuitive, to write the OS introduced in the %proof of \refcom{theoremstrengthelemos}c slightly differently. First of all we note, that %we could have replaced $\psi$ by the function $\vartheta$ %as introduced in \cite{rathjenweiermann} and the proof %works with almost the same argument. Further we can write %the cantornormalform to the basis $\Omega$ instead %as a matrix, i.e. we replace %$\Omega^{a_1} \cdot b_1 +\cdots+ \Omega^{a_m}\cdot b_m$ by %$\left (\begin{array}{ccc}a_1&\cdots&a_m\\b_1&\cdots&b_m \end{array}\right)$. %So the notation $\Omega^{\Omega^a \cdot b + d}\cdot e + \Omega^f \cdot g$ %which is $\Omega^{\Omega^a \cdot b + \Omega^0 \cdot d}\cdot e %+ \Omega^{\Omega^0 \cdot f } \cdot g$ %is replaced by \\ %$\left ( \begin{array}{cc} e &g\\ %\left (\begin{array}{cc}b & d \\a&0 \end{array} \right )& %\left (\begin{array}{c}f \\0 \end{array} \right )\end{array} \right)\enspace .$\\ %These matrices are ordered by the same nested lexicographic ordering %as it was done for the terms in $\Omega$-Cantor-normalform. %Now $\vartheta(A)$ can be regarded as an extended Klammer symbol. %More precisely, define, if $\Ord$ is the set of ordinals %with ordering $<$, %$\Mbb_m$ for $m \leq n$ together %with $<_m$ on $\Mbb_m(X,<)$ by\\ %$(\Mbb_0,<_0):= \Ord$, %$(\Mbb_{k+1},<_{k+1}):= %{(\Ord \setminus \{ 0 \},<) \choose (\Mbb_m,<_m)}^\ast_\des $\\ %Define $\varphi_m:\Mbb_m \ar \Ord$ by\\ %$\varphi_0(\alpha):= \epsilon_\alpha$, %and, if $D = \left(\begin{array}{ccc} \alpha_0 &\ldots&1+ \alpha_m \\ % A_0 &\ldots&A_m %\end{array}\right)\in \Mbb_{k+1}$, then\\ %$\varphi_{k+1}(D) %:= \alpha_m$th fixed point of all functions %$\lambda \gamma.\omega^\gamma$ and\\ %$\lambda \gamma.\varphi_{k+1} %\left(\begin{array}{cccc} \beta_0 &\ldots&\beta_m&\gamma \\ % B_0 &\ldots&B_m&B_{m+1} %\end{array}\right) $ %with\\ %$\left (\begin{array}{ccc} \beta_0 &\ldots&\beta_m \\ % B_0 &\ldots&B_m %\end{array}\right) <_m %\left(\begin{array}{ccc} \alpha_0 &\ldots&\alpha_m \\ % A_0 &\ldots&A_m %\end{array}\right)$\\ %and where $\beta_i$ and the ordinals $A_i$ are below some of the %ordinals in $D$ or can be majorized by the same process,\\ %which is more precisely %the least ordinal not in %$\C(D)$, where\\ %$\C(D)$ is the %closure of $0$ under %$\lambda \gamma.\omega^\gamma$ and %$\gammavec \mapsto \varphi \left (\begin{array}{ccc} \beta_0 &\ldots&\beta_m \\ % B_0 &\ldots&B_m %\end{array}\right)$, %where $\gammavec$ are the ordinals in $B_i$ and $\beta_i$ %and %$\varphi \left (\begin{array}{ccc} \beta_0 &\ldots&\beta_m \\ % B_0 &\ldots&B_m %\end{array}\right) <_m A$.\\ %In other words, $\varphi(D)$ is the least ordinal %which cannot be reached using the basic functions %and $\varphi(D')$ for $D' <_m D$, i.e. by functions %defined before $\varphi(D)$.\\ %The last definition is in the case $k=2$ equivalent %to the definition of the Sch{\"u}tte-Klammer symbols %based on $\lambda \gamma.\omega^\gamma$, %and $\varphi_m$ are the straight-forward generalization of %the Klammer symbols.\\ %If we define further %$f_k : \Mbb_k \ar \Ord$ where $\Ord$ are the full ordinals, by %$f_0(\alpha):= \alpha$, and, if $D$ is as above, %$f_{k+1}(D):= %\Omega^{f_k(A_1)}\alpha_1 +\cdots+ %\Omega^{f_k(A_m)}\alpha_m$. %Then $\varphi_k(D) = \vartheta(f_k(D))$. %Therefore the ordinals above $\Omega$ can be seen as %a more elegant way of writing matrices %and the system based on the $\vartheta$-function %is another description of the %extended Sch{\"u}tte-Klammer symbols. The notation systems constructed %reach every ordinal below the BHO (therefore %we can reach BHO ``from below''). %\medskip %{\bf Relationship between $\psi$- and $\vartheta$-function} The %above considerations illustrate the relationship between the $\psi$- and %$\vartheta$-function. For the $\psi$-function condition (OS 1) %is guaranteed by having $\psi(a)$ is a term in normal form %only if for the ordinal denoted by $a$ we have %$\ordinal(a) \in \C(\ordinal(a))$ which means exactly $\k(a) \prec \psi(a)$. %In thhe case of the $\vartheta$-function, one %forces $\vartheta(a)$ to be bigger than $k(a)$.\par % %{\bf Equivalences of different ordinal systems.} There are several %variations of the $\psi$- and $\vartheta$-function, which depend %essentially on the choice of the basic functions: One %can start with $0$ and $\lambda \alpha,\beta.\omega^\alpha + \beta$, %or only with $0$ and addition %(and additionally $\lambda \alpha.\Omega^\alpha$, %$0$, $1$ and addition, %$0$, addition and the Veblen function, %$0$, addition and $n$-ary Veblen function or even %add the Sch{\"u}tte Klammer symbols, based on the %basic functions added before. %Now we can see now immediately, that for all these systems %we have $\psi(\epsilon_{\Omega+1})$ (or %$\vartheta(\epsilon_{\Omega+1})$ is the BHO. %First of all, all these systems are above the weakest %where we add only $0$ and addition, which can be seen %in \cite{buchholzanewsys} (Buchholz does not need %$\Omega^\alpha$ since one can simulate %this function by the function $\psi_2$) %to reach the BHO. For $\vartheta$ we have %always that, if $a \in \OT_\psi$, then %(if we replace the symbol $\psi$ by $\vartheta$ %$a \in \OT_\vartheta$ (where $\OT_\psi$ and %$\OT_\vartheta$ are the notation systems based %on $\psi$, $\vartheta$ respectively) and %we have for $a,b \in \OT_\psi$, $a \prec_\psi b \Iff %a \prec_\vartheta b$, and therefore the ordertype %of $\OT_\varphi$ is less than the ordertype of $\OT_\psi$ %(In \cite{rathjenweiermann} one can find %a more precise calculation). %For the other versions we see that we %can interpret the system built from $0$, $+$ and %$\lambda \alpha.\Omega^\alpha$ ($\psi$ or $\vartheta$-version) %into it in the same way as the interpretation of the %$\psi$-system into the $\vartheta$-system and get %again a lower bound.\par %For the upper bound one sees just, that all variations can %be generated by an elementary OS: We take always as %$\Arg$ $\T$ and order the $\psi$ (or $\vartheta$-terms) as %before above all other notations and order them with %respect to the arguments of it and the nested lexicographic %ordering. Now only the terms generated by %the basic functions need to be ordered, %$0$ will be always the least element. In %case of the function addition (in normal form) %(with notations being $(a_1 ,\ldots, a_m)$ %for $a_1 +\cdots+ a_m$), we have to work %a little bit, since we have here the lexicographic %ordering on weakly descending sequences, $\TI$ on which %does not reduce to $\TI$ on the underlying ordering. However, %we can replace this by %by tupels $(a_1,m_1 ,\ldots, a_m,m_m)$, where %$m_i$ are of the form $\Succ^k(0)$ and the %sequence $a_1 ,\ldots, a_m$ are strictly %descending, as a notation for %$a_1 \cdot m_1 +\cdots+ a_m \cdot m_m$ and have %to add the successor function. %Let $\nat ':= \{ S^k(0) \mid k \in \omega \setminus \{ 0 \} \} $ %ordered as is $\omega$. %Order now the initial %functions by %$S(\OT_m) \preccirc (\OT_m \cdot \nat'_-)_{\des}^\ast$ %we get an elementary OS from below and the underlying %notation system is (in $\PRA$ provable) isomorphic %to the original one. %If we have apart from addition the $\varphi$-function, %the $\phi$-terms will be ordered above the addition terms %and ordered lexicographically, if we have %additionally the Klammer symbols they will be ordered %above all other functions and ordered by lexicographic ordering %on descending sequences based on lexicographic ordering of %pairs. That we have an OS can now be in all cases verified easily. \section{$n$-times Iterated Ordinal Systems} \laprint{sectniterate} \subsection{Introduction} The usual way of getting beyond the Bachmann-Howard ordinal is to violate condition (OS 1), which was the basis for our analysis in the last two sections of \cite{setzvenedig}. However, the foundationally more interesting approach seems to keep the condition that the ordinals are built from below and instead weaken the requirement that $\TI$ over $\prec '$ reduces to $\TI$ over $\prec$ in an elementary way, namely in $\PRA$.\par If we look at the OS corresponding to Example \refcom{exmplordfun}k we can see that we generated by meta recursion a sequence of matrices of increasing complexity. We can replace this meta recursion by using a second OS: Let $\calF_0:=(\T_0,\prec,\prec',\k,\length)$ be the primitive recursive (but non-elementary) OS based on $\calO$, defined by the method used in Lemma \ref{theoexampleos}. Let $\T_1:= \{ A \mid \phibar(A) \in \T_0 \}$ with the ordering $A \prec_1 A' :\Iff \phibar(A) \prec' \phibar(A')$. Define $\k_{0,j}: \T_0 \ar_\omega \T_j$ for $i,j=0,1$ by: $\k_{0,0}:= \k$, $\k_{0,1}(\Sigmabar'(\avec)):= \emptyset$, $\k_{0,1}(\phibar(A)):= \{ A \}$ and let for $D \subseteq \T_0$, $E \subseteq \T_i$, $D \restriction_{0,j}E:= \k_{0,j}^{-1}(E)$. Then if $B \subseteq \T_0$, $C \subseteq \T_1$ are well-ordered w.r.t. $\prec$, $\prec_1$, then $(\T_0 \restriction_{0,0} B) \restriction_{0,1} C$ is well-ordered. If we take as $C$ the set of matrices built from notations in $B$ only and, if we know that $C$ is well-ordered, then $\T_0 \restriction_{0,0} B = (\T_0 \restriction_{0,0} B) \restriction_{0,1} C$ is well-ordered, and we have shown that $\calF_0$ is an OS.\par Now in order to show that $C$ is an well-ordered we use a second OS: Define $\k_{1,i}: \T_1 \ar_\omega \T_i$ by: if $a \in \T_0$, $\k_{1,0}(a) := \{ a \}$, $\k_{1,1}(a):= \emptyset$, and if $A = {a_1 \cdots a_m \choose A_1 \cdots A_n}$, then %\left (\begin{array}{ccc} \alpha_1 &\cdots&\alpha_m \\ %A_1 &\ldots&A_m \end{array}\right)$, then $\k_{1,0}(A):= \{ a_1 ,\ldots, a_n \} \cup \bigcup_{j=1}^m \k_{1,0}(A_j)$, $\k_{1,1} (A):= \{ A_1 ,\ldots, A_m \}$ and define $C\restriction_{1,j}D$ as before. Let $\calF_1:= (\T_1,\k_{1,1},\prec ',\prec ',\length)$. and for $B \subseteq \T_0$ $\calF_1[B]:= (\T_1 \restriction_{1,0} B,\prec_1,\prec_1,\k_{1,1},\length)$. If $B$ is $\prec$-well-ordered, then $\calF_1[B]$ is now an ordinal system, and therefore $C:= \T_1 \restriction_{1,0}B$ is well-ordered and with this $C$ the above holds.\par $\calF_1$ is a system which internalizes what was before meta-induction. It is a relatively weak OS which is the relativized extension of the OS for the Cantor normal form. Expanding the OS we introduced in the last section we can get now more complex ``matrices'', which can be used by the first OS. As before, we will exhaust the strength of this concept (which will be called $2$-OS) by using the hierarchy of extended Klammer symbols. In order to go beyond this, we can iterate the step from OS to $2$-OS once more and yield $3$-OS, $4$-OS etc. We are going to formalize in the following $n$-OS for arbitrary natural numbers $n$.\par % % % % \subsection{$n$-Ordinal Systems} In the example before we had as basic structures two ordinal structures $\calF_j:=(\T_j,\prec_j,\break \prec_j',\k_{j,j},\length_j)$ ($j=0,1$) together with functions $\k_{i,1-i}:\T_i \ar_\omega \T_{1-i}$. It can be visualized as follows:\\ \noindent%%% %%% begin pic4.pictex \font\thinlinefont=cmr5 % \begingroup\makeatletter\ifx\SetFigFont\undefined % extract first six characters in \fmtname \def\x#1#2#3#4#5#6#7\relax{\def\x{#1#2#3#4#5#6}}% \expandafter\x\fmtname xxxxxx\relax \def\y{splain}% \ifx\x\y % LaTeX or SliTeX? \gdef\SetFigFont#1#2#3{% \ifnum #1<17\tiny\else \ifnum #1<20\small\else \ifnum #1<24\normalsize\else \ifnum #1<29\large\else \ifnum #1<34\Large\else \ifnum #1<41\LARGE\else \huge\fi\fi\fi\fi\fi\fi \csname #3\endcsname}% \else \gdef\SetFigFont#1#2#3{\begingroup \count@#1\relax \ifnum 25<\count@\count@25\fi \def\x{\endgroup\@setsize\SetFigFont{#2pt}}% \expandafter\x \csname \romannumeral\the\count@ pt\expandafter\endcsname \csname @\romannumeral\the\count@ pt\endcsname \csname #3\endcsname}% \fi \fi\endgroup \mbox{\beginpicture \setcoordinatesystem units <0.900000cm,0.90000cm> \unitlength=1.00000cm \linethickness=1pt \setplotsymbol ({\makebox(0,0)[l]{\tencirc\symbol{'160}}}) \setshadesymbol ({\thinlinefont .}) \setlinear % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 4.029 21.605 3.810 21.749 3.935 21.519 / % \circulararc 48.455 degrees from 4.286 20.320 center at 2.461 20.505 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 2.801 22.566 2.540 22.543 2.781 22.441 / % \circulararc 46.397 degrees from 3.810 21.749 center at 2.249 20.664 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 4.502 21.918 4.286 22.066 4.407 21.834 / % \circulararc 43.003 degrees from 4.921 20.320 center at 2.387 20.387 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) \circulararc 61.928 degrees from 4.286 22.066 center at 3.016 20.849 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 10.102 21.873 9.842 21.907 10.056 21.755 / % \circulararc 46.997 degrees from 11.430 20.320 center at 8.811 19.288 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 7.722 22.565 7.461 22.543 7.702 22.440 / % \circulararc 11.812 degrees from 9.842 21.907 center at 5.583 10.716 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 9.627 22.402 9.366 22.384 9.605 22.277 / % \circulararc 54.913 degrees from 12.065 20.320 center at 8.730 18.755 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 7.706 22.635 7.461 22.543 7.721 22.508 / % \circulararc 22.620 degrees from 9.366 22.384 center at 8.017 17.701 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 2.769 22.669 2.540 22.543 2.802 22.546 / % \circulararc 29.680 degrees from 7.461 22.543 center at 5.001 13.256 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 4.691 22.190 4.921 22.066 4.776 22.284 / % \circulararc 61.928 degrees from 4.921 22.066 center at 3.334 20.320 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 5.673 20.578 5.715 20.320 5.799 20.568 / % \circulararc 58.395 degrees from 5.715 20.320 center at 3.756 20.483 % % Fig POLYLINE object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) \putrule from 2.540 24.130 to 2.540 20.320 %\putrule from 2.540 20.320 to 6.350 20.320 \putrule from 2.540 20.320 to 7.779 20.320 % % Fig POLYLINE object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) \putrule from 10.160 24.130 to 10.160 20.320 %\putrule from 10.160 20.320 to 13.970 20.320 \putrule from 10.160 20.320 to 15.081 20.320 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T_1,<_1')$} [lB] at 2.699 23.495 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T_2,<_2')$} [lB] at 10.319 23.495 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T_1,<_1)$} [lB] at 6.191 20.479 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T_2,<_2)$} [lB] at 13.176 20.479 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 2.223 22.543 \put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 2.023 22.543 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$r$} [lB] at 4.286 20.003 \put{\SetFigFont{12}{14.4}{rm}$r$} [lB] at 3.986 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$s$} [lB] at 4.921 20.003 \put{\SetFigFont{12}{14.4}{rm}$s$} [lB] at 4.621 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 5.715 20.003 \put{\SetFigFont{12}{14.4}{rm}$t$} [lB] at 5.415 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$u$} [lB] at 11.430 20.003 \put{\SetFigFont{12}{14.4}{rm}$u$} [lB] at 11.130 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$v$} [lB] at 12.065 20.003 \put{\SetFigFont{12}{14.4}{rm}$v$} [lB] at 11.765 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$k_{1,1}$} [lB] at 3.886 21.273 \put{\SetFigFont{12}{14.4}{rm}$k_{1,1}$} [lB] at 3.886 21.273 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k_{1,2}$} [lB] at 7.461 22.860 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k_{1,1}(t)=$} [lB] at 0.318 22.241 %\put{\SetFigFont{12}{14.4}{rm}$k_{1,1}(t)=$} [lB] at 0.318 21.749 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm} $\{r,s\}$} [lB] at 0.318 21.749 %\put{\SetFigFont{12}{14.4}{rm} $\{r,s\}$} [lB] at 0.318 21.241 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k_{1,2}(t)=$} [lB] at 0.318 21.033 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm} $\{u,v\}$} [lB] at 0.318 20.525 \linethickness=0pt \putrectangle corners at 0.318 24.155 and 13.995 19.952 \endpicture} % % % %%%%begin pic5.pictex \noindent \font\thinlinefont=cmr5 % \begingroup\makeatletter\ifx\SetFigFont\undefined % extract first six characters in \fmtname \def\x#1#2#3#4#5#6#7\relax{\def\x{#1#2#3#4#5#6}}% \expandafter\x\fmtname xxxxxx\relax \def\y{splain}% \ifx\x\y % LaTeX or SliTeX? \gdef\SetFigFont#1#2#3{% \ifnum #1<17\tiny\else \ifnum #1<20\small\else \ifnum #1<24\normalsize\else \ifnum #1<29\large\else \ifnum #1<34\Large\else \ifnum #1<41\LARGE\else \huge\fi\fi\fi\fi\fi\fi \csname #3\endcsname}% \else \gdef\SetFigFont#1#2#3{\begingroup \count@#1\relax \ifnum 25<\count@\count@25\fi \def\x{\endgroup\@setsize\SetFigFont{#2pt}}% \expandafter\x \csname \romannumeral\the\count@ pt\expandafter\endcsname \csname @\romannumeral\the\count@ pt\endcsname \csname #3\endcsname}% \fi \fi\endgroup \mbox{\beginpicture \setcoordinatesystem units <0.90000cm,0.90000cm> \unitlength=1.00000cm \linethickness=1pt \setplotsymbol ({\makebox(0,0)[l]{\tencirc\symbol{'160}}}) \setshadesymbol ({\thinlinefont .}) \setlinear % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 7.555 22.406 7.779 22.543 7.517 22.527 / % \circulararc 18.325 degrees from 7.779 22.543 center at 9.446 17.224 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 6.011 21.559 6.191 21.749 5.943 21.667 / % \circulararc 25.361 degrees from 6.191 21.749 center at 8.652 17.859 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 9.913 22.932 10.160 23.019 9.901 23.058 / % \circulararc 11.812 degrees from 10.160 23.019 center at 11.271 11.271 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 11.109 21.856 10.954 22.066 10.992 21.807 / % \circulararc 14.250 degrees from 11.430 20.320 center at 4.207 19.288 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 10.398 22.909 10.160 23.019 10.318 22.810 / % \circulararc 22.620 degrees from 10.954 22.066 center at 8.176 20.558 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 10.418 23.066 10.160 23.019 10.409 22.939 / % \circulararc 45.667 degrees from 11.430 22.384 center at 10.041 21.193 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 11.629 22.214 11.430 22.384 11.526 22.140 / % \circulararc 36.870 degrees from 12.065 20.320 center at 8.652 20.399 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 12.460 22.172 12.700 22.066 12.538 22.272 / % \circulararc 34.432 degrees from 12.700 22.066 center at 9.893 18.444 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % arrow head % \plot 14.084 20.484 14.287 20.320 14.185 20.561 / % \circulararc 10.389 degrees from 14.287 20.320 center at 3.889 12.462 % % Fig CIRCULAR ARC object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % arrow head % \plot 4.857 21.453 5.080 21.590 4.819 21.574 / % \circulararc 36.870 degrees from 5.080 21.590 center at 6.112 18.336 % % Fig POLYLINE object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) \putrule from 2.540 24.130 to 2.540 20.320 \putrule from 2.540 20.320 to 7.779 20.320 % % Fig POLYLINE object % \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) \putrule from 10.160 24.130 to 10.160 20.320 \putrule from 10.160 20.320 to 15.081 20.320 \linethickness= 0.500pt \setplotsymbol ({\thinlinefont .}) % % Fig INTERPOLATED PT SPLINE % \plot 5.080 21.590 5.196 21.642 5.303 21.690 5.403 21.734 5.496 21.775 5.581 21.813 5.661 21.848 5.734 21.880 5.802 21.909 5.922 21.960 6.025 22.002 6.114 22.037 6.191 22.066 6.298 22.104 6.422 22.145 6.492 22.167 6.568 22.191 6.650 22.216 6.739 22.243 6.836 22.272 6.941 22.303 7.055 22.336 7.179 22.372 7.244 22.391 7.312 22.410 7.383 22.430 7.456 22.451 7.533 22.473 7.612 22.495 7.694 22.519 7.779 22.543 / % % arrow head % \plot 7.551 22.412 7.779 22.543 7.517 22.535 / % % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T_1,<_1')$} [lB] at 2.699 23.495 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T_2,<_2')$} [lB] at 10.319 23.495 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$(T_1,<_1)$} [lB] at 6.191 20.479 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k_{2,1}(w)=$} [lB] at 0.318 22.241 %\put{\SetFigFont{12}{14.4}{rm}$k_{2,1}(w)=$} [lB] at 0.318 21.749 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm} $\{r,s\}$} [lB] at 0.318 21.749 %\put{\SetFigFont{12}{14.4}{rm} $\{r,s\}$} [lB] at 0.318 21.241 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k_{2,2}(w)=$} [lB] at 0.318 21.033 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm} $\{u,v\}$} [lB] at 0.318 20.525 % % Fig TEXT object % %%%\put{\SetFigFont{12}{14.4}{rm}$(T_2,<_2)$} [lB] at 14.446 20.479 \put{\SetFigFont{12}{14.4}{rm}$(T_2,<_2)$} [lB] at 14.087 21.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$w$} [lB] at 9.842 23.178 \put{\SetFigFont{12}{14.4}{rm}$w$} [lB] at 9.692 23.198 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$r$} [lB] at 3.334 20.003 \put{\SetFigFont{12}{14.4}{rm}$r$} [lB] at 3.234 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$s$} [lB] at 4.763 20.003 \put{\SetFigFont{12}{14.4}{rm}$s$} [lB] at 4.663 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$u$} [lB] at 11.430 20.003 \put{\SetFigFont{12}{14.4}{rm}$u$} [lB] at 11.330 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$v$} [lB] at 12.065 20.003 \put{\SetFigFont{12}{14.4}{rm}$v$} [lB] at 11.965 20.003 % % Fig TEXT object % %\put{\SetFigFont{12}{14.4}{rm}$w$} [lB] at 14.287 20.003 \put{\SetFigFont{12}{14.4}{rm}$w$} [lB] at 14.187 20.003 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k_{2,2}$} [lB] at 11.271 21.273 % % Fig TEXT object % \put{\SetFigFont{12}{14.4}{rm}$k_{2,1}$} [lB] at 4.445 21.907 \linethickness=0pt %\putrectangle corners at 0.318 24.155 and 15.107 19.964 %\putrectangle corners at 0.318 24.155 and 13.995 19.952 \endpicture} % % % \noindent For simplicity assume $\T_0 \cap \T_1 = \emptyset$ and write $\prec$, $\prec '$, $\length$ instead of $\prec_j$, $\prec_j'$, $\length_j$ and write $\restriction_j$ instead of $\restriction_{i,j}$ as defined before.\par In the example $\calF_j$ fulfilled all conditions of an OS except (OS 4). We used that, if $A \subseteq \T_0$, $B \subseteq \T_1$ are well-ordered, then $(\T_0 \restriction_0 A) \restriction_1 B$ is $\prec '$-well-ordered. In order to have that $\calF_1[A]$ is an OS, we need as well that under the same conditions for $A$, $B$ $(\T_1 \restriction_0 A) \restriction_1 B$ is well-ordered. Further we needed that $(\T_0 \restriction_0 A) \restriction_1 (\T_1 \restriction_0 A) = \T_0 \restriction_0 A$ for all $A \subseteq \T_0$. Only $\supseteq$ needs to be fulfilled, which is equivalent to $\k_{1,0}[\k_{0,1}(a)] \subseteq \k_{0,0}(a)$. In order to get that $\calF_1[A]$ is an OS-structure, we need $\k_{1,1}: \T_1 \restriction_0 A \ar_\omega \T_1 \restriction_0 A$ for all $A \subseteq \T_0$, i. e. $\k_{1,0}[\k_{1,1}(a)] \subseteq \k_{1,0}(a)$. The generalization to $n$-ordinal systems is now straight-forward and we get the following definition: %So we get the following conditions:\\ %\condition{2-\OS\ 1}$\calF_i$ fulfill (OS % 1) and (OS 3)\\ %\condition{2-\OS\ 2}$\length[\k_{i,j}(a)] < \length(a)$ for %$j=0,1$, $a \in \T_i$. %\condition{2-\OS\ 3}$\k_{1,0} \circ \k_{1,1} \subseteq \k_{1,0}$ and %$\k_{1,0} \circ \k_{0,1} \subseteq \k_{0,0}$.\\ %\condition{2-\OS\ 4}If $A_i \subseteq \T_i$ are $\prec$-well-ordered, %$(\T_j \restriction_0 A_0) \restriction_1 A_1$ are %$\prec'$-well-ordered.\\ % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{definition}{\rm \laprint{defnos} \begin{enumerate} \ssubitem a An \underlinedef{$n$-times iterated Ordinal-System-structure}, in short \underlinedef{$n$-OS-struc-}\break \underlinedef{ture} is a triple $\calF = ((\calG_i)_{i < n},(\k_{i,j})_{i,j < n}, (\length_i)_{i < n})$ such that $\calF_i:= $\\ $(\calG_i,\k_{i,i},\length_i)$ are OS-structures and $\k_{i,j}: \T_i \ar_\omega \T_j$ ($i,j-1$ $\k_{j,-1} \circ \k_{i,j} \subseteq \k_{i,-1}$ and such that $\calF$ fulfills the conditions of an $n$-OS except for condition$(n-\OS\ 3)$, which is replaced by: if $A_i\subseteq \T_i$ are $\prec$-well-ordered ($-1 \leq i0$) is less than $|\ID_n| = \psi_{\Omega_1}(\epsilon_{\Omega_i +1})$ ($\psi$ as in \cite{buchholzasimplified}). \end{theorem} % % % {\bf Proof:}\\ By Lemma \refcom{nosisos}e and, since the strength of $\kpomega$ extended by the existence of $n-1$ admissibles is $|\ID_n|$.\QED\par \medskip % % %From the well-ordering proof before we get the following procedure, which %shows the well-ordering of all $\T_i$ in a way, which is completely from below: %We start by defining $a_{\alpha_0} \in \T_0$ as for an OS. However, %in order to get a well-defined definition we need that %$\T_1 \restriction A_{\alpha_0},\ldots, \T_n \restriction A_{\alpha_0}$ %are well-ordered. So before defining $a_{\alpha_0}$, we will %we start a subprocess in which we enumerate in an increasing %order all elements of $\T_i \restriction A_{\alpha_0}$ and %therefore show that they are well-ordered. %We first define $a_{\alpha_0,\alpha_1} \in \T_1$ for the %OS-structre $(\T_1 \restriction_0 A_{\alpha_0},\prec,\prec ',\k_1, %\length)$, using again the process as for OS. %And as before, in order to make it work, we %first define by recursion on $\alpha_2$ %$a_{\alpha_0,\alpha_1,\alpha_2} \in \T_2$ for the OS structure %$((\T_2 \restriction_0 A_{\alpha_0}) \restriction_1 A_{\alpha_0,\alpha_1} , %\ldots $ %etc. Since we have only finitely many OS-structures, eventually %we will arrive at the last OS, enumerate all elements of $\T_{n-1}$ %relativized to the sets defined before, and then can proceed one step %further with the definition of $a_{\alpha_0 ,\ldots, \alpha_{n-2}}$. %Again this process stops and we can %finally proceed with the definition of %$a_{\alpha_0 ,\ldots, \alpha_{n-3}}$ etc. %At the end we get that $A_{\alpha_0,\alpha_1} = %\T_1 \restriction A_{\alpha_0}$ for some $\alpha_1$. %Now we enumerate all elements %of $\T_2 \restriction_0 A_{\alpha_0} %= (\T_2 \restriction_0 A_{\alpha_0}) \restriction_1 A_{\alpha_0,\alpha_1}$, %then of $\T_3 \restriction_0 A_{\alpha_0}$ etc. in the same %way as before and once we have finished we can %select $a_{\alpha_0}$. Now we have to start to define %$a_{\alpha_0+1,\alpha_1}$, $a_{\alpha_0+1,\alpha_1,\alpha_2}$ as before %from scratch.\par %The following Lemma formalizes this argument: %% %% %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%% %% % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% %\begin{lemma} %\laprint{lemintuitnos} %\begin{enumerate} %\ssubitem a Let $\calF$ be an $n$-OS, %$\bot \not \in \T_i$. %Let $\lesstil$ be the following ordering on %$\Ord^n:= \{ (\alpha_0 ,\ldots, \alpha_k) \mid kk$ we conclude %%that $\T_k'\restriction_{i=0}^{k-1} A_{\alpha_1 ,\ldots, \alpha_i}$ %%are well-ordered, therefore the process of defining %%$a_{\alpha_1 ,\ldots, \alpha_{k-1},\gamma}$ is well-defined stops %%for some $\gamma<\omega_1^\ck$ and therefore %%$A_{\alpha_1 ,\ldots, \alpha_{k-1},<\gamma}$ exhausts $\T_k$ %%restricted as before. %% %% %% \subsection{Constructive Well-ordering Proof.} We will give now a proof of Lemma \refcom{nosisos}e which can be formalized even in constructive theories like Martin-L{\"o}f's type theory extended by an at most $n$ times nested ${\mathrm W}$-type or intuitionistic $\ID_n$:\\ Define inductively $\M_i, \Acc_i \subseteq \T_i$: $\M_{i}:= \T_i \restriction_{ji$ and $\k(c) \cap [\Omega_i,\Omega_{i+1}[> \eval(a)$. So we do no longer have $a \notin \NF \ar \eval(a) \in \k(a)$ and the above argument does no longer go through. We will use the easiest way of dealing with these problems: we add only $\eval(c)$ to $\C(a)$, if $\NF(c)$ holds. % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{definition} \laprint{defnOFG}{\rm \begin{enumerate} \ssubitem a An {\em $n$-ordinal function generator}, in short {\em $n$-OFG} is a quadruple $\calO:= (\Arg_i,\k_i, \lrm_i,<_i')_{ii$, and, if $\NF(b)$ and $\k(b) \subseteq M$, then $\eval_j(b) \in \M$. \ssubitem b $\C_i(a) \cap \Omega_{i+1} \segment \Ord$.\\ Therefore especially $\eval_i(a) = \C_i(a) \cap \Omega_{i+1}$ \ssubitem c If $a \in \Arg_i$, then $\eval_i(a) \in [\Omega_i,\Omega_{i+1}[$. \ssubitem{ca} If $a,b \in \NF_i$, then $\eval(a) < \eval(b) \Iff (a <' b \land \k_{i,i}(a) < \eval(b)) \lor \eval(a) \leq \k_{i,i}(b)$.\\ Especially $\eval \restriction \NF_i$ is injective and therefore $\length$ and $\k'_{i,j}$ are well-defined. \ssubitem{cb} If $a \in \Arg[\Cl]_i$, $l \length[\k(a)]$. %\item For every subsets $A_{i,j}$ of $\T_{i,j}$ ($j \geq i-1$) %$f[\{ t \in \T '_{i,j} \mid \all k \geq i-1.\k'_{i,j,k}(t) \subseteq A_{i,k}\}] %= %\{ a \in \Arg \mid \k(a) \subseteq A_{i,i-1} \cup \bigcup_{j \geq i} %\eval_j[f_{i,j}[A_{i,j}]] \} $. %\item If $A_{i,j} \subseteq \T'_{i,j}$, $f_{i,j} \restriction A_{i,j}$ is injective ($j \geq i$), %then $f_{i,j} \restriction \{ t \in \T '_{i,j} \mid \all k \geq i. %\k '_{i,j,k}(t) \subseteq A_{i,k} \} $ %is injective. %\item For $a,b \in \T$ we can determine by a $\Delta$-formula %from $\prec$ and $\approx$ restricted to $\k(a) \cup \k(b)$ %(coded as a finite list) %whether $a,b \in \T '$ and, if this is the %case, whether $a \prec ' b$. %\item $a \in \T_{i,j} \Iff a \in \T '_{i,j}\land f(a) \in \NF \land %\all k \geq i.\k_{i,j,k}(a) \subseteq \T_{i,k}$. %\end{itemize} %Then $\T_{i,j}[a]$, $\T'_{i,j}[a]$ are $\Sigma$-definable %in $a$, $\prec'$, $\prec$, $\approx$ are $\Delta$-definable, %$(\T,\prec,\prec ',\k',\length)$ is a OS based on $\calO$ %and $\eval_i(a) \in [\Omega_i,\Omega_{i+1}[$ for $a \in \Arg_i$. %In this case $\calO$ is called a {\em recursivity based %ordinal system} %\ssubitem b If in case $i=0$ the above holds for %a cardinality based or recursivity based ordinal system %with $\Delta$-definable, %$\Sigma$-definable replaced by primitive recursive (especially %$\T''_{0,j}$ is a primitive recursive subset of $\nat$) and, %in case of cardinality based, with $\Omega_i^\rec$ replaced by %$\Omega_i$, then the conclusion holds as well with $\Sigma$-definable, %$\Delta$-definable replaced by primitive recursive. %\end{enumerate} %\end{lemdef} %% %% %% %{\bf Proof:} The results on $\Sigma$-/$\Delta$-definability %and on primitive recursiveness %follow exactly as in Lemma \ref{defprimresksys}. In order to %show that $\eval_i(a) < \Omega_{i+1}^\rec$, which will be done %by main induction on $n-i$, side-induction on $a \in \Arg_i$, %we show that there exists sets $\C_{i,j}'(a) \subseteq %\T_{i+1,j}$ ($j \geq i$) which are %$\Delta_0$ in $[0,\Omega_i^\rec[$ such that %$\eval_j[f_{i+1,j}[\C_{i,j}'(a)]] = \C_i(f(a)) \cap [\Omega_j^\rec,\Omega_{j+1}^\rec[$, %$j \geq i+1$ and %$\C_{i,i}'(a) = \C_i(f(a)) \cap [0,\Omega_{i+1}^\rec[$. %$\C_{i,j}'(a)$ will be the least collection of sets such that %$[0,\Omega_i^\rec[ \cup \bigcup (\k'_(a) \cap \Omega_{i+1}^\rec) %\cup \lrm(a) \subseteq \C_{i,i}'(a)$, %that if ??? % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% %% %% %\begin{definition} %\laprint{defnOFG}{\rm %Let $\calO$ be a fixed $n$-OFG %\begin{enumerate} %\ssubitem a Define $\T_i \subseteq [\Omega_i,\Omega_{i+1} [$ simultaneousl %for all $i$ by:\\ %If $a \in \Arg_i$, $\NF(a)$, %$\k(a) \subseteq \bigcup_{i1$ or $\beta_m> 1$,}\\ \emptyset&\text{otherwise.}}$\\ $(|\Arg'_i|,\k'_{i},\lrm'_{i},<_{\Arg'_i})$ is a cardinality based $n$-OFG such that\\ $\eval_0(\CNF'_0(\alpha_1 ,n_1 \ldots, \alpha_m ,n_m)) = \omega^{\alpha_1}n_1 +\cdots+ \omega^{\alpha_m}n_m$,\\ $\eval_{i+1}(\CNF'_{i+1}(\alpha_1 ,\beta_1 \ldots, \alpha_m ,\beta_m)) = \Omega_{i+1}^{\alpha_1} \beta_1 +\cdots+ \Omega_{i+1}^{\alpha_m}\beta_m$. \ssubitem b Let $\calS_l$, $\k^l$ be defined as in Example \refcom{exmplordfun}i, but with the restriction to ordinals $< \Omega_{n+1}$ always. Let $\Arg_i'$, $\k_i'$, $\lrm_i'$ be as before, $\calF_i:= \Arg_i' \preccirc \psibar_i(\calS_l)$, $\k_i \restriction \Arg_i':= \k_i'$, $\lrm_i\restriction \Arg_i':= \lrm_i'$, $\k_i(\psibar_i(a)):= \k^l(a)$, $\lrm_i(\psibar_i(a)):= \k^l(a) \cap [\Omega_i,\Omega_{i+1}[$ for $a \in |\calS_l|$. The resulting cardinality based $n$-OFG can be seen as a generalization of the extended Sch{\"u}tte Klammer symbols. \ssubitem c Let $f^n_l: \calS_l \ar \Ord$, $f^n_0(\alpha):= \alpha$, $f^n_{l+1} {\beta_1 \cdots \beta_m \choose A_1 \cdots A_m}:= %\left(\begin{array}{ccc}\beta_1& \cdots&\beta_m\\ %A_1 &\cdots &A_m\end{array} \right):= \Omega_{n}^{f^n_l(A_1)}\beta_1 +\cdots+ \Omega_{n}^{f^n_l(A_m)} \beta_m$. %then one can easily see that in $\calO_i$ %$\eval_{j}(\psi_j(A))= \psi_j(f_i(A))$, where $\psi_j$ is the %generalization of the $\psi$-function in \cite{rathjenweierman} %defined by: %$\C'_i(\delta,\rho):= $ closure of $[0,\Omega_i] \cup \rho$ under %$+$, $\lambda \xi \omega^\xi$, %$\psi_j '$ for $j>i$, $\psi_i$ restricted to ordinals %$\xi < \delta$, $\psi_i(\delta):= %\min \{ \rho \mid \delta \in \C_i(\delta,\rho) \land %\C_i(\delta,\rho) \cap \Omega_{i+1} \subseteq \rho \} $. If we restrict now $\psibar_i(\calS^l)$ to $\psibar_i(A)$ such that $f^n_l(A) \in \C_{\Omega_{i+1}}'(f^n_l(A))$, where $\C_{\Omega_{i+1}}'(a)$ is the $\C$-set for the function $\psi_{\Omega_{i+1}}$ as in \cite{buchholzasimplified}, but with $0$, $+$, $\omega^\cdot$ as basic function, we get $\eval_i(\psibar_i(A)) = \psi_{\Omega_{i+1}} (f^n_l(A))$. Again, with this last modification we get that in the resulting ordinal notation system $\prec_i$ and $\prec_i'$ coincide for terms of the form $\psibar_i(A)$. \end{enumerate} } \end{example} % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{remark} \laprint{remprimreksysn} \begin{enumerate} \ssubitem a The straightforward generalization of Lemma \ref{defprimreksys} holds as well for cardinality based $n$-OFG with the exception that we can conclude that $a \prec b$ is primitive recursive only for $a \in \T$, $b \in \T'$. Further under the assumptions of this generalized lemma the function corresponding to $\k'_{i,j}$, which takes the place of $\k_{i,j}$ in the resulting $n$-OS, is primitive recursive. \ssubitem b In order to replace $\Omega_i$ by $\Omega_i^\rec$ (the $i$ th admissible, starting with $\Omega_0=0$, $\Omega_1 = \omega_1^\ck$) we need some additional conditions, which essentially express that we have terms as in \refact a for the higher number classes and arguments, but based on ordinals in $[0,\Omega_i^\rec[$. They can be developed in a similar way as the conditions in \refact a, but because of lack of space, we omit them here. \end{enumerate} \end{remark} % % % {\bf Proof of \refact a:} As in Lemma \ref{defprimreksys}. Only the primitive recursive determination of $r \prec s$ follows as follows: Note that $\krmhat_{i,j}$ corresponds to $\k_{i,j}^0$. Let for $s \in \T'_i$ $\C^j(s):= \{ r \in \T_j \mid \eval(f(r)) \in \C_i(f(s)) \}$. We determine for $s \in \T'_i$, $r \in \T_j$ such that $\length(r), \length(s) \leq \length(t)$ by recursion on $\length(r)$ primitive recursively whether $r \in \C^j(s)$: If $j< i$, $r \in \C^j(s)$. If $j = i$, $r \in \C^j(s) \Iff r\preceq \krmhat_{i,i}(s) \lor (r \preceq' s \land \all li$, $\k_{i,j}(a) \subseteq \Cl_j$ by main IH. %If $j < i$, then %$\k_{i,j}[\k_{i,i}(a)] \subseteq \k_{i,j}(a) \subseteq \Cl_j$. %By side-IH therefore $\k_{i,i}(a) \subseteq \Cl_i$. %Sinc $\k_{i,j}(a) \subseteq \Cl_j$ for $jk$ (without the restriction to $\beta< \alpha$) and one %of the usual choices of initial functions, then for the resulting %ordinal notation system $\OT'$ we have, that %$\psi_0\epsilon_{\Omega_n+1}$ denotes the same %orderinal as in the system $\OT$ where we have the %restriction. This follows, since %obviously $\OT \subseteq \OT'$ and, if $r,s \in \OT$, %$r \prec s$ in $\OT$ iff $r \prec s$ in $\OT '$, so %the ordertype of $\OT '$ is stronger. But the approximations %of both systems can be seens as part of an elementary $n$-OS %from below, therefore %$\psi_0\epsilon_{\Omega_n+1}$ denotes in both systems an ordinal %$< |\ID_n|$. \section{Transfinitely Iterated Ordinal Systems} \laprint{sectsigmaiterate} \subsection{Definition of $\sigma$-OS} The na{\"{\i}}ve way of extending the approach used in the last section to the transfinite does not work. In the proof of well-ordering of $n$-OS we always reduced well-ordering of an $n$-OS $\calF_n$ to $\calF_n[A]$ for well-ordered sets $A \subseteq \T_0$. If we try this with $n$ replaced by $\omega$, we will reduce the well-ordering of an $\omega$-OS to the well-ordering of an $\omega$-OS, which does not work. In the proof using the accessibility predicate we had to use induction by $n-i$ instead of $i$, and this induction does not work if $n$ is replaced by $\omega$.\par Proof theoretically, when moving to at least $\omega$-iterated OS, we go beyond the strength of $\Pi_1^1-\CA$, so $\Pi^1_1$-arguments, which we used in the intuitive well-ordering proofs there, do no longer work.\par Our proof proceeded in some sense by induction on the lexicographic ordering of $(\T_0 ,\T_1 ,\ldots, T_{n-1} )$. Whereas the lexicographic ordering on tuples of fixed length is well-ordered, if the underlying orderings are, this does no longer hold for tuples of arbitrary length. However, for sequences descending along some well-ordering this holds. The solution for our problem is now the following: Introduce a function $\level:\T_\mu \ar \L$, where \break $(\L,\prec_\L)$ is an ordering. Let $\T_\mu^{\leq l}$ ($\T_\mu^{\prec l}$) be the restriction of $\T_\mu$ to those $a$ such that $\level_\mu (a) \leq l$ ($\level_\mu (a) \prec_\L l$). Now let $\T_\mu^{\leq l}$ refer to $\T_\nu^{\prec l}$ only (if $\mu < \nu$), i.e. $\level_\nu[\k_{\mu,\nu}(t)]$\break $\prec_\L \level_\mu(t)$ for $\mu < \nu $, and assume $\T_\mu^{\leq l} \segment \T_\mu$, i.e. $r \prec_\mu s \ar \level_\mu(r) \preceq_\L \level_\mu(s)$. Then we will proceed by working on sequences $\T_{\mu_1}^{\leq l_1},\T_{\mu_2}^{\leq l_2} ,\ldots $ such that $l_1 \succ_\L l_2 \succ_\L \cdots$.\par We need now that $(\L,\prec_\L)$ is a well-ordering. But to demand this directly would be a too strong requirement. What suffices is, to have functions $\krmtil_\mu: \L \ar \T_\mu$ such that, if we define $\L \restriction_{\nu<\sigma} B_\nu$ as usual, but referring to $\krmtil_\mu$, well-ordering of $\L \restriction_{\nu<\sigma} B_\nu$ reduces to well-ordering of $B_\nu$. We only need additionally to demand that, if we relativize the sets of terms and the levels to some set $B$, the levels of the terms in the relativized sets are in the relativized set of levels, i.e. $\all a \in \T_\nu.\krmtil_\mu(\level(a)) \subseteq \k_{\nu,\mu}(a)$.\par A last necessary modification is that, since we are no longer introducing first the $n$th OS completely, then the $(n-1)$th OS completely, etc., we need to demand that there is a descend in length when moving to higher components, i.e. $\nu> \mu \ar \length[\k_{\mu,\nu}(r)]< \length(r)$.\par % % % %Somehow our definition of OS corresponds to the definition of %the $\psi$-function as pointed out at the end of last section, %where we close $\C_i(\alpha)$ under the full function %$\lambda \beta.\psi_j(\beta)$ for $j>i$, with no restriction %$\beta < \alpha $. This definition does again not work for the %definition of $\psi_\alpha$ for $\alpha \geq \omega$. One overcomes %this problem by defining the functions $\psi_\alpha$ simultaneously.\par %If we look at the porcess in Lemma \ref{lemintuitnos}, in %its generalization an $\omega$-OS would call now for an $\omega$-OS as a %subprocess and this %gives a loop. We can avoid such a loop, if we bound every of these %processes to run up to some element of a new well-ordering in such %a way that, when we call a subprocess, this subprocess will %be restricted to a smaller element of this well-ordering.\par %For the case of a $\sigma$-times iterated OS, %we start now with a family of OS %$\calF_\alpha = (\calG_\alpha,\k_{\alpha,\alpha})$ for %$\alpha< \sigma$ and functions $\k_{\alpha,\beta}: %\T_\alpha \ar_\omega \T_\nu$. %We add now a new ordered set $(\L, \prec_\L)$ of levels %together with functions $\level_\alpha:\T_\alpha \ar \T_\sigma$ and %component functions $\krmtil_\alpha:\L \ar \T_\alpha$. %The relativization of $\L$ to some well-ordered subsets of %$\T_\alpha$ should be now well-ordered and $\level_\alpha$ should %respect the komponents of its underlying sets: %$\krmtil_\nu(\level_\alpha(r))\subseteq \k_{\alpha,\beta}(r)$; %we can weaken this condition, to %$\krmtil_\nu(\level_\alpha(r))\subseteq \k_{\alpha,\beta}(r) %\cup %\bigcup_{\xi<\sigma} %\krmtil_{\beta}[\level_{\xi}[\k_{\alpha,\xi}(r)]]$, %i.e. the components need essentially %only occur in a heriditarily subterm of $r$.\\ % % % Apart from the conditions stated before we need the (na{\"{\i}}ve) generalization of the conditions for $n$-OS, which will include that for every $a$ only for finitely many $\nu$ $\k_{\mu,\nu}(a) \not = \emptyset$. We can now (although for the concrete examples this is not necessary, but it might be useful in the future) weaken the condition (OS 2) in the sense that if $r \prec_\mu s$, then one new alternative is that $\level_\mu(r) \prec_\L\level_\mu(s)$.\par %There is one more change to be made: %we have to strengthen the closure conditions. %$\Cl_{\calF_\mu } = \T_\mu$ does no longer suffice, since we could %have a term $f_0(f_1(f_2( \cdots$, where %$f_i(f_{i+1}( ,\cdots \in \T_i$ having as only non empty %componentset the set $i+1$th one, which is %$\{ f_{i+1}( ,\cdots \} $. The new condition subsumes the old %condition $\T_\mu = \Cl_{\calF_\mu}$. % % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{assumption} \laprint{assordering} In the following we assume that some well-ordering $(\Sigma,<)$ of order type $\sigma>0$, where $\sigma$ is an ordinal below the Bachmann-Howard ordinal, is given. Let $0= \min_<\Sigma$ We will identify $(\Sigma,<)$ with $\sigma$, writing $\mu < \sigma$ for $\mu \in \Sigma$, $\Omega_\mu$ for $\Omega_{f(\mu)}$, where $f: \Sigma \ar \sigma$ is the order isomorphism, etc.. In the following we assume $\mu,\nu,\xi < \sigma$. (Note that we use the same symbol $<$ as for the ordering on ordinals). \end{assumption} % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{definition}{\rm \laprint{defsigmaos} \begin{enumerate} \ssubitem a A \underlinedef{$\sigma$-times iterated Ordinal-System-structure relative} \underlinedef{to $(\Sigma,<)$}, in short \underlinedef{$\sigma$-OS-structure} is a quadruple\\ $\calF= %%%%(\calGvec,\krmvec,\Lvec,\lengthvec)= ((\calG_\mu),(\k_{\mu,\nu }),(\L,\prec_\L,(\level_\mu), (\krmtil_\mu)),\length_\mu ) $\\ \hbox{\quad\ }$=((\calG_\mu)_{\mu <\sigma },(\k_{\mu,\nu })_{\mu,\nu< \sigma}, (\L,\prec_\L,(\level_\mu)_{\mu<\sigma},(\krmtil_\mu)_{\mu<\sigma}), (\length_\mu)_{\mu<\sigma})$\\ such that, with $\calG_\mu = (\T_\mu,\prec_\mu,\prec'_\mu)$ and $\calF_\mu:= (\calG_\mu,\k_{\mu,\mu},\length_\mu)$, it holds that $\calF_\mu$ are OS-structures, $\k_{\mu,\nu}: \T_\mu \ar_\omega \T_\nu$, $(\L,\prec_\L)$ is an ordering, $\krmtil_\mu: \L \ar_\omega \T_\mu$ and $\level_\mu:\T_\mu \ar \L$ ($\mu,\nu \in \Sigma$).\\ We will always assume that $\T_\mu$ are disjoint and $\L$ is disjoint from $\T_\mu$ and write therefore $\prec$, $\prec'$, $\length$, $\level$ instead of $\prec_\mu$, $\prec'_\mu$, $\length_\mu$, $\level_\mu$ and $\prec$ instead of $\prec_\L$. Let in the following $\calF$ be as above. % % % \ssubitem{ab} If $\calF$ is a $\sigma$-OS-structure as above, $A \subseteq \T_\mu$, $B \subseteq \T_\nu$, $A \restriction_{\nu} B:= A \cap \k_{\mu,\nu}^{-1}[B]$. If $B_\nu \subseteq \T_\nu$ for all $\nu < \xi$, then $A \restriction_{\nu < \xi} B_\nu:= A \cap \bigcap_{\nu < \xi} \k_{\mu,\nu}^{-1}[B_\nu]$. In the same way we define for $A \subseteq \L$ $A \restriction_\nu B$, $A \restriction_{\nu<\xi}B_\nu$, referring to $\krmtil_\nu$ instead of $\k_{\mu,\nu}$. %\ssubitem {ac} In an $\sigma$-ordinal system structure as above we define %for $\mu<\nu<\sigma$, $a \in \T_\mu$, %$\T^{\preceq a}_\nu:= \{ b \in \T_\nu \mid b \prec \k_{\mu,\nu}(a) \lor %\level(b) \prec \level(a) \} $. \ssubitem b A $\sigma$-OS-structure as above is a \underlinedef{$\sigma$-times iterated Ordinal System} relative to $\Sigma$, in short \underlinedef{$\sigma$-OS}, if for all $\mu,\nu,\xi< \sigma$ and $r,s \in \T_\mu$ the following holds\\ \condition{\sigma-\OS\ 1} $\k_{\mu,\mu}(r) \prec r$;\\ \condition{\sigma-\OS\ 2} $\mu \leq \nu \ar \length[\k_{\mu,\nu}(r)]< \length(r)$;\\ \condition{\sigma-\OS\ 3} if $r \prec s$, then $r \preceq \k_{\mu,\mu}(s) \lor r \prec ' s \lor \level(r) \prec \level(s)$;\\ %$ r \preceq \k_{\mu,\mu}(s) \lor (r \prec ' s \land %\all \nu < \sigma.\mu \leq \nu \ar \k_{\mu,\nu}(r) \subseteq \T_\nu^{\preceq s})$. %%$r \preceq \k_{\mu,\mu}(s) \lor (r \prec ' s %\lor \level(r)\prec \level(s)$;\\ %\condition{\sigma-\OS\ 3} $\level[\k_{\mu,\nu}(a)] < %\level(a)$ for all $\mu,\nu$, $a \in \T_\mu$;\\ \condition{\sigma-\OS\ 4} if $\xi < \nu$, then $\k_{\nu,\xi} \circ \k_{\mu,\nu} \subseteq \k_{\mu,\xi}$;\\ \condition{\sigma-\OS\ 5} $\k_{\mu,\xi'}(r) = \emptyset$ for almost all $\xi'< \sigma$;\\ \condition{\sigma-\OS\ 6} if $\mu<\nu$, then $\level[\k_{\mu,\nu}(r)] \prec \level(r)$;\\ \condition{\sigma-\OS\ 7} if $r \prec s$, then $\level(r)\preceq \level(s)$;\\ \condition{\sigma-\OS\ 8} $\krmtil_\nu(\level(r))\subseteq \k_{\mu,\nu}(r)$;\\ \condition{\sigma-\OS\ 9} if $A_\xi \subseteq \T_\xi$ are $\prec$-well-ordered ($\xi< \sigma$), then $(\T_\nu \restriction_{\mu< \sigma}A_\mu, \prec ')$ and \break \conditionbox{} $(\L \restriction_{\mu< \sigma}A_\mu, \prec)$ are well-ordered, too. % % % \ssubitem c A $\sigma$-OS $\calF$ is {\em well-ordered}, if $(\T_0,\prec)$ is (where $0=\min_<{\Sigma}$), and its {\em order type} is that of $(\T_0,\prec)$. It is {\em primitive recursive}, if the involved sets (including $\Sigma$) are primitive recursive subsets of the natural numbers (parameterized in $\Sigma$, i. e. $t \in \T_{\mu}$ is primitive recursive in $t$ and $\mu$), all functions, relations (including $<$) are primitive recursive, the finitely many $\nu$ such that $\k_{\mu,\nu}(a) \not = \emptyset$ can be computed primitive recursively from $\mu$, $\nu$, $a$, and all properties (including linearity of $<$ and that the chosen $\nu$ such that $\k_{\mu,\nu}(a) \not = \emptyset$ are the only ones) except of the well-ordering condition can be shown in primitive recursive arithmetic. It is {\em elementary}, if additionally the well-ordering condition follows in $\PRA$ in the sense of reducibility of transfinite induction in $\PRA$ to transfinite induction on $\{ (\mu,a) \mid \mu < \sigma \land a \in \T_\mu \}$ with the lexicographic ordering $(\mu,a) < (\nu,b) \Iff \mu < \nu \lor (\mu = \nu \land a <_\mu b)$. \ssubitem d ``Two $\sigma$-OS are isomorphic'' is defined as for $n$-OS. \end{enumerate}} \end{definition} % % % {\bf Comparison with $n$-OS.} $n$-OS have now been defined twice, since $\sigma$ can be finite. So more precisely we have to distinguish between ``finite $n$-OS'' and ``transfinite $n$-OS''. However, one can see easily that a finite $n$-OS $\calF$ can be considered as a special cases of a transfinite $n$-OS. Let $\Sigma:= \{ 0 ,\ldots, n-1 \} $, $<$ be the usual ordering on $\Sigma$, $\L:= \{ n-1, n-2 ,\ldots, 0 \} $, $\krmtil_i(j):= \emptyset$, $i \prec j :\Iff j < i$, $\level(r):= i$ for $r \in \T_i$. Replace $\length_i(r)$ by $\length'_i(r):= \max \{ \length_i(r) \} \cup \bigcup_{j \geq i}\length'_j[\k_{i,j}(r)]$ (defined by recursion on $n-i$ side-recursion on $\length(r)$). One can easily see, that, if we extend the structure by the above and replace $\length$ by $\length'$, we get a transfinite $n$-OS. This illustrates again why a na{\"{\i}}ve generalization of $n$-OS to $\omega$-OS does not work: We get the reverse ordering of the natural numbers, which is not well-ordered. % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %\begin{deflemma} %\laprint{lemclosureossigma} %\begin{enumerate} %\ssubitem a %Let $(\calGvec,\krmvec)$ be a $\sigma$-OS, $\mu < \sigma$, %$A_\nu \subseteq \T_\nu$ ($\nu < \mu$), %$\Avec:= (A_\nu)_{\nu<\mu }$. %Let $\M_\nu:= A_\nu$ for $\nu<\mu$, %$\M_\nu:= \bigcap_{\xi<\mu}\k_{\nu,\xi}^{-1}(A_\xi) %\cap \T_\nu$. %For $s \in \T_\mu$, define simultanteously %for all $\nu$ %inductively set $\C^\Avec_\nu(s) \subseteq \T$ by: %If $\nu<\mu$, $\C^\Avec_\nu(s):= A_\nu$.\\ %If $r \in \M_\mu$, $r \preceq \k(s)$, $r \in \C^\Avec_\nu$.\\ %Assume now $r \in \M_\nu$, $\k_{\nu,\xi}(r) \subseteq %\C^\Avec_\xi(s)$ for all $\xi<\sigma$. %If now $\level(r) \prec \level(s)$ %or $\nu = \mu$ and $r \prec ' s$, then %$r \in \C^\Avec_\nu(s)$. %Then $\C^\Avec_\mu(s)= \{ t \in \M_\mu \mid t \prec s \} $, %and for $\mu < \nu $, %$\C^\Avec_\nu(s)= \{ t \in \M_\nu \mid %\level(t) \prec \level(s) \land %\all \xi < \nu. \k_{\nu,\xi}(t) \subseteq %\C^\Avec_\xi(s) \} $, %\ssubitem b %If $C^\Avec_\nu(s)$ is defined as before, $\mu < \nu$, %$r \in C^\Avec_\nu(s)$, then for all $\xi <\nu$ %follows $\k_{\nu,\xi}(r) \subseteq \C^\Avec_\xi(s)$. %\end{deflemma} %% %% %% %{\bf Proof:} \refact a ``$\subseteq$'' Induction on the definition %of $\C^\Avec_\nu(s)$. Assume $t \in \C^\Avec_\nu(s)$ according to induction. %If $\nu>\mu$, the assertion follows by IH. Otherwise, if %$\level(t) \prec \level(s)$ or %$t \preceq_\mu \k_\mu(s)$ the assertion follows as well using the IH. %If $t \prec ' s$, then by $\k_\mu(s) \subseteq %\C^\Avec_\nu(s)$ follows %$\k_\mu(t) \prec ' s$, and therefore %$t \prec s$.\\ %``$\supseteq$'': We show the assertion using %$\T_\nu = \Cl_\nu$ by induction on %$t \in \Cl_\nu$. If $\nu> \mu$, we have for $\xi<\nu$, %$\k_{\nu,\xi}(t) \subseteq \C^\Avec_\xi(s)$, %and for $\nu \leq \xi$ by induction %pon $\xi$ and using $\level_\xi(\k_{\nu,\xi}(t)) \preceq %\level(t)$, $\k_{\xi,\delta}[\k_{\nu,\xi}(t)] %\subseteq \k_{\nu,\delta}(t)$ and the IH that %$\k_{\nu,\xi}(t) \subseteq \C^\Avec_\xi(s)$ and %therefore $t \in \C^\Avec_\xi(s)$. %If $\nu = \mu$ follows from $t \preceq_\mu \k_{\mu,\mu}(s)$, %therefore $t \in \C^\Avec_\mu(s)$ %or $\level (t)\prec \level(s)$ and %as before the assertion or $t \prec ' s$, %and using that $\level_\xi[\k_{\mu,\xi}(t)] %\prec \level(t) \preceq \level(t)$ similarly %as in the case $\mu<\nu$ %$t \in \C^\Avec_\mu(s)$.\par %\refact b Immediate by induction on the definition %% % % % \subsection{Constructive Well-ordering Proof.} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{theorem} \laprint{theoremstrengthesigmaos} \begin{enumerate} \ssubitem a Every $\sigma$-OS is well-ordered. \ssubitem b Every elementary $\sigma$-OS has order type below $|\ID_{\sigma}|= \psi(\epsilon_{\Omega_\sigma+1})$. \end{enumerate} \end{theorem} % % % {\bf Proof:} \refact a: Define by recursion on $\mu \in \Sigma$ inductively $\M_\mu, \Acc_\mu \subseteq \T_\mu$:\\ $\M_{\mu}:= \T_\mu \restriction_{\nu < \mu}\Acc_\nu$, $\Acc_\mu:= \Acc_{\prec}(\M_\mu)$.\\ $\Acc_\mu':= \T_\mu \restriction_{\nu < \sigma} \Acc_\nu$, $\Acc_\L':= \L \restriction_{\nu < \sigma \Acc_\nu}$.\\ Further, if $l \in \L$, $A \subseteq \T_\mu$ $A^{\preceq l}:= \{ x \in A \mid \level(x) \preceq l \} $, similarly we define $A^{\prec l}$.\\ $(\Acc_\mu,\prec)$, $(\Acc_\mu',\prec')$ and $(\Acc_\L',\prec)$ are well-ordered.\\ We show by induction on $l \in \Acc_\L'$ $$\all l \in \Acc_\L'. \all \mu < \sigma . \M_\mu^{\preceq l} \subseteq \Acc_\mu \enspace ,$$ and assume $l$ according to induction.\\ We show $$\all s \in {\Acc_\mu'}^{\preceq l}.s \in \Acc_\mu$$ by (side-)induction on $(\Acc_\mu',\prec')$ and assume $s$ according to induction:\\ $s \in \M_\mu$. We define $\C^\nu(s) \subseteq \T_\nu$ ($\nu<\sigma$):\\ For $\nu<\mu$, $\C^\nu(s):= \Acc_\nu$.\\ $\C^\mu(s):= \{ r \in \M_\mu \mid r \prec s \} $.\\ If $\mu<\nu$, $\C^\nu(s):= \{ r \in \T_\nu \mid \level(r) \prec \level(s)\land \all \xi < \nu.\k_{\nu,\xi}(r) \subseteq \C^\xi(s) \} $.\\ Note that by ($\sigma$-OS 4) for $\nu>\mu$\\ $\C^\nu(s)= \{ r \in \T_\nu \mid \level(r) \prec \level(s) \land \all \xi < \mu(\k_{\nu,\xi}(r) \subseteq \Acc_\xi) \land \k_{\nu,\mu}(r) \prec s \land $\\ \hbox{\qquad \qquad\ }$\all \xi(\mu < \xi < \nu \ar \level[\k_{\nu,\xi}(r)] \prec \level(s)) \}$.\\ The last equation allows to define $\C^\nu(s)$ in $|\ID_\sigma|$ as needed in \refact b.\\ % % % We prove \fornum{\all \nu(\mu \leq \nu \ar \all \xi < \sigma. \k_{\nu,\xi}[\C^\nu(s)]\subseteq \C^\xi(s))}{$\ast$}% \noindent by induction on $\xi$:\\ For $\xi < \nu$ this follows by the definition of $\C^\nu(s)$. Otherwise for $\xi'<\xi$, $\k_{\xi,\xi'}[\k_{\nu,\xi}[\C^\nu(s)]] \subseteq \k_{\nu,\xi'}[\C^\nu(s)] \subseteq \C^{\xi'}(s)$ by IH. Let $r \in \C^\nu(s)$. In case $\mu = \nu = \xi$ we have $\k_{\nu,\xi}(r) \prec r \prec s$ and, if $\mu < \xi$, it follows $\level[\k_{\nu,\xi}(r)] \preceq \level(r) \preceq \level(s)$, and one of the $\preceq$ is actually $\prec$, so in both cases we get the assertion.\\ % % %\fornum{\all \nu.\mu \leq \nu\ar %\all r \in \T_\nu.r \in \C^\nu(s) \ar \all \xi. %\krmtil_\xi(\level(r))\subseteq \C^\xi(s)}{$\ast \ast $}% %follows now by induction on $\length(r)$ simultaneously for %all $\nu$, using \\ %$\krmtil_\xi[\level[\C^\nu(s)]] %\subseteq \k_{\nu,\xi}[\C^\nu(s)] %\cup \bigcup_{\delta < \sigma} %\krmtil_{\xi}[\level[\k_{\nu,\delta}[\C^\nu(s)]]]$ %and $(\ast)$.\\ %% We show by (side-side-)induction on $\length(r)$ simultaneously for all $\nu$ $$\all \nu.\all r \in \C^\nu(s) .r \in \Acc_\nu$$ and assume $r$ according to induction, $r \in \C^\nu(s)$. If $\nu < \mu$, $r \in \Acc_\nu$. Assume $\mu \leq \nu$. By side-side-IH and $(\ast)$ follows for all $\xi$, $\k_{\nu,\xi}(r) \subseteq \Acc_\xi$ and $\krmtil_\xi(\level(r)) \subseteq \k_{\nu,\xi}(r) \subseteq \Acc_\xi$, $r \in \Acc_\nu'$, $\level(r) \in \Acc_\L'$.\\ If $\mu = \nu$, $r \prec s$, $r \preceq \k_{\mu,\mu}(s) \subseteq \Acc_\mu$, $r \in \M_\mu$, $r \in \Acc_\mu$ or $r \prec ' s$, $r \in \Acc_\mu '$, $\level(r) \preceq \level(s) \preceq l$, and by side-IH $r \in \Acc_\mu$, or $\level(r) \prec \level(s)$ and as in the next case ``$\mu < \nu$'' follows the assertion.\\ If $\mu < \nu$, $\level(r) \prec \level(s) \preceq l$, $\level(r) \in \Acc_\L'$, $r \in \M_\nu$, by main IH $r \in \Acc_\nu$.\\ Now follows $\all r \in \M_\mu(r \prec s \ar r \in \Acc_\mu)$, and, since $s \in \M_\mu$, $s \in \Acc(\M_\mu) = \Acc_\mu$, and the side-induction is complete.\\ Now by induction on $\length(s)$ it follows $\all s \in \M_\mu^{\preceq l}. s \in \Acc_\mu$: If $s \in \M_\mu^{\preceq l}$ we first show $\all \nu.\k_{\mu,\nu}(s) \subseteq \Acc_\mu$. For $\nu< \mu$ this follows by assumption. For $\mu \leq \nu$ we show this by induction on $\nu$. With the usual argument we get using the IH $\k_{\mu,\nu}(s) \subseteq \M_\nu^{\preceq l}$, and therefore by IH $\k_{\mu,\nu}(s) \subseteq \Acc_\nu$. Therefore $s \in \Acc'_\mu$ and by the proven statement of the side-induction it follows $s \in \Acc_\mu$. Therefore the main-IH is completed.\\ Now follows by induction on $\length(r)$, simultaneously for all $\mu$, $\all r \in \T_\mu(r \in \Acc_\mu \land \level(r) \in \Acc'_\L)$: By IH $\k_{\mu,\nu}(r) \subseteq \Acc_\nu$, $\krmtil_{\nu}(\level(r)) \subseteq \Acc_\nu$, $\level(r) \in \Acc'_\L$, $r \in \M_\mu^{\preceq \level(r)}$, $r \in \Acc_\mu$.\\ Therefore it follows $\T_\mu$ is well-ordered and we are done.\par \smallskip \refact b The proof of \refact a can be carried out in $\ID_\sigma$. (Note, that transfinite induction over $\sigma$ is one of the axioms of $\ID_\sigma$).\QED %\smallskip % %\refact c %Again we %start take the system in \cite{buchholzschuettebook} (or %a modified version of \cite{buchholzanewsys}), however %have to change it as follows: %Instead of the function $\lambda\mu.\Omega_\mu$, %we have as basic constants $\Omega_\mu$ for $\mu< \sigma$ %Instead of having the functions $\lambda \mu,\nu.\psi_\mu \nu$ %we define the functions $\lambda \nu.\psi_\mu \nu$ for %all $\nu < \Sigma$. %Correspondingly, we add to the sets $\C_\sigma(\nu)$ %always all $\Omega_\xi$ %and $\psi_\nu \xi$, if $\xi \in \C_\sigma(\mu) \cap \xi$ %and $\nu < \sigma$. From this we define %now the ordinal notation system $\OT'$ (ordinals %below $\sigma$ are denoted by elements of $\Sigma$). %$\OT$ be the set of ordinal notation systems built %from ordinalnotations $\prec \omega_m(\Omega_\sigma+1)$ only, %and let for $\mu \in \Sigma$, %$\T_{\mu}:= \OT \cap [\Omega_{\mu},\Omega_{\mu}[$, %$\T_{\leq \mu}:= \bigcup_{\nu \leq \mu}\T_\nu$. %Let the $\prec'$ on $\T_\mu$ correspond to the %ordering on %$\{ \Omega_\mu \} \preccirc %((\omega^{\T_{\leq \mu}}\cdot \T_{\leq \mu})\restriction \T_\mu) %\preccirc (\psi_\mu(\M) \restriction \T_\mu)$, %where $M:= \Omega_{\sigma} \uparrow(m)\T_{< \sigma}$ %We define $\k: \T_{< \sigma} \ar_\omega \T_{< \sigma}$ by %induction on the length of the terms. %$\k(0):= \k(\Omega_\xi):= \emptyset$, %$\k(\omega^a+b):= \{ a,b \} $, $\k(\psi(a)):= %\krmtil(a)$, $\krmtil$ defined according to defintion %\refcom{defOmegapower}b.\\ %Let $\krmcheck: \T_{<\sigma} \ar_\omega \T_{< \sigma}$ %defined by %$\krmcheck(t):= \k(t) \cup \krmcheck[\k(t)]$.\\ %Now define $\k'_{\mu,\nu}, %\krmcheck'_{\mu,\nu}: \T_\mu \ar_\omega \T_\nu$, %y$\k'_{\mu,\nu}(t) := \k(t) \cap \T_{\nu}$, %$\krmcheck'_{\mu,\nu}(t) := \krmcheck(t) \cap \T_{\nu}$. %Define $\k_{\mu,\nu}; \T_\mu \ar_\omega \T_\nu$, %such that $\k_{\mu,\nu}(t) \subseteq \krmcheck_{\mu,\nu}(t)$ %(and therefore $\k_{\mu,\nu}(t)=\emptyset$ for almost all %$\nu$) by: %$\k_{\mu ,\nu }(t):= %\k'_{\mu ,\nu }(t) \cup \bigcup_{\nu<\xi \in \Sigma} %\k_{\xi ,\nu }[\k_{\mu,\xi}(t)]$. %$\krmvec':= (\k'_{i,j})_{i,j < n}$ %(more precisely this definition is by induction on the %reversed order $<$, which is possible, since %$\k_{\mu,\nu}(t)= \emptyset$ if $\krmcheck'_{\mu,\nu}(t) = \emptyset$.\\ %We define $\L:= M$, and $\prec$ is the ordering induced from $\OT$. %$\krmtil_\mu(t):= \krmtil(t) \cap \T_\mu$.\\ %$\level(t):= \min \{ s \mid t \in \C_\mu(s) \} $, %which can be defined as %$\max \{ s \mid \exists \nu \in \Sigma.\mu \leq \nu \land %\psi_\nu(s) \in \krmcheck(s) \} $ and %one verifies that this is primitive recursive.\\ %We verify, that for the primitive recursive sets %$\C_\mu(s)$ corresponding to the sets $\C_\mu(\nu)$ %we have %$t \in \C_\mu(s) \ar \all \nu < \sigma.\mu \leq \nu %\ar \k_{\mu,\nu}(t) \subseteq \C_\mu(s)$.\\ %We verify, that $((\T_\mu,\prec,\prec '),(\k_{\mu,\nu}), %(\L,\prec,(\krmtil_\mu))$ is a $\sigma$-OS.\\ %($\sigma$-OS 1): For %$r = \sigma$ and $\omega^s+t$ this is clear, %and for $r=\psi_\mu(s)$ this follows %by $s \in \C_\mu(s)$, $\k_{\mu,\mu}(s) \subseteq %\C_\mu(s) \cap \T_\mu \prec \psi_\mu(s)$. %($\sigma$-OS 2)???????????????????????? %($\sigma$-OS 3) follows as in the previous proofs, %($\sigma$-OS 4) was enforced, %($\sigma$-OS 5) since the components of a term have %a smaller length. %($\sigma$-OS 6) is only difficult for the term %$\psi_\mu(r)$, and here we have %$\psi_\mu(r) \not \in \C_\mu(r)$, %$r \in \C_\mu(r)$, therefore $\k_{\mu,\nu}(r) \subseteq %\C_\mu(r)$, $\level[\k_{\mu,\nu}(r)] %\prec r = \level(r)$. ($\sigma$-OS 7) is %easy and ($\sigma$-OS 8) can be verified by induction on the length %of the terms. %In ($\sigma$-OS 9) we verify first %that $\TI$ on $M$ relativezed to $A_\mu$ %reduces to well-ordering of the $A_\mu$ and %of $(\Sigma,<)$, which implies the %condition for the relativization of $\L$ and from which %the assertion for the argument sets follows as usual.\\ %The resulting $\sigma$-OS has now strength %$\psi_0(\omega_n(\Omega_\sigma +1))$ %and that this is in the limit the strength of $|\ID_\sigma|$ %is a fact usually referred to as ``folklore'', although for precisely the %system we have taken it has not been carried through. % % \subsection{$\sigma$-Ordinal Function Generators} The ordinal function generators referring to $\sigma$-OS are now defined similarly as for $n$-OFG. The only difference is that in the definition of $\C_\mu(a)$ we will refer only to $b \in \Arg_\nu$ ($\nu>\mu$) such that $\level_\nu(b)< \level_\mu(a)$, which is the obvious adaption of the principles for $\sigma$-OS to OFG.\par %In the definition of $n$-OFG we could have added to %$\C_n(a)$ $\eval(b)$ only for those $b$ such that %$\NF(b)$ holds and in the definition of $\NF(b)$, %$\k_{n,l}(b)$ ($l> n$) did not play a role, since %$\k_{n,l}(b) \subseteq \C_n(b)$ follows for all $b \in \Cl \cup %\Arg[\Cl]$. In the $\sigma$-OFG, we have to demand %for $\NF(b)$ that $\k_{\mu,\nu}(b) \subseteq \C_\mu(b)$ %for all $\nu \geq \mu$. We need to demand for %adding $\eval(b)$ to $\C_\mu(a)$ that $\NF(b)$ holds, %since we can no longer obtain from $b$ a $c$ such that %$\eval(c)= \eval(b)$ and $\NF(c)$ by moving %to the components of $b$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{definition} \laprint{defsigmaOFG}{\rm \begin{enumerate} \ssubitem a A {\em $\sigma$-ordinal function generator}, in short {\em $\sigma$-OFG} is a triple $\calO:= (\calA,\calL,\krmtil)$, where $\calA= (\Arg_\mu,\k_\mu, \lrm_\mu,<_\mu',\level_\mu)_{\mu<\sigma}$, $\calL = (\L,<_\L)$, $\Arg_\mu$ are classes (in set theory), $\k_\mu,\lrm_\mu: \Arg_\mu \ar_\omega \Ord$, $\level_\mu: \Arg_\mu \ar \L$, $\all a \in \Arg_\mu.\lrm_\mu(a) \subseteq \k_\mu(a)$, $<_\mu'$ is a well-ordered relation on $\Arg_\mu$, $\all a,b \in \Arg_\mu(a <_\mu ' b \ar \level_\mu(a) \leq'_\mu \level_\mu(b))$, $\calL$ is a well-ordering, $\krmtil: \calL \ar_\omega \Ord$, $\all a \in \Arg_\mu.\krmtil[\level_\mu(a)] \subseteq \k_\mu(a)$.\\ We assume in the following that $\Arg_\mu$ and $\L$ are disjoint and omit therefore the index $\mu$ in $\k$, $\lrm$, $<'$, $\level$ and the index $\L$ in $<'$. Let $\calO$ always be as above. \ssubitem b $\Omega_0:= 0$, $\Omega_\mu:= \aleph_\mu$ otherwise. \ssubitem c A $\sigma$-OFG is {\em cardinality based}, if for all $B \subseteq \Ord$ countable $\k_\mu^{-1}(B)$ is countable, $\lrm_\mu(a) \subseteq \k_\mu(a) \cap [\Omega_\mu,\Omega_{\mu+1}[$ and $\all a \in \Arg_\mu.\all \nu>\mu. \level_\nu[\k(a) \cap [\Omega_{\nu},\Omega_{\nu+1}[] < \level_\mu(a)$. In this case we define for $a \in \Arg_\mu$, $\k_{\mu,\nu }(a):= \k(a) \cap [\Omega_\nu,\Omega_{\nu+1}[$ and for $a \in \L$ $\krmtil_\nu(a):= \k(a) \cap [\Omega_\nu,\Omega_{\nu+1}[$. \ssubitem d If $\calO$ as above is a cardinality based $\sigma$-OFG, we define for $a \in \Arg_\mu$ simultaneously for all $\mu<\sigma$ by recursion on $\level_\mu(a) \in \L$, side-recursion on $(<',\Arg_\mu)$, $\eval_\mu(a) \in \Ord$ and subsets $\C_\mu(a) \subseteq \Ord$ by: $\C_\mu(a):= \bigcup_{n=0}^\omega \C_\mu^n(a) $ where \\ $\C_\mu^0(a):= [0,\Omega_\mu[\cup (\bigcup (\k_\mu(a) \cap \Omega_{\mu+1})) \cup \lrm_\mu(a)$,\\ $\C_\mu^{l+1}(a):= \C_\mu^l(a) \cup $\\ \hbox{\qquad \qquad \quad}$ \bigcup_{\nu \geq \mu}\{ \eval_\mu(b) \mid b \in \Arg_\nu, ((\nu = \mu \land b <' a \land \level(b) = \level(a)) \lor$\\ \hbox{\qquad \qquad \quad \qquad \quad}$ (\level(b) < \level(a))) \land \k(b) \subseteq \C_\mu^l(a) \land \NF_\nu(b) \} $,\\ where $\NF_\nu(b):\Iff \k(b) \subseteq \C_\nu(b)$.\\ $\eval_\mu(a):= \min \{ \alpha \mid \alpha \not \in \C_\mu(a) \} $. \ssubitem e Let $\calO$ be a cardinality based $\sigma$-OFG. Referring to the definition of $\NF(b)$ as above and assuming that $\eval \restriction \NF_\mu$ is injective, which will be shown later, $\NF_\mu$, $\Cl_\mu$, $\Cl$, $\Arg[\Cl]_\mu$ and $\Arg[\Cl]$ are defined as in Definition \ref{defnOFG}.\\ Further we define $\k^0_{\mu,\nu},\k'_{\mu,\nu}: \Arg[Cl]_\mu \ar_\omega \Cl_\nu$ by\\ $\k_{\mu,\nu}^0(b):= \eval_\nu^{-1}[\k_{\mu,\nu}(b)] \cap \Cl_\nu$, $\k_{\mu,\nu}'(b):= \k^0_{\mu,\nu}(b) \cup \bigcup_{\nu \leq \xi<\sigma}\k'_{\xi,\nu}[\k^0_{\mu,\xi}(b)]$,\\ $\length$ as in Definition \ref{defnOFG} and $\level'_\mu:\Cl_\mu \ar \L$ by $\level'_\mu(r):= \max \{ \level_\mu(r) \} \cup \level'_\mu[\k_{\mu,\mu}(r)]$. \ssubitem f For $r,s \in \Arg_\mu$ we define $r \prec s :\Iff r \prec_\mu s :\Iff \eval_\mu(r) < \eval_\mu(s)$. %\ssubitem f We define $\level'_\mu: \Cl_\mu \ar \L$ by: %Let simultaneously for $\mu \leq \nu$, $\level'_{\mu,\nu}: %\Cl_\nu \ar \L$ be defined by:\\ %Let for $\nu \geq \mu$, $a \in \Cl_\nu$, $\S_{\mu,\nu}(a):= %\mycases{\S(a)&\text{if }\nu> \mu\\ %a&\text{otherwise.}}$ Then %$\level'_{\mu,\nu}(a):= %\max( \{ \S_{\mu,\nu}(\level_\nu(a)) \} \cup %\bigcup_{\xi \geq \mu } \S_{\mu,\xi}[\level'_{\mu,\xi}[ %\k_{\nu,\xi}(a)]])$.\\ %$\level'_\mu(a):= \level'_{\mu,\mu}(a)$.\\ %Further define for $l \in \L$, $\Cl_{\mu,\nu}^{\leq' l} \subseteq \Cl_\nu$ %simultaneously for all $\nu$ inductively by:\\ %$\Cl_{\mu,\nu}^{\leq ' l} = \Cl_{\nu}$ for $\nu < \mu$.\\ %if $\mu \leq \nu$, %$b \in \Cl_\nu$, $\mu \leq \nu $, %$\k(b) \subseteq %\bigcup_{\mu \leq \nu }\Cl_{\mu,\nu}^{\leq' l}$, %$\level(b) < l \lor (\mu = \nu \land \level(b) = l)$, then %$b \in \Cl^{\leq' l}_\nu$. \end{enumerate}} \end{definition} % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{lemma} \laprint{lemalphaOFG1} Let $\calO$ be a cardinality based $\sigma$-OFG. \begin{enumerate} \ssubitem a Lemma \refcom{lemnOFG1}a - \refsub{lemnOFG1}{cd} holds mutatis mutandis. %\ssubitem b $\C_\mu(a) \cap \Omega_{\mu+1} \segment \Ord$.\\ %Therefore especially $\eval_\mu(a) = \C_\mu(a) \cap \Omega_{\mu+1}$ %\ssubitem c If $a \in \Arg_\mu $, %then $\eval_\mu(a) \in [\Omega_\mu,\Omega_{\mu+1}[$. %\ssubitem {ca} If $\mu \leq \nu$, $a \in \Cl_\nu$, %then $\level'_{\mu,\nu}(a) = %\min \{ l \mid a \in \Cl_{\mu,\nu}^{\leq l} \} $, %especially %$\level'_\mu(a) = \min \{ l \in \L \mid \eval_\mu(a) %\in\Cl_{\mu,\mu}^{\leq l}\}$. %\ssubitem b If $a,b \in \Cl_\mu$, %$\eval_\mu(a) < \eval_\mu(b)$, then $\level'(a) %\leq \level'(b)$. %\ssubitem d For $a,b \in \Arg[\Cl]_\mu$ we have %\begin{eqnarray*} %\eval_\mu(a) < \eval_\mu(b) &\Iff& (a <' b \land \k_{\mu,\mu}(a) %< \eval_\mu(b) \land \all \nu . %(\nu > \mu \ar (\all \xi \in \k_{\mu,\nu}(a) %(\xi < \k_{\mu,\nu}(b) \lor \level(c) < \level(b)))) %\lor \eval_\mu(a) < \k_{\mu,\mu}(b) \lor \eval_{\mu}(a) %\leq \lrm(b) \lor \exists \mu<\nu . \exists \xi % \in \k_{\mu,\nu}(b).\\ %\eval_\mu(a) = \eval_\mu(b) &\Iff& (a <' b \land %\eval_\mu(b) = \max( \k(a)) \land %\eval_i(b) \not \in \lrm(a)) \lor \\ %&& (b <' a \land \eval_i(a) = \max(\k(b)) \land \eval_i(a) \not \in \lrm(b)) \lor \\ %&&a=b %\end{eqnarray*} %\ssubitem e For $a,b \in \Arg_i$, $\NF(a)$, $\NF(b)$ %$\eval_i(a) < \eval_i(b) \iff (a <' b \land (\k(a) \cap \Omega_{i+1}) < %\eval_i(b)) %\lor \eval_i(a) \leq (\k(b) \cap \Omega_{i+1}) $.\\ %Especially: $\eval_i \restriction \{ a \in \Arg.\NF(a) \}$ is %injective. \ssubitem f $\calF:= ((\Cl_\mu,\prec_\mu)_{\mu<\sigma}, (\k'_{\mu,\nu})_{\mu,\nu < \sigma}, (\length_i)_{i \mu$, $\level'_\nu(r) < \level'_\mu(s)$, by main induction on $\length(s)$, side-induction on $\length(r)$, which is immediate.\QED % % % % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{example} \laprint{exmplsigmaofg}{\rm \begin{enumerate} \ssubitem a The straight forward generalization of Example \refcom{exmplnofg}a together with $\L:= \{ 0 \}$, $\krmtil_\mu(0):= \emptyset$, $\level_\mu(a):= 0$ yields a cardinality based $\sigma$-OFG for the Cantor normal form with basis $\omega$ ($\mu=0$) and $\Omega_\mu$ ($\mu>0$). \ssubitem b Example \refcom{exmplnofg}b generalizes again to a cardinality based $\sigma$-OFG with $\L:= \calS_l$ as in Example \refcom{exmplordfun}i, $\krmtil(a):= \k^l(a)$, $\level(\Sigma'_\mu(\tvec)):= 0$ (where $0 := () \in \L$), $\level(\psibar_\mu(A)):= (A)$ (only in case $l=0$ we have to modify $\L$ in order to make it disjoint from $\T_\mu$). The resulting system can be seen as a further generalization of the extended Sch{\"u}tte Klammer symbols. Note that, whereas for $n$-OS for all terms $t= \psibar(A) \in \T'$ it holds $t \in \T$ (in the fixed point free version), this is no longer the case here. \ssubitem c If $f_\sigma^l$ is defined similarly and we apply a similar restriction as in Example \refcom{exmplnofg}c, then we get $\eval_\mu(\psibar_\mu(a)) = \psi_{\Omega_{\mu+1}} (f_\sigma^l(a))$ with $\psi_{\Omega_{\mu+1}}$ the usual $\psi$-function based on $0$, $+$, $\omega^\cdot$. \end{enumerate} } \end{example} % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{remark} \laprint{remremprimreksyssig} Assume the assumptions of the straight forward generalization of Lemma \ref{defprimreksys} to cardinality based $\sigma$-OFG. Additionally assume sets $\Lhat \subseteq \Lhat' \subseteq \Lhat''$ corresponding to $\L$ such that $\Lhat''$ is primitive recursive, a function $f: \Lhat \ar \L$ and primitive recursive functions $\krmhattil_\mu: \Lhat'' \ar_\omega \T_\mu''$, $\levelhat_\mu: \T_\mu'' \ar \Lhat$ corresponding to $\krmtil_\mu$, $\level_\mu$. Define for $l,l' \in \L$, $l \prec_\L l' :\Iff f(l) <_\L f(l')$. Assume the adaption of condition \refsub{defprimreksys}b of Lemma \ref{defprimreksys} for the new structure and \refsub{defprimreksys}a, \refsub{defprimreksys}c - \refsub{defprimreksys}f for $\Lhat$, $\krmhattil$ instead of $\T$, $\krmhat$, where appropriate, and omitting $\NF$. E.g. the adaption of condition \refsub{defprimreksys}d to $\L$ reads: If $A_\mu\subseteq \T'_\mu$, $f \restriction A_\mu$ is injective ($\mu < \sigma$), then $f \restriction \{ t \in \L' \mid \all \mu < \sigma. \krmhattil_\mu(t) \subseteq A_\mu \} $ is injective. Then the conclusion of this lemma generalized to our setting holds as well in the weakened version of Remark \ref{remprimreksysn}, and additionally $\Lhat$, $\Lhat'$, $\prec_\L$ are primitive recursive. \end{remark} % % % {\bf Proof:} As before.\QED % % % % Only the %determination of $r \prec s$, $r \sim s$ follows as follows: %We can determine first for all $r \in \T_\nu %=: \T$, $s \in \T'_\mu$, $\length(r), \length(s) \leq \length(t)$ by %induction on $\length(r)$ whether %$\eval(r) \in \C_\mu(s)$ by having: %if $\nu< \mu$, $\eval(r) \in \C_\mu(s)$. %If $\nu = \mu$, %$\eval(r) \in \C_\mu(s) \Iff \eval(r) \preceq \k_{\mu,\mu}(s) %\lor r \preceq' s \land \k(r) \subseteq \C_\mu(s)$, %and, if $\mu < \nu$ $\eval(r) \in \C_\mu(s) \Iff %\level(r) < \level(s) \land \k(r) \subseteq \C_\mu(s)$. %Then $\eval(r) \prec \eval(s) \Iff \eval(r) \in \C_\mu(s)$ %for $r \in \Arg_\mu$, $s \in \Arg_\nu$. %Now for $t \in \Arg_\mu$ %$\NF(t) \Iff \k(t) \subseteq \C_\mu(t)$, if $t \in \Arg_\mu$. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % \begin{theorem} \laprint{lemexampleossig} \begin{enumerate} \ssubitem a For every OFG in the Example \ref{exmplsigmaofg} there exists an elementary OS based on it. \ssubitem b The supremum of the strength of $\sigma$-OS is $|\ID_\sigma|$. \end{enumerate} \end{theorem} % % {\bf Proof:} As for Theorem \ref{lemexampleosn}.\QED % % % % % % \bibliography{/home/setzer/tex/ordsys/submitted/litbank} \end{document} %%% Local Variables: %%% mode: latex %%% TeX-dvi-file: "ordsys100498b" %%% End: