\documentstyle[art12]{article}
\pagestyle{empty}
%This file contains additional macros, specific for LATEX,
%which should be added to the general macros-files, when LATEX is used
%            on documentstyle 
%                   ARTICLE
\textheight=210mm
\textwidth=145 mm
\def \Ar{\Rightarrow}
\def \ar{\rightarrow}
\def \all{\forall}
%%%%%%     Symbols for dealing with ordinals
%
\def \OT{{\rm OT}}
\def \T{{\rm T}}
\def \NF{{\rm NF}}
%%%%%%     special symbols for vec tilde etc.
%
\def \alphavec{{\vec \alpha }}
\def \betavec{{\vec \beta}}
\def \tvec{{\vec t}}
%
%
%%%%%%     Theories
\def \PRA{{\rm PRA}}
\def \ID{{\rm ID}}
%
%
\begin{document}
\bibliographystyle{plain}
%\bibliographystyle{alpha}
\centerline{\large \bf Why 
large cardinals are not needed for denoting small ordinals.}
\smallskip 
\centerline{Anton Setzer, Department of Mathematics, Uppsala University}
\centerline{email: setzer@math.uu.se}  
\medskip 
In the article ``Well-ordering proofs in Martin-L\"of's Type Theory''
(submitted) 
we introduced the notion of ordinal notation systems ``from below''. These
were  systems of terms $\OT$ built from one ordinal function $f$
(which codes several ordinal functions usually needed) together
with an ordering $<$ such that
for some additional ordering $<'$ on the arguments of $f$ essentially the 
following conditions hold:\par 
\begin{itemize}
\item  $f$ is inflating, i.e. $\beta_i < f(\betavec)$.
\item The  well-foun\-ded\-ness of $<'$ reduces in an elementary way to
the well-\break 
foun\-ded\-ness of $<$.
\item If $\alpha< f(\betavec)$, then $\alpha < \beta_i$ for some $i$ or
$\alpha = f(\alphavec)$ for some $\alphavec <' \betavec$.
\end{itemize} 
We could show that the Bachmann-Howard ordinal
is an upper bound for the order type of such systems and recently as well 
that this bound is sharp.\par \medskip 
In this talk we will explore the result  of replacing
the set of arguments of $f$ by more complicated structures
and of using stronger principles in the 
reduction of $<'$ to $<$.\par 
\medskip 
In a first step, this set of arguments will be 
essentially a set of terms $\OT_2$ based on the 
ordinal notations $\OT$ to be defined and
the reduction of $<'$ to $<$ follows by $(\OT_2,<')$ being
an ordinal notation system from below in the original sense, but
based on $(\OT,<)$. This
construction will reach $\psi(\epsilon_{\Omega_2+1})$ and
can be regarded as ``from below'': the
function $f$ will still be inflating with respect to
$\OT$.\par 
\medskip 
The next construction will be to add a third level $(\OT_3,<'')$ and
by adding even more levels indexed by ordinals we 
will eventually reach  the strength of ${\rm KPI}$ or
$(\Delta^1_2-{\rm CA})+ ({\rm BI})$.\par \medskip 
These constructions  are just another way of looking at
ordinary ordinal notation systems which use collapsing 
functions and large cardinals or their recursive analogues.
(We will only consider the levels up to one inaccessible cardinal, but
it is only a matter of bureaucracy to extend this 
to systems using larger cardinals.) In this sense large
cardinals are not needed for denoting these ordinals but
are only used to define in a short way 
ordinal notation systems.\par
\end{document}