%
\documentstyle{report}
%
\topmargin 0mm
\oddsidemargin 5mm
\evensidemargin 5mm
\textwidth 150mm
\textheight 222mm
\marginparwidth 0mm
\marginparsep 0mm
\marginparpush 0pt
\columnwidth\textwidth
%
\pagestyle{empty}
\parindent0mm
%
%
% Math sans serif
%
\newmathalphabet{\msf}
\addtoversion{normal}{\msf}{cmss}{m}{n}
\addtoversion{bold}{\msf}{cmss}{sbc}{n}
%
%
\begin{document}
%
%
\begin{center}
%
 {\large\bf Aspects of metapredicativity}\\[1ex]
 {\bf Thomas Strahm}\\[1ex]
%
Institut f\"ur Informatik und angewandte Mathematik \\ Universit\"at Bern, 
Switzeland\\ {\tt strahm@iam.unibe.ch}
%
\end{center}
%
\par\medskip
%
%
We address proof-theoretic aspects of various kinds of transfinitely
iterated fixed point theories, thereby providing examples
of so-called {\it metapredicative}\/ theories, i.e.~theories which
have proof-theoretic ordinal beyond the Feferman-Sch\"utte ordinal
$\Gamma_0$, but can still be treated by methods of predicative
proof theory.
%
\par\medskip
%
The theories $\widehat{\msf{ID}}_n$\/ for finitely iterated fixed 
points of positive arithmetic operators have been shown by 
Feferman [3] to provide a framework for predicative mathematics,
i.e.~the limit of the proof-theoretic ordinals of the 
theories $\widehat{\msf{ID}}_n$\/ for $n<\omega$\/ is exactly 
$\Gamma_0$. Reporting joint work with J\"ager, Kahle, and Setzer [4],
we provide an ordinal analysis of the theories $\widehat{\msf{ID}}_\alpha$\/
of $\alpha$\/ times iterated fixed points. The proof-theoretic
ordinal of these theories can be characterized by means of
a {\it ternary}\/ Veblen function. Interesting connections between
transfinitely iterated fixed point theories and extensions of
Friedman's $\msf{ATR}_0$\/ with dependent choice are addressed 
(cf.~J\"ager and Strahm [5]). In particular, we have that
$\msf{ATR}_0 +(\Sigma_1^1\hbox{-}\msf{DC})$\/ and 
$\msf{ATR} +(\Sigma_1^1\hbox{-}\msf{DC})$\/ are proof-theoretically
equivalent to $\widehat{\msf{ID}}_{<\omega^\omega}$\/ and
$\widehat{\msf{ID}}_{<\varepsilon_0}$, respectively.
%
\par\medskip
%
It is natural to ask about the proof-theoretic strength of
the intuitionistic counterparts $\widehat{\msf{ID}}_\alpha^{\, i}$\/
of $\widehat{\msf{ID}}_\alpha$. Recently, Buchholz [2] has shown
that $\widehat{\msf{ID}}_1^{\, i}$\/ is not stronger than Heyting arithmetic
$\msf{HA}$, and subsequently Arai [1] has strengthened this
result to $\widehat{\msf{ID}}_n^{\, i}$\/ for arbitrary $n$.
In R\"uede and Strahm [6] a proof-theoretic analysis of the theories
$\widehat{\msf{ID}}_\alpha^{\, i}$\/ for larger $\alpha$'s
is provided. A general relationship between these theories and systems
for iterated arithmetic comprehension without set parameters
is given. For example, $\widehat{\msf{ID}}_\omega^{\, i}$\/
is proof-theoretically equivalent to $(\Pi^0_\infty\hbox{-}\msf{CA})$.
%
\par\medskip
%
Finally, we provide a general discussion of autonomous
fixed point processes with classical and intuitionistic
logic, and we study the so-called principle of
{\it transfinite fixed point recursion}\/ $(\msf{FTR})$,
thereby giving a proof-theoretic treatment of the
associated theories $\msf{Aut}(\widehat{\msf{ID}})$,
$\msf{FTR}_0$\/ as well as $\msf{FTR}$, cf.~Strahm [7].
%
\par\bigskip
%
{\bf References}
%
\begin{enumerate}
%
\item T.~Arai, From the attic. To appear in {\it Annals of
Pure and Applied Logic}.
%
\item W.~Buchholz, An intuitionistic fixed point theory.
To appear in {\it Archive for Mathematical Logic}.
%
\item S.~Feferman, Iterated inductive fixed-point theories:
application to Hancock's conjecture. In {\it The Patras Symposion},
G.~Metakides, Ed., North Holland, Amsterdam, 1982.
%
\item G.~J\"ager, R.~Kahle, A.~Setzer, T.~Strahm, The proof-theoretic
analysis of transfinitely iterated fixed point theories. Submitted for
publication.
%
\item G.~J\"ager, T.~Strahm, Fixed point theories and dependent
choice. Submitted for publication.
%
\item C.~R\"uede, T.~Strahm, Transfinitely iterated fixed point
theories with intuitionistic logic. In preparation.
%
\item T.~Strahm, Autonomous fixed point processes and transfinite
fixed point recursion. In preparation.
%
\end{enumerate}
%
%
\end{document}