\documentclass[10pt]{article}
\title{Transfinite ordinals}
\usepackage[left=1cm,right=1cm,top=2cm,bottom=2cm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{amsfonts}
\usepackage{amsmath}
\begin{document}

\title{A Tutorial Overview of Ordinal Notations}
\author{Jacques Bailhache (jacques.bailhache@gmail.com)}
\date{January-February 2018}

\maketitle

\setlength{\parindent}{0pt}

\section{Interest of transfinite ordinal numbers}

The domain of transfinite ordinals has the particularity of being the only mathematical domain that cannot be automated. In all other domains of mathematics, it is at least theoretically possible to deduce the theorems automatically from a formal system consisting of a finite set of axioms and rules. But Gödel proved that given any formal system of a theory sufficiently powerful to contain arithmetics, it is possible to build a proposition that expresses its own unprovability in this formal system. This proposition, which is very huge, has also a meaning as an ordinary arithmetic proposition, but is very useless in ordinary arithmetics. If the formal system is consistent, then this proposition is undecidable. 

At first sight one could think that we just have to add this proposition to the system as an axiom, but this augmented system also have its own Gödelian proposition. By adding successively Gödelian propositions, we obtain an infinite sequence of systems, and the system defined as the union of all these systems also has its Gödelian proposition, and so on. 
But according to Solomon Feferman in "Penrose’s Gödelian argument" http://math.stanford.edu/~feferman/papers/penrose.pdf p.9 : 

"one obtains completeness for all arithmetical sentences in a progression based on the transfinite iteration of the so-called global or uniform reflection principle" 

The uniform reflection principle, which is something similar to adding the Gödelian proposition as an axiom, is described for example in John Harrison's paper "Metatheory and Reflection in Theorem Proving: A Survey and Critique" 

http://www.cl.cam.ac.uk/~jrh13/papers/reflect.ps.gz p.18 : 

\[ \vdash \forall n . Pr(\lceil \phi[n] \rceil) \Rightarrow \phi[n] \]

Harrison also says p.19 : 

"Feferman showed that a transfinite iteration based on it proves all true sentences of number theory". 

So we can say that the construction of transfinite ordinals can store all the creative part of mathematics. 


\section{Defining transfinite ordinal numbers}

Natural numbers can be represented by sets. Each number is represented by the set of all numbers smaller than it.
\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( 0 = \lbrace\rbrace \) (the empty set)
\item \( 1 = \lbrace 0 \rbrace = \lbrace\lbrace\rbrace\rbrace \)
\item \( 2 = \lbrace 0, 1 \rbrace = \lbrace\lbrace\rbrace,\lbrace\lbrace\rbrace\rbrace\rbrace \)
\item \( 3 = \lbrace 0, 1, 2 \rbrace = \lbrace\lbrace\rbrace,\lbrace\lbrace\rbrace\rbrace,\lbrace\lbrace\rbrace,\lbrace\lbrace\rbrace\rbrace\rbrace\rbrace \)
\item ...
\end{itemize}
The successor of a natural number can be defined by \( suc(n) = n+1 = n \cup \lbrace n \rbrace \).

We have \( n \leq p \) if and only if \( n \subseteq p \).

\( \mathbb{N} \) is the set of all natural numbers : \( \mathbb{N} = \lbrace0,1,2,3,\ldots\rbrace \)
The natural numbers can be generalized to what is called "transfinite ordinal numbers", or simply "ordinal numbers" or "ordinals", by considering that infinite sets represent ordinal numbers. \( \mathbb{N} \) considered as an ordinal number is written \( \omega \).
\( \omega \) is the least ordinal which is greater than all the numbers 0, 1, 2, 3, ... We say that \( \omega \) is a limit ordinal and 0, 1, 2, 3, ... is a fundamental sequence of \( \omega \). This is written : \( \omega = sup \lbrace 0, 1, 2, 3, ... \rbrace \) or \( \omega = lim ( n \mapsto n )  \) because the n-th element (starting with 0) of the sequence is n. An ordinal does not have a unique fundamental sequence, for example 1, 2, 3, 4, ... is also a fundamental sequence of \( \omega \), because the least ordinal that is greater than all ordinals of this sequence is also \( \omega \) (more generally the limit ordinal is the same if any number of the least items of a sequence are removed), and the same stands for the sequence 0, 2, 4, 6, ...

Any ordinal can be defined as the least ordinal strictly greater than all ordinals of a set : the empty set for 0, \(\lbrace \alpha \rbrace\) for the successor of \( \alpha \),  \(\lbrace \alpha_0,\alpha_1,\alpha_2,...\rbrace\) for an ordinal with fundamental sequence \(\alpha_0, \alpha_1, \alpha_2, ...\)

The successor can be generalized to transfinite ordinal numbers : \( suc(\omega) = \omega+1 =\omega \cup \lbrace \omega \rbrace = \lbrace 0, 1, 2, 3, \ldots, \omega \rbrace ; suc(suc(\omega)) = \omega+2 = \lbrace 0, 1, 2, 3, \ldots, \omega, \omega+1 \rbrace \) and so on.

Then we can consider the set \( \lbrace 0, 1, 2, 3, \ldots, \omega, \omega+1, \omega+2, \omega+3, \ldots \rbrace \) which is a limit ordinal, and \( \omega, \omega+1, \omega+2, \omega+3, \ldots \) is a fundamental sequence of this ordinal. This ordinal is \( \omega+\omega = \omega \cdot 2 \) or \( \omega \times 2 \) or \( \omega 2 \).

Then we can go on building greater and greater ordinals : \( \omega \cdot 3, \ldots, \omega \cdot \omega = \omega^2, \omega^3, \ldots, \omega^\omega, \omega^{\omega^\omega}, \ldots \).

\bigskip

For natural numbers, arithmetical operations are defined as follows :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item addition : \( a+0=a ; a+suc(b)=suc(a+b) \)

\item multiplication : \( a \cdot 0 = 0 ; a \cdot suc(b) = (a \cdot b) + a \)

\item exponentiation : \( a^0 = 1 ; a^{suc(b)} = a^b \cdot a  \)
\end{itemize}

The definitions of arithmetical operations can be generalized to ordinals by adding canonical rules for limit ordinals :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item addition : \( \alpha+0=\alpha ; \alpha+suc(\beta)=suc(\alpha+\beta); \alpha+lim(f)=lim(n \mapsto \alpha+f(n)) \)

\item multiplication : \( \alpha \cdot 0 = 0 ; \alpha \cdot suc(\beta) = (\alpha \cdot \beta) + \alpha ; \alpha \cdot lim(f) = lim (n \mapsto \alpha \cdot f(n)) \)

\item exponentiation : \( \alpha^0 = 1 ; \alpha^{suc(\beta)} = \alpha^\beta \cdot \alpha ; \alpha^{lim(f)} = lim (n \mapsto \alpha^{f(n)}) \)
\end{itemize}

Note that addition and multiplication are not commutative, for example \( 1+\omega = \omega \neq \omega+1 \), because if we take 0, 1, 2, 3, ... as fundamental sequence of \( \omega \), then a fundamental sequence of \( 1+\omega \) is 1+0, 1+1, 1+2, 1+3, ... = 1, 2, 3, 4, ... and the least ordinal which is greater than all ordinals of this sequence is \( \omega \). We will say that "1+" is "absorbed" by \( \omega \). More generally, we have \( 1+\alpha = \alpha \) for any ordinal \( \alpha \geq \omega \).

\bigskip

For tutorial introductions to transfinite ordinal numbers, see also :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item Madore's introduction in French : 

 http://www.madore.org/\%7Edavid/weblog/2011-09-18-nombres-ordinaux-intro.html

\item Pointless Gigantic List of Infinite Numbers : 

 https://sites.google.com/site/pointlesslargenumberstuff/home/l/pglin?tmpl=\%2Fsystem\%2Fapp\%2Ftemplates\%2Fprint\%2F

\item Sbiis Saibian's !!! FORBIDDEN LIST !!! of Infinite Numbers : 

 https://sites.google.com/site/largenumbers/home/appendix/a/infinite\_numbers



\end{itemize}

\section{Veblen functions}

The next step is the limit or least upper bound of \( \omega, \omega^\omega, \omega^{\omega^\omega}, \ldots \) which is called \( \varepsilon_0 \). Note that we have \( \omega^{\varepsilon_0} = \varepsilon_0 \). We say that \( \varepsilon_0 \) is a fixed point (the least one) of the function \( \alpha \mapsto \omega^\alpha \).

Then we can go on with \( \varepsilon_0+1, \varepsilon_0+2, \ldots, \varepsilon_0+\varepsilon_0 = \varepsilon_0 \cdot 2, \ldots, \varepsilon_0 \cdot \varepsilon_0 = {\varepsilon_0}^2, \varepsilon_0^{\varepsilon_0}, ...\)

The limit of \( \varepsilon_0, \varepsilon_0^{\varepsilon_0}, \varepsilon_0^{\varepsilon_0^{\varepsilon_0}}, \ldots \) is called \( \varepsilon_1 \). It can be shown that it is also the limit of \( \varepsilon_0+1, \omega^{\varepsilon_0+1}, \omega^{\omega^{\varepsilon_0+1}}, \ldots \) (see proof below).

These two fundamental sequences are examples of two ways of ascending ordinals :
\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item Build greater ordinals from known ones by increasing them using operations like successor, addition, multiplication, exponentiation, ... This method is used by the RSH0 notation which we will study later.

\item When we have found a function that, when applied to a given ordinal, gives a greater one (for example \( \alpha \mapsto \omega^\alpha \)), use it ad infinitum starting for example with 0, and then to go further use it ad infinitum starting with the successor of the previous result, and so on. This is called an enumeration of the fixed points of this function. A fixed point of a function f is a value (for example an ordinal) \( \alpha \) with \( f(\alpha) = \alpha \). Under some conditions (see below), the least fixed point of f is the limit of 0, f(0), f(f(0)), f(f(f(0))), ... If it is called \( \alpha \), the next fixed point is the limit of \( \alpha+1, f(\alpha+1), f(f(\alpha+1)), f(f(f(\alpha+1))), \ldots \).
More generally, the least fixed point of f that is greater or equal to \( \zeta \) is the limit of \( \zeta, f(\zeta), f(f(\zeta)), \ldots\).
The Veblen functions use this method.

\end{itemize}

The required conditions are described for example in http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/Fruitful.pdf page 8 lemma 3.9 : 

For each fruitful function f and each ordinal \( \zeta, f^\omega(\zeta+1) \) is the least ordinal \( \nu \) such that \( \zeta < \nu = f(\nu) \), or the least fixed point of f that is strictly greater than \( \zeta \) (or greater than or equal to \( \zeta+1 \)). 

\( f^\omega(\zeta+1) \) is the limit of \( \zeta+1, f(\zeta+1), f(f(\zeta+1)), \ldots \). 

A fruitful function is a function that is inflationary, monotone, big, and continuous.

A function f is inflationary if \( \alpha \leq f(\alpha) \), monotone if \( \alpha \leq \beta \Rightarrow f(\alpha) \leq f(\beta) \), big if \( \omega^\alpha \leq f(\alpha) \) except possibly for \( \alpha = 0 \), continuous if f(VA) = Vf[A] where VA is the pointwise supremum of the set A.

\bigskip

We will now prove by induction the equivalence of the two fundamental sequences above.

We will use the notation \( \alpha^{\vdots^{\alpha^\beta}} \) for an an "exponential tower" with \( \alpha \) repeated n times. 


Note that the ordinals respectively limits of the fondamental sequence whose n-th term is \(\varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}} \) and the one whose n-th term is \( \varepsilon_0^{\varepsilon_0^{\vdots^{\varepsilon_0^{\varepsilon_0}}}} \) is the same, the least fixed point of the function \( \alpha \mapsto {\varepsilon_0}^\alpha \), which is greater than \( \omega \) and also than \( \varepsilon_0 \).

So we have proved what we want if we prove that, for any n, we have \( \omega^{\omega^{\vdots^{\omega^{\omega^{\varepsilon_0+1}}}}} = \varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}} \). 

For n = 0, we have \( \omega^{\omega^{\varepsilon_0+1}} = \omega^{\omega^{\varepsilon_0}\cdot\omega} = \omega^{\varepsilon_0\cdot\omega} = (\omega^{\varepsilon_0})^\omega = {\varepsilon_0}^\omega \). 

Now suppose we have \( \omega^{\omega^{\vdots^{\omega^{\omega^{\varepsilon_0+1}}}}} = \varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}} \). 

We must prove the equality for n+1, which can be written \( \omega^{\omega^{\omega^{\vdots^{\omega^{\omega^{\varepsilon_0+1}}}}}} = \varepsilon_0^{\varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}}} \). 

We have \( \omega^{\omega^{\omega^{\vdots^{\omega^{\omega^{\varepsilon_0+1}}}}}} = \omega^{\varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}}} \) (by our hypothesis) \( = \omega^{\varepsilon_0^{1+\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}}} \) (for the same reason than \( 1+\omega = \omega \), see above) \( = \omega^{\varepsilon_0\cdot\varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}}} = (\omega^{\varepsilon_0})^{\varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}}} = \varepsilon_0^{\varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}}} \). QED.


In a similar way, the limit of \( \varepsilon_1, \varepsilon_1^{\varepsilon_1}, \varepsilon_1^{\varepsilon_1^{\varepsilon_1}}, \ldots \) is called \( \varepsilon_2 \) and is also the limit of \( \varepsilon_1+1, \omega^{\varepsilon_1+1}, \omega^{\omega^{\varepsilon_1+1}}, \ldots \).

We can define the same way \( \varepsilon_n \) for any natural number n. Then \( \varepsilon_\omega \) is defined as the limit of \( \varepsilon_0, \varepsilon_1, \varepsilon_2, \varepsilon_3, \ldots \), and \( \varepsilon_{\omega+1} \) as the limit of \( \varepsilon_\omega, \varepsilon_\omega^{\varepsilon_\omega}, \varepsilon_\omega^{\varepsilon_\omega^{\varepsilon_\omega}}, \ldots \) or \( \varepsilon_\omega+1, \omega^{\varepsilon^\omega+1}, \omega^{\omega^{\varepsilon_\omega+1}}, \ldots \).

After comes \( \varepsilon_{\varepsilon_0} \), and the limit of \( \varepsilon_0, \varepsilon_{\varepsilon_0}, \varepsilon_{\varepsilon_{\varepsilon_0}}, \ldots \) which is called \( \zeta_0 \). 
This is the least fixed point of \( \alpha \mapsto \varepsilon_\alpha \). The next one is \( \zeta_1 \) which is the limit of \( \zeta_0+1, \varepsilon_{\zeta_0+1}, \varepsilon_{\varepsilon_{\zeta_0+1}}, \ldots \). 
Then we get \( \zeta_2, \zeta_3, \ldots, \zeta_\omega, \zeta_{\omega+1}, \ldots, \zeta_{\varepsilon_0}, \ldots, \zeta_{\zeta_0}, \ldots, \zeta_{\zeta_{\zeta_0}}, \ldots \).
The limit of \( 0, \zeta_0, \zeta_{\zeta_0}, \zeta_{\zeta_{\zeta_0}}, \ldots \) is called \( \eta_0 \). 

We can go on using successively different greek letters, or we can use functions indiced by numbers

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \varphi_0(\alpha) = \omega^\alpha \)
\item \( \varphi_1(\alpha) = \varepsilon_\alpha \)
\item \( \varphi_2(\alpha) = \zeta_\alpha \)
\item \( \varphi_3(\alpha) = \eta_\alpha \)
\item \( \varphi_{\alpha+1}(\beta) \) is the \( (1+\beta) \)-th fixed point of \( \xi \mapsto \varphi_\alpha(\xi) \) .
\end{itemize}

or a function with two variables : 

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \varphi(0,\alpha) = \omega^\alpha \)
\item \( \varphi(1,\alpha) = \varepsilon_\alpha \)
\item \( \varphi(2,\alpha) = \zeta_\alpha \)
\item \( \varphi(3,\alpha) = \eta_\alpha \)
\item \( \varphi(\alpha+1,\beta) \) is the \( (1+\beta) \)-th fixed point of \( \xi \mapsto \varphi(\alpha,\xi) \) .
\end{itemize}

Then we can enumerate the fixed points of the function \( \alpha \mapsto \varphi(\alpha,0) \) and define \( \Gamma_\alpha \) as the \( (1+\alpha) \)-th fixed point of this function, or add another variable to the \( \varphi \) function 
and define \( \varphi_{1,0}(\alpha) \) or \( \varphi(1,0,\alpha) \) as the \( (1+\alpha) \)-th fixed point of this function. So we have \( \Gamma_\alpha = \varphi_{1,0}(\alpha) = \varphi(1,0,\alpha) \).

More generally, we can define a function with any (finite) number of variables \( \varphi_{\alpha_n,\alpha_{n-1},\ldots,\alpha_1,\alpha_0}(\beta) = \varphi(\alpha_n, \alpha_{n-1}, \ldots, \alpha_1, \alpha_0, \beta) \), with \( \varphi(\alpha) = \varphi_0(\alpha) = \varphi(0,\alpha) = \omega^\alpha \). 

The notation \( \varphi_{\alpha_n,\alpha_{n-1},\ldots,\alpha_1,\alpha_0}(\beta) \) has the advantage of highlighting the different role played by the last variable \( \beta \).

\bigskip

For a complete definition of this Veblen function with finitely many variables, see for example :

https://en.wikipedia.org/wiki/Veblen\_function :

"Let \(z\) be an empty string or a string consisting of one or more comma-separated zeros \(0,0,...,0\) and \(s\) be an empty string or a string consisting of one or more comma-separated ordinals \(\alpha _{1},\alpha _{2},...,\alpha _{n}\) with \(\alpha _{1}>0\). The binary function \(\varphi (\beta ,\gamma )\) can be written as \(\varphi (s,\beta ,z,\gamma )\) where both \(s\) and \(z\) are empty strings.

The finitary Veblen functions are defined as follows:

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \(\varphi (\gamma )=\omega ^{\gamma }\)
\item \(\varphi (z,s,\gamma )=\varphi (s,\gamma )\)
\item if \(\beta >0\), then \(\varphi (s,\beta ,z,\gamma )\) denotes the \((1+\gamma )\)-th common fixed point of the functions \(\xi \mapsto \varphi (s,\delta ,\xi ,z)\) for each \(\delta <\beta\)

\end{itemize}

(...)

The limit of the \(\varphi(1,0,...,0)\) where the number of zeroes ranges over \( \omega \), is sometimes known as the "small" Veblen ordinal.

Every non-zero ordinal \(\alpha\) less than the small Veblen ordinal (SVO) can be uniquely written in normal form for the finitary Veblen function:

\(\alpha =\varphi (s_{1})+\varphi (s_{2})+\cdots +\varphi (s_{k})\)

where

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \(k\) is a positive integer
\item \(\varphi (s_{1})\geq \varphi (s_{2})\geq \cdots \geq \varphi (s_{k})\)
\item \(s_{m}\) is a string consisting of one or more comma-separated ordinals \(\alpha _{m,1},\alpha _{m,2},...,\alpha _{m,n_{m}}\) where \(\alpha _{m,1}>0\) and each \(\alpha _{m,i}<\varphi (s_{m})\)

\end{itemize} 

For limit ordinals \(\alpha<SVO\), written in normal form for the finitary Veblen function:

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \((\varphi(s_1)+\varphi(s_2)+\cdots+\varphi(s_k))[n]=\varphi(s_1)+\varphi(s_2)+\cdots+\varphi(s_k)[n]\),
\item \(\varphi(\gamma)[n]=\)
\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item n if \( \gamma=1 \)
\item \(\varphi(\gamma-1)\cdot n \) if \( \gamma \) is a successor ordinal
\item \( \varphi(\gamma[n]) \) if \( \gamma \) is a limit ordinal
\end{itemize}
\item \(\varphi(s,\beta,z,\gamma)[0]=0\) and \(\varphi(s,\beta,z,\gamma)[n+1]=\varphi(s,\beta-1,\varphi(s,\beta,z,\gamma)[n],z)\) if \(\gamma=0\) and \(\beta\) is a successor ordinal,
\item \(\varphi(s,\beta,z,\gamma)[0]=\varphi(s,\beta,z,\gamma-1)+1\) and \(\varphi(s,\beta,z,\gamma)[n+1]=\varphi(s,\beta-1,\varphi(s,\beta,z,\gamma)[n],z)\) if \(\gamma\) and \(\beta\) are successor ordinals,
\item \(\varphi(s,\beta,z,\gamma)[n]=\varphi(s,\beta,z,\gamma[n])\) if \(\gamma\) is a limit ordinal,
\item \(\varphi(s,\beta,z,\gamma)[n]=\varphi(s,\beta[n],z,\gamma)\) if \(\gamma=0\) and \(\beta\) is a limit ordinal,
\item \(\varphi(s,\beta,z,\gamma)[n]=\varphi(s,\beta[n],\varphi(s,\beta,z,\gamma-1)+1,z)\) if \(\gamma\) is a successor ordinal and \(\beta\) is a limit ordinal. "

\end{itemize}

The Veblen function can be generalized to transfinitely many variables with a finite number different from 0. Instead of writing the list of all the variable of the Veblen function, we can write only the non zero variables with position as indice, for example \( \varphi(\alpha,0,\beta,\gamma) = \varphi(\alpha_3,\beta_1,\gamma_0) \). We can then generalize the Veblen function by allowing any ordinal as indices, writing for example \( SVO = \varphi(1_\omega) \). The limit of the ordinals that can be written with this notation is called the large Veblen ordinal (LVO).

\bigskip

According to Wikipedia, "The definition can be given as follows: let \(\alpha\) be a transfinite sequence of ordinals (i.e., an ordinal function with finite support) which ends in zero (i.e., such that \(\alpha_0\)=0), and let \(\alpha[0\mapsto\gamma]\) denote the same function where the final 0 has been replaced by \(\gamma\). Then \(\gamma\mapsto\varphi(\alpha[0\mapsto\gamma])\) is defined as the function enumerating the common fixed points of all functions \( \xi \mapsto \varphi(\beta) \) where \( \beta \) ranges over all sequences which are obtained by decreasing the smallest-indexed nonzero value of \( \alpha \) and replacing some smaller-indexed value with the indeterminate \( \xi \) (i.e., \( \beta = \alpha [\iota_0 \mapsto \zeta, \iota \mapsto \xi ] \) meaning that for the smallest index \( \iota_0 \)  such that \( \alpha_{\iota_0} \)  is nonzero the latter has been replaced by some value \( \zeta < \alpha_{\iota_0} \)  and that for some smaller index \( \iota < \iota_0 \) , the value \( \alpha_\iota = 0 \) has been replaced with \( \xi \) )."

\bigskip

Schütte brackets or Klammersymbols are another way to write Veblen fuctions with transfinitely many variables. A Schütte bracket consists in a matrix with two lines, with the positions of the variables in the second line in increasing order, and the corresponding values in the first line. This matrix is preceded by the function  \( \xi  \mapsto \varphi(\xi) \). If we take \( \xi \mapsto \omega^\xi \), we get the equivalent of the Veblen function. With this notation, the previous example is written : 

\[
( \xi \mapsto \omega^\xi ) 
  \begin{pmatrix}
    \gamma & \beta & \alpha \\
    0 & 1 & 3
  \end{pmatrix}
\]

In some of his papers, Harold Simmons puts the function after the matrix, which is more logical, the matrix being considered as a function which, when applied to a function, gives an ordinal :

\[
  \begin{pmatrix}
    \gamma & \beta & \alpha \\
    0 & 1 & 3
  \end{pmatrix}
( \xi \mapsto \omega^\xi ) 
\]

\bigskip


When the function at the left of the matrix is \( \xi \mapsto \omega^\xi \), it is sometimes omitted. Example :

\[
  \begin{pmatrix}
    \gamma & \beta & \alpha \\
    0 & 1 & 3
  \end{pmatrix}
\]

The corresponding fundamental sequences can be found in https://sites.google.com/site/travelingtotheinfinity/fundamental-sequences-for-extended-veblen-function .

\bigskip

Another possible notation is to represent the parameters of the \( \varphi \) function by a polynom of variable \( \Omega \) where the exponent corresponds to the position of the variable, for example \( \varphi(\alpha,0,\beta,\gamma) = \varphi(\gamma_0,\beta_1,\alpha_3) = (\xi \mapsto \omega^\xi) \begin{pmatrix} \gamma & \beta & \alpha \\ 0 & 1 & 3 \end{pmatrix} = \varphi(\Omega^3 \cdot \alpha + \Omega \cdot \beta + \gamma) \). For \( \Omega \), we can choose an ordinal which is greater than all the ordinals we want to produce. Since they all are countable, we can take for example \( \Omega = \omega_1 \) which is the least uncountable ordinal. The method consisting in using uncountable ordinals to define countable ordinals is called "collapsing". We will see later other examples of notations using this method.

Note that \( \varphi(1,0) = \varphi(\Omega) \) is the least \( \alpha \) such that \( \alpha = \varphi(\alpha) = \omega^\alpha \) (the least fixed point of \( \alpha \mapsto \omega^\alpha) ; \varphi(1,0,0) = \varphi(\Omega^2) = \varphi(\Omega \cdot \Omega) \) is the least \( \alpha \) such that \( \alpha = \varphi(\alpha,0) = \varphi(\Omega \cdot \alpha) \). Generally speaking, we can see that \( f(\Omega) \) is the least fixed point of f. We shall see other examples of this equality later concerning ordinal collapsing functions. Note also that "\(\Omega\)" can be replaced by "1,0" in the formulas.

\bigskip

See Veblen's article "Continuous Increasing Functions of Finite and Transfinite Ordinals" ( http://www.ams.org/journals/tran/1908-009-03/S0002-9947-1908-1500814-9/S0002-9947-1908-1500814-9.pdf ) for more information.

\bigskip

Here is an Agda implementation of the Veblen function with transfinitely many variables :

\begin{verbatim}

{- 
   A definition of the large Veblen ordinal in Agda
   by Jacques Bailhache, March 2016

   See https://en.wikipedia.org/wiki/Veblen_function

    (1) phi(a)=w**a for a single variable,

    (2) phi(0,an-1,...,a0)=phi(an-1,...,a0), and

    (3) for a>0, c->phi(an,...,ai+1,a,0,...,0,c) is the function enumerating the common fixed points of the
        functions x->phi(an,...,ai+1,b,x,0,...,0) for all b<a.

    (4) Let a be a transfinite sequence of ordinals (i.e., an ordinal function with finite support) which ends in 
        zero  (i.e., such that a0=0), and let a[0->c] denote the same function where the final 0 has been replaced 
        by c. 
        Then c->phi(a[0->c]) is defined as the function enumerating the common fixed points of all functions 
        x->phi(b) where b ranges over all sequences which are obtained by decreasing the smallest-indexed nonzero 
        value of a  and replacing some smaller-indexed value with the indeterminate x (i.e., b=a[i0->z,i->x] 
        meaning that for the smallest index i0 such that ai0 is nonzero the latter has been replaced by some value 
        z<ai0 and that for some smaller index i<i0, the value ai=0 has been replaced with x).

-}


module LargeVeblen where

 data Nat : Set where
  O : Nat
  1+ : Nat -> Nat

 data Ord : Set where
  Zero : Ord
  Suc : Ord -> Ord
  Lim : (Nat -> Ord) -> Ord

 -- rpt n f x = f^n(x)
 rpt : {t : Set} -> Nat -> (t -> t) -> t -> t
 rpt O f x = x
 rpt (1+ n) f x = rpt n f (f x)

 -- smallest fixed point of f greater than x, limit of x, f x, f (f x), ...
 fix : (Ord -> Ord) -> Ord -> Ord
 fix f x = Lim (\n -> rpt n f x)

 w = fix Suc Zero -- not a fixed point in this case !

 -- cantor a b = b + w^a
 cantor : Ord -> Ord -> Ord
 cantor Zero a = Suc a
 cantor (Suc b) a = fix (cantor b) a
 cantor (Lim f) a = Lim (\n -> cantor (f n) a)

 -- phi0 a = w^a
 phi0 : Ord -> Ord
 phi0 a = cantor a Zero

 -- Another possibility is to use phi'0 instead of phi0 in the definition of phi,
 -- this gives a phi function which grows slower
 phi'0 : Ord -> Ord
 phi'0 Zero = Suc Zero
 phi'0 (Suc a) = Suc (phi'0 a)
 phi'0 (Lim f) = Lim (\n -> phi'0 (f n))

 -- Associative list of ordinals
 infixr 40 _=>_&_
 data OrdAList : Set where
  Zeros : OrdAList
  _=>_&_ : Ord -> Ord -> OrdAList -> OrdAList

 -- Usage : phi al, where al is the associative list of couples index => value ordered by increasing values,
 -- absent indexes corresponding to Zero values

 phi : OrdAList -> Ord 
 phi              Zeros  = phi0 Zero -- (1) phi(0) = w**0 = 1 
 phi (Zero => a & Zeros) = phi0 a    -- (1) phi(a) = w**a
 phi (            k => Zero & al) = phi al -- eliminate unnecessary Zero value
 phi (Zero => a & k => Zero & al) = phi (Zero => a & al) -- idem
 phi (Zero => a & Zero => b & al) = phi (Zero => a & al) -- should not appear but necessary for completeness
 phi (Zero => Lim f & al) = Lim (\n -> phi (Zero => f n & al)) -- canonical treatment of limit
 phi (                Suc k => Suc b & al) = fix (\x -> phi (k => x & Suc k => b & al)) Zero 
  -- (3) least fixed point
 phi (Zero => Suc a & Suc k => Suc b & al) = fix (\x -> phi (k => x & Suc k => b & al)) (Suc (phi (Zero => a & 
Suc k => Suc b & al))) -- (3) following fixed points
 phi (                Suc k => Lim f & al) = Lim (\n -> phi (Suc k => f n & al)) -- idem 
 phi (Zero => Suc a & Suc k => Lim f & al) = Lim (\n -> phi (k => Suc (phi (Zero => a & Suc k => Lim f & al)) & 
Suc k => f n & al)) -- idem  
 phi (                Lim f => Suc b & al) = Lim (\n -> phi (f n => (Suc Zero) & Lim f => b & al)) 
 phi (Zero => Suc a & Lim f => Suc b & al) = Lim (\n -> phi (f n => phi (Zero => a & Lim f => Suc b & al) & Lim 
f => b & al))
 phi (                Lim f => Lim g & al) = Lim (\n -> phi (Lim f => g n & al))
 phi (Zero => Suc a & Lim f => Lim g & al) = Lim (\n -> phi (f n => phi (Zero => a & Lim f => Lim g & al) & Lim 
f => g n & al)) 

 SmallVeblen = phi (w => Suc Zero & Zeros)

 LargeVeblen = fix (\x -> phi (x => Suc Zero & Zeros)) (Suc Zero)

{-
Normally it should terminate because the parameter of phi lexicographically decreases, but Agda is not clever enough to see it, 
so it must be called with no termination check option :

$ agda -I --no-termination-check LargeVeblen.agda
                 _ 
   ____         | |
  / __ \        | |
 | |__| |___  __| | ___
 |  __  / _ \/ _  |/ __\     Agda Interactive
 | |  |/ /_\ \/_| / /_| \
 |_|  |\___  /____\_____/    Type :? for help.
        __/ /
        \__/

The interactive mode is no longer supported. Don't complain if it doesn't work.
Checking LargeVeblen (/perso/ord/LargeVeblen.agda).
Finished LargeVeblen.
Main> phi Zeros
Suc Zero

\end{verbatim}

\section{Going beyond Veblen function with transfinitely many variables}


We start with the large Veblen ordinal which is the least fixed point of the function \( \alpha \mapsto \varphi(1_\alpha) \). Then we consider a function F which enumerates the fixed points of \( \alpha \mapsto \varphi(1_\alpha) \). So we have LVO = F(0). The next fixed point F(1) is the limit of \( LVO+1, \varphi(1_{LVO+1}), \varphi(1_{\varphi(1_{LVO+1})}), ... \)

Then we can consider the fixed points of the function F and define a function G which enumerates these fixed points, then a function H which enumerates the fixed points of G, and so on.

This construction is similar to \( \varepsilon \) which enumerates the fixed points of \( \alpha \mapsto \omega^\alpha \), \( \zeta \) which enumerates the fixed points of \( \varepsilon \), \( \eta \) which enumerates the fixed points of \( \zeta \).

Like we have defined :

 - \( \varphi_0(\alpha) = \omega^\alpha \)

 - \( \varphi_1(\alpha) = \varepsilon(\alpha) \)

 - \( \varphi_2(\alpha) = \zeta(\alpha) \)

...

we can define :

 - \( \varphi^+_0(\alpha) = F(\alpha) \)

 - \( \varphi^+_1(\alpha) = G(\alpha) \)

 - \( \varphi^+_2[\alpha) = H(\alpha) \)

 ...

With this notation we can write \( LVO = \varphi^+_0(0) \).

Then \( \varphi^+_\alpha(\beta) \) can be written as a binary function \( \varphi^+(\alpha,\beta) \) which can be generalized to finitely many variables like \( \varphi^+(\alpha,\beta,\gamma) \) and transfinitely many variables like \( \varphi^+(1_\omega) \).

Then we can consider the fixed points of the function \( \alpha \mapsto \varphi^+(1_\alpha) \) and define a function \( \varphi^{++}_0 \) which enumerates these fixed points.

The same way we can define \( \varphi^{+++} \), \( \varphi^{++++} \), ...

We can then define a new notation : 

 - \( \Phi_0 = \varphi \)
 
 - \( \Phi_1 = \varphi^+ \)

 - \( \Phi_2 = \varphi^{++} \)

 ...

\bigskip

There is another way to express this construction.

There are different conventions for \( \varphi_0(x) \), like \( \omega^x \) or \( \varepsilon_x \). We can write explicitely the convention chosen for \( \varphi_0 \) by writing "\( \varphi_f(\alpha,\beta) \)" for "\( \varphi_\alpha(\beta) \) with function f used for \( \varphi_0 \)".  With this notation we have:

 - \( \varphi_f(0,\beta) = f(\beta) \)
 
 - \( \varphi_f(\alpha+1,\beta) = (1+\beta) \)th fixed point of the function \( \beta \mapsto \varphi_f(\alpha,\beta) \)
 
 - \( \varphi_f(\lambda,\beta) = (1+\beta) \)th common fixed point of the function \( \beta \mapsto \varphi_f(\alpha,\beta) \) for all \( \alpha < \lambda \), if \( \lambda \) is a limit ordinal.

( See http://www.cs.man.ac.uk/~hsimmons/TEMP/OrdNotes.pdf )

Then we generalize the binary function \( \varphi_f(\alpha,\beta) \) to finitely many variables: for example \( \varphi_f(1,0,\alpha) = (1+\alpha) \)th common fixed point of the function \( \xi \mapsto \varphi(\xi,0) \) ( see https://en.wikipedia.org/wiki/Veblen\_function ) and to infinitely many variables with a finite number of them different from 0, for example \( \varphi_f(1_\omega) \).

Then we can define new \( \varphi \) functions by taking for \( \varphi_0 \) the function \( \xi \mapsto \varphi_f(1_\xi) \) and define functions \( \varphi_{\xi \mapsto \varphi_f(1_\xi)} \) with 2 variables, with finitely many variables and with transfinitely many variables.

To make a correspondence with my previous construction, if f is the function \( \xi \mapsto \omega^\xi \), then \( \varphi_f(\alpha,\beta) \) corresponds to what I wrote \( \varphi_\alpha(\beta) \), and \( \varphi_{\xi \mapsto \varphi_f(1_\xi)}(\alpha,\beta) \) to \( \varphi^+_\alpha(\beta) \). 

If we define the function S by \( S(f)(\xi) = \varphi_f(1_\xi) \), then \( \varphi_{\xi \mapsto \varphi_f(1_\xi)}\) can be written \( \varphi_{S(f)} \). We can then consider \( \varphi_{S(S(f))} \) and so on.

Given an ordinal \( \alpha \), we can iterate transfinitely "\( \alpha \) times" the application of S to an initial function \( f_0 \), for example \( f_0(\xi) = \omega^\xi \), to obtain a function which I will write \( S^\alpha(f_0) \). We can use this function to define a function \( \varphi_{S^\alpha(f_0)} \) which permits to construct big ordinals.




\section{Simmons notation}

Harold Simmons defined a notation ( see http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/ordinal-notations.html ) based on fixed points enumeration which "contains" Veblen functions and permits to go further. 

He uses the lambda calculus formalism, in which f x represents the application of function f to x, and f x y = (f x) y the application of function f to x which gives another function which is applied to y giving the final result. 
He uses tho notation \( x \mapsto y \) to represent the function which, when applied to x, gives y (instead of the traditional lambda calculus notation \( \lambda x . y \) ).

He also uses the notation \( \omega^\bullet \) for \( \alpha \mapsto \omega^\alpha \).

\( f \circ g \) represents the composition of functions f and g : \( (f \circ g) \alpha = f(g \alpha) \).

\( f^\alpha \) is a canonical generalization of of exponentiation of a function to an ordinal power : \( f^n \) represents \( f \circ f \circ \ldots \circ f \) with f repeated n times, \( f^\omega \zeta \) is the limit of \( \zeta, f\ \zeta, f(f\ \zeta), \ldots \), \( f^{\omega+1} \zeta = f(f^\omega \zeta) \) and so on.

\bigskip

More precisely, Simmons gives the following definitions in http://www.cs.man.ac.uk/~hsimmons/TEMP/OrdNotes.pdf page 11 : 

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( g^0 \zeta = \zeta \)
\item \( g^{\alpha+1} \zeta = g (g^\alpha \zeta) \)
\item \( g^\lambda \zeta = V \lbrace g^\alpha \zeta | \alpha < \lambda \rbrace \) (if \( \lambda \) is a limit ordinal, where V denotes the poinwise supremum)
\end{itemize}

and the following equivalent definitions in http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/Fruitful.pdf page 4 :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( g^0 = id \)
\item \( g^{\alpha+1} = g \circ g^\alpha \)
\item \( g^\lambda = V \lbrace g^\alpha | \alpha < \lambda \rbrace \)
\end{itemize}

\bigskip

and he generalizes these definitions to higher order functions.

\bigskip

Then Simmons defines the following functions :


\( Fix\ f \zeta = f^\omega (\zeta+1) \) = limit of \( \zeta+1, f (\zeta+1), f (f (\zeta+1)), \ldots \) is the least fixed point of the function f which is strictly greater than \( \zeta \), which means the least ordinal \( \nu \) satisfying \( f\ \nu = \nu \) and \( \nu > \zeta \).

\( Next = Fix\ \omega^\bullet = Fix (\alpha \mapsto \omega^\alpha) \) ; \( Next\ \zeta \) is the next \( \varepsilon_\alpha \) after \( \zeta \).

\( [0] h = Fix (\alpha \mapsto h^\alpha 0) \)

\( [1] h g = Fix (\alpha \mapsto h^\alpha g 0) \)

\( [2] h g f = Fix (\alpha \mapsto h^\alpha g f 0) \) 

... and so on ...

\bigskip

In http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/OrdSlides.pdf Simmons gives another equivalent definition :

\( [0] h = Fix (\alpha \mapsto h^\alpha \omega) \)

\( [1] h g = Fix (\alpha \mapsto h^\alpha g \omega) \)

\( [2] h g f = Fix (\alpha \mapsto h^\alpha g f \omega) \) 

\bigskip

Simmons also defines : 

\( Veb\ f\ \zeta = (Fix\ f)^{1+\zeta} 0 \) is the \( (1+\zeta) \)-th fixed point of f

\( Enm\ h\ \alpha = h^{1+\alpha} 0 \)

\( Veb = Enm \circ Fix \)

\( [0] = Fix \circ Enm \)

\( Fix \circ Veb = Fix \circ Enm \circ Fix = [0] \circ Fix \)

\( Fix \circ Veb^\alpha = [0]^\alpha \circ Fix \)

\( \Delta[0] = \omega \)

\( \Delta[1] = Next\ \omega = \varepsilon_0 \)

\( \Delta[2] = [0] Next\ \omega = \) least \( \nu \) with \( \nu = Next^\nu \omega = \zeta_0 \)

\( \Delta[3] = [1] [0] Next\ \omega = \) least \( \nu \) with \( \nu = [0]^\nu Next\ \omega = \Gamma_0 \)

\( \Delta[4] = [2] [1] [0] Next\ \omega = \) least \( \nu \) with \( \nu = [1]^\nu [0] Next\ \omega = LVO \) (large Veblen ordinal)

... and so on ...


\subsection{Implementation}

Here is an implementation of the Simmons hierarchy in Haskell :

\begin{verbatim}

module Simmons where

 -- Natural numbers
 data Nat 
  = ZeroN
  | SucN Nat

 -- Ordinals
 data Ord 
  = Zero
  | Suc Ord
  | Lim (Nat -> Ord)

 -- Ordinal corresponding to a given natural
 ordOfNat ZeroN = Zero
 ordOfNat (SucN n) = Suc (ordOfNat n)

 -- omega
 w = Lim ordOfNat

 lim0 s = Lim s
 lim1 f x = lim0 (\n -> f n x)
 lim2 f x = lim1 (\n -> f n x)

 -- this does not work :
 -- lim ZeroN s = Lim s
 -- lim (SucN p) f = \x -> lim p (\n -> f n x)

 -- f^a(x)
 fpower0 f Zero x = x
 fpower0 f (Suc a) x = f (fpower0 f a x)
 fpower0 f (Lim s) x = Lim (\n -> fpower0 f (s n) x)

 fpower l f Zero x = x
 fpower l f (Suc a) x = f (fpower l f a x)
 fpower l f (Lim s) x = l (\n -> fpower l f (s n) x)

 -- fix f z = least fixed point of f which is > z
 fix f z = fpower lim0 f w (Suc z) -- Lim (\n -> fpower0 f (ordOfNat n) (Suc z))

 -- cantor b a = a + w^b
 cantor Zero a = Suc a
 cantor (Suc b) a = fix (cantor b) a
 cantor (Lim s) a = Lim (\n -> cantor (s n) a)
 
 -- expw a = w^a
 expw a = cantor a Zero

 -- next a = least epsilon_b > a
 next = fix expw

 -- [0]
 simmons0 h = fix (\a -> fpower lim0 h a Zero)

 -- [1]
 simmons1 h1 h0 = fix (\a -> fpower lim1 h1 a h0 Zero)

 -- [2]
 simmons2 h2 h1 h0 = fix (\a -> fpower lim2 h2 a h1 h0 Zero)

 -- Large Veblen ordinal 
  lvo = simmons2 simmons1 simmons0 next w



$ hugs
__   __ __  __  ____   ___      _________________________________________
||   || ||  || ||  || ||__      Hugs 98: Based on the Haskell 98 standard
||___|| ||__|| ||__||  __||     Copyright (c) 1994-2005
||---||         ___||           World Wide Web: http://haskell.org/hugs
||   ||                         Bugs: http://hackage.haskell.org/trac/hugs
||   || Version: September 2006 _________________________________________

Haskell 98 mode: Restart with command line option -98 to enable extensions

Type :? for help
Hugs> :load simmons
Simmons> lvo
ERROR - Cannot find "show" function for:
*** Expression : lvo
*** Of type    : Ord

Simmons>



\end{verbatim}

\subsection{Correspondence with Veblen functions}

\( \varepsilon_0 \) is the next \( \varepsilon_\alpha \) after 0 (or after \( \omega \), or after any ordinal less than \( \varepsilon_0 \), so we have \( \varepsilon_0 = Next\ 0 = Next\ \omega \).

\( \varepsilon_1 \) is the next \( \varepsilon_\alpha \) after \( \varepsilon_0 \), so we have \( \varepsilon_1 = Next\ \varepsilon_0 = Next\ (Next\ 0) = Next^2 0 = Next\ (Next\ \omega) = Next^2 \omega \).

\( \varepsilon_2 \) is the next \( \varepsilon_\alpha \) after \( \varepsilon_1 \), so we have \( \varepsilon_2 = Next\ \varepsilon_1 = Next\ (Next\ (Next\ 0)) = Next^3 0 = Next\ (Next\ (Next\ \omega)) = Next^3 \omega \).

...

\( \varepsilon_\omega \) is the limit of \( \varepsilon_0, \varepsilon_1, \varepsilon_2, \ldots \). It is the limit of \( Next^1 0, Next^2 0, Next^3 0, ... \) which is \( Next^\omega 0 \).

More generally, we have \( \varepsilon_\alpha = \varphi(1,\alpha) = Next^{1+\alpha} 0 = Next^{1+\alpha} \omega \).

\bigskip

\( \zeta_0 = \varphi(2,0) \) is the least fixed point of \( \alpha \mapsto \varepsilon_\alpha \) (greater than 0), so \( \zeta_0 = Fix (\alpha \mapsto \varepsilon_\alpha) 0 = Fix (\alpha \mapsto Next^{1+\alpha} 0) 0 = Fix (\alpha \mapsto Next^\alpha 0) 0 \) (because the "1+" is "absorbed" after a few iterations) \( = [0] Next\ 0 \). Since \( \zeta_0 \) is also greater than \( \omega \), it is also \( [0] Next\ \omega \) according to a similar computation. 

\( \zeta_1 = \varphi(2,1) \) is the next fixed point of \( \alpha \mapsto \varepsilon_\alpha \), the least one which is strictly greater than \( \zeta_0 \), so \( \zeta_1 = Fix (\alpha \mapsto \varepsilon_\alpha) \zeta_0 = Fix (\alpha \mapsto Next^\alpha 0) \zeta_0 = [0] Next\ \zeta_0 = [0] Next ([0] Next\ 0) = ([0] Next)^2 0 = [0] Next ([0] Next\ \omega) = ([0] Next)^2 \omega \).

More generally, \( \zeta_\alpha = ([0] Next)^{1+\alpha} 0 \).

Similar computations give \( \eta_0 = \varphi(3,0) = [0]^2 Next\ 0 \) and \( \eta_\alpha = ([0]^2 Next)^{1+\alpha} 0 \).

More generally, \( \varphi(1+\beta,\alpha) = ([0]^\beta Next)^{1+\alpha} 0 \) or \( ([0]^\beta Next)^{1+\alpha} \omega \).

\bigskip

\( \Gamma_0 = \varphi(1,0,0) \) is the least fixed point (greater than 0) of the function \( \alpha \mapsto \varphi(\alpha,0) \) or \( \alpha \mapsto \varphi(1+\alpha,0) \) (for the same reason of "absorbsion" of "1+" than previously), so \( \Gamma_0 = Fix (\alpha \mapsto \varphi(1+\alpha,0) 0 = Fix (\alpha \mapsto ([0]^\alpha Next)^(1+0) 0) 0 = Fix (\alpha \mapsto [0]^\alpha Next\ 0) 0 = [1] [0] Next\ 0 \).

\( \Gamma_1 = \varphi(1,0,1) \) is the next fixed point : \( \Gamma_1 = Fix (\alpha \mapsto [0]^\alpha Next\ 0) \Gamma_0 = [1] [0] Next\ \Gamma_0 = [1] [0] Next\ ([1] [0] Next\ 0) = ([1] [0] Next)^2 0 \).

More generally, we have \( \varphi(1,0,\alpha) = ([1] [0] Next)^{1+\alpha} 0 \).

\( \varphi(1,1,0) \) is the least fixed point (greater than 0) of the function \( \alpha \mapsto \varphi(1,0,\alpha) \), so it is \( Fix (\alpha \mapsto \varphi(1,0,\alpha)) 0 = Fix (\alpha \mapsto ([1] [0] Next)^{1+\alpha} 0) 0 = Fix (\alpha \mapsto ([1] [0] Next)^{\alpha} 0) 0 \) (absorbsion of 1+) \( = [0] ([1] [0] Next) 0 \).

\( \varphi(1,1,1) \) is the next fixed point \( Fix (\alpha \mapsto ([1] [0] Next)^{\alpha} 0) \varphi(1,1,0) = ([0] ([1] [0] Next) ([0] ([1] [0] Next) 0) = ([0] ([1] [0] Next))^2 0 \).

More generally, \( \varphi(1,1,\alpha) = ([0] ([1] [0] Next))^{1+\alpha} 0 \).

\( \varphi(1,2,0) \) is the least fixed point (greater than 0) of the function \( \alpha \mapsto \varphi(1,1,\alpha), Fix (\alpha \mapsto \varphi(1,1,\alpha)) 0 = Fix ([0] ([1] [0] Next)^{1+\alpha} 0) 0 = Fix (\alpha \mapsto ([0] ([1] [0] Next))^\alpha 0) 0 = [0] ([0] ([1] [0] Next)) 0 = [0]^2 ([1] [0] Next) 0 \).

Like previously, \( \varphi(1,2,\alpha) \) is the \( (1+\alpha) \)-th fixed point of the previous function, which is \( ([0]^2 ([1] [0] Next))^{1+\alpha} 0 \).

More generally, \( \varphi(1,\beta,\alpha) = ([0]^\beta ([1] [0] Next))^{1+\alpha} 0 \).

\( \varphi(2,0,0) \) is the least fixed point (greater than 0) of the function \( \beta \mapsto \varphi(1,\beta,0) \), which is \( Fix (\alpha \mapsto \varphi(1,\beta,0)) 0 = Fix (\beta \mapsto ([0]^\beta ([1] [0] Next))^{1+0} 0) 0 = Fix (\beta \mapsto [0]^\beta ([1] [0] Next) 0) 0 = [1] [0] ([1] [0] Next) 0 = ([1] [0])^2 Next\ 0 \).

The \( (1+\alpha) \)-th fixed point of the previous function is \( \varphi(2,0,\alpha) = (([1] [0])^2 Next)^{1+\alpha} 0 \).

The least fixed point of the function \( \alpha \mapsto \varphi(2,0,\alpha) \) is \( \varphi(2,1,0) = Fix (\alpha \mapsto \varphi(2,0,\alpha)) 0 = Fix (\alpha \mapsto (([1] [0])^2 Next)^(1+\alpha) 0) 0 = Fix (\alpha \mapsto (([1] [0])^2 Next)^\alpha 0) = [0] (([1] [0])^2 Next) 0 \) and its \( (1+\alpha) \)-th fixed point is \( \varphi(2,1,\alpha) = ([0] (([1] [0])^2 Next))^{1+\alpha} 0 \).

More generally, we have \( \varphi(2,\beta,\alpha) = ([0]^\beta (([1] [0])^2 Next))^{1+\alpha} 0 \).

\bigskip

The general formula with three variables (with \( \gamma \neq 0 \) ) is \( \varphi(\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma Next))^{1+\alpha} 0 \).

In particular, we have \( \varphi(\gamma,0,0) = ([1] [0])^\gamma Next 0 \).

\bigskip

\( \varphi(1,0,0,0) \) is the least fixed point of the function \( \gamma \mapsto \varphi(\gamma,0,0), Fix (\gamma \mapsto \varphi(\gamma,0,0)) 0 = Fix (\gamma \mapsto ([1] [0])^\gamma Next\ 0) 0 = [1] ([1] [0]) Next\ 0 = [1]^2 [0] Next\ 0 \).

All of these computations could be done with \( \omega \) instead of 0 at the end of the formulas so we also have \( \varphi(\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma Next))^{1+\alpha} \omega \).

In a similar way, we can obtain the formula with 4 variables :

\( \varphi(1,0,0,\alpha) = ([1]^2 [0] Next)^{1+\alpha} 0 \)

\( \varphi(1,0,1,0) = Fix (\alpha \mapsto ([1]^2 [0] Next)^\alpha 0) 0 = [0] ([1]^2 [0]) 0 \)

\( \varphi (1,0,1,\alpha) = ([0] ([1]^2 [0] Next))^{1+\alpha} 0 \)

\( \varphi(1,0,\beta,\alpha) = ([0]^\beta ([1]^2 [0] Next))^{1+\alpha} 0 \)

\( \varphi(1,1,0,0) = Fix (\alpha \mapsto \varphi(1,0,\alpha,0)] 0 = Fix (\alpha \mapsto [0]^\alpha ([1]^2 [0] Next) 0] 0 = [1] [0] ([1]^2 [0] Next) 0 \)

\( \varphi(1,1,0,\alpha) = ([1] [0] ([1]^2 [0] Next))^{1+\alpha} 0 \)

\( \varphi(1,1,1,0) = Fix (\alpha \mapsto \varphi(1,1,0,\alpha)) 0 = Fix (\alpha \mapsto ([1] [0] ([1]^2 [0] Next))^\alpha 0) 0 = [0] ([1] [0] ([1]^2 [0] Next)) 0 \)

\( \varphi(1,1,1,\alpha) = ([0] ([1] [0] ([1]^2 [0] next)))^{1+\alpha} 0 \)

\( \varphi(1,1,\beta,\alpha) = ([0]^\beta ([1] [0] ([1]^2 [0] Next)))^{1+\alpha} 0 \)

\( \varphi(1,2,0,0) = Fix (\alpha \mapsto \varphi(1,1,\alpha,0)) 0 = Fix (\alpha \mapsto [0]^\alpha ([1] [0] ([1]^2 [0] next)) 0) 0 = [1] [0] ([1] [0] ([1]^2 [0] Next)) 0 = ([1] [0])^2 ([1]^2 [0] Next) 0 \)

\( \varphi(1,0,0,0) = [1]^2 [0] Next 0 \)

\( \varphi(1,1,0,0) = [1] [0] ([1]^2 [0] Next) 0 \)

\( \varphi(1,2,0,0) = ([1] [0])^2 ([1]^2 [0] Next) 0 \)

\( \varphi(1,\gamma,0,0) = ([1] [0])^\gamma ([1]^2 [0] Next) 0 \)

\( \varphi(1,\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma ([1]^2 [0] Next)))^{1+\alpha} 0 \)

\( \varphi(2,0,0,0) = Fix (\alpha \mapsto \varphi(1,\alpha,0,0)] 0 = Fix (\alpha \mapsto ([1] [0])^\alpha ([1]^2 [0] Next) 0] 0 = [1] ([1] [0]) ([1]^2 [0] Next) 0 = [1]^2 [0] ([1]^2 [0] Next) 0 = ([1]^2 [0])^2 Next 0 \)

\( \varphi(\delta,0,0,0) = ([1]^2 [0])^\delta Next\ 0 \)

The general formula with four variables is : 

\( \varphi(\delta,\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma (([1]^2 [0])^\delta Next)))^{1+\alpha} 0 = ([0]^\beta (([1] [0])^\gamma (([1]^2 [0])^\delta Next)))^{1+\alpha} \omega \) 

and so on.

\bigskip

The small Veblen ordinal is the limit of :

 \( \varphi(1) = \omega, \varphi(1,0) = Next\ \omega, \varphi(1,0,0) = [1] [0] Next\ \omega, \varphi(1,0,0,0) = [1]^2 [0] Next\ \omega, \varphi(1,0,0,0,0) = [1]^3 [0] Next\ \omega, \ldots \). 

This limit is \( [1]^\omega [0] Next\ \omega = [1]^\omega [0] Next\ 0 \).

\bigskip

Allowing variables at any finite or transfinite positions (which is equivalent to Schütte brackets or Klammersymbols) gives ordinals smaller than the large Veblen ordinal which is the least fixed point of the function \( \alpha \mapsto \varphi(1_\alpha) \). It is \( Fix (\alpha \mapsto \varphi(1_\alpha)) 0 = Fix (\alpha \mapsto [1]^\alpha [0] Next\ 0) 0 = [2] [1] [0] Next\ 0 \)


\( [2] [1] [0] Next\ 0 \) or \( [2] [1] [0] Next\ \omega \). 

The conversion rule from Schütte Klammersymbol to Simmons notation are described by Simmons in his paper : http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/FromBelow.pdf (Simmons also wrote other papers but it seems to me that they contain inaccuracies and maybe even errors).

In summary :

\( Fix\ f \zeta = f^\omega (\zeta+1) \)

\( Enm\ h\ \alpha = h^{1+\alpha} 0 \)

\( Next = Fix (\alpha \mapsto \omega^\alpha) \)

\( [0] h = Fix (\alpha \mapsto h^\alpha 0) \)

\( [1] h g = Fix (\alpha \mapsto h^\alpha g 0) \)

\( \nabla \begin{bmatrix} \alpha+1 \\
                                    i+1      \end{bmatrix} =
 ([1]^i [0])^{1+\alpha} \) if \( i \neq 0 ; [0]^\alpha \) if \( i = 0 \)

\( \nabla \begin{bmatrix} \alpha_1+1 & \ldots & \alpha_s+1 \\
                                    i_1+1      & \ldots & \i_s+1     \end{bmatrix} 
= \nabla \begin{bmatrix} \alpha_1+1 \\
                                   i_1+1      \end{bmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                    i_s+1      \end{bmatrix}
\)

where \( f \circ g \) is the composition of functions f and g : \( (f \circ g) x = f\ (g\ x) \)

\( Sch \begin{bmatrix} 1+\alpha_1 & \ldots & 1+\alpha_s \\
                       1+i_1      & \ldots & 1+i_s      \end{bmatrix} 
= Enm\ \circ \nabla \begin{bmatrix} 1+\alpha_1 & \ldots & 1+\alpha_s \\
                                          1+i_1      & \ldots & 1+i_s      \end{bmatrix} o\ Fix
\)


f may be any function but it is usually \( \alpha \mapsto \omega^\alpha \).

\( f \begin{pmatrix} \zeta & 1+\alpha_1 & \ldots & 1+\alpha_s \\
                     0     & 1+i_1      & \ldots & 1+i_s      \end{pmatrix} \)

\( = Sch \begin{bmatrix} 1+\alpha_1 & \ldots & 1+\alpha_s \\
                      1+i_1      & \ldots & 1+i_s      \end{bmatrix} f \zeta \)

\( = (Enm \circ \nabla \begin{bmatrix} 1+\alpha_1 & \ldots & 1+\alpha_s \\
                                       1+i_1      & \ldots & 1+i_s      \end{bmatrix} \circ Fix) f \zeta \)

\( = (Enm \circ \nabla \begin{bmatrix} \alpha_1+1 \\
                                       i_1+1      \end{bmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                              i_s+1      \end{bmatrix} \circ Fix) f \zeta \)

\( = Enm ((\nabla \begin{bmatrix} \alpha_1+1 \\
                                  i_1+1      \end{bmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                         i_s+1      \end{bmatrix}) (Fix f)) \zeta \)

\( = (\nabla \begin{bmatrix} \alpha_1+1 \\
                             i_1+1      \end{bmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                    i_s+1      \end{bmatrix}) (Fix f))^{1+\zeta} 0 \)

\bigskip

If \( f = \alpha \mapsto \omega^\alpha \), then Fix f = Next and 

\( f \begin{pmatrix} \zeta & 1+\alpha_1 & \ldots & 1+\alpha_s \\
                     0     & 1+i_1      & \ldots & 1+i_s      \end{pmatrix} 
 = (\nabla \begin{bmatrix} \alpha_1+1 \\
                             i_1+1      \end{bmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                    i_s+1      \end{bmatrix}) Next)^{1+\zeta} 0 \)

\bigskip

Examples :

\bigskip

\( \varphi(1+\beta,\alpha) \)

\( = (\xi \mapsto \omega^\xi) \begin{pmatrix} \alpha & 1+\beta \\
                                              0      & 1       \end{pmatrix} \)

\( = ((\nabla \begin{bmatrix} \beta+1 \\
                              1       \end{bmatrix}) (Fix (\xi \mapsto \omega^\xi)))^{1+\alpha} 0 \)

\( = ((\nabla \begin{bmatrix} \beta+1 \\
                              1       \end{bmatrix}) Next)^{1+\alpha} 0 \)

\( = ([0]^\beta Next)^{1+\alpha} 0 \)

\bigskip

\( \varphi(1+\gamma,1+\beta,\alpha) \)

\( = (\xi \mapsto \omega^\xi) \begin{pmatrix} \alpha & 1+\beta & 1+\gamma \\
                                              0      & 1       & 2        \end{pmatrix} \)

\( = ((\nabla \begin{bmatrix} \beta+1 \\
                              1       \end{bmatrix} \circ [0] \circ \nabla \begin{bmatrix} \gamma+1 \\
                                                                                           2        \end{bmatrix}) (Fix (\xi \mapsto \omega^\xi)))^{1+\alpha} 0 \)

\( = ((\nabla \begin{bmatrix} \beta+1 \\
                              1       \end{bmatrix} \circ [0] \circ \nabla \begin{bmatrix} \gamma+1 \\
                                                                                           2        \end{bmatrix}) Next)^{1+\alpha} 0 \)

\( = (([0]^\beta  \circ [0] \circ ([1] [0])^{1+\gamma}) Next)^{1+\alpha} 0 \)

\( = ([0]^{1+\beta} (([1] [0])^{1+\gamma} Next))^{1+\alpha} 0 \)

Compare with the previously found formula :

if \( \gamma > 0, \varphi(\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma Next))^{1+\alpha} 0 \)

and note the "round trip" \( 1+\gamma \rightarrow \gamma+1 \rightarrow 1+\gamma \).

\bigskip

\( \varphi(1+\delta,1+\gamma,1+\beta,\alpha) \)

\( = (\xi \mapsto \omega^\xi) \begin{pmatrix} \alpha & 1+\beta & 1+\gamma & 1+\delta \\
                                              0      & 1       & 2        & 3        \end{pmatrix} \)

\( = ((\nabla \begin{bmatrix} \beta+1 \\
                              1       \end{bmatrix} \circ [0] \circ \nabla \begin{bmatrix} \gamma+1 \\
                                                                                           2        \end{bmatrix} \circ [0] \circ \nabla \begin{bmatrix} \delta+1 \\
                                                                                                                                                         3        \end{bmatrix}) (Fix (\xi \mapsto \omega^\xi)))^{1+\alpha} 0 \)

\( = ((\nabla \begin{bmatrix} \beta+1 \\
                              1       \end{bmatrix} \circ [0] \circ \nabla \begin{bmatrix} \gamma+1 \\
                                                                                           2        \end{bmatrix} \circ [0] \circ \nabla \begin{bmatrix} \delta+1 \\
                                                                                                                                                         3        \end{bmatrix}) Next)^{1+\alpha} 0 \)

\( = (([0]^\beta \circ [0] \circ ([1] [0])^{1+\gamma} \circ [0] \circ ([1]^2 [0])^{1+\delta}) Next)^{1+\alpha} 0 \)

\( = ([0]^{1+\beta} (([1] [0])^{1+\gamma} ([0] (([1]^2 [0])^{1+\delta} Next))))^{1+\alpha} 0 \)

\( = ([0]^{1+\beta} (([1] [0])^{1+\gamma} (([1]^2 [0])^{1+\delta} Next)))^{1+\alpha} 0 \) 

because [0] is absorbed by the following operator (see http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/FromBelow.pdf p 33, 6.7)

Compare with the previously mentioned formula :

\( \varphi(\delta,\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma (([1]^2 [0])^\delta Next)))^{1+\alpha} 0 \)

\bigskip

The equality

\( (\xi \mapsto \omega^\xi) \begin{pmatrix} \zeta & 1+\alpha_1 & \ldots & 1+\alpha_s \\
                                            0     & 1+i_1      & \ldots & 1+i_s      \end{pmatrix} 
 = (\nabla \begin{bmatrix} \alpha_1+1 \\
                             i_1+1      \end{bmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                    i_s+1      \end{bmatrix}) Next)^{1+\zeta} 0 \)

can be reformulated, distinguishing four cases :

\begin{itemize}

\item 
\( (\xi \mapsto \omega^\xi) \begin{pmatrix} \zeta \\
                                            0     \end{pmatrix} = \varphi(0,\zeta) = \omega^\zeta \)

\item 
\( (\xi \mapsto \omega^\xi) \begin{pmatrix} \zeta & 1+\alpha \\
                                            0     & 1        \end{pmatrix} = \varphi(1+\alpha,\zeta) 
= (\nabla \begin{bmatrix} \alpha+1 \\
                          1        \end{bmatrix} Next)^{1+\zeta} 0 = ([0]^\alpha Next)^{1+\zeta} 0 \)

\item 
\( (\xi \mapsto \omega^\xi) \begin{pmatrix} \zeta & 1+\alpha_1 & 1+\alpha_2 & \ldots & 1+\alpha_s \\
                                                  0     & 1          & 1+i_2      & \ldots & 1+i_s      \end{pmatrix} \)

\( = ((\nabla \begin{bmatrix} \alpha_1+1 \\
                              1          \end{bmatrix} \circ [0] \circ \nabla \begin{pmatrix} \alpha_2+1 \\
                                                                                              i_2+1      \end{pmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                                                                                     i_s+1      \end{bmatrix}) Next)^{1+\zeta} 0 \)

\( = (([0]^{\alpha_1} \circ [0] \circ ([1]^{i_2} [0])^{1+\alpha_2} \circ [0] \circ \ldots \circ [0] \circ ([1]^{i_s} [0])^{1+\alpha_s}) Next)^{1+\zeta} 0 \) 

\( = (([0]^{1+\alpha_1} \circ ([1]^{i_2} [0])^{1+\alpha_2} \circ [0] \circ \ldots \circ [0] \circ ([1]^{i_s} [0])^{1+\alpha_s}) Next)^{1+\zeta} 0 \)

\( = (([0]^{1+\alpha_1} \circ ([1]^{i_2} [0])^{1+\alpha_2} \circ \ldots \circ ([1]^{i_s} [0])^{1+\alpha_s}) Next)^{1+\zeta} 0 \)

The first separating [0] is combined with \( [0]^{\alpha_1} \) giving \( [0]^{1+\alpha_1} \) and the other are absorbed.

\item
\( (\xi \mapsto \omega^\xi) \begin{pmatrix} \zeta & 1+\alpha_1 & \ldots & 1+\alpha_s \\
                                            0     & 1+i_1      & \ldots & 1+i_s      \end{pmatrix} \) with \( i_1 \neq 0 \)

\( = ((\nabla \begin{bmatrix} \alpha_1+1 \\
                              i_1+1      \end{bmatrix} \circ [0] \circ \ldots \circ [0] \circ \nabla \begin{bmatrix} \alpha_s+1 \\
                                                                                                                     i_s+1      \end{bmatrix}) Next)^{1+\zeta} 0 \)

\( = ((([1]^{i_1} [0])^{1+\alpha_1} \circ [0] \circ \ldots \circ [0] \circ ([1]^{i_s} [0])^{1+\alpha_s}) Next)^{1+\zeta} 0 \) 

\( = ((([1]^{i_1} [0])^{1+\alpha_1} \circ \ldots \circ ([1]^{i_s} [0])^{1+\alpha_s}) Next)^{1+\zeta} 0 \) 

The separating [0] are absorbed.

\end{itemize}

We can see that the third case is contained in the fourth one if we remove the restriction \( i_1 \neq 0 \) because if \( i_1 = 0 \) we have \( ([1]^{i_1} [0])^{1+\alpha_1} = [0]^{1+\alpha_1} \) like in the third case.

\bigskip

For more information concerning the correspondence between Simmons notation and Schütte Klammersymbols, see :

http://www.cs.man.ac.uk/~hsimmons/ORDINAL-NOTATIONS/FromBelow.pdf pages 28 - 34.

\bigskip

The Simmons notation can also be used to represent the notation going beyond Veblen functions that we saw previously.

As we saw previously, the large Veblen ordinal is the least fixed point of the function \( \alpha \mapsto \varphi(1_\alpha) \) or \( \alpha \mapsto (\xi \mapsto \omega^\xi) \begin{pmatrix} 1 \\ \alpha \end{pmatrix} \). It is \( Fix (\alpha \mapsto \varphi(1_\alpha)) 0 = Fix (\alpha \mapsto [1]^\alpha [0] Next\ 0) 0 = [2] [1] [0] Next\ 0 \). The fixed points of this function are enumerated by the function F, so we have LVO = F(0). More generally, the \( (1+\alpha\)-th fixed point of  \( \alpha \mapsto \varphi(1_\alpha) \) is \( F(\alpha) = \varphi^+_1(\alpha) = ([2] [1] [0] Next)^{1+\alpha} 0 \).

Then the fixed points of \( F = \varphi^+_1 \) are enumerated by \( G = \varphi^+_2 \). The least fixed point of F is \( G(0) = \varphi^+_2(0) = Fix (\alpha \mapsto ([2] [1] [0] Next)^{1+\alpha} 0) 0 = [0] ([2] [1] [0] Next) 0 \) (because of the absorbsion of "1+") and its \( (1+\alpha) \)-th fixed point is \( G(\alpha) = \varphi^+_2(\alpha) = ([0] ([2] [1] [0] Next))^{1+\alpha} 0 \).

Then the fixed points of \( G = \varphi^+_2 \) are enumerated by \( H = \varphi^+_3 \). The least fixed point of H is \( H(0) = \varphi^+_3(0) = Fix (\alpha \mapsto ([0] ([2] [1] [0] Next)^{1+\alpha} 0) 0 = [0] ([0] ([2] [1] [0] Next)) 0 = [0]^2 ([2] [1] [0] Next) 0 \) and its \( (1+\alpha) \)-th fixed point is \( H(\alpha) = \varphi^+_3(\alpha) = ([0]^2 ([2] [1] [0] Next))^{1+\alpha} 0 \).

More generally, we have \( \varphi^+_{1+\alpha}(0) = [0]^\alpha ([2] [1] [0] Next) 0 \) and \( \varphi^+_{1+\alpha}(\beta) = ([0]^\alpha ([2] [1] [0] Next))^{1+\beta} 0 \).

Then we generalize the function \( \varphi^+ \) to any number of variables : 

\( \varphi^+(\alpha,\beta) = \varphi^+_\alpha(\beta) \)

\( \varphi^+(1,0,0) \) is the least fixed point of the function \( \alpha \mapsto \varphi^+(\alpha,0) = \alpha \mapsto [0]^\alpha ([2] [1] [0] Next) 0 \). It is \( Fix (\alpha \mapsto [0]^\alpha ([2] [1] [0] Next) 0) 0 = [1] [0] ([2] [1] [0] Next) 0 \).

Compare with \( \varphi(1,0,0) = [1] [0] Next 0 \).

More generally, like we found \( \varphi(\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma Next))^{1+\alpha} 0 \), we have \( \varphi^+(\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma ([2] [1] [0] Next)))^{1+\alpha} 0 \).

Like we generalized the \( \varphi \) function to transfinitely many variables reaching all ordinals less than \( LVO = [2] [1] [0] Next\ 0 \), we can generalize the \( \varphi^+ \) function to transfinitely many variables and reach all ordinals less than a new limit which we will call \( LVO^+ = [2] [1] [0] ([2] [1] [0] Next) 0 \) which is the least fixed point of \( \alpha \mapsto [1]^\alpha [0] ([2] [1] [0] Next) 0 \).

Then we can do the same with \( \varphi^{++} = \Phi_2 \) and we shall get similar results with \( ([2] [1] [0])^2 Next \), and generally with \( \Phi_\alpha \), getting formulas with \( ([2] [1] [0])^\alpha Next \).


\bigskip



The limit of Next 0, [0] Next 0, [1] [0] Next 0, [2] [1] [0] Next 0, [3] [2] [1] [0] Next 0, ... 

or \( Next\ \omega, [0] Next\ \omega, [1] [0] Next\ \omega, [2] [1] [0] Next\ \omega, [3] [2] [1] [0] Next\ \omega, \ldots \) 

is called the Bachmann-Howard ordinal (BHO). 

It could be written \( [\omega \ldots 0] Next\ 0 \) or \( [\omega \ldots 0] Next\ \omega \).


\section{Rationalization of the Veblen functions}

When we have defined the different notations, we have arbitrarily chosen some conventions, for example the limit of \( \omega, \omega^\omega, \omega^{\omega^\omega}, \ldots \) have been called  \( \varepsilon_0 \). We could have called it \( \varepsilon_1 \). In this case, \( \varepsilon_\alpha \) would have been the \( \alpha \)-th fixed point of \( \xi \mapsto \omega^\xi \) instead of the the \( (1+\alpha) \)-th one. Also we chose to define \( \varphi(0,\alpha) = \omega^\alpha \). We could have chosen to define \( \varphi(0,\alpha) = \varepsilon_\alpha \). The "1+" which appear in the correspondence between Simmons and Veblen notations may be due to the fact that the choices that have been made are not the most logical. 

We will define a rationalized variant of the Veblen notations which simplifies the correspondence with the Simmons notation :

\begin{itemize}

\item \( \varepsilon_\alpha = \varphi(1,\alpha) = \varepsilon'_{1+\alpha} = \varphi'(0,1+\alpha) \)

\item \( \zeta_\alpha = \varphi(2,\alpha) = \zeta'_{1+\alpha} = \varphi'(1,1+\alpha) \)

\item \( \eta_\alpha = \varphi(3,\alpha) = \eta'_{1+\alpha} = \varphi'(2,1+\alpha) \)

\item Generally, \( \varphi(1+\beta,\alpha) = \varphi'(\beta,1+\alpha) \)

\item \( \Gamma_0 = \varphi(1,0,0) = \varphi'(1,0,1) \)

\item Generally, if \( \gamma \neq 0, \varphi(\gamma,\beta,\alpha) = \varphi'(\gamma,\beta,1+\alpha) \)

\item In a similar way, if \( \gamma \neq 0 \) or \( \delta \neq 0, \varphi(\delta,\gamma,\beta,\alpha) = \varphi'(\delta,\gamma,\beta,1+\alpha) \) and so on.

\end{itemize}

With this notation, the correspondence with Simmons notation becomes simpler, for example we have :

\begin{itemize}

\item 
\( \varepsilon'_\alpha = Next^\alpha 0 \) instead of \( \varepsilon_\alpha = Next^{1+\alpha} 0 \)

\item
\( \varphi'(\beta,\alpha) = ([0]^\beta Next)^\alpha 0 \) 
instead of
\( \varphi(1+\beta,\alpha) = ([0]^\beta Next)^{1+\alpha} 0 \) 

\item
\( \varphi'(\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma Next))^\alpha 0 \)
instead of 
\( \varphi(\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma Next))^{1+\alpha} 0 \)

\item
\( \varphi'(\delta,\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma (([1]^2 [0])^\delta Next)))^{1+\alpha} 0  \) 
instead of 
\( \varphi(\delta,\gamma,\beta,\alpha) = ([0]^\beta (([1] [0])^\gamma (([1]^2 [0])^\delta Next)))^{1+\alpha} 0  \) 

\end{itemize}

It appears that the last variable (\(\alpha\) in the previous examples) plays a different role from the other variables, so it could be more logical to write for example  \( \varphi'_{\delta,\gamma,\beta}(\alpha) \) instead of \( \varphi'(\delta,\gamma,\beta,\alpha) \) and to consider that \( \beta \) is at position 0, \( \gamma \) at position 1 and \( \delta \) at position 2. In this case, we see that the position corresponds to the exponent of [1] in the Simmons representation.

We can also use collapsing to represent the index list, writing for example :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \Gamma_0 = \varphi'_{1,0}(1) = \varphi'_\Omega(1) \)
\item Ackermann ordinal = \( \varphi'_{1,0,0}(1) = \varphi'_{\Omega^2}(1) \)
\item \( SVO = \varphi'_{\Omega^\omega}(1) \)
\end{itemize}

This notation even permits writing ordinals that are out of range of Veblen notation like :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( LVO = \varphi'_{\Omega^\Omega}(1) \)
\item \( \varphi'_{\Omega^{\Omega^\Omega}}(1) \)
\item \( \ldots \)
\end{itemize}

\section{RHS0 notation}

\subsection{Basic principles}

Like Simmons notation, the RHS0 notation uses lambda calculus formalism.

The basic method consists in :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item    Start from 0
\item    If we don't see any regularity, take the successor (add 1)
\item    If we see a regularity and we don't have a notation for it, invent it and jump to the limit
\item    If we see a regularity and we already have a notation for it, use it and jump to the limit. 
\end{itemize}

The difficulty, which requires intelligence, is to see the regularities. It gives the following sequence :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \(    0 \) : no regularity, take the successor
\item \(    suc\ 0 \) : no regularity, take the successor
\item \(    suc (suc\ 0) \) : regularity : suc repeatedly applied to 0. No notation, invent it : H f x = limit of x, f x, f (f x), ... 
\item \(    H suc\ 0 \) : no regularity, take the successor
\item \(    suc (H suc\ 0) \) : no regularity, take the successor
\item \(    suc (suc (H suc\ 0)) \) : regularity : suc repeatedly applied to H suc 0, notation exists
\item \(    H suc (H suc\ 0) \) : regularity : H suc repeatedly applied to 0, notation exists
\item \(    H (H suc) 0 \) : regularity : H repeatedly applied to suc, notation exists
\item \(    H H suc\ 0 \) : regularity (suc 0, ..., H suc 0, ... H H suc 0, ... H H H suc 0, ...), invent notation \( R_1 H suc\ 0 \) for the limit of this sequence 
\item \(    R_1 H suc\ 0 \) : no regularity, take the successor
\item \(    suc (R_1 H suc\ 0) \)
\item \(    suc (suc (R_1 H suc\ 0)) \)
\item \(    H suc (R_1 H suc\ 0) \)
\item \(    suc (H suc (R_1 H suc\ 0)) \)
\item \(    suc (suc (H suc (R_1 H suc\ 0))) \)
\item \(    H suc (H suc (R_1 H suc\ 0)) \)
\item \(    H (H suc) (R_1 H suc\ 0) \)
\item \(    H H suc (R_1 H suc\ 0) \)
\item \(    R_1 H suc (R_1 H suc\ 0) \)
\item \(    H (R_1 H suc) 0 \)
\item \(    suc (H (R_1 H suc) 0) \)
\item \(    suc (suc (H (R_1 H suc) 0)) \)
\item \(    H suc (H (R_1 H suc) 0) \)
\item \(    suc (suc (H suc (H (R_1 H suc) 0))) \)
\item \(    H suc (H suc (H (R_1 H suc) 0))) \)
\item \(    H (H suc) (H (R_1 H suc) 0) \)
\item \(    H H suc (H (R_1 H suc) 0) \)
\item \(    R_1 H suc (H (R_1 H suc) 0) \)
\item \(    suc (R_1 H suc (H (R_1 H suc) 0)) \)
\item \(    suc (suc (R_1 H suc (H (R_1 H suc) 0))) \)
\item \(    H suc (R_1 H suc (H (R_1 H suc) 0)) \)
\item \(    suc (H suc (R_1 H suc (H (R_1 H suc) 0))) \)
\item \(    suc (suc (H suc (R_1 H suc (H (R_1 H suc) 0)))) \)
\item \(    H suc (H suc (R_1 H suc (H (R_1 H suc) 0))) \)
\item \(    H (H suc) (R_1 H suc (H (R_1 H suc) 0)) \)
\item \(    H H suc (R_1 H suc (H (R_1 H suc) 0)) \)
\item \(    R_1 H suc (R_1 H suc (H (R_1 H suc) 0)) \)
\item \(    H (R_1 H suc) (H (R_1 H suc) 0) \)
\item \(    H (H (R_1 H suc)) 0 \)
\item \(    H H (R_1 H suc) 0 \)
\item \(    R_1 H (R_1 H suc) 0 \)
\item \(    H (R_1 H) suc\ 0 \)
\item \(    ... \)
\item \(    R_1 H (R_1 H) suc\ 0 \)
\item \(    R_1 (R_1 H) suc\ 0 \)
\item \(    H R_1 H suc\ 0 \)
\item \(    ... \)
\item \(    R_1 H R_1 H suc\ 0 \) : invent notation \( R_2 R_1 H suc\ 0 = \) limit of \( suc\ 0, R_1 H suc\ 0, R_1 H R_1 H suc\ 0, ... \)
\item \(    ... \)
\item \(    R_3 R_2 R_1 H suc\ 0 \) : invent notation \( R_{3...1} H suc\ 0 \) and jump to limit
\item \(    R_{\omega...1} H suc\ 0 \)
\item \(    ... \)
\item \(    R_2 R_{\omega...1} H suc\ 0 \) : invent notation \( R_{\omega+1...1} H suc\ 0 \)
\item \(    ...  \)

\end{itemize}

To progress faster, we can use the following rule :

If we have found an ordinal \( \alpha \), and later another ordinal \( \beta \) of the form \( f (s (s z)) \), we may produce an ordinal \( \gamma = f ([suc \rightarrow s,0 \rightarrow z] \alpha) \) where \( [suc \rightarrow s, 0 \rightarrow z] \alpha \) means the expression obtained by replacing suc by s and 0 by z in \( \alpha \).

For example :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \( \alpha = R_1 H suc\ 0 \)
\item \( \beta = R_1 H (R_1 H suc) 0 \)
\item \( s = R_1 H \)
\item \( z = suc \)
\item \( f x = x\ 0 \)
\item \( [suc \rightarrow R_1 H,0 \rightarrow suc] \alpha = R_1 H (R_1 H) suc \)
\item \( \gamma = f ([suc \rightarrow R_1 H,0 \rightarrow suc] \alpha) = R1 H (R1 H) suc\ 0 \)

\end{itemize}


With the following rules :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \( 0 : \rightarrow 0 \)
\item \( suc : x \rightarrow suc\ x \)
\item \( H : f (f x) -> H f x \)
\item \( R_1 : f f -> R_1 f \)
\item \( R_2 : f g f g -> R_2 f g \)
\item \( R_3 : f g h f g h -> R_3 f g h \)
\item ...
\item \( Repl : \alpha, f (s (s z)) \rightarrow f([suc \rightarrow s,0 \rightarrow z] \alpha) \)

\end{itemize} 

we can produce the following sequence of ordinals :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item    0 : \( 0 : 0 \)
\item    1 : \( suc\ 0 : suc\ 0 \)
\item    2 : \( suc\ 1 : suc\ (suc\ 0) \)
\item    3 : \( H 2 : H suc\ 0 \)
\item    4 : \( suc\ 3 : suc\ (H suc\ 0) \)
\item    5 : \( suc\ 4 : suc\ (suc\ (H suc\ 0)) \)
\item    6 : \( H 5 : H suc\ (H suc\ 0) \)
\item    7 : \( H 6 : H (H suc) 0 \)
\item    8 : \( H 7 : H H suc\ 0 \)
\item    9 : \( R_1 8 : R_1 H suc\ 0 \)
\item    10 : \( suc\ 9 : suc\ (R_1 H suc\ 0) \)
\item    11 : \( suc\ 10 : suc\ (suc\ (R_1 H suc\ 0)) \)
\item    12 : \( Repl\ 9\ 11 [suc->suc,0->R_1 H suc\ 0] : R_1 H suc\ (R_1 H suc\ 0) \)
\item    13 : \( Repl\ 9\ 12 [suc->R_1 H suc,0->0] : R_1 H (R_1 H suc) 0 \)
\item    14 : \( Repl\ 9\ 13 [suc->R_1 H,0->suc] : R_1 H (R_1 H) suc\ 0 \)
\item    15 : \( R_1 14 : R_1 (R_1 H) suc\ 0 \)
\item    16 : \( Repl\ 9\ 15 [suc->R_1,0->H] : R_1 H R_1 H suc\ 0 \)
\item    17 : \( R_2 16 : R_2 R_1 H suc\ 0  \)

\end{itemize}

The rules \( R_1, R_2, R_3, \) ... may be replaced by H or Repl if f1 ... fn ... f1 ... fn 
is reformulated in \( <f_1,...,f_n> ( ... (<f_1,...,f_n> I)...) \) with \( <f_1,...,f_n> g = g\ f_1 ... f_n \) :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item    0 : 0 : 0
\item    1 : suc 0 : suc 0
\item    2 : suc 1 : suc (suc 0)
\item    3 : H 2 : H suc 0
\item    4 : suc 3 : suc (H suc 0)
\item    5 : suc 4 : suc (suc (H suc 0))
\item    6 : Repl 3 5 [suc-$>$suc,0-$>$H suc 0] : H suc (H suc 0)
\item    7 : Repl 3 6 [suc-$>$H suc,0-$>$0] : H (H suc) 0
\item    8 : Repl 3 7 [suc-$>$H,0-$>$suc] : H H suc 0 = $<$H$>$ ($<$H$>$ I) suc 0
\item    9 : Repl 3 8 [suc-$>$$<$H$>$,0-$>$I] : H $<$H$>$ I suc 0
\item    10 : suc 9 : suc (H $<$H$>$ I suc 0)
\item    11 : suc 10 : suc (suc (H $<$H$>$ I suc 0))
\item    12 : Repl 9 10 [suc-$>$suc,0-$>$H $<$H$>$ I suc 0] : H $<$H$>$ I suc (H $<$H$>$ I suc 0)
\item    13 : Repl 9 12 [suc-$>$H $<$H$>$: I suc,0-$>$0] : H $<$H$>$ I (H $<$H$>$ I suc) 0
\item    14 : Repl 9 13 [suc-$>$H $<$H$>$ I,0-$>$suc] : H $<$H$>$ I (H $<$H$>$ I) suc 0 = $<$H $<$H$>$ I$>$ ($<$H $<$H$>$ I$>$ I) suc 0
\item    15 : Repl 3 14 [suc-$>$$<$H $<$H$>$ I$>$,0-$>$I] : H $<$H $<$H$>$ I$>$ I suc 0 = [H $<$*$>$ I] ([H $<$*$>$ I] H) suc 0
\item    16 : Repl 9 15 [suc-$>$[H $<$*$>$ I],0-$>$H] : H $<$H$>$ I [H $<$*$>$ I] H suc 0 
\item     = [H $<$*$>$ I] H [H $<$*$>$ I] H suc 0 = $<$[H $<$*$>$ I],H$>$ ($<$[H $<$*$>$ I], H$>$ I) suc 0
\item    17 : Repl 3 16 [suc-$>$$<$[H $<$*$>$ I],H$>$,0-$>$I] : H $<$[H $<$*$>$ I], H$>$ I suc 0 

\end{itemize}

More formally, the RHS0 notation uses lambda calculus with De Bruijn indexes.
\( \lambda.x \) is written [ x ] and variables are written *, **, ***..., or \( \bullet, \bullet \bullet, \bullet \bullet \bullet, \) ...
for example [ ... * ... ] = \( [ ... \bullet ... ] = \lambda x ( ... x ... ) \)

\begin{verbatim}

CI = C I is defined by CI x f = f x.
CI x = <x>
<x1,...,xn> f = f x1 ... xn
tuple n f x1 ... xn = f <x1,...,xn>
tuple 0 = <I>
tuple (n+1) f x = tuple n [ f (insert x *) ]
with insert x a f  = a (f x)

r 0 f x = x
r (n+1) f x = f (r n f x)
r (lim g) f x = lim [r * f x]

H f x represents the limit of x, f x, f (f x), ...
H f x = r w f x

\end{verbatim}

\( R_1 = [H <\bullet> I] = tuple\ 1 [H \bullet I] \)

\( R_2 = [[H <\bullet\bullet,\bullet> I]] = tuple\ 2 [H \bullet I] \)

\( R_3 = [[[H <\bullet\bullet\bullet,\bullet\bullet,\bullet> I]]] = tuple\ 3 [H \bullet I] \)

\( R_n = tuple\ n [H \bullet I] \)

\( R_{n \ldots 1} = R_n \ldots R_1 \)

\( S_{n...1} = [S_{\bullet...1}] n = <R_n,...,R_1> \)

\( R_{n \ldots 1} = S_{n \ldots 1} I \)

\( [S_{\bullet \ldots 1}] 0 = I \)

\( [S_{\bullet \ldots 1}] (n+1) = insert (tuple (n+1) [H \bullet I]) ([S_{\bullet \ldots 1}] n) \)

\begin{verbatim}

L f = lim f 0, f 1, ...
L f x = L [f * x]
H = [[L [r * *** **]]]
or
L0 = lim f 0, f 1, ...
L n f = tuple n [ L0 [ ** (f *) ]]
L n = [ tuple n [ L0 [ ** (*** *) ]]]
L = [[ tuple ** [ L0 [ ** (*** *) ]]]
 = \n \f (tuple n \a (L0 \i (a (f i)) ) )
 
\end{verbatim}

To represent the replacement \( [suc \rightarrow s,0 \rightarrow z] \) we can represent ordinals by ordinal functions which, when applied to suc and 0, give the considered ordinal. For example, \( R_1 H suc\ 0 \) is represented by the ordinal function \( s \mapsto z \mapsto R_1 H s z, R_1 H (R_1 H suc) 0 \) by \( s \mapsto z \mapsto R_1 H (R_1 H s) z \). From these ordinals, with the replacement \( [suc \rightarrow R_1 H,0 \rightarrow suc] \) we can produce a new ordinal represented by \( s \mapsto z \mapsto ((s \mapsto z \mapsto R_1 H s z) (R_1 H) s z) = s \mapsto z \mapsto R_1 H (R_1 H) s z) \) which, when applied to suc and 0, gives \( R_1 H (R_1 H) suc\ 0 \).

Operations can be represented with replacements :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \( \alpha+\beta = [0 \rightarrow \alpha] \beta \)
\item \( \alpha \cdot \beta = [suc \rightarrow [\bullet+\alpha]] \beta = [suc->[[0 \rightarrow \bullet\bullet] \alpha]] \beta \)
\item \( \alpha^\beta = [suc \rightarrow [\bullet \cdot \alpha], 0 \rightarrow 1] \beta = [suc \rightarrow [[suc \rightarrow[[0 \rightarrow \bullet\bullet] \bullet\bullet\bullet]] \alpha], 0 \rightarrow suc\ 0] \beta \)
\item \( \omega^\alpha = [suc \rightarrow [suc \rightarrow H suc], 0 \rightarrow suc\ 0] \alpha = [suc \rightarrow H,0 \rightarrow suc] \alpha\ 0 \) 
\item \( {\varepsilon_0}^\alpha = [suc \rightarrow R_1 H,0 \rightarrow suc] \alpha 0 \)
\item \( \varepsilon_a = [suc \rightarrow R_1, 0 \rightarrow H] (1+\alpha) suc\ 0 ; 1+\alpha = [0 \rightarrow suc\ 0] \alpha \) 

\end{itemize}



\subsection{Correspondence with other notations}

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \( suc\ 0 = 0 + 1 = 1 \)
\item \( suc\ (suc\ 0) = 1 + 1 = 2 \)
\item \( H suc\ 0 = \omega \)
\item \( suc\ (H suc\ 0) = \omega + 1 \)
\item \( H suc\ (H\ suc\ 0) = \omega + \omega = \omega \cdot 2 \)
\item \( H (H suc)\ 0 = \omega \cdot \omega = \omega^2 \)
\item \( H H suc\ 0 = \omega^\omega \)
\item \( R_1 H suc\ 0 = \) limit of \( suc\ 0, H suc\ 0, H H suc\ 0, H H H suc\ 0, \ldots = \varepsilon_0 = \varphi(1,0) = \varphi'(0,1) = Next\ \omega \)
\item \( suc (R_1 H suc\ 0) = \varepsilon_0 + 1 \)
\item \( R_1 H suc (R_1 H suc\ 0) = \varepsilon_0 + \varepsilon_0 = \varepsilon_0 \cdot 2 \)
\item \( R_1 H (R_1 H suc) 0 = \varepsilon_0 \cdot \varepsilon_0 = {\varepsilon_0}^2 \)
\item \( R_1 H (R_1 H) suc\ 0 = {\varepsilon_0}^{\varepsilon_0} \)
\item \( R_1 H (R_1 H) (R_1 H) suc\ 0 ) = {\varepsilon_0}^{{\varepsilon_0}^{\varepsilon_0}} \)
\item \( R_1 (R_1 H) suc\ 0 = \varepsilon_1 = \varphi(1,1) = \varphi'(0,2) = Next (Next\ \omega) \) ( note again that the correspondence is clearer with the rationalized function \( \varphi' \)

\end{itemize}

We have previously seen that \( \varepsilon_1 \) is the limit of \( \varepsilon_0, {\varepsilon_0}^{\varepsilon_0}, {\varepsilon_0}^{{\varepsilon_0}^{\varepsilon_0}}, \ldots \) and is also the limit of \( \varepsilon_0+1, \omega^{\varepsilon_0+1}, \omega^{\omega^{\varepsilon_0+1}}, \ldots \) and we have proved the equivalence of these two fundamental sequences. We have seen that the first fundamental sequence is equivalent to \( \omega, {\varepsilon_0}^\omega, {\varepsilon_0}^{{\varepsilon_0}^\omega}, \ldots \), so we proved the equivalence of the two fundamental sequences by proving that for any n, we have :

 \( \omega^{\omega^{\vdots^{\omega^{\omega^{\varepsilon_0+1}}}}} = \varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}} \)

We will now see how we can prove it using RHS0 notation.

First we will write the two sides of this equality using RHS0 notation :

We will use the notation \( X \ldots X \) for X repeated n times.

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \varepsilon_0 = R_1 H suc\ 0 \)
\item \( \varepsilon_0 + 1 = suc (R_1 H suc\ 0) \)
\item \( \omega^{\varepsilon_0+1} = [suc \rightarrow H, 0 \rightarrow suc] (suc (R_1 H suc 0)) 0 = H (R_1 H H suc) 0 = H (R_1 H suc) 0 \)
\item \( \omega^{\omega^{\varepsilon_0+1}} = H (R_1 H H) suc\ 0 = H (R_1 H) suc\ 0 \)
\item \( \omega^{\omega^{\omega^{\varepsilon_0+1}}} = H (R_1 H) H suc\ 0 \)
\item \( \omega^{\omega^{\omega^{\omega^{\varepsilon_0+1}}}} = H (R_1 H) H H suc\ 0 \)
\item \( \ldots \)
\item \( \omega^{\omega^{\vdots^{\omega^{\omega^{\varepsilon_0}}}}} = H (R_1 H) H \ldots H suc\ 0 \)
\end{itemize}

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \omega = H suc\ 0 \)
\item \( \varepsilon_0^\omega = [suc \rightarrow R_1 H, 0 \rightarrow suc] \omega 0 = H (R_1 H) suc\ 0 \)
\item \( \varepsilon_0^{\varepsilon_0^\omega} = H (R_1 H) (R_1 H) suc\ 0 \)
\item \( \varepsilon_0^{\varepsilon_0^{\varepsilon_0^\omega}} = H (R_1 H) (R_1 H) (R_1 H) suc\ 0 \)
\item \( \ldots \)
\item \( \varepsilon_0^{\varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}}} = H (R_1 H) \ldots (R_1 H) (R_1 H) suc\ 0 \)
\end{itemize}

We will now prove the equality \( H (R_1 H) H \ldots H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) suc\ 0 \) for any n by induction.

\bigskip

For n = 0, the equality is trivial : \( H (R_1 H) suc\ 0 = H (R_1 H) suc\ 0 \).

\bigskip

We will now suppose \( H (R_1 H) H \ldots H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) suc\ 0 \) for a given n and prove it for n + 1 :

\( H (R_1 H) H \ldots H H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) (R_1 H) suc\ 0  \)

\bigskip

By elevating \( \omega \) at the power of each side of this equality, we get : 

\( [suc \rightarrow H, 0 \rightarrow suc] (H (R_1 H) H \ldots H suc\ 0) 0 = [suc \rightarrow H, 0 \rightarrow suc] (H (R_1 H) \ldots (R_1 H) (R_1 H) suc\ 0) 0 \)

(1) \( H (R_1 H) H \ldots H H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) H suc\ 0 \)

\bigskip

We also have :

\( H (R_1 H) \ldots (R_1 H) suc\ 0 = H (R_1 H) \ldots (R_1 H) suc (suc\ 0) \)

which corresponds to the RHS0 notation for :

\( \varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}} = 1 + \varepsilon_0^{\vdots^{{\varepsilon_0}^\omega}} \)

by absorpsion of "1+" and "suc".

Now we elevate \( \varepsilon_0 \) to the power of each side of this equality, which gives :

\( [suc \rightarrow R_1 H, 0 \rightarrow suc] (H (R_1 H) \ldots (R_1 H) suc\ 0) 0 = [suc \rightarrow R_1 H, 0 \rightarrow suc] (H (R_1 H) \ldots (R_1 H) suc (suc\ 0)) 0 \)

\( H (R_1 H) \ldots (R_1 H) (R_1 H) suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) (R_1 H suc) 0 \)

Then we elevate \( \omega \) to the power of each side of this equality :

\( [suc \rightarrow H, 0 \rightarrow suc] (H (R_1 H) \ldots (R_1 H) (R_1 H) suc\ 0) 0 = [suc \rightarrow H, 0 \rightarrow suc] (H (R_1 H) \ldots (R_1 H) (R_1 H) (R_1 H suc) 0) 0 \)

\( H (R_1 H) \ldots (R_1 H) (R_1 H) H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) (R_1 H H) suc\ 0 \)

which can be simplified to :

\( H (R_1 H) \ldots (R_1 H) (R_1 H) H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) (R_1 H) suc\ 0 \)

Noting that the left side of this last equality is the same as the right side of (1), we get by transitivity of equality, equating the left side of (1) with the right side of the last equality :

\( H (R_1 H) H \ldots H H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) (R_1 H) suc\ 0  \)

which corresponds to the equality we wanted to prove for n+1.

\bigskip

Then the correspondence continues with :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \( R_1 (R_1 (R_1 H)) suc\ 0 = \varepsilon_2 = \varphi(1,2) = \varphi'(0,3) = Next (Next (Next\ \omega)) \)
\item \( H R_1 H suc\ 0 = \varepsilon_\omega = \varphi(1,\omega) = \varphi'(0,\omega) = Next^\omega \omega \)
\item \( R_1 H R_1 H suc\ 0 = \varepsilon_{\varepsilon_0} \)
\item \( R_1 H R_1 H R_1 H suc\ 0 = \varepsilon_{\varepsilon_{\varepsilon_0}} \)
\item \( R_2 R_1 H suc\ 0 = \zeta_0 = \varphi(2,0) = \varphi'(1,1) = [0] Next\ \omega \)

\end{itemize}

The next step is \( \zeta_1 \) which is the next fixed point of the function \( \alpha \mapsto \varepsilon_\alpha \), the limit of \( \zeta_0+1, \varepsilon_{\zeta_0+1}, \varepsilon_{\varepsilon_{\zeta_0+1}}, \ldots \). \( \varepsilon_\alpha \) is \( [suc \rightarrow R_1, 0 \rightarrow H] (1+\alpha) suc\ 0 \), or \( [suc \rightarrow R_1, 0 \rightarrow H] \alpha\ suc\ 0 \) if \( \alpha \geq \omega \) by absorbsion of "1+". This is the result of replacing suc by \( R_1 \) and 0 by H in \( \alpha \) and applying the result to suc and 0. So by iterating this transformation we get that \( \zeta_1 \) is the limit of :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \zeta_0+1 = suc (R_2 R_1 H suc\ 0) \)
\item \( R_1 (R_2 R_1 H R_1 H) suc\ 0 = R_1 (R_2 R_1 H) suc\ 0 \)
\item \( R_1 (R_2 R_1 H) R_1 H suc\ 0 \)
\item \( R_1 (R_2 R_1 H) R_1 H R_1 H suc\ 0 \)
\item \( \ldots \)
\end{itemize}

In the previous correnspondence formulas, we can see a correspondence between RHS0 and Simmons notations :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_2 \leftrightarrow [0] \)
\item \( R_1 \leftrightarrow Next \)
\item \( H \leftrightarrow \omega \)
\item suc 0 at the end of the RHS0 notation
\end{itemize}

If we apply this correspondence to \( \zeta_1 = [0] Next ([0] Next\ \omega) \) (see "Simmons notation / Correspondence with Veblen functions") we get \( \zeta_1 = R_2 R_1 (R_2 R_1 H) suc\ 0 \).

\bigskip

This is the limit of :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_1 (R_2 R_1 H) suc\ 0 \) 
\item \( R_1 (R_2 R_1 H) R_1 (R_2 R_1 H) suc\ 0 \)
\item \( R_1 (R_2 R_1 H) R_1 (R_2 R_1 H) R_1 (R_2 R_1 H) suc\ 0 \)
\item \( \ldots \)
\end{itemize}

Compare with what we found previously :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \zeta_0+1 = suc (R_2 R_1 H suc\ 0) \)
\item \( R_1 (R_2 R_1 H R_1 H) suc\ 0 = R_1 (R_2 R_1 H) suc\ 0 \)
\item \( R_1 (R_2 R_1 H) R_1 H suc 0 \)
\item \( R_1 (R_2 R_1 H) R_1 H R_1 H suc 0 \)
\item \( \ldots \)
\end{itemize}

and with the previously proven equality :

\( H (R_1 H) H \ldots H suc\ 0 = H (R_1 H) \ldots (R_1 H) (R_1 H) suc\ 0 \)

which could also be written :

\( H (R_1 H) H \ldots H suc\ 0 = H (R_1 H) (R_1 H) \ldots (R_1 H) suc\ 0 \)

There is probably a similar equality :

\( R_1 (R_2 R_2 H) R_1 H \ldots R_1 H suc\ 0 = R_1 (R_2 R_1 H) R_1 (R_2 R_1 H) \ldots R_1 (R_2 R_1 H) suc\ 0 \)

which would prove the equivalence of the two fundamental sequences.

\bigskip

So we can go on with our correspondences :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_2 R_1 (R_2 R_1 H) suc\ 0 = \zeta_1 = \varphi(2,1) = \varphi'(1,2) = [0] Next ([0] Next\ \omega) \)
\item \( H (R_2 R_1) H suc\ 0 = \zeta_\omega \)
\item \( R_2 R_1 H (R_2 R_1) H suc\ 0 = \zeta_{\zeta_0} \)
\item \( R_2 (R_2 R_1) H suc\ 0 = \eta_0 = \varphi(3,0) = \varphi'(2,1) = [0] ([0] Next) \omega \)
\item \( H R_2 R_1 H suc\ 0 = \varphi(\omega,0) = \varphi'(\omega,1) \)
\item \( R_1 H R_2 R_1 H suc\ 0 = \varphi(\varepsilon_0,0) = \varphi(\varphi(1,0),0) = \varphi'(\varepsilon_0,1) = \varphi'(\varphi'(0,1),1) \)
\item \( R_2 R_1 H R_2 R_1 H suc\ 0 = \varphi(\zeta_0,0) = \varphi(\varphi(2,0),0) = \varphi'(\zeta_0,1) = \varphi'(\varphi'(1,1),1) \)
\item \( R_3 R_2 R_1 H suc\ 0 = \Gamma_0 = \varphi(1,0,0) = \varphi'(1,0,1) = [1] [0] Next\ \omega \)
\end{itemize}

We may then extend our correspondence rule :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_3 \leftrightarrow [1] \)
\item \( R_2 \leftrightarrow [0] \)
\item \( R_1 \leftrightarrow Next \)
\item \( H \leftrightarrow \omega \)
\item suc 0 at the end of the RHS0 notation
\end{itemize}

It is likely that this correspondence can be generalized in a simple and logical way, and it seems to me that the simpler generalization is :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_{n+2} \leftrightarrow [n] \)
\item \( R_1 \leftrightarrow Next \)
\item \( H \leftrightarrow \omega \)
\item suc 0 at the end of the RHS0 notation
\end{itemize}

I will call it the "Simmons - RHS0 correspondence conjecture".



\bigskip

Then, if the correspondence conjecture is true, the correspondence goes on with : 

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_3 R_2 R_1 H suc\ 0 = \Gamma_0 = \varphi(1,0,0) = \varphi'(1,0,1) = [1] [0] Next\ \omega \)
\item \( R_3 (R_3 R_2) R_1 H suc\ 0 = \varphi(1,0,0,0) = \varphi'(1,0,0,1) = [1] ([1] [0]) Next\ 0 \) (Note that in the \( \varphi \) and \( \varphi' \) functions, the last variable plays a different role than the others, as mentioned previously, so the most logical representation should probably be \( \varphi'_{1,0,0}(1) \) where the first 1 should be considered at position 2 and not 3, in this case its position corresponds to the number of occurences (or the exponent) of \( R_3 \) and [1])
\item \( H R_3 R_2 R_1 H suc\ 0 = SVO = [1]^\omega [0] Next\ \omega \)
\item \( R_4 R_3 R_2 R_1 H suc\ 0 = LVO = [2] [1] [0] Next\ \omega \)
\item \( R_{\omega \ldots 1} H suc\ 0 = BHO \)
\item \( \ldots \)
\end{itemize}

Note the importance of using logical notations to make correct conjectures : if, instead of \( \varphi' \), we use the less logical function \( \varphi \), we have the correspondence :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_1 H suc\ 0 = \varepsilon_0 = \varphi(1,0) \)
\item \( R_2 R_1 H suc\ 0 = \zeta_0 = \varphi(2,0) \)
\end{itemize}

and we could think that it continues with :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R_3 R_2 R_1 H suc\ 0 = \eta_0 = \varphi(3,0) \)
\item \( R_{\omega \ldots 1} H suc\ 0 = \varphi(\omega,0) \)
\end{itemize}

\subsection{Going further with RHS0 notation and collapsing}

The Bachmann-Howard ordinal (BHO) is the limit of \( R_1 H suc\ 0, R_2 R_1 H suc\ 0, R_3 R_2 R_1 H suc\ 0, \ldots \) which we will write \( R_{\omega \ldots 1} H suc\ 0 \).

We can go on ascending ordinals after BHO :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item \( BHO = R_{\omega \ldots 1} H suc\ 0 \)
\item \( suc (R_{\omega \ldots 1} H suc\ 0) \)
\item \( R_{\omega \ldots 1} H suc\ (R_{\omega \ldots 1} H suc\ 0) \)
\item \( R_{\omega \ldots 1} H (R_{\omega \ldots 1} H suc) 0 \)
\item \( R_{\omega \ldots 1} H (R_{\omega \ldots 1} H) suc\ 0 \)
\item \( R_1 (R_{\omega \ldots 1} H) suc\ 0 \)
\item \( R_{\omega \ldots 1} (R_{\omega \ldots 1} H) suc\ 0 \)
\item \( H R_{\omega \ldots 1} H suc\ 0 \)
\item \( R_2 R_{\omega \ldots 1} H suc\ 0 \)
\item \( R_3 R_2 R_{\omega \ldots 1} H suc\ 0 \)
\item \( R_{\omega \ldots 2} R_{\omega \ldots 1} H suc\ 0 \) which we will write \( R_{\omega \cdot 2 \ldots 1} H suc\ 0 \)
\item \( R_{\omega \ldots 3} R_{\omega \ldots 2} R_{\omega \ldots 1} H suc\ 0 \) which we will write \( R_{\omega \cdot 3 \ldots 1} H suc\ 0 \)
\item \( R_{\omega^2 \ldots 1} H suc\ 0 \)
\item \( R_{\varepsilon_0 \ldots 1} H suc\ 0 = R_{R_1 H suc\ 0 \ldots 1} H suc\ 0 \) 

\end{itemize}

Then we can take the least fixed point of the function \( \alpha \mapsto R_{\alpha \ldots 1} H suc\ 0 \) which we can also write \( [R_{\bullet \ldots 1} H suc\ 0] \). This fixed point is \(  H [R_{\bullet \ldots 1} H suc\ 0] 0 \) which we may also write \( R^1_1 H suc\ 0 \) if we define \( R^1_1 x_1 x_2 x_3 = H [R_{\bullet \ldots 1} x_1 x_2 x_3] 0 \). Then the ascension goes on with :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( H [R_{\bullet \ldots 1} H suc\ 0] 0 = R^1_1 H suc\ 0 \)
\item \( R_2 R^1_1 H suc\ 0 \)
\item \( R_3 R_2 R^1_1 H suc\ 0 \)
\item \( R_{\omega \ldots 2} R^1_1 H suc\ 0 \)
\item \( H [R_{\bullet \ldots 2} R^1_1 H suc\ 0] 0 = R^1_2 R^1_1 H suc\ 0 = R^1_{2 \ldots 1} H suc\ 0 \) with \( R^1_2 x_1 x_2 x_3 x_4 = H [R_{\bullet \ldots 2} x_1 x_2 x_3 x_4] 0 \) 
\item \( R^1_3 R^1_2 R^1_1 H suc\ 0 = R^1_{3 \ldots 1} H suc\ 0 \)
\item \( R^1_{\omega \ldots 1} H suc\ 0 \)
\item \( H [R^1_{\bullet \ldots 1} H suc\ 0] 0 = R^2_1 H suc\ 0 \) with \( R^2_1 x_1 x_2 x_3 = H [R^1_ {\bullet \ldots 1} x_1 x_2 x_3] 0 \)
\item \( R^3_1 H suc\ 0 \)
\item \( R^\omega_1 H suc\ 0 \)
\item \( H [R^\bullet_1 H suc\ 0] 0 = R^{1,0}_1 H suc\ 0 \) with \( R^{1,0}_1 x_1 x_2 x_3 = H [R^\bullet_1 x_1 x_2 x_3] 0 \)
\item \( R^{1,0,0}_1 H suc\ 0 \)

\end{itemize}

We can number the positions in the list of upper indices of R or introduce collapsing to write

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( R^1_1 = R^{1_0}_1 = R^{0:1}_1 \)
\item \( R^{1,0}_1 = R^{1_1}_1 = R^{1:1}_1 = R^\Omega_1 \)
\item \( R^{1,0,0}_1 = R^{1_2}_1 = R^{2:1}_1 = R^{\Omega^2}_1 \)
\item \( \ldots \)
\end{itemize}

We also need a notation for uncountable ordinals. We can take \( \Omega = \omega_1 \) the least uncountable ordinal and  use a notation similar to the one we used for countable ordinals, replacing H by \( H_1 \) when \( \omega \) is replaced by \( \Omega = \omega_1 \), writing for example :

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item \( \Omega = \omega_1 = H_1 suc\ 0 \)
\item \( \Omega^2 = H_1 (H_1 suc) 0 \)
\item \( \Omega^\omega = H H_1 suc\ 0 \)
\item \( \Omega^\Omega = H_1 H_1 suc\ 0 \)
\item \( \Omega^{\Omega^\Omega} = H_1 H_1 H_1 suc\ 0 \)
\item \( \ldots \)
\end{itemize}

Then we can go on ascending ordinals by using greater and greater uncountable ordinals as upper indices of R, for example :

\( R^{H [R^\bullet_1 H_1 suc\ 0] 0}_1 H suc\ 0 \)

\bigskip

Because of the correspondence between RHS0 and Simmons notations, we could probably do something similar with Simmons notation.



\section{Ordinal collapsing functions}

An ordinal collapsing function is a function which, when applied to an uncountable ordinal, gives a countable ordinal.

The general idea is to define a set of ordinals C(a) or C(a,b) where a and b are ordinals, which contains all ordinals that can be built using an initial set of ordinals and some operations or functions, and then define \( \psi(a) \) or \( \psi(a,b) \) as the smallest ordinal which is not in C(a) or C(a,b), or the least ordinal which is greater than than all countable ordinals of C(a) or C(a,b).

Different ordinal collapsing functions are described in http://googology.wikia.com/wiki/Ordinal\_notation .

These functions are extensions of functions on countable ordinals, whose fixed points can be reached by applying them to an uncountable ordinal.

Here is a correspondence between basic notation systems and their collapsing extensions based on formula : least fixed point of \( f = f(\Omega) \) :

\bigskip

\begin{tabular}{|c|c|c|c|c|c|} \hline
Basic notation	& Formula			& Limit					& Extension		& Correspondence					& Crossing 				\\ \hline
Cantor		& \( cantor(\alpha,\beta) \)	& least \( \alpha = cantor(\alpha,0) \)	& Taranovsky's C	& \( C(\alpha,\beta) = \beta+\omega^\alpha \)		& \( C(\Omega,0) = \varepsilon_0 \)	\\
		& \( = \beta + \omega^\alpha \)	& \( = \omega^\alpha = \varepsilon_0 \)	&			& iff \( C(\alpha,\beta) \geq \alpha \)			&					\\ \hline
Epsilon		& \( \varepsilon_\alpha	\)	& least \( \alpha = \varepsilon_\alpha\)& Madore's \( \psi \)	& \( \psi(\alpha) = \varepsilon_\alpha \)		& \( \psi(\Omega) = \zeta_0 \)		\\
		&				& \( = \zeta_0 \)			&			& for all \( \alpha < \zeta_0 \)			& 					\\ \hline
Binary Veblen	& \( \varphi_\alpha(\beta) \)	& least \( \alpha = \varphi(\alpha,0) \)& \( \theta \)		& \( \theta(\alpha,\beta) = \varphi(\alpha,\beta) \)	& \( \theta(\Omega,0) = \Gamma_0 \)	\\
		& or \( \varphi(\alpha,\beta) \)& \( = \Gamma_0 \)			&			& below \( \Gamma_0 \)					&					\\ \hline
													
\end{tabular}

\subsection{Madore's \( \psi\)}

This ordinal collapsing function is described in https://en.wikipedia.org/wiki/Ordinal\_collapsing\_function and http://quibb.blogspot.fr/2012/03/infinity-impredicative-ordinals.html .

The definition of this function uses the ordinal \( \Omega \) which is the least uncountable ordinal. 

\( C(\alpha) \) is the set of all ordinals constructible using only \( 0, 1, \omega, \Omega \) and addition, multiplication, exponentiation, and the function \( \psi \) (which will be defined later) restricted to ordinals smaller than \( \alpha \).

\( \psi(\alpha) \) is the smallest ordinal not in \( C(\alpha) \). 

The smallest ordinal not in C(0) is the limit of \( \omega, \omega^\omega, \omega^{\omega^\omega}, \ldots \) which is \( \varepsilon_0 \), so \( \psi(0) = \varepsilon_0 \). More generally, \( \psi(\alpha) = \varepsilon_\alpha \) for all \( \alpha < \zeta_0, \psi(\alpha) = \zeta_0 \) for \( \zeta_0 \leq a \leq \Omega \), and \( \psi(\Omega+\alpha) = \varepsilon_(\zeta_0+\alpha) \) for \( \alpha <= \zeta_1 \). 

Note that \( \psi(\Omega) = \zeta_0 \) is the least fixed point of \( \alpha \mapsto \varepsilon_\alpha \); we already saw such an equality when we introdiced collapsing in the Veblen function.

The limit \( \psi(\epsilon_(\Omega+1)) \) of \( \psi(\Omega), \psi(\Omega^\Omega), \psi(\Omega^{\Omega^\Omega}), \ldots \) is the Bachmann-Howard ordinal. 

Some examples of fundamental sequences (FS) are :

A FS of \( \omega \) is 0, 1, 2, 3, ...

A FS of \( \psi(0) \) is \( \omega, \omega^\omega, \omega^{\omega^\omega}, \ldots \).

A FS of \( \psi(\alpha+1) \) is \( \psi(\alpha), \psi(\alpha)^{\psi(\alpha)}, \psi(\alpha)^{\psi(\alpha)^{\psi(\alpha)}}, \ldots \).

A FS of \( \psi(f(\Omega)) \) is \( \psi(0), \psi(f(\psi(0))), \psi(f(\psi(f(\psi(0))))), \ldots \).

For example :

A FS of \( \psi(\Omega) \) is \( \psi(0), \psi(\psi(0)), \psi(\psi(\psi(0))), \ldots \).

A FS of \( \psi(\Omega \cdot 2) \) is \( \psi(0), \psi(\Omega+\psi(0)), \psi(\Omega+\psi(\Omega+\psi(0))), \ldots \).

A FS of \( \psi(\Omega^\Omega \cdot 3) \) is \( \psi(0), \psi(\Omega^\Omega \cdot 2+\Omega^{\psi(0)}), \psi(\Omega^\Omega \cdot 2+\Omega^{\Omega^\Omega \cdot 2+\Omega^{\psi(0)}}), \cdots \).

\subsection{Correspondence between Veblen functions and Madore's \( \psi \)}

To distinguish between the different Veblen functions, let us call \( \varphi_F \) the Veblen function with finitely many variables, and \( \varphi_T \) the Veblen function with transfinitely many variables.

\( \varphi_F \) is a function which, when applied to a list of countable ordinals, gives a countable ordinal. A list of countable ordinals can be seen as a function which, when applied to a natural number, gives a countable ordinal, with the restriction that the result differs from 0 for finitely many integers. If we denote \( \omega \) the set of natural numbers and \( \Omega \) the set of countable ordinals, then this can be written : \( \varphi_F : (\omega \rightarrow \Omega) \rightarrow \Omega \). If we replace \( \alpha \rightarrow \beta \) by \( \beta^\alpha \), we get \( \Omega^{\Omega^\omega} \), and if we apply \( \psi \) to it, we get \( \psi(\Omega^{\Omega^\omega}) \), which is the small Veblen ordinal, the least ordinal that cannot be reached using \( \varphi_F \).

For \( \varphi_T \), the position of a variable is represented by a countable ordinal instead of a natural number, also with the restriction that finitely many variables differ from 0, so we have \( \varphi_T : (\Omega \rightarrow \Omega) \rightarrow \Omega \). If we replace \( \alpha \rightarrow \beta \) by \( \beta^\alpha \), we get \( \Omega^{\Omega^\Omega} \), and if we apply \( \psi \) to it, we get \( \psi(\Omega^{\Omega^\Omega}) \), which is the large Veblen ordinal, the least ordinal that cannot be reached using \( \varphi_T \).

\subsection{\( \theta \) function}

\( \theta  \) function is a binary function. It’s defined as follows:

\begin{itemize}

\item \( C_0(\alpha,\beta) = \lbrace \gamma|\gamma<\beta \rbrace \cup \lbrace 0 \rbrace \).

\item \( C_{n+1}(\alpha,\beta) = \lbrace \gamma+\delta|\gamma,\delta \in C_n(\alpha,\beta) \rbrace \cup \lbrace \theta(\gamma,\delta)|\gamma<\alpha \& \gamma,\delta \in C_n(\alpha,\beta) \rbrace \cup \lbrace \Omega_c|c \in C_n(\alpha,\beta) \rbrace \).

\item \( C(\alpha,\beta) = \cup_{n<\omega} C_n(\alpha,\beta) \)

\item \( \theta(\alpha,\beta) = min \lbrace c|~(c \in C(\alpha,\gamma) \& (\forall \delta<\beta:\gamma>\theta(\alpha,\delta)) \rbrace \)

where \( \Omega_0 = 0 \) and \( \Omega_a \) represents the a-th uncountable ordinal.

\end{itemize}

It means that \( \theta(\alpha,\beta) \) is the \( (1+\beta) \)-th ordinal such that it cannot be built from ordinals less than it by addition, applying \( \theta(\delta,\ldots) \) where \( \delta < \alpha \) and getting an uncountable cardinal.

It seems that \( \theta(\alpha,\beta) = \varphi(\alpha,\beta) \) below \( \Gamma_0 \), making \( \theta \) function an extension of \( \varphi \) function. Even \( \theta(\Gamma_0,\beta) = \varphi(\Gamma_0,\beta) \) is true.

\bigskip

Other important values are :

\begin{itemize}

\item \( \theta(\Omega,\alpha) = \Gamma_\alpha \)

\item \( \theta(\Omega^\omega,0) = \) small Veblen ordinal

\item \( \theta(\Omega^\Omega,0) = \) large Veblen ordinal

\item \( \theta(\varepsilon_{\Omega+1},0) = \) Bachmann Howard ordinal

\end{itemize}

See https://stepstowardinfinity.wordpress.com/2015/05/04/ordinal2/ for more information. 

\subsection{Taranovsky's C}


C(a,b) is the least element above b that has degree a.

Definition: A degree for a well-ordered set S is a binary relation on S such that :

\begin{itemize}
	\item Every element \( c \in S \) has degree \( 0_S \) (the least element of S). \( 0_S \) only has degree \( 0_S \).
	\item For a limit a, c has degree a iff it has every degree less than a.
	\item For a successor a'=a+1, either of the following holds:
	\begin{itemize}
		\item An element has degree a' iff it is a limit of elements of degree a.
		\item There is a limit element d <= a such that for every c in S, c has degree a' iff it has degree a and either c <= d or c is a limit of elements of degree a (or both).
	\end{itemize}
\end{itemize}

Note: The third condition can be equivalently written as \( \forall a (C_{a+1} = lim(C_a) \vee \exists d \in lim(S) \cap (a+1) C_{a+1} = lim(C_a) \cup (C_a \cap (d+1))) \), where S is identified with an ordinal (so a+1 consists of ordinals \( \leq a), C_a \) is the set of elements that have degree a, and lim is limit points.

In other terms : Let \( \eta \) be an ordinal, and let \( 0_S \) and let Ld(a,b) be the statement that a is a limit of ordinals c such that \( (c,b) \in D \). Let D be the following binary relation over \( \eta \) :

\begin{itemize}
	\item \( \forall a<\eta:(a,0) \in D \)
	\item \( \forall a<\eta:a \neq 0 \Rightarrow (0,a) \notin D \)
	\item \( \forall b\in Lim \cup \eta:(a,b)\in D \Leftrightarrow \forall c<b:(a,c)\in D \)
	\item \( \forall b:(a,b)\in D \Leftrightarrow Ld(a,b+1)\forall b:(a,b)\in D \Leftrightarrow Ld(a,b+1) \)
	\item \( \forall b:\exists d\in Lim \cup  \eta :d<=b \Rightarrow \forall c:(c,a+1)\in D \Leftrightarrow (c<=d \vee Ld(c,b)) \)
\end{itemize}

Then \( C(a,b)=min{c:c\in  \eta  \wedge c>b \wedge (c,a)\in D} \).

\( C(a, b) = b+\omega^a \) iff \( C(a, b) \geq  a \).


For ordinals in the standard representation written in the postfix form, the comparison is done in the lexicographical order where \( 'C' < '0' < '\Omega' \): For example, \( C(C(0,0),0) < C(\Omega, 0) \) because \( 000CC < 0 \omega C \). (This does not hold for non-standard representations of ordinals.)

The fundamental sequences of Taranovsky’s notation can be easily defined.

Let \( L(\alpha) \) be the amount of C’s in standard representation of \( \alpha \), then \( \alpha [n]=max \lbrace \beta | \beta < \alpha  \wedge L(\beta) \leq L(\alpha)+n \rbrace \).

Here is a summary of the system by Taranovsky (see https://cs.nyu.edu/pipermail/fom/2012-March/016349.html) :

\begin{verbatim}

I discovered a conjectured ordinal notation system that I conjecture 
reaches full second order arithmetic.  I implemented the system in a 
python module/program:
http://web.mit.edu/dmytro/www/other/OrdinalArithmetic.py
along with ordinal arithmetic operations (addition, multiplication, 
exponentiation, etc.) and other functions.  The ordinal arithmetic 
functionality is useful even if you are only interested in ordinals 
below epsilon_0.

The notation system is simple enough to be defined in full here.

Definition: An ordinal a is 0-built from below from b iff a<=b
a is n+1-built from below from b iff the standard representation of a 
does not use ordinals above a except in the scope of an ordinal n-built 
from below from b.

(Note: "in the scope of" means "as a subterm of".)

The nth (n is a positive integer) ordinal notation system is defined as 
follows.

Syntax: Two constants (0, W_n) and a binary function C.
Comparison: For ordinals in the standard representation written in the 
postfix form, the comparison is done in the lexicographical order where 
'C' < '0' < 'W_n': For example, C(C(0,0),0) < C(W_n, 0) because 0 0 0 C 
C < 0 W_n C.

Standard Form:
0, W_n are standard
"C(a, b)" is standard iff
1. "a" and "b" are standard,
2. b is 0 or W_n or "C(c, d)" with a<=c, and
3. a in n-built from below from b.

I conjecture that the strength of the nth ordinal notation system is 
between Pi^1_{n-1}-CA and Pi^1_n-CA_0, and thus the sum of the order 
types of these ordinal notation systems is the proof-theoretical ordinal 
of second order arithmetic.

The full notation system is obtained by combining these notation systems 
as follows:
Constants 0 and W_i (for every positive integer i), and a binary function C.
W_i = C(W_{i+1}, 0) and the standard form always uses W_i instead of 
C(W_{i+1}, 0).
To check for standard form and compare ordinals use W_i = C(W_{i+1}, 0) 
to convert each W to W_n for a single positive integer n (it does not 
matter which n) and then use the nth ordinal notation system.

To make C a total function for a and b in the notation system (this is 
not required for standard forms), let C(a, b) be the least ordinal (in 
the notation system) of degree >=a above b, where the degree of W_i is 
W_{i+1} and the degree of C(c,d) is c if "C(c,d)" is the standard form.  
A polynomial time computation of C(a, b) (that I believe is correct) is 
included in the program.

To complete ordinal analysis of second order arithmetic, one would need:
* A canonical assignment of notations to formulas that provably in 
second order arithmetic denote an ordinal, and such that for every two 
ordinals/formulas, comparison is provable in second order arithmetic.  
The idea is that the notation system captures not only provably 
recursive ordinals of second order arithmetic but all ordinals that have 
a provable canonical definition in second order arithmetic.  For 
example, W_1 is best assigned to the least admissible ordinal above 
omega. A partial assignment is in my paper.  (It is because of such 
assignment that I believe that the system reaches full second order 
arithmetic.)
* Proof that the system is well-founded and that it has the right 
strength, etc.  (If you do not fully understand the notation system, or 
if you think that it is not well-founded, let me know.)

Historical Note:  In 2005, I discovered the right general form of C, 
defined a notation system at the level of alpha-recursively inaccessible 
ordinals (FOM postings in August 2005), and had an idea for reaching 
second order arithmetic.  In January 2006 (or possibly late 2005), I 
defined the notation system with W_2 and in 2009 (June 29, 2009 FOM 
posting) implemented it is a computer program.  This year I defined the 
key concept -- n-built from below -- that allowed me to complete the 
full notation system.

Details about the ordinal notation system and its initial segments are 
in my paper:
http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm

Sincerely,
Dmytro Taranovsky

\end{verbatim}

Here are some examples of representations of some ordinals : 

\begin{itemize}
\item \( 0 = 0 \)
\item \( 1 = 0+\omega^0 = C(0,0) \)
\item \( 2 = 1+\omega^0 = C(0,1) = C(0,C(0,0)) \)
\item \( \omega = 0+\omega^1 = C(1,0) \)
\item \( \omega+1 = \omega+\omega^0 = C(0,\omega) = C(0,C(1,0)) \)
\item \( \omega \cdot 2 =\omega+\omega^1 = C(1,\omega) = C(1,C(1,0)) \)
\item \( \omega^2 = 0+\omega^2 = C(2,0) \)
\item \( \omega^\omega = 0+\omega^\omega = C(\omega,0) = C(C(1,0),0) \)
\item \( \omega^{\omega^\omega} = 0+\omega^{\omega^\omega} = C(\omega^\omega,0) = C(C(C(1,0),0),0) \)
\item \( \varepsilon_0 = \varphi(1,0) = \varphi'(0,1) = C(\Omega_1,0) \)
\item \( \varepsilon_1 = \varphi(1,1) = \varphi'(0,2) = C(W,C(W,0)) \) (note that the correspondence with \( \varphi' \) is simpler than with \( \varphi \))
\item \( \zeta_0 = \varphi(2,0) = \varphi'(1,1) = C(C(\Omega_1,\Omega_1),0) = C(\Omega_1 \cdot 2,0) \) with \( \Omega_1 \cdot 2 = C(\Omega_1,\Omega_1)
 \)
\item \( \zeta_1 = \varphi(2,1) = \varphi'(1,2) = C(\Omega_1 \cdot 2,C(\Omega_1 \cdot 2,0)) \)
\item \( \eta_0 = \varphi(3,0) = \varphi'(2,1) = C(\Omega_1 \cdot 3,0) \) with \( \Omega_1 \cdot 3 = C(\Omega_1,C(\Omega_1,\Omega)) \)
\item \( \Gamma_0 = \varphi(1,0,0) = \varphi'(1,0,1) = C(C(\Omega_1 \cdot 2,\Omega_1),0) = C({\Omega_1}^2,0) \) with \( {\Omega_1}^2 = C(\Omega_1 \cdot 2,\Omega_1) \)
\item \( \Gamma_1 = C({\Omega_1}^2,C({\Omega_1}^2,0)) \)
\item \( \Gamma_\omega = C({\Omega_1}^2+1,0) \)
\item Small Veblen ordinal \( = C({\Omega_1}^\omega,0) \)
\item Large Veblen ordinal \( = C({\Omega_1}^{\Omega_1},0) \)
\item Bachmann Howard ordinal \( = C(C(\Omega_2,\Omega_1),0) \)
\end{itemize}

See http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm and 

https://stepstowardinfinity.wordpress.com/2015/06/22/ordinal3/ for more information. 




\section{Summary}

Any ordinal can be defined as the least ordinal strictly greater than all ordinals of a set : the empty set for 0, \(\lbrace \alpha \rbrace\) for the successor of \( \alpha \),  \(\lbrace \alpha_0,\alpha_1,\alpha_2,...\rbrace\) for an ordinal with fundamental sequence \(\alpha_0, \alpha_1, \alpha_2, ...\)

\subsection{Algebraic notation}

We define the following operations on ordinals :

\smallskip
\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item addition : \( \alpha+0=\alpha ; \alpha+suc(\beta)=suc(\alpha+\beta); \alpha+lim(f)=lim(n \mapsto \alpha+f(n)) \)

\item multiplication : \( \alpha \times 0 = 0 ; \alpha \times suc(\beta) = (\alpha \times \beta) + \alpha ; \alpha \times lim(f) = lim (n \mapsto \alpha \times f(n)) \)

\item exponentiation : \( \alpha^0 = 1 ; \alpha^{suc(\beta)} = \alpha^\beta \times \alpha ; \alpha^{lim(f)} = lim (n \mapsto \alpha^{f(n)}) \)
\end{itemize}


\subsection{Veblen functions}

These functions use fixed points enumaration : \(\varphi(\ldots,\beta,0,\ldots,0,\gamma) \) represents the \((1+\gamma)^{th}\) common fixed point of the functions \( \xi \mapsto \varphi(\ldots,\delta,\xi,0,\ldots,0)\) for all \(\delta < \beta\).


\subsection{Simmons notation}

\( Fix f z = f^w(z+1)\) = least fixed point of f strictly greater than z.

\( Next = Fix (\alpha \mapsto \omega^\alpha) \) 

\( [0] h = Fix (\alpha \mapsto h^\alpha \omega) \) ;
\( [1] h g = Fix (\alpha \mapsto h^\alpha g \omega) \) ;
\( [2] h g f = Fix (\alpha \mapsto h^\alpha g f \omega) \) ; etc...

Correspondence with Veblen's \(\phi\) : \( \phi(1+\alpha,\beta) = ([0]^\alpha Next)^{1+\beta} \omega ; 
 \phi(\alpha,\beta,\gamma) = ([0]^\beta (([1] [0])^\alpha Next))^{1+\gamma} \omega \)




\subsection{RHS0 notation}

We start from 0, if we don(t see any regularity we take the successor, if we see a regularity, if we have a notation for this regularity, we use it, else we invent it, then we jump to the limit.

\( H f x = lim\ x, f x, f (f x), \ldots ; R_1 f g x = lim\ g x, f g x, f f g x, \ldots ; R_2 f g h x = lim\ h x, f g h x, f g f g h x, \ldots \)

Correspondence with Simmons notation : 
\( \ldots, [3] \rightarrow R5, [2] \rightarrow R4, [1] \rightarrow R3, [0] \rightarrow R2, Next \rightarrow R1, \omega \rightarrow H suc\ 0 \)



\subsection{Ordinal collapsing functions}

These functions use uncountable ordinals to define countable ordinals.

We define sets of ordinals that can be built from given ordinals and operations, then we take the least ordinal which is not in this set, or the least ordinal which is greater than all contable ordinals of this set.

These functions are extensions of functions on countable ordinals, whose fixed points can be reached by applying them to an uncountable ordinal.

Examples :

\smallskip
\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}
\item Madore's \(\psi\) : \(\psi(\alpha) = \varepsilon_\alpha \) if \(\alpha < \zeta_0 ; \psi(\Omega) = \zeta_0 \) which is the least fixed point of \( \alpha \mapsto \varepsilon_\alpha \).

\item Feferman's \(\theta\) : \(\theta(\alpha,\beta) = \varphi(\alpha,\beta) \) if \( \alpha < \Gamma_0 \) and \( \beta < \Gamma_0 ; \theta(\Omega,0) = \Gamma_0 \) which is the least fixed point of \( \alpha \mapsto \varphi(\alpha,0) \).

\item Taranovsky's C : \( C(\alpha,\beta) = \beta+\omega^\alpha \) if \( \alpha \) is countable; \( C(\Omega_1,0) = \varepsilon_0 \) which is the least fixed point of \( \alpha \mapsto \omega^\alpha \).
\end{itemize}

\section{Comparison table}

\begin{tabular}{|c|c|c|c|c|c|c|c|c|}
\hline
Name		& Symbol		& Algebraic			& Veblen			& Simmons			& RHS0 		& Madore				& Taranovsky 			\\
\hline
Zero		& 0			& 0				& 				& 				& 0			& 					& 0				\\ \hline
One		& 1			& 1				& \(\varphi(0,0)\)		& 				& suc 0			& 					& C(0,0)			\\ \hline
Two		& 2			& 2				& 				& 				& suc (suc 0)		& 					& C(0,C(0,0))			\\ \hline
Omega		& \(\omega\)		& \(\omega\)			& \(\varphi(0,1)\)		& \(\omega\)			& H suc 0		& 					& C(1,0)			\\ \hline
		& 			& \(\omega+1\)			& 				& 				& suc (H suc 0)		& 					& C(0,C(1,0))			\\ \hline
		&			& \(\omega\times2\)		&				& 				& H suc (H suc 0)	& 					& C(1,C(1,0))			\\ \hline
		&			& \(\omega^2\)			& \(\varphi(0,2)\)		& 				& H (H suc) 0		& 					& C(C(0,C(0,0)),0)		\\ \hline
		&			& \(\omega^\omega\)		& \(\varphi(0,\omega)\)		& 				& H H suc 0		& 					& C(C(1,0),0)			\\ \hline
		&			& \(\omega^{\omega^\omega}\)	& \(\varphi(0,\omega^\omega)\)	&				& H H H suc 0		&					& C(C(C(1,0),0),0)		\\ \hline
Epsilon zero	& \(\varepsilon_0\)	& \(\varepsilon_0\)		& \(\varphi(1,0)\)		& \(Next\ \omega\)		& \(R_1 H suc\ 0\)	& \(\psi(0)\)				& \(C(\Omega_1,0)\)		\\ \hline
		& 			& \(\varepsilon_1\)		& \(\varphi(1,1)\)		& \(Next^2 \omega\)	& \(R_1 (R_1 H) suc\ 0\)& \(\psi(1)\)				& \(C(\Omega_1,C(\Omega_1,0)\)	\\ \hline
		& 			& \(\varepsilon_\omega\)	& \(\varphi(1,\omega)\) 	& \(Next^\omega \omega\) & \(H R_1 H suc\ 0\)	& \(\psi(\omega)\)			& \(C(C(0,\Omega_1),0)\)	\\ \hline
		& 			&\(\varepsilon_{\varepsilon_0}\)& \(\varphi(1,\varphi(1,0))\)	& \(Next^{Next \omega} \omega \) & \(R_1 H R_1 H suc\ 0\)& \(\psi(\psi(0))\)			& \(C(C(C(\Omega_1,0),\Omega_1),0)\)\\ \hline
Zeta zero	& \(\zeta_0\)		& \(\zeta_0\)			& \(\varphi(2,0)\)		& \([0] Next\ \omega\)		& \(R_2 R_1 H suc\ 0\)	& \(\psi(\Omega)\)			& \(C(C(\Omega_1,\Omega_1),0)\)	\\ \hline
Eta zero	& \(\eta_0\)		& \(\eta_0\)			& \(\varphi(3,0)\)		& \([0]^2 Next\ \omega\) 	& \(R_2 (R_2 R_1) H suc\ 0\)&					& \(C(C(\Omega,C(\Omega,\Omega)),0)\) \\ \hline
		&			&			& \(\varphi(\omega,0)\)		& \([0]^\omega Next\ \omega\) & \(H R_2 R_1 H suc\ 0\)&					& \(C(C(C(0,\Omega_1),\Omega_1),0)\) \\ \hline
Feferman	& \(\Gamma_0\)		
								& \(\Gamma_0\)			& \(\varphi(1,0,0)\)		& \([1] [0] Next\ \omega\)	& \(R_3 R_2 R_1 H suc\ 0\) & \(\psi(\Omega^\Omega)\)		& \(C(C(C(\Omega_1,\Omega_1),\) \\ 
-Schütte	&			&				& \(=\varphi(2 \mapsto 1)\)	&				& \(= R_{3 \ldots 1} H suc\ 0\) & 					& \(\Omega_1),0)\)		\\ \hline
Ackermann	&			&				& \(\varphi(1,0,0,0)\)		& \([1]^2 [0] Next\ \omega\) & \(R_3 (R_3 R_2) R_1 H suc\ 0\) & \(\psi(\Omega^{\Omega^2})\)		&				\\ 
		&			&				& \(=\varphi(3 \mapsto 1)\)	&				&			&					&				\\ \hline
Small Veblen	&			&				& \(\varphi(\omega \mapsto 1)\)	& \([1]^\omega [0] Next\ \omega\) & \(H R_3 R_2 R_1 H suc\ 0\) & \(\psi(\Omega^{\Omega^\omega})\)	& \(C(\Omega_1^\omega,0)\)	\\
ordinal		&			&				&				&				&			&					& \(=C(C(C(C(0,\Omega_1), \)	\\ 
		&			&				&				&				&			&					& \(\Omega_1),\Omega_1),0)\)	\\ \hline
Large Veblen	&			&				& least ord.	 	 	& \([2] [1] [0] Next\ \omega\)	& \(R_4 R_3 R_2 R_1 H suc\ 0\) & \(\psi(\Omega^{\Omega^\Omega})\)	& \(C(\Omega_1^{\Omega_1},0)\)	\\
ordinal		&			&				& not rep.			&				& \(= R_{4 \ldots 1} H suc\ 0\) &					& \(=C(C(C(C(\Omega_1,\Omega_1),\) \\ 
		&			&				&				&				&			&					& \( \Omega_1),\Omega_1),0) \)	\\ \hline
Bachmann-	&			&				&				& least ord.			& \(R_{\omega \ldots 1} H suc\ 0\) & \(\psi(\varepsilon_{\Omega+1})\)	& \(C(C(\Omega_2,\Omega_1),0)\)	\\
Howard		&			&				&				& not rep.			&			&					&				\\ 
ordinal		&			&				&				&				&			&					&				\\ \hline
  
\end{tabular}

\section{Links}

\begin{itemize}
     \setlength{\itemsep}{1pt}
     \setlength{\parskip}{0pt}
     \setlength{\parsep}{0pt}

\item http://www.madore.org/\%7Edavid/weblog/2011-09-18-nombres-ordinaux-intro.html :
Tutorial introduction to ordinal numbers in French

\item https://sites.google.com/site/pointlesslargenumberstuff/home/l/pglin?tmpl=\%2Fsystem\%2Fapp\%2Ftemplates\%2Fprint\%2F : 
Pointless Gigantic List of Infinite Numbers

\item https://sites.google.com/site/largenumbers/home/appendix/a/infinite\_numbers : 
Sbiis Saibian's !!! FORBIDDEN LIST !!! of Infinite Numbers

\item http://quibb.blogspot.fr/p/infinity-series-portal.html : 
Professor Quibb's Infinity Series Portal

\item http://googology.wikia.com/wiki/Ordinal\_notation : 
Ordinal notation

\item https://sites.google.com/site/travelingtotheinfinity/ : 
Traveling to the infinity

\item http://www.cs.man.ac.uk/~hsimmons/TEMP/OrdNotes.pdf : 
A short introduction to Ordinal Notations by Harold Simmons

\item http://www.mathematik.uni-muenchen.de/~buchholz/articles/jaegerfestschr\_buchholz3.pdf : 
A survey on ordinal notations around the Bachmann-Howard ordinal by Wilfried Buchholz

\item http://web.mit.edu/dmytro/www/other/OrdinalNotation.htm : 
Ordinal Notation by Dmytro Taranovsky

\item http://arxiv.org/html/1203.2270 : 
Higher Order Set Theory with Reflective Cardinals by Dmytro Taranovsky

\item https://www1.maths.leeds.ac.uk/~rathjen/realm.pdf : 
The Realm of Ordinal Analysis by Michael Rathjen

\item https://cage.ugent.be/~jvdm/Site/Research\_files/DissertationJeroenVanderMeerenPrinted.pdf : 
Connecting the Two Worlds: Well-partial-orders and Ordinal Notation Systems</a> by Jeroen Van der Meeren<br>

\item https://en.wikipedia.org/wiki/Veblen\_function : 
Veblen function on Wikipedia

\item http://www.ams.org/journals/tran/1908-009-03/S0002-9947-1908-1500814-9/S0002-9947-1908-1500814-9.pdf : 
Continuous increasing functions of finite and transfinite ordinals by
Oswald Veblen

\item http://en.wikipedia.org/wiki/Ordinal\_collapsing\_function : 
Ordinal collapsing function on Wikipedia

\item https://en.wikipedia.org/wiki/Buchholz\_psi\_functions : 
Buchholz psi functions on Wikipedia

\item http://www.madore.org/\%7Edavid/math/ordtrees.pdf : 
Ordinal trees

\item https://johncarlosbaez.wordpress.com/2016/06/29/large-countable-ordinals-part-1/ : Large Countable Ordinals by John Baez, Part 1
\item https://johncarlosbaez.wordpress.com/2016/07/04/large-countable-ordinals-part-2/ : Large Countable Ordinals by John Baez, Part 2
\item https://johncarlosbaez.wordpress.com/2016/07/07/large-countable-ordinals-part-3/ : Large Countable Ordinals by John Baez, Part 3

\item https://medium.com/@joshkerr/mind-blown-the-fast-growing-hierarchy-for-laymen-aka-enormous-numbers-d9a865c6443b : Mind blown: the fast growing hierarchy for laymen — aka enormous numbers

\item https://sites.google.com/site/largenumbers/home : 
Sbiis Saibian's Large Number Site

\item http://forums.xkcd.com/viewtopic.php?f=14\&t=7469 : 
My number is bigger !

\item http://www.cl.cam.ac.uk/\%7Ejrh13/papers/reflect.html : 
Metatheory and Reflection in Theorem Proving: A Survey and Critique</a> by John Harrison<br>

\item http://math.stanford.edu/\%7Efeferman/papers/penrose.pdf : 
Penrose's G\&ouml;delian argument by Solomon Feferman

\item http://www.turingarchive.org/browse.php/B/15 : 
Systems of logic based on ordinals by Alan Turing

\item https://coq.inria.fr/documentation : 
Coq documentation

\item http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation : 
Agda documentation

\end{itemize}


\end{document}

