\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{ordinal analysis}

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{relation_to_predicativity}{Relation to Predicativity}\dotfill \pageref*{relation_to_predicativity} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{methods}{Methods}\dotfill \pageref*{methods} \linebreak
\noindent\hyperlink{upper_bounds}{Upper bounds}\dotfill \pageref*{upper_bounds} \linebreak
\noindent\hyperlink{lower_bounds}{Lower bounds}\dotfill \pageref*{lower_bounds} \linebreak
\noindent\hyperlink{table_of_ordinal_analyses}{Table of Ordinal Analyses}\dotfill \pageref*{table_of_ordinal_analyses} \linebreak
\noindent\hyperlink{ordinal_notations}{Ordinal notations}\dotfill \pageref*{ordinal_notations} \linebreak
\noindent\hyperlink{systems_of_firstorder_arithmetic_foa}{Systems of first-order arithmetic (FOA)}\dotfill \pageref*{systems_of_firstorder_arithmetic_foa} \linebreak
\noindent\hyperlink{systems_of_secondorder_arithmetic_soa}{Systems of second-order arithmetic (SOA)}\dotfill \pageref*{systems_of_secondorder_arithmetic_soa} \linebreak
\noindent\hyperlink{kripke_platek_set_theories}{Kripke Platek Set theories}\dotfill \pageref*{kripke_platek_set_theories} \linebreak
\noindent\hyperlink{martinlf_type_theories}{Martin-L\"o{}f type theories}\dotfill \pageref*{martinlf_type_theories} \linebreak
\noindent\hyperlink{constructive_set_theories}{Constructive Set theories}\dotfill \pageref*{constructive_set_theories} \linebreak
\noindent\hyperlink{explicit_mathematics_systems}{Explicit mathematics systems}\dotfill \pageref*{explicit_mathematics_systems} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

An ordinal analysis of a formal system precisely measures its proof-theoretic strength, which is its strength at justifying [[transfinite induction]]. In practice, it also measures the system's ability to prove totality of complex computable functions.

Giving a concrete ``ordinal notation'' that describes the proof-theoretic strength of a system is sometimes seen as providing a constructive justification for the reasoning principles of the system. However, ordinal analysis is not limited to systems that are [[constructive]] in the sense of not assuming [[excluded middle]]. But in practice, classical systems with ordinal notations are interpretable constructively.

\hypertarget{relation_to_predicativity}{}\subsubsection*{{Relation to Predicativity}}\label{relation_to_predicativity}

While it is classically true that any [[deductive system\#FormalSystems|effective formal system]] has some limit to its proof-theoretic strength, only systems of limited strength have had their strength concretely described by a good ordinal notation. Specifically, all systems with ordinal analyses so far are significantly weaker than full [[second-order arithmetic]]. Consequently, so far, systems that have been given ordinal notations feel more like [[predicative]] systems than like familiar impredicative systems such as [[ZFC]], [[higher-order logic|higher-order arithmetic]], and [[ETCS]].

Many have argued, however, that the boundary between predicatively-justifiable and impredicative systems lies somewhere within the range of proof-theoretic ordinals already analyzed. In other words, that the stronger systems in the table below are actually slightly impredicative, even when it isn't obvious.

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

\begin{defn}
\label{}\hypertarget{}{}
The \textbf{proof-theoretic ordinal} of a [[theory]] $T$ is (commonly) defined as

\begin{displaymath}
{\vert T\vert} = \sup\{ \mathrm{otyp}({\prec}) \mid {\prec}\text{is primitive recursive and}\;
 T \vdash \mathrm{TI}({\prec},X) \}
\end{displaymath}
where $\mathrm{otyp}({\prec})$ is the [[order-type]] of the [[well-order]] $\prec$ and $\mathrm{TI}({\prec},X)$ means that $X$ (a free parameter) satisfies transfinite induction along $\prec$; this is the constructive way to say that $\prec$ is well-ordered. For most theories, this ordinal is equal to the $\Pi^1_1$-ordinal of the theory,

\begin{displaymath}
{\vert T\vert}_{\Pi^1_1} := \sup\{ \mathrm{tc}(F) \mid F\;\text{is a}\;\Pi^1_1\text{-sentence and }\;
 T \vdash F \}
\end{displaymath}
where $\mathrm{tc}(F)$ is the truth-complexity of the $\Pi^1_1$-sentence $F$ (if $T$ is a first-order theory, we interpret $T \vdash \forall X.F(X)$ as $T \vdash F(X)$ with a free set parameter $X$).

\end{defn}
The proof-theoretic ordinal is always a recursive [[ordinal]] ($\lt\omega_1^{\mathrm{CK}}$) if the theory is recursive.

Note that the proof-theoretic ordinal is a rather blunt invariant, because if $F$ is any true $\Sigma^1_1$-sentence, then

\begin{displaymath}
{\vert T\vert}_{\Pi^1_1} = {\vert T+F\vert}_{\Pi^1_1}
\end{displaymath}
So this tells us nothing about the provable arithmetical sentences of $T$! And indeed, all true arithmetical sentences have truth-complexity less than $\omega$.

The solution is to refine the analysis to give a $\Pi^0_2$ ordinal analysis of the theory, using a measure of the computational complexity of provable $\Pi^0_2$-sentences/provably recursive functions. However, there's no natural hierarchy of all subrecursive functions. We can define such a computational complexity depending on a choice of starting function and a choice of ordinal notation system (indeed, the $\Pi^0_2$ ordinal should be thought of as an ordinal notation, rather than an actual ordinal). But for all the ordinal analyses we have so far, these choices turn out not to matter, basically because any \emph{natural ordinal notation system} will give the same result. A major issue is, however, that we have no definition of what a natural ordinal notation system is (but we know one when we see it!).

All of the ordinal analyses mentioned below also give a $\Pi^0_2$ ordinal analysis, and thus control of the computational complexity of the provably recursive functions.

\hypertarget{methods}{}\subsection*{{Methods}}\label{methods}

\hypertarget{upper_bounds}{}\subsubsection*{{Upper bounds}}\label{upper_bounds}

Most ordinal analyses proceed by embedding the theory in an infinitary proof calculus deriving judgments $\vdash^\alpha_\rho F$ meaning $F$ has an infinitary derivation of height less than $\alpha$ using only cuts of rank less than $\rho$, or some refinement of such, for instance using operator controlled derivations. Then one analyzes how the height of a derivation changes during cut-elimination. For predicative theories, we'll have

\begin{displaymath}
\vdash^\alpha_\rho \Delta \Rightarrow \vdash^{\varphi\rho\alpha}_0 \Delta
\end{displaymath}
One sets up the calculus so that $\vdash^\alpha_0 F$ implies $\mathrm{tc}(F)\lt\alpha$, so this yields upper bounds for the proof-theoretic ordinal.

\hypertarget{lower_bounds}{}\subsubsection*{{Lower bounds}}\label{lower_bounds}

Lower bounds are usually done by directly deriving $T \vdash \mathrm{TI}({\prec_n},X)$ for a sequence of primitive recursive well-orderings $\prec_n$ whose order-types approximate the proof-theoretic ordinal. We get these primitive recursive well-orderings from good ordinal notation systems, see below.

\hypertarget{table_of_ordinal_analyses}{}\subsection*{{Table of Ordinal Analyses}}\label{table_of_ordinal_analyses}

See below for explanations.

\begin{tabular}{l|l|l|l}
Ordinal&FOA&SOA&Other\\
\hline 
\textbf{Finitist systems}&&&\\
$\omega^3$&EFA&RCA$_0^*$&\\
$\omega^\omega$&PRA,I$\Sigma_1$&RCA$_0$, WKL$_0$&CPRC\\
\textbf{Predicative systems}&&&\\
$\varepsilon_0=\varphi(1,0)$&PA&ACA$_0$, $\Delta_1^1$-CA$_0$, $\Sigma^1_1$-AC$_0$&EM$_0$\\
$\varphi(1,\varepsilon_0)$&&ACA&\\
$\varphi(\omega,0)$&ID$_1^#$&$\Delta_1^1$-CR&EM$_0$+JR\\
$\varphi(\varepsilon_0,0)$&$\widehat{\mathrm{ID}}_1$&$\Delta_1^1$-CA, $\Sigma^1_1$-AC&EM$_0$+J, ML$_1$\\
$\Gamma_0=\varphi(1,0,0)$&$\widehat{\mathrm{ID}}_{\lt\omega}$, U(PA)&ATR$_0$,$\Delta^1_1$-CA+BR&ML$_{\lt\omega}$, MLU, KPi$^0$\\
\textbf{Meta-predicative systems}&&&\\
$\varphi(1,0,\varepsilon_0)$&$\widehat{\mathrm{ID}}_{\omega}$&ATR&KPl$^0$+F-I$_\omega$\\
$\varphi(1,\omega,0)$&$\widehat{\mathrm{ID}}_{\lt\omega^\omega}$&ATR$_0$+($\Sigma^1_1$-DC)&KPi$^0$+$\Sigma_1$-I$_\omega$\\
$\varphi(1,\varepsilon_0,0)$&$\widehat{\mathrm{ID}}_{\lt\varepsilon_0}$&ATR+($\Sigma^1_1$-DC)&KPi$^0$+F-I$_\omega$\\
$\varphi(1,\Gamma_0,0)$&$\widehat{\mathrm{ID}}_{\lt\Gamma_0}$&&MLS\\
$\varphi(2,0,0)$&Aut($\widehat{\mathrm{ID}}$)&&KPh$^0$\\
$\varphi(\omega,0,0)$&&&KPm$^0$\\
\textbf{Inductive types}&&&\\
$\psi_\Omega(\varepsilon_{\Omega+1})$&ID$_1$&&KP$\omega$, CZF, ML$_1$V\\
$\psi_\Omega(\Gamma_{\Omega+1})$&U(ID$_1$)&&\\
$\psi_\Omega(\Omega_\omega)$&ID$_{\lt\omega}$&$\Pi^1_1$-CA$_0$,$\Delta^1_2$-CA$_0$&\\
$\psi_\Omega(\Omega_\omega \varepsilon_0)$&W-ID$_\omega$&$\Pi^1_1$-CA&W-KPl\\
$\psi_\Omega(\varepsilon_{\Omega_\omega+1})$&ID$_\omega$&$\Pi^1_1$-CA+BI&KPl\\
$\psi_\Omega(\Omega_{\omega^\omega})$&ID$_{\lt\omega^\omega}$&$\Delta^1_2$-CR&\\
$\psi_\Omega(\Omega_{\varepsilon_0})$&ID$_{\lt\varepsilon_0}$&$\Delta^1_2$-CA, $\Sigma^1_2$-AC&W-KPi\\
$\psi_\Omega(\varepsilon_{I+1})$&&$\Delta^1_2$-CA+BI, $\Sigma^1_2$-AC+BI&KPi, T$_0$, CZF+REA\\
$\psi_\Omega(\Omega_{I+\omega})$&&&ML$_1$W\\
$\psi_\Omega(\Omega_L)$&&&KPh, ML$_{\lt\omega}$W\\
\textbf{Inductive-recursive types}&&&\\
$\psi_\Omega(\varepsilon_{M+1})$&&$\Delta^1_2$-CA+BI+(M)&CZFM, KPm\\
$\psi_\Omega(\Omega_{M+\omega})$&&&KPM$^+$, MLM, ``Agda''\\
\end{tabular}

The sections of the table corresponds roughly to the kinds of reasoning captured by the systems:

\begin{itemize}%
\item Finitistic reasoning about the natural numbers (and other finitistic inductive types)
\item Predicative reasoning about the natural numbers
\item Meta-predicative reasoning about the natural numbers
\item Reasoning about general inductive types
\item Reasoning about general inductive-recursive types

\end{itemize}
Note that these are all very much weaker than full second-order arithmetic, and of course much weaker than Zermelo or Zermolo-Fraenkel set theory.

After the meta-predicative systems, all ordinals use a notation which refers to a much larger ordinal, often patterned on a large cardinal.

Rathjen (2005) analyzed systems up to $\Delta^1_2$-CA+BI+$\Pi^1_2$-CA$^-$ (the last part is parameter-free $\Pi^1_2$-comprehension), corresponding to a stable ordinal, Arai has work on a bit stronger systems, up to about $\Sigma^1_4$-DC, in terms of ordinal diagrams defined in terms of iterated stability.

With current technology, we are very far from having ordinal analyses of stronger systems such as full second order arithmetic, ZFC set theory, or impredicative type theories such as the calculus of (inductive) constructions.

\hypertarget{ordinal_notations}{}\subsubsection*{{Ordinal notations}}\label{ordinal_notations}

\begin{itemize}%
\item $\varphi$ is either the binary or the ternary Veblen function
\item $\Omega=\Omega_1$ is the first recursively admissible ordinal
\item $\Omega_\xi$ is the $\xi$th recursively admissible ordinal
\item $I$ is the first recursively inaccessible ordinal
\item $L$ is the limit of the first $\omega$ recursively inaccessible ordinals
\item $M$ is the first recursively Mahlo ordinal

\end{itemize}
The $\psi$ functions are ordinal collapsing functions.

\hypertarget{systems_of_firstorder_arithmetic_foa}{}\subsubsection*{{Systems of first-order arithmetic (FOA)}}\label{systems_of_firstorder_arithmetic_foa}

These assert some hierarchy of inductive defined sets of natural numbers.

\begin{itemize}%
\item EFA is elementary function arithmetic
\item PRA is [[primitive recursive arithmetic]]
\item PA is first-order Peano arithmetic
\item $\widehat{\mathrm{ID}}_\nu$ extends PA by $\nu$ iterated fixed points of monotone operators (not necessarily least).
\item ID$_1^#$ is $\widehat{\mathrm{ID}}_1$ with induction only for positive formulas.
\item ID$_\nu$, the theory of $\nu$-times [[iterated inductive definitions]], extends PA by $\nu$ iterated least fixed points of monotone operators.

\end{itemize}
Many of the results in the table concerning these can be summarized as

\begin{displaymath}
{\vert \mathrm{ID}_\nu \vert} = \psi_\Omega(\varepsilon_{\Omega_\nu+1})
\end{displaymath}
For any of these, we get the same proof-theoretic ordinal whether we use classical or intuitionistic logic. For the ID$_\nu$-systems, this is due to Sieg.

The unfolding systems U(PA) and U(ID$_1$) are not exactly first-order arithmetic systems, but capture what we can get by predicative reasoning based on the natural numbers or one generalized inductive definition, respectively.

\hypertarget{systems_of_secondorder_arithmetic_soa}{}\subsubsection*{{Systems of second-order arithmetic (SOA)}}\label{systems_of_secondorder_arithmetic_soa}

\begin{itemize}%
\item Comprehension or choice principles.
\item RCA$_0^*$ is the second-order version of EFA: $\exp$ is a function symbol.
\item WKL is weak K\"o{}nig's lemma.
\item BR is the bar induction rule.
\item BI is the bar induction axiom.
\item ATR is arithmetical transfinite recursion.
\item (M) says every true $\Pi^1_3$ sentence with parameters holds in a $\beta$-model of $\Delta^1_2$-CA.

\end{itemize}
A zero subscript indicates that we have the induction axiom rather than the induction scheme, except for RCA$_0$ which has the $\Sigma^0_1$-induction scheme.

\hypertarget{kripke_platek_set_theories}{}\subsubsection*{{Kripke Platek Set theories}}\label{kripke_platek_set_theories}

\begin{itemize}%
\item KP$\omega$ is Kripke-Platek set theory, whose universe is an admissible set containing $\omega$.
\item KPl asserts that the universe is a limit of admissible sets
\item KPi asserts that the universe is inaccessible sets
\item KPh asserts that the universe is hyperinaccessible: a limit of inaccessible sets
\item KPm asserts that the universe is a Mahlo set

\end{itemize}
A superscript zero indidcates that $\in$-induction is removed.

About the Mahlo level: this also corresponds to inductive-recursive definitions (Dybjer-Setzer).

\hypertarget{martinlf_type_theories}{}\subsubsection*{{Martin-L\"o{}f type theories}}\label{martinlf_type_theories}

\begin{itemize}%
\item CPRC is the Herbelin-Patey Calculus of Primitive Recursive Constructions.
\item ML$_n$ is type theory without W-types with $n$ universes.
\item ML$_{\lt\omega}$ is type theory without W-types with an infinite hierarchy of universes.
\item MLU is type theory with a next universe operator.
\item MLS is type theory without W-types with a superuniverse.
\item ML$_1$V is type theory with one universe and Aczel's type of iterative sets.
\item ML$_1$W is type theory with W-types and one universe.
\item ML$_{\lt\omega}$W is type theory with W-types and an infinite hierarchy of universes (this corresponds to the type theory in Lean's HoTT mode).
\item MLM is Martin-L\"o{}f type theory with a Mahlo universe.

\end{itemize}
\hypertarget{constructive_set_theories}{}\subsubsection*{{Constructive Set theories}}\label{constructive_set_theories}

\begin{itemize}%
\item CZF is Aczel's constructive set theory.
\item REA is the regular extension axiom.
\item CZFM is CZF with a Mahlo universe

\end{itemize}
\hypertarget{explicit_mathematics_systems}{}\subsubsection*{{Explicit mathematics systems}}\label{explicit_mathematics_systems}

\begin{itemize}%
\item EM$_0$ is basic [[explicit mathematics]] with elementary comprehension
\item JR is the join rule, J is the join axioms
\item T$_0$ is EM$_0$+J+IG, where IG is inductive generation

\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\begin{itemize}%
\item Aczel, The Type Theoretic Interpretation of Constructive Set Theory, Logic Colloquium 1977.


\item Arai, A sneak preview of proof theory of ordinals, \href{http://arxiv.org/abs/1102.0596}{arXiv 1102.0596}.


\item Arai, Proof theory for theories of ordinals III: $\Pi_N$-reflection, \href{http://arxiv.org/abs/1007.0844}{arXiv 1007.0844}.


\item Buchholz, A simplified version of local predicativity, Proc. Proof Theory Meeting Leed `90.


\item Buchholz, A Note on the Ordinal Analysis of KPM (2002).


\item Buchholz, Feferman, Pohlers and Sieg, Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics 897 (1981).


\item Dybjer and Setzer, Induction-recursion and initial algebras, APAL 124(1-3), 2003, pp. 1-47. DOI: 10.1016/S0168-0072(02)00096-9


\item Feferman: Iterated inductive fixed-point theories: Application to Hancock's conjecture, in: G. Metakides (ed.): Patras Logic Symposium (North-Holland, Amsterdam, (1982), 171--196.


\item J\"a{}ger, Kahle, Setzer, and Strahm, The proof-theoretic analysis of transfinitely iterated fixed point theories, Journal of Symbolic Logic


\item J\"a{}ger and Strahm, Fixed point theories and dependent choice. Archive for Mathematical Logic.


\item Rathjen, Ordinal notations based on a weakly Mahlo cardinal, Archive for Mathematical Logic 29 (1990), 249-263.


\item Rathjen, Proof-theoretic analysis of KPm, Archive for Mathematical Logic (1991).


\item Rathjen, The Recursively Mahlo Property in Second Order Arithmetic, Mathematical Logic Quarterly 42 (1996), 59-66.


\item Rathjen, The strength of Martin-L\"o{}f type theory with a superuniverse. Part II, 2001, AML, DOI: 10.1007/s001530000051


\item Rathjen, The strength of Martin-L\"o{}f type theory with a superuniverse. Part I, 2000, AML, DOI: 10.1007/s001530050001


\item Rathjen, An ordinal analysis of parameter free $\Pi^1_2$-comprehension. Arch. Math. Log. 44(3), 263--362 (2005).


\item Rathjen, The constructive Hilbert program and the limits of Martin-L\"o{}f type theory (2005), Synthese, DOI: 10.1007/s11229-004-6208-4


\item Rathjen, Griffor and Palmgren, Inaccessibility in Constructive Set Theory and Type Theory, APAL 94 (1998), 181-200.


\item Setzer, An upper bound for the proof theoretical strength of Martin-L\"o{}f Type Theory with W-type and one universe (2006)


\item Strahm, Autonomous fixed point progressions and fixed point transfinite recursion, Proc. of Logic Colloquium `98, 449-464, \href{http://www.iam.unibe.ch/ltgpub/2000/str00a.pdf}{web}



\end{itemize}
[[!redirects proof-theoretic ordinal]]



\end{document}