Infinitary Proof Theory
Wolfram Pohlers
Westf�lische Wilhems Universit�t M�nster
August 20, 1999
2
Contents
Contents
1 Proof theoretic ordinals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.2 Some basic facts about ordinals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.3 Truth complexity for 1 sentences . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1
1.4 Inductive definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
1.5 The stages of an inductive definition . . . . . . . . . . . . . . . . . . . . . . . . . . 17
1.6 Positively definable inductive definitions . . . . . . . . . . . . . . . . . . . . . . . . 18
1.7 Well founded trees and positive inductive definitions . . . . . . . . . . . . . . . . . 19
1.8 The 1 ordinal of an axiom system . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1
2 The ordinal analysis for PA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.1 Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.2 The theory NT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
2.3 The upper bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.4 The lower bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3 Ordinal analysis of non iterated inductive definitions . . . . . . . . . . . . . . . . 37
3.1 The theory ID1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.2 The language L"(NT ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.3 Inductive definitions and L"(NT ) . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.4 The semi formal system for L"(NT ) . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.5 Controlling operators for ID1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.6 The upper bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.7 The lower bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.7.1 Coding ordinals in L(NT ) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.7.2 The well ordering proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
3
Contents
4
1. Proof theoretic ordinals
1.1 Preliminaries
One of the aims of infinitary proof theory is the computation of the proof theoretical ordinal of
axiom systems. We will indicate in these lectures that there are different types of proof theoretical
ordinals for axiom systems.
Proof theory was launched by the consistency problem for axioms systems. Its original aim
was to give finitary consistency proofs. However, according to G�DEL s second incompleteness
theorem, finitary consistency proofs are impossible for axiom systems which allow sufficiently
much coding machinery.
Ordinals entered the stage when GENTZEN in [5] and [6] proved the consistency of the axioms
of number theory using a transfinite induction. His proof is completely finitary except for the
transfinite induction. The infinite content of the axioms for Number Theory is thus pinpointed in
the transfinite induction used in the consistency proof. Therefore it seemed to be a good idea to
regard the order type of the least well ordering which is needed in the consistency proof for an
axioms system as characteristic for these axioms and to call it its proof theoretic ordinal. But as
observed by KREISEL there is a serious obstacle.
To state KREISEL s theorem we use some obvious abbreviations. The system EA of Elementary
Arithmetic is formulated in the language of arithmetic with the non-logical symbols
(0, 1, +, �, 2x, =, d")
together with their defining axioms among them
(exp) 20 =1 and 2x+1 =2x +2x
(d") x d" 0 "! x =0 and
x d" y +1"! x d" y (" x = y +1.
The scheme
(Ind) �(0) '" ("x)[�(x) �(x +1)] ("x)�(x)
of Mathematical Induction is restricted to "0 formulas �. A formula is "0 iff it only contains
bounded quantifiers ("xfor all primitive recursive functions and in which the scheme of mathematical induction is re-
stricted to Ł0 formulas. By Ą" we denote the false sentence 0 =1. We assume that there is an
1
elementary coding for the language of arithmetic and that there is a predicate
Prf (i, v) :�!  i codes a proof from Ax of the formula coded by v .
Ax
For an axiom system Ax we obtain the provability predicate as
x :�! ("y)Prf (y, x).
Ax
Ax
By PRWO(z") we denote that there are no primitive recursive infinite descending sequences in
field z". By TI (z") we denote the scheme of induction along z".
1.1.1 Theorem (Kreisel) For any consistent axiom system Ax there is a primitive recursive
well ordering z"Ax of order type � such that
PRA + PRWO(z"Ax ) Con(Ax )
5
1. Proof theoretic ordinals
Sketch of the proof of Theorem 1.1.1 Define
xAx
x z"Ax y :�! (i)
y and let
F (x) :�! ("i d" x)[ŹPrf (i, Ą" )]. (ii)
Ax
Now we obtain
PRA ("xz"Ax y)F (x) F (y) (iii)
since if we assume ŹF (x) we have ("i d" x)[Prf (i, Ą" )] and get x +1 z"Ax x and thus
Ax
together with the premise of (iii) also F (x +1). But this implies F (x), a contradiction.
Since F (x) is primitive recursive we obtain from (iii)
PRA + PRWO(z"Ax ) ("x)F (x) (iv)
and thus
PRA + PRWO(z"Ax ) Con(Ax). (v)
Since Con(Ax) is true we have otyp(z"Ax ) =�.
CK
Recall that �1 denotes the first ordinal which cannot be represented as the order type of a
CK
recursive well ordering. It is well-known that for every ordinal  < �1 there is a primitive
recursive (even elementary) well ordering of order type . There is a theorem recently observed
by BEKLEMISHEV which points exactly in the opposite direction of Theorem 1.1.1.
CK
1.1.2 Theorem (Beklemishev) For any  <�1 there is a primitive recursive well ordering
of order type  such that

PRA + PRWO(z") Con(PA).
To show Theorem 1.1.2 we first observes two other facts.
CK
1.1.3 Theorem (Beklemishev) For every ordinal  < �1 there is a primitive recursive well
ordering E of order type  such that
PA Con(PRA + TI (E)).
Sketch of the proof of Theorem. 1.1.3 Let R be a primitive recursive well ordering such that
otyp(R) =. (i)
Put
xRz y :�! x + y d" z '" xRy. (ii)
Then Rz is a finite ordering and we get a proof of TI (Rz) primitive recursively from z. Hence
�
PRA ("z) TI (Rz ). (iii)
PRA
By the arithmetical fixed-point theorem we define a formula
xEy :�! xRy '" ("uwhere C(u, v) is the primitive recursive predicate saying that v is a code for xEy and u codes a
proof of a contradiction from PRA + TI (E). Then
6
1.1. Preliminaries
PRA C(z, (xEy) ) '" ("u (xEy "! xRz y)
(v)
�
("z) (xEy "! xRz y)
PRA
TI (E)
PRA
by (iii). Since PA proves Con(PRA) and the least number principle we get from (v)
PA ("z)C(z, (xEy) ) Con(PRA + TI (E)). (vi)
But (vi) means
PA Con(PRA + TI (E)). (vii)
This, however, also entails that E and R coincide and we have otyp(E) =otyp(R) =.
1.1.4 Theorem Let Ax and Ax2 be theories which comprise PRA (either directly or via in-
1
terpretation). Then Ax Con(Ax2) implies Ax2 ą" 0 Ax1, i.e. Ax is 0 conservative over
1 1
1
1
Ax2.
Sketch of the proof of Thm.1.1.4 By formalized Ł0 completeness we get for a 0 formula P
1 1
PRA ŹP ŹP (i)
Ax
2
and thus
PRA Ź ŹP P. (ii)
Ax
2
If Ax2 P we get PRA P and thus also
Ax2
PRA ŹŹP. (iii)
Ax2
Hence
PRA Ź Ą" Ź ŹP (iv)
Ax Ax
2 2
which is
PRA Con(Ax2) Ź ŹP. (v)
Ax
2
Because of
Ax1 Con(Ax2) (vi)
we obtain from (vi),(v) and (ii)
Ax1 P
and are done.
Now we obtain Theorem 1.1.2 from Theorems 1.1.4 and 1.1.3 by choosing z" to be the well
ordering E constructed in Theorem 1.1.3.
It follows from Theorems 1.1.1 and 1.1.2 that the order type of a well ordering which suffices
for a consistency proof by induction along this well ordering is not a very intrinsic measure. The
order relation constructed in proving both theorems, however, appear quite artificial. For  natural
well orderings these pathological phenomena do not arise. But the real obstacle here is to find
a mathematically sound definition of  naturalness for well orderings. Therefore one is looking
for a more stable definition of the proof theretic ordinal of an axiom system.
Already GENTZEN in [7] observed that his consistency proof also entails the result that the axioms
of Peano Arithmetic cannot prove the well foundedness of primitive recursive well orderings of
order typs exceeding the order type of the well ordering which he used in his consistency proof.
7
1. Proof theoretic ordinals
On the other hand he could show that for any lower order type  there is a primitive recursive
well ordering of order type  whose well foundedness can be derived from the axioms of Peano
arithmetic. So his ordinal is characteristic for PA in that sense that it is the least upper bound
for the order types of primitiv recursive well oderings whose well foundedness can be proved in
PA. The well foundedness of a relation z" can be expressed by the formula
TI (z", X) :�! ("x)[("y z" x)(y " X) x " X] ("x)[x " X].
Let PR denote the collection of primitive recursive relations. According to GENTZEN s observa-
tion we define

||Ax || := sup otyp(z") z"" PR '" Ax TI (z", X) (1.1)
and call ||Ax|| the proof theoretic ordinal of the axiom system Ax . For reasons which will be-
come clear in the next sections we call ||Ax|| the 1 ordinal of Ax and will later indicate that
1
there are also other characteristic ordinals for a set Ax of axioms.
1.2 Some basic facts about ordinals
Ordinals are originally introduced as equivalence classes of well orderings. From a set theoretical
point of view this is problematic since these equivalence classes are not sets but proper classes.
Ordinals in the set theoretical sense are therefore introduced as sets which are well ordered by
the " relation. This entails that an ordinal ą the set of all ordinals � < ą. When we talk about
ordinals we have the set theoretical meaning of ordinals in mind. But this is of no importance.
All we have to know about ordinals are a few basic facts which we will describe shortly.
(On1) The class On of ordinals is a non void transitive class, which is well-ordered by the mem-
bership relation ". We define ą<�as ą " On '" � " On '" ą " �.
In general we use lower case Greek letters as syntactical variables for ordinals. The well-foundedness
of " on the class On implies the principle of transfinite induction
("� " On)[("� <�)F (�) �! F (�)] �! ("� " On)F (�)
and transfinite recursion which, for a given function g, allows the definition of a function f satis-
fying the recursion equation

f(�) =g( f(�) � <� ).
(On2) The class On of ordinals is unbounded, i.e., ("� " On)("� " On))[� <�]. The cardinal-
ity |M| of a set M is the least ordinal ą such that M can be mapped bijectively onto ą.
An ordinal ą is a cardinal if |ą| = ą.
(On3) If M ą" On and |M| "On then M is bounded in On, i.e., there is an ą " On such that
M ą" ą.
For every ordinal ą we have by (On1) and (On2) a least ordinal ą which is bigger than ą. We
call ą the successor of ą. There are three types of ordinals:
" the least ordinal 0,
" successor ordinals, i.e., ordinals of the form ą ,
" ordinals which are neither 0 nor successor ordinals. Such ordinals are called limit ordinals. We
denote the class of limit ordinals by Lim.
Considering these three types of ordinals we reformulate transfinite induction and recursion as
follows:
8
1.2. Some basic facts about ordinals
Transfinite induction: If F (0) and ("ą " On)[F (ą) �! F (ą )] as well as ("� <)F (�) �! F ()
for  " Lim then ("� " On)F (�).
Transfinite recursion: For given ą " On and functions g, h there is a function f satisfying the
recursion equations
f(0) = ą
f(� ) =g(f(�))

f() =h( f(�) �< ) for  " Lim.
An ordinal � satisfying
(R1) � " Lim
(R2) If M ą" � and |M| <�then M is bounded in �, i.e., there is an ą " � such that M ą" ą
is called regular. The class of regular ordinals is denoted by R.
(On4) The class R is unbounded, i.e., ("� " On)("� " R)[� d" �].
We define

sup M := min � " On ("� " M)(� d" �)
as the least upper bound for a set M ą" On. In set theoretic terms it is sup M = M. It follows
that sup M is either the biggest ordinal in M, i.e., sup M =max M, or sup M " Lim. By � we
denote the least limit ordinal. It exists according to (O4) and (O1). The ordinal �1 denotes the
first uncountable ordinal, i.e., the first ordinal whose cardinality is bigger than that of �. It exists
by (On3).
For every class M ą" On there is a uniquely determined transitive class otyp(M) ą" On and an
onto
order preserving function enM : otyp(M) - M. The function enM enumerates the elements
of M in increasing order. Since otyp(M) is transitive it is either otyp(M) =On or otyp(M) "
On. We call otyp(M) the order type of M. In fact otyp(M) is the MOSTOWSKI collapse of
M and enM the inverse of the collapsing function (usually denoted by Ą). By (On3) we have
otyp(M) " On iff M is bounded in On. Unbounded, i.e., proper classes of ordinals have order
type On. If M is a set of ordinals then otyp(M) " On.
If M is a transitive class and f: M - On an order preserving function then ą d" f(ą) for all
ą " M.
Aclass M is closed (in a regular ordinal �) iff sup N " M holds for every class N ą" M such
that |N| "On (|N| <�). We call M club (in �) iff M is closed and unbounded (in �).
We call an order preserving function f: M On (�-) continuous iff M is (�-) closed and f
-
preserves suprema, i.e., sup f(�) � " N = f(sup(N)) for any N ą" M such that |N| "On
(|N| <�).
A normal (�-normal) function is an order-preserving continuous function
f: On - On or f: � - � respectively.
For M ą" On (M ą" �) the enumerating function enM is a (�-)normal function iff M is club (in
�).
Extending their primitive recursive definitions continuously into the transfinite we obtain the basic
arithmetical functions +, � and exponentiation for all ordinals. The ordinal sum, for example,
satisfies the recursion equations
ą +0=ą
ą + � =(ą + �)
ą +  =sup� <(ą + �) for  " Lim.

It is easy to see that the function � . ą + � is the enumerating function of the class � " On ą d" �
9
1. Proof theoretic ordinals
which is club in all regular �>ą. Hence � . ą + � is a �-normal function for all regular �>ą.
We define

H := ą " On ą =0 '" ("� <ą)("� <ą)[� + �<ą]

and call the ordinals in H additively indecomposable. Then H is club (in any regular ordinal >�),
1 :=0 " H, � " H and � )" H = {1}. Hence enH(0) = 1 and enH(1) = � which are the first
two examples of the fact that
("� " On)[enH(�) =��]. (1.2)
Thus � . �� is a (�-)normal function (for all � " R bigger than �). We have
H ą" Lim *"{1}
and obtain
ą " H iff ("� <ą)[� + ą = ą].
Thus for a finite set {ą1, . . . , ąn} ą"H we get
ą1 + . . . + ąn = ąk + . . . + ąk
1 m
for {k1, . . . , km} ą" {1, . . . , n} such that ki < ki+1 and ąk e" ąk . By induction on ą we
i i+1
obtain thus ordinals {ą1, . . . , ąn} ą"H such that for ą =0 we have

ą = ą1 + . . . + ąn and ą1 e" . . . e" ąn. (1.3)
This is obvious for ą " H and immediate from the induction hypothesis and the above remark if
ą = � + � for �, � < ą. It follows by induction on n that the ordinals ą1, . . . , ąn in (1.3) are
uniquely determined. We therefore define an additive normal form
ą =NF ą1 + . . . + ąn : �! ą = ą1 + . . . + ąn, {ą1, . . . , ąn} ą"H and ą1 e" . . . e" ąn.
We call {ą1, . . . , ąn} the set of additive components of ą if ą =NF ą1 + . . . + ąn.
We use the additive components to define the symmetric sum of ordinals ą =NF ą1 + . . . + ąn
and � =NF ąn+1 + . . . + ąm by
ą = � := ąĄ(1) + . . . + ąĄ(m)
where Ą is a permutation of the numbers {1, . . . , m} such that
1 d" i In contrast to the  ordinary ordinal sum the symmetric sum does not cancel additive components.
By definition we have
ą = � = � = ą.
It is easy to check that the symmetric sum is order preserving in its both arguments.
As another consequence of (1.3) we obtain the CANTOR normal form for ordinals for the basis �,
which says that for every ordinal ą =0 there are ordinals �1, . . . , �n such that

1 n
ą =NF �� + . . . + �� .
Since � . �� is a normal function we have ą d" �ą for all ordinals ą. We call ą an �-number if
�ą = ą and define

�0 := min ą �ą = ą .
more generally let � . �� enumerate the fixed points of � . �� . If we put
n
exp0(ą, �) :=� and expn+1(ą, �) :=ąexp (ą,�)
10
1.2. Some basic facts about ordinals
we obtain
�0 := sup expn(�, 0).
n<�
For 0 <ą <�0 we have ą <�ą and obtain by the CANTOR Normal Form Theorem uniquely
1 n
determined ordinals ą1, . . . , ąn <ąsuch that ą =NF �ą + . . . + �ą .
For a class M ą" On we define its derivative

M := � " On enM (�) =� .
The derivative f of a function f is defined by f := enFix (f), where

Fix (f) := � f(�) =� .
Thus f enumerates the fixed-points of f. If M is club (in some regular �) then M is also club
(in �). Thus if is a normal function f is a normal function, too.
f
If Mą ą " I is a collections of classes club (in some regular �) and |I| " On (|I| " �) then
Mą is also club (in �).
ą"I
These facts give raise to a hierarchy of club classes. We define
Cr (0) := H
Cr (ą ) :=Cr(ą)
Cr () := Cr(�) for  " Lim.
�<
If we put
�ą := enCr(ą),
then all �ą are normal functions and we have by definition
ą<� �! �ą(��(ł)) = ��(ł). (1.4)
The function � is commonly called VEBLEN function. From (1.4) we obtain immediately
�ą (�1) d" �ą (�2) iff ą1 <ą2 and �1 d" �ą (�2) (1.5)
1 2 2
or ą1 = ą2 and �1 d" �2
or ą2 <ą1 and �ą (�1) d" �2.
1
We define the VEBLEN normal form for ordinals ��(�) by
ą =NF ��(�) : �! ą = ��(�) and � <ą.
Then ą =NF �� (�1) and ą =NF �� (�2) �! �1 = �2 and �1 = �2. Since � < ą and
1 2
� <� " Cr(ą) implies ��(�) <� we call Cr(ą) the class of ą critical ordinals.. If ą is itself
ą critical then �, � < ą �! ��(�) <ą. Therefore we define the class SC of strongly critical
ordinals by

SC := ą " On ą " Cr (ą) .
The class SC is club (in all regular ordinals � > �). Its enumerating function is denoted by
� . �� . Regarding that by (1.5) � . ��(0) is order preserving one easily proves

SC = ą �ą(0) = ą .
If we define ł0 := 0 and łn+1 := �ł (0) then we obtain
n
�0 = sup łn.
n<�
We define the set of strongly critical components SC (ą) of an ordinal ą by
11
1. Proof theoretic ordinals
ńł
{0} if ą =0
�ł
�ł
{ą} if ą " SC
SC (ą) := (1.6)
�ł SC (�) *" SC (�) if ą =NF ��(�)
ół
SC (ą1) *" . . . SC (ąn) if ą =NF ą1 + . . . + ąn.
For every ą < �0 there are uniquely determined ordinals �1, . . . , �n < ą and �1, . . . , �n < ą
such that
ą =NF �� (�1) +. . . + �� (�n) and �i <�� (�i) for i "{1, . . . , n}. (1.7)
1 n i
Recall that a relation z" is well founded if there is no infinite descending sequence � � � xn+1 z"
xn z" � � � in field(z"). For x " field(z") we define

otypz"(x) :=sup otypz"(y) y z" x
and

otyp(z") :=sup otypz"(x) x " field(z") .
We call otyp(z") the ordertype of z". It is easy to see that otypz"(x) and otyp(z") are ordinals.
This is all we need to know about ordinals for the moment. We will have to come back to the
theory later.
1.3 Truth complexity for 1 sentences
1
1.3.1 Definition The TAIT language for arithmetic contains the following symbols
" Set variables X, Y , X1,. . .
" The logical symbols '", (", ", "
" The binary relation symbols ",", =, =.
/
" The constant 0.
" Symbols for all primitive recursive functions.
Terms and formulas are constructed in the usual way.
Since there is no negation symbol we define
" <"(s = t) :a" s = t; <"(s = t) :a" s = t

" <"(s " X) :a" s " X; <"(s " X) :a" s " X
/ /
" <"(A '" B) :a"<"A ("<"B; <"(A (" B) :a"<"A '"<"B
" <"("x)F (x) :a" ("x)<"F (x); <"("x)F (x) :a" ("x)<"F (x).
We observe that for any assignment Ś of subsets of N to the set variables occurring in F we obtain
N |= <"F [Ś] �! N |= ŹF [Ś]. (1.8)
Therefore we commonly write ŹF instead of <"F .
Let D(N) be the diagram of N, i.e. the set of true atomic sentences.
1.3.2 Observation The true arithmetical sentences can be characterized by the following types
" the sentences in D(N)
" the sentences of the form (F0 (" F1) or ("x)F (x) where Fi and F (k) is true for some i "
{0, 1} or k " � respectively
12
1.3. Truth complexity for 1 sentences
1
" the sentences of the form (F0 '" F1) or ("x)F (x) where Fi and F (k) is true for all i "{0, 1}
or k " � respectively
According to Observation 1.3.2 we divide the arithmetical sentences into two types.
1.3.3 Definition
 type := D(N) *"{sentences of the form (F0 '" F1)}*"
{sentences of the form ("x)F (x)}

 type := ŹF F "  type =
ŹD(N) *"{sentences of the form (F0 (" F1)}
*"{sentences of the form ("x)F (x)}
and define a characteristic sequence CS (F ) of sub sentences of F by
1.3.4 Definition
ńł
�ł " if F is atomic
CS (F ) := (F0, F1) if F a" (F0 ć% F1)
ół
(F (k)| k " �) if F a" (Qx)F (x)
for ć% " {'", ("} and Q " {", "}. The length of the type of a sentence F is the length of its
characteristic sequence CS (F ).
From Observation 1.3.2 and Definition 1.3.3 we get immediately
1.3.5 Observation
F "  type �! [N |= F �! ("G " CS (F ))(N |= G)]
and
F "  type �! [N |= F �! ("G " CS (F ))(N |= G)]
We use Observation 1.3.5 to define the truth complexity of a sentence F .
ą
1.3.6 Definition We define the validity relation F inductively by the following two clauses
ąG ą
( ) If F "  type and ("G " CS (F ))[ G & ąG <ą] then F
ąG ą
( ) If F "  type und ("G " CS (F ))[ G & ąG <ą] then F .
Finally we put

ą
tc(F ) :=min ą F *"{�}
and call tc(F ) the truth complexity of the sentence F .
The next theorem is obvious from Observation 1.3.5 and Definition 1.3.6.
ą
1.3.7 Theorem F implies N |= F .
1.3.8 Observation Let rnk(F ) be the number of logical symbols accurring in F . Then we get
N |= F �! tc(F ) d" rnk(F )
and
13
1. Proof theoretic ordinals
N |= F �! tc(F ) <�.
According to Observation 1.3.8 the notion of truth complexity is not very exciting for arithmetical
sentences. This, however, will change if we extend it to the class of formulas containing also free
set variables.
1.3.9 Definition We call an arithmetical formula which does not contain free number variables
but may contain free set parameters a pseudo 1 sentence. For pseudo 1 sentences F (X) we
1 1
define
N |= F (X) :�! N |=("X)F (X).
For pseudo 1 sentences there is a third type of open atomic pseudo sentences which are the
1
sentences of the form
(t " X) and (s " X).
/
ą
1.3.10 Definition For a finite set " of pseudo 1 sentences we define the validity relation "
1
inductively by the following clauses
ą
(Ax ) sN = tN �! " , s " X, t " X
/
ąG
ą
( ) If F "  type )" " and ("G " CS (F )) " , G& ąG <ą then "
ąG
ą
( ) If F "  type )" " and ("G " CS (F )) " , G& ąG <ą then "
Observe that for finite sets of formulas we always write F1, . . . , Fn instead of {F1, . . . , Fn}. We
often also write ", � instead of " *" �.
The aim is now to extend the second claim in observation 1.3.8 to formulas also containing set pa-
rameters. We will do that using the method of search trees as introduced by SCH�TTE. Therefore
we regard for the moment finite sequences " of pseudo 1 sentences. The leftmost non atomic
1
formula in a sequence " is its redex R("). The sequence "r is obtained from " by canceling its
redex R("). We put
Ax (") :�! "s, t, X[sN = tN '"{t " X, s " X} ą""].
/
For the definition of a tree cf. Definition 1.7.1. Two pseudo 1 sentences are numerical equiva-
1
lent if they only differ in terms whose evaluation yield the same value.
1.3.11 Definition For a finite sequence " of pseudo 1-sentences we define its search tree S"
1
together with a label function
�: S" - finite sequences of pseudo 1 sentences
1
inductively by the following clauses
(S ) " S" '" �( ) ="
For the following clauses assume s " S" and ŹAx (�(s))
(SId ) R(�(s)) = " �! s 0 "S" '" �(s 0 ) =�(s)
(S ) R(�(s)) "  type �! ("Fi " CS (R(�(s))))[s i "S"] '" �(s i ) ="r, Fi
(S ) R(�(s)) "  type �! s 0 "S" '" �(s 0 ) ="r, Fi, R(�(s)), where Fi is the
first formula in CS (F ) which is not numerical equivalent to a formula in �(s0).
s0ą"s
14
1.3. Truth complexity for 1 sentences
1
1.3.12 Remark The search tree S" and � are primitive recursively constructed from ".
otyp(s)
1.3.13 Lemma (Syntactical Main Lemma) If S" is well founded then " holds for
all s " S".
Proof An easy induction on otyp(s).
1.3.14 Lemma (Semantical Main Lemma) If S" is not well founded then there is an assign-
ment S1, . . . , Sn to the set variables occurring in " such that N |= F [S1, . . . , Sn] for all F " ".
Sketch of the proof of Lemma 1.3.14. Pick an infinite path f in S" and let
f[n] := f(0), . . . , f(n - 1) .
Observe
F atomic '" F " �(f[n]) �! ("me"n)[F " �(f[m])] (i)
F " �(f[n]) )"  type �! ("m)("G " CS (F ))[G " �(f[m])] (ii)
F " �(f[n]) )"  type �! ("G " CS (F ))("m)[G " �(f[m])]. (iii)
Notice that we identify numerical equivalent formulas.
We define an assignment

Ś(X) := tN ("m)[(t " X) " �(f[m])]
/
and show by induction on rnk(F ) that N |= F [Ś] for all F " �(f[m]) using (ii) and (iii).
m"�
1.3.15 Theorem (� completeness Theorem) For a 1 sentence ("X1) . . . ("Xn)F (X1, . . . , Xn)
1
we have
ą
CK
N |=("X1) . . . ("Xn)F (X1, . . . , Xn) �! ("a<�1 ) F (X1, . . . , Xn).
Proof First we show by an straight forward induction on ą
ą
" �! N |= "[Ś] (i)
for any assignment of subsets of N to the set variables occurring in ". The direction from right
to left follows from (i).
For the opposite direction we assume
ą
F (X1, . . . , Xn) (ii)

CK
for all ą <�1 . Then SF (X1,...,Xn) cannot be well founded by the Syntactical Main Lemma
(Lemma 1.3.13). By the Semantical Main Lemma we thus obtain an assignment Ś to the set
variables X1, . . . , Xn such that N |= F (X1, . . . , Xn)[Ś].
1.3.16 Definition Let ("X)F (X) be a 1 sentence. We put
1

ą
CK
tc(("X)F (X)) := min ą F (X) *" �1
and call tc(F ) the truth complexity of F . For a pseudo 1 sentence G(X) containing the free
1
set parameters X we define
tc(G(X)) := tc(("X)G(X)).
15
1. Proof theoretic ordinals
1.3.17 Theorem For any (pseudo) 1 sentence F we have
1
CK
N |= F �! tc(F ) <�1 .
1.4 Inductive definitions
In order to link truth complexities with the proof theoretic ordinal of Ax defined in (1.1) we make
a quick excursion into the theory of inductively defined sets.
1.4.1 Definition An n ary clause on an infinite set N has the form
(C) P - c,
where P ą" Nn is the set of premises and c " Nn is the conclusion of the clause (C).
Aset S ą" Nn satisfies (C) if P ą" S implies c " S.

An inductive definition on N s a set Ś := Pą - cą ą " I of clauses on N.
The least (with respect to set inclusion) set I ą" Nn which simultaneously satisfies all clauses in
an inductive definition Ś is called inductively defined by Ś.
The special thing about inductive definition is the principle of proof by induction on the definition
which says:
1.4.2 Theorem If I ą" Nn is inductively defined by an inductive definition Ś and � is a  prop-
erty which is preserved by all clauses in Ś, i.e.
Pą - cą " Ś '" ("s " Pą)�(s) �! �(cą),
then all elements of the set I have the property �, i.e.
("s " I)[�(s)].
Proof Obvious.
1.4.3 Observation An inductive definition Ś induces an operator
�Ś: Pow(Nn) - Pow(Nn)
by defining

�Ś(S) := c ("P )[P - c " Ś '" P ą" S]
which is monotonic, i.e.
S ą" T ą" Nn �! �Ś(S) ą" �Ś(T ).
Generalizing the situation in Observation 1.4.3 we make the following definition.
1.4.4 Definition Let N be a set. An n ary generalized monotone inductive definition on N is a
monotone operator
�: Pow(Nn) - Pow(Nn).
Aset S ą" Nn is closed under �, if �(S) ą" S.
Aset F ą" Nn is a fixed point of � iff �(F ) =F .
The least fixed point (with respect to set inclusion) of an operator � is called the fixed point of
�.
16
1.5. The stages of an inductive definition
1.4.5 Observation Every generalized monotone inductive definition � on a set N possesses a
least fixed point I� which is the intersection of all � closed sets.
Proof Let

M� := S �(S) ą" S
and
I� := M�.
For S " M� we have I� ą" S and thus �(I�) ą" �(S) ą" S by monotonicity. Thus
�(I�) ą" M� = I�. (i)
From (i) we obtain
�(�(I�)) ą" �(I�) (ii)
again by monotonicity. Hence �(I�) " M� which entails
I� ą" �(I�). (iii)
But (i) and (iii) show that I� is a fixed point and by definition of I� this has to be the least one.
1.5 The stages of an inductive definition
1.5.1 Definition For an arbitrary operator �: Pow(Nn) - Pow(Nn) we define its ą th iter-
ation �ą by
�0(S) :=S
�ą+1(S) :=�(�ą(S))

�(S) :=�( ��(S) � < ) for  " Lim.
We will frequently use the shorthand
�<ą(S) := ��(S).
�<ą
We define
ą
I� := �<ą(") *" �(�<ą("))
and use the shorthand
�
<ą
I� := I�.
�<ą
1.5.2 Lemma For a monotone operator � we have
ą <ą
I� := �(I� ).
1.5.3 Lemma Let �: Pow(Nn) - Pow(Nn) be an operator. Then there is a least ordinal
|�| < |N|+ such that
|�| <|�|
I� = I� .
17
1. Proof theoretic ordinals
We call |�| the closure ordinal of the operator �.
Proof This is obvious for cardinality reasons.
1.5.4 Theorem Let � be a generalized monotone inductive definition. Then
|�| <|�|
I� = I� = I� .
<|�| |�| <|�| |�| |�|
Proof Since �(I� ) =I� = I� we have I� " M� and thus I� ą" I� . For the opposite
inclusion we prove
�
I� ą" I� (i)
<�
by induction on � d" |�|. By induction hypothesis we have I� ą" I� which by monotonicity
� <�
entails I� =�(I� ) ą" �(I�) =I�.
The following definition is an obvious generalization of Theorem 1.5.4.
1.5.5 Definition A generalized inductive definition on a set N is an operator
�: Pow(Nn) - Pow(Nn).
|�|
The fixed point of a generalized inductive definition � is the set I� := I� .
1.5.6 Definition For a generalized inductive definition � and n " I� we define

�
|n|� := min � n " I� .
1.5.7 Theorem Let � be an generalized inductive definition on a set N. Then

|�| =sup |n|� +1 n " I� .
Proof By definition we have

� := sup |n|� +1 n " I� d"|�|. (i)
<� �
Assuming � <|�| we get I� I� and find some x " I� such that � d"|x|� < |x|� +1 d" �.
A contradiction.
1.6 Positively definable inductive definitions
1.6.1 Definition Let S = (S, � � �) be some infinite structure and F a class of L(S) formulas.
We will now and for ever assume that F contains all atomic formulas and is closed under the
positive boolean operations (" and '" and substitution with relations definable by formulas in F.
An operator
�: Sn - Sn
is F definable on the structure S iff there is an F formula �(x, X, y) and a tuple a of elements
of S such that

�(M) = y " Sn S |= �[y, M, a] .
If F is the class of first order formulas we call � first order or  synonymously  elementarily
definable.
We denote the operator defined by a formula �(X, x) by �� and the fixed point of �� by I�.
ą ą
Anaologously we write shortly I� instead of I� , |�| instead of |��| and |x|� instead of |x|� .
�
�
18
1.7. Well founded trees and positive inductive definitions
1.6.2 Definition The class of X positive L(S) formulas is the least class containing all atomic
formulas without occurrences of X and all atomic formulas of the shape t " X which is closed
under the positive boolean operations (" and '" and under arbitrary quantifications.
1.6.3 Observation Any operator �� which is defined by an X positive formula is monotone. We
call such operators positive.
Proof Show
M ą" N '" S |= �[M, n] �! S |= �[N, n]
for all n " Sk by induction on the length of the X positive formula �(X, x).
1.6.4 Definition Let F be a class of L(S) formulas. A relation R ą" Sn is called positively
F inductive on the structure S =(S, � � �) if there is an X positive formula �(X, x, y) in F and
a tuple s " Sm such that
x " R �! (x, s) " I�.
In the case that F is the class of first order formulas we talk about positively inductive relations.
1.6.5 Theorem Every positively inductive relation on a structure S is 1-definable.
1
Proof This follows immediately from Observations 1.6.3 and 1.4.5.
1.6.6 Definition The ordinal

�S := sup |�| �(X, x) is an X positive elementary L(S) formula
is called the closure ordinal of the structure S.
1.7 Well founded trees and positive inductive definitions
We now leave the general situation and return to the structure N of arithmetic.
1.7.1 Definition A tree is a set of (codes for) finite number sequences which is closed under
initial sequences. I.e.
T is a tree :�! T ą" Seq '" ("t " T )[s ą" t s " T ],
where s ą" t stands for lh(s) d" lh(t) '" ("i Apathina tree T is a subset f ą" T which is linearly ordered by and closed under ą".
A tree is well founded if it has no infinite path.
For a node s " T in a well founded tree we define

otypT (s) :=sup otypT (s y ) s y "T
and
otyp(T ) :=otypT ( ).
1.7.2 Definition Let T be a tree. We define the X positive formula
�T (X, x) :�! ("y)[x y "T x y "X].
otypT
1.7.3 Lemma Let T be a well founded tree and s " T . Then s " I� (s).
T
19
1. Proof theoretic ordinals
Proof We induct on otypT (s). If otypT (s) =0 then there is no x " S such that s x " T .
0
Hence �T (", s) which entails s " I� . Now let otypT (s) > 0. For every s x " T we have
T
ą
ą := otypT (s x ) < otypT (s). By induction hypothesis we therefore obtain s x "I� ą"
T
I� (s). Hence �T (I� (s), s) which entails s " I� (s).
T T T
1.7.4 Corollary For a well founded tree T we have |s|� d" otypT (s) for all s " T . Hence
T
|�T | d"otyp(T ).
For a tree T and a node s " T we define the restriction of T above s as

T s := t " Seq s t " T .
Apparently T s is again a tree. If T s possesses an infinite path P then there is an s y " T
such that the tail of P above s belongs to T s y . This shows that T s is well-founded if
T s y is well founded for all s y "T .
1.7.5 Lemma Let T be a tree and s " T . If s " I� then T s is well founded and otyp(T s) d"
T
|s|� .
T
Proof The proof is by induction on |s|� . If |s|� =0 then we have �T (", s), i.e. ("x)[s x "
/
T T
T ]. Hence T s = and otyp(T s) = 0. If |s|� > 0 we have ("x)[s x " T �!
T
<|s|�T
s x " I� ]. Then by induction hypothesis T s x is well founded for all s x " T
T
and otyp(T s x ) < |s|�. This implies that T s is well-founded, too and otyp(T s) d"|s|�.
As a consequence of Corollary 1.7.4 and Lemma 1.7.5 we obtain
1.7.6 Theorem A tree T is well-founded iff " I� and for well-founded trees T we have
otyp(T ) +1=|�|.
Proof Let T be well founded. Then " I� by Lemma 1.7.3. If conversely " I� then
T = T is well founded by Lemma 1.7.5. For a well-founded tree T we get by Corollary 1.7.4
and Lemma 1.7.5
otypT (s) =otyp(T s) d"|s|� d" otypT (s).
T
Hence
T well founded '" s " T �! otypT (s) =|s|� (1.9)
T
and
otyp(T ) =otyp(T ) =| |� < |s|�
T T

for all s " T . But |�T | =sup |s|� +1 s " I� = | |� +1=otyp(T ) +1.
T T
1.7.7 Theorem The 1 relations on N are exactly the positively inductive relations .
1
Proof By Theorem 1.6.5 we know that all positively inductive relations are 1 definable. Con-
1
versely let R be a 1 relation. Then there is a 1 formula ("X)Ć(X, x) such that by Theorem
1 1
1.7.6
s " R �! N |=("X)Ć(X, s)
�! SĆ(X,s) is well founded
(i)
�! " I� .
S
Ć(X,s)
20
1.7. Well founded trees and positive inductive definitions
ą
1.7.8 Theorem (Boundedness Theorem) If ("x)[�(X, x) '" x " X], "(X, Y ) for a finite
/
ą
set "(X, Y ) of X positive formulas then N |= "[I� , S] for any set S ą" N.
Proof To show the theorem by induction on ą we need a more general statement. For a set
M ą" Nn and an X positive formula �(X, x) we introduce the formula
�M (X, x) :�! �(X, x) (" x " M. (i)
If M = { tN, . . . , tN} we write � t ,..., tn instead of �M . We claim
1 n
1
ą ą+1
I� ą" I� *"{s}. (ii)
M*"{s} M
In the proof of claim (ii) we need the observation
�(X *"{s}, x) Ć(X, x) (" x = s (1.10)
for X positive formulas �(X, x) which is easily proved by induction on the complexity of the
<ą
formula �(X, x). We prove (ii) by induction on ą. The induction hypothesis gives I� ą"
M*"{s}
ą
I� *"{s}. Therefore we obtain
M
ą <ą <ą
x " I� �! �(I� , x) (" x " I�
M*"{s} M*"{s} M*"{s}
ą ą
�! �(I� *"{s}, x) (" x " I� (" x = s
M M
ą ą
�! �(I� , x) (" x " I� (" x = s
M M
ą+1
�! x " I� (" x "{s}.
M
Let S be an arbitrary subset of N. We show
ą
ą
("x)[�(X, x) '" x " X], t1 " X, . . . , tn " X, "[X, Y ] �! N |="[I� , S] (iii)
/ / /
t1 ,..., tn
for a finite set "[X, Y ] of X positive formulas by induction on ą. If (iii) holds by (Ax ) then
"[X, Y ] contains a formula s " X such that sN = tN for some i " {1, . . . , n}. Since tN "
i i
ą ą
I� we obtain N |= "[I� , S].
t1,..., tn t1,..., tn
If the last inference is

ąą
("x)[�(X, x) '" x " X], t1 " X, . . . , tn " X, "ą[X, Y ] ą " J �!
/ / /
ą
("x)[�(X, x) '" x " X], t1 " X, . . . , tn " X, "[X, Y ]
/ / /
then we have by induction hypothesis
ą0
N |= "ą[I� , S] (iv)
t1,..., tn
ą ą
for all ą " J. Hence N |= "ą[I� , S] for all ą " J which entails N |= "[I� , S]
t1,..., tn t1 ,..., tn
by the soundness of the inferences of the infinitary calculus.
The really interesting case is
ą0
("x)[�(X, x) '" x " X], t1 " X, . . . , tn " X, �(X, s) '" s " X, "[X, Y ] �!
/ / / /
(v)
ą
("x)[�(X, x) '" x " X], t1 " X, . . . , tn " X, "[X, Y ].
/ / /
From the premise in (v) we obtain
ą0
("x)[�(X, x) '" x " X], t1 " X, . . . , tn " X, �(X, s), "[X, Y ] (vi)
/ / /
and
ą0
("x)[�(X, x) '" x " X], t1 " X, . . . , tn " X, s " X, "[X, Y ]. (vii)
/ / / /
From the induction hypothesis for (vii) we obtain
ą0
N |= "[I� , S] (viii)
t1 ,..., tn ,s
21
1. Proof theoretic ordinals
which together with (ii) imply
ą0
N |= "[I� *"{s}, S]. (ix)
t1 ,..., tn
Assuming
ą
N |= "[I� , S] (x)
t1 ,..., tn
we also have
ą0
N |= "[I� , S] (xi)
t1 ,..., tn
which together with the induction hypothesis for (vi) imply
ą0
N |= �(I� , s). (xii)
t1 ,..., tn
Hence
ą0
ą
s " I� +1 ą" I� . (xiii)
t1,..., tn t1,..., tn
By (xiii) and (ix) we finally obtain
ą
N |= "[I� , S].
t1 ,..., tn
So we have (iii). The theorem, however, is a special case of (iii).
1.7.9 Definition For an order relation z" let
�z"(X, x) :�! ("y z" x)[y " X] (1.11)
ą
and Acc(z") :=I� . We call Acc(z") the accessible part of z". By Accą(z") :=I� we denote
z"
z"
the ąth stage of the accessible part.
1.7.10 Observation For a well-founded relation z" we have
x " Accą(z") �! otypz"(x) =ą.
CK
1.7.11 Theorem It is �N = �1 .
Proof If z" is a recursive well ordering then by Observation 1.7.10 we obtain otyp(z") d"

CK CK
|�z"| d"�N. Since �1 =sup otyp(z") z" is recursive this implies �1 d" �N.
For an X positive formula �(X, x) we have
s " I� �! N |=("X)[("x)(�(X, x) x " X) s " X]
ą
CK
�! ("ą<�1 ) Ź ("x)(�(X, x) x " X), s " X
(i)
CK ą
�! ("ą<�1 ) N |= s " I� .
CK CK
So |�| d"�1 holds for all positive elementary inductive definitions which entails �N d" �1 .
1.8 The 1 ordinal of an axiom system
1
1.8.1 Definition For a theory Ax in the language of (2nd order) arithmetic we define

||Ax || 1 := sup tc(F ) F " 1 '" Ax F .
1
1
We call ||Ax|| 1 the 1 ordinal of Ax.
1
1
22
1.8. The 1 ordinal of an axiom system
1
We are going to show that the 1 ordinal and the proof theoretic ordinal defined in (1.1) coincide.
1
1.8.2 Lemma For a well ordering z" we have
otyp(z") d" tc(TI (z", X)).
Proof Apply the Boundedness Theorem (Theorem 1.7.8) to the formula �z"(X, x) defined in
(1.11) and then apply Observation 1.7.10.
For a primitive recursive well-ordering z" and s " field(z") we obtain by an easy induction on
otypz"(s)
5�(otypz"(s)+1)
Ź ("x)[("y z" x)(y " X) x " X], s " X. (1.12)
From (1.12) and Lemma 1.8.2 we obtain the following theorem.
1.8.3 Theorem For an arithmetical definable well ordering z" we have
otyp(z") =tc(TI (z", X)).
We just want to remark that this can be extended to Ł1 definable well orderings. Details are in [2].
1
1.8.4 Lemma For any axiom system Ax in the language of (2nd order) arithmetic we have
||Ax|| d" ||Ax|| 1.
1
Proof This is an immediate consequence of Theorem 1.8.3.
1.8.5 Lemma If Ax is an axiom system comprising PA then ||Ax|| = ||Ax|| 1.
1
Sketch of the proof Assume that Ax is a theory comprising PA and let ("Y )F (Y ) be a 1-
1
sentence. Denote by z"S the KLEENE BROUWER ordering in the search tree SF (Y ) for F (Y )
F (Y )

and assume that Ax TI (z"S , X) . Then there is a model M |= Ax and an assignment
F (Y )
T ą" M for X such that M |= TI (z"S , X)[T ]. Therefore there is an infinite path, say P ą" M,
F (Y )
through SF (Y ) which is definable by an first order formula with parameter T . According to the
Semantical Main Lemma we get assignments Ś(Yi) ą" M for all Yi belonging to Y which are
definable by first order formulas with parameter T . Since we have induction in M for first order
formulas we obtain M |= F (Y )[Ś] as in the proof of the Semantical Main Lemma using a local

truth predicate. Hence Ax F (Y ) andwe have shown
Ax F (Y ) �! Ax TI (z"S , X).
F (Y )
Since z"S is primitive recursively definable and we have tc(F (Y )) d" otyp(z"S ) d"||Ax||
F (Y ) F (Y )
for Ax F (Y ) this implies ||Ax|| 1 d"||Ax||.
1
1.8.6 Theorem Let Ax be a Ł1 set of arithmetical sentences. The theory Ax is 1 sound iff
1 1
CK
||Ax|| <�1 .
CK CK
Proof If ||Ax|| <�1 we have ||Ax|| 1 <�1 and thus N |= F for all F such that Ax F
1

by Theorem 1.3.17. If conversely Ax is 1 sound then tc(F ) Ax F is a Ł1 definable
1 1

CK CK
subset of �1 . Hence ||Ax|| = ||Ax|| 1 =sup tc(F ) Ax F <�1 .
1
The following theorem is an immediate consequence of Theorem 1.8.3.
23
1. Proof theoretic ordinals
1.8.7 Theorem

||Ax || d" sup otyp(z") z"" PR '" Ax TI (z")

d" sup otyp(z") z"" " '" Ax TI (z")
0

d" sup otyp(z") z"" Ł1 '" Ax TI (z")
1
d"||Ax|| 1 = ||Ax||
1
1.8.8 Theorem (Kreisel) Let Ax be a theory which contains PA. Then
||Ax || 1 = ||Ax + F || 1
1 1
holds for every true Ł1 sentence F .
1
Proof Assume
Ax + F TI (z", X) (i)
for a primitive recursive ordering z". Then
Ax ŹF (" TI (z", X) (ii)
which implies
ą
Ź F, TI (z", X) (iii)
for some ą<||Ax|| 1. Let
1
Prog(z", X) :�! ("x)[("y z" x)(y " X) x " X]. (iv)
Then
TI (z", X) a" Prog(z", X) ("x " field(z"))[x " X]. (v)
For F a" ("Y )F0(Y ) we obtain from (iii)
ą
Ź Prog(z", X), ŹF0(Y ), ("x " field(z"))[x " X] (vi)
which by the Boundedness Theorem (Theorem 1.7.8) implies
N |= ŹF0[S] (" ("x " field(z"))[x " Accą(z")] (vii)
for every set S ą" N. Since N |=("Y )F0(Y ) there is a set S ą" N such that N |= F0[S] and we
obtain from (vii)
N |=("x " field(z"))[otypz"(x) d" ą]. (viii)
Hence
||Ax + F || 1 = ||Ax + F || d" ||Ax|| 1.
1 1
The opposite inequality holds obviously.
It follows from KREISEL s theorem that the 1 ordinal of an axiom system does not characterize
1
its arithmetical power. Therefore more refined notions of proof theoretic ordinals have been
developed (e.g. in [13]). Most recently BEKLEMISHEV could define the 0  ordinal of a theory
n
for all levels of the arithmetical hierarchy using iterated reflection principles. All these notions,
however, need a representation of ordinals either by notation systems or by elementarily definable
order relations on N. But it can be shown that different representations satisfying mild conditions
yield the same proof theoretic ordinals.
24
1.8. The 1 ordinal of an axiom system
1
In this lecture we will concentrate on the computation of the 1 ordinals. In the second part
1
Weierman will say something about the 0 ordinal of PA which characterizes its provably recur-
2
sive functions. We just want to mention that the computations we are going to show are profound
ordinal analyses in the sense of [12] and [13] and thus also comprise a computation of the the 0
2
ordinals. But we don t want to give details about that here.
25
1. Proof theoretic ordinals
26
2. The ordinal analysis for PA
2.1 Logic
To fix the logical frame we introduce a formal system for first order logic (without identity) which
is based on a one sided sequent calculus ą la TAIT.
2.1.1 Definition
m
(AxL) ", A, ŹA for any m, if A is an atomic formula
m0 m
((") If ", Ai for some i "{1, 2}, then ", A1 (" A2 for all m>m0
mi m
('") If ", Ai and mi m0 m
(") If ", A(t), then ", ("x)A(x) for all m>m0
m0 m
(") If ", A(u) and u not free in ", ("x)A(x), then ", ("x)A(x) for all m>m0.
One should observe the similarity of this calculus to the truth definition given in Definition 1.3.10.
By an easy induction on m we obtain
m
2.1.2 Lemma If " then |= ".
Using the technique of search trees one can also prove the completeness of this calculus. I.e. we
have
2.1.3 Theorem A formula of first order predicate calculus is logically valid iff there is a natural
m
number m such that F .
We will omit the proof which is very similar to the proof of the � completeness theorem. One
has to modify the definition of search tree in the obvious way. The Syntactical Main Lemma
then follows as before. To show the Semantical Main Lemma one assumes that the search tree
contains an infinite path and constructs a term model together with an assignment of terms to
the free variables such that all formulas occurring in the infinite path become false under this
assignment.
One of the consequences of the completeness theorem for the TAIT calculus is the admissibility
of the cut rule. We obtain
m n k
2.1.4 Theorem If ", F and ", ŹF then there is a k such that ".
But Theorem 2.1.5 does not say anything about the size of k. Therefore one augments the clauses
in Definition 2.1.1 by a cut rule
m m n
(Cut) If rnk(F ) m
r r r
m m
and replaces ", . . . in all clauses by ", . . .. The subscript r is thus a measure for the
r
m m
complexity of all cut formulas occurring in the derivation. Obviously we have " �! ".
0
m 2r(m)
2.1.5 Theorem (Gentzen s Hauptsatz) If " then " where 2r(x) is defined by 20(x) =
r
0
n
x and 2n+1(x) =22 (x)
27
2. The ordinal analysis for PA
We will not prove the Hauptsatz but leave it as an exercise which should be solved after having
seen the cut elimination for the semi formal calculus which we are going to introduce in 2.3.3.
2.1.6 Theorem Let "(x) be a finite set of formulas in the the language of arithmetic with all
m m
number variables shown. Then "(x) implies "(n) for all tuples n of numerals.
The proof of Theorem 2.1.6 is straightforward by induction on m using the obvious property
ą ą
sN = tN and "(s) �! "(t). (2.1)
2.2 The theory NT
Instead of analyzing the axioms in PA we do that for a richer language which has constants for
all primitive recursive functions and relations.
The language L(NT ) is a first order language which contains set parameters denoted by capital
Latin letters X, Y , Z, X1, . . . and constants for 0 and all primitive recursive functions and rela-
tions. We assume that the symbols for primitive recursive functions are built up from the symbols
n n
Ck for the constant function, Pk for the projection on the n-th component, S for the successor
function by a substitution operator Sub and the recursion operator Rec.
The theory NT comprises the universal closure of the following formulas:
The successor axioms
("x)[Ź0 = Sx]
("x)("y)[S(x) =S(y) �! x = y]
The defining axioms for function and relation symbols which are the universal closures of the
following formulas
n
Ck (x1, . . . , xn) =k
n
Pk (x1, . . . , xn) =xk
Sub(g, h1, . . . , hm)(x1, . . . , xn) =g(h1(x1, . . . , xn)) . . . (hm(x1, . . . , xn))
Rec(g, h)(0, x1, . . . , xn) =g(x1, . . . , xn)
Rec(g, h)(Sy, x1, . . . , xn) =h(y, Rec(g, h)(y, x1, . . . , xn), x1, . . . , xn)
(x1, . . . , xn) " R "! �R(x1, . . . , xn) =0
The scheme of Mathematical Induction
F (0) '" ("x)[F (x) F (S(x))] ("x)F (x)
for all L(NT )-formulas F (u).
The identity axioms
("x)[x = x]
("x)("y)[x = y y = x]
("x)("y)("z)[x = y '" y = z x = z]
("x)("y)[x1 = y1 '" . . . '" xn = yn f(x1, . . . , xn) =f(y1, . . . , yn)]
("x)("y)[x1 = y1 '" . . . '" xn = yn (R(x1, . . . , xn) R(y1, . . . , yn))]
("x)("y)[x = y (x " X y " X)].
If NT F there are finitely many axioms A1, . . . , An of NT such that ŹA1 (" � � � (" ŹAn (" F
is logically valid. Due to the completeness of the TAIT calculus (cf. Theorem 2.1.3) we therefore
have the following theorem.
28
2.3. The upper bound
2.2.1 Theorem Let F be a formula which is provable in NT . Then there are finitely many axioms
m
A1, . . . , An and an m<�such that ŹA1, . . . , ŹAn, F.
2.3 The upper bound
It follows from Theorems 2.1.3 and 2.1.6 that we have
m
ŹA1, . . . , ŹAn, F (2.2)
for the provable pseudo 1 sentences of NT . In order to determine the 1 ordinal of NT we
1 1
have to compute tc(F ). Our strategy will be the following. First we compute an upper bound,
say ą, for the truth complexities of all axioms in NT . This gives
ą
A (2.3)
i
for all axioms Ai. Then we extend the infinitary calculus for the truth definition to an infinitary
calculus with cut and use the cut rule to get rid of all the axioms. Then we eliminate the cuts. If
we succeed in controlling the length of an infinite derivation during the cut elimination procedure
we will obtain an upper bound for the truth complexity of F .
We start with the computation of the truth complexities of the axioms of NT .
All numerical instances of the defining axioms for primitive recursive function and relations be-
long to the diagram D(N). Therefore we obtain their universal closure by a finite number of
applications of the  rule. The same is true for all identity axioms except the last one. But there
we observe
5
("x)("y)[x = y (x " X y " X)] .
So we have
tc(F ) <� (2.4)
for all mathematical and identity axioms except induction. What really needs checking is the truth
complexity of the scheme of Mathematical Induction. Here we need the following lemmas.
2�rnk(F )
2.3.1 Lemma (Tautology Lemma) For every L(NT )-formula we have ", ŹF, F .
The proof is by induction on rnk(F ).
2.3.2 Lemma (Induction Lemma) For any natural number n and any L(NT )-sentence F (n)
we have
2�[rnkF (n))+n]
ŹF (0), Ź("x)[F (x) F (S(x))], F(n) .
The proof by induction on n is very similar to that of (1.12). For n =0 this is an instance of the
Tautology Lemma. For the induction step we have
2�[rnkF (n))+n]
ŹF (0), Ź("x)[F (x) F (S(x))], F(n) (i)
by the induction hypothesis and obtain
2�rnkF (n))
ŹF (0), Ź("x)[F (x) F (S(x))], ŹF (S(n)), F(S(n)) (ii)
by the Tautology Lemma. From (i) and (ii) we get by ( )
2�[rnkF (n))+n]+1
ŹF (0), Ź("x)[F (x) F (S(x))], F(n) '"ŹF (S(n)), F(S(n)) . (iii)
29
2. The ordinal analysis for PA
By a clause (") we finally obtain
2�[rnkF (n))+n]+2
ŹF (0), Ź("x)[F (x) F (S(x))], F(S(n)) .
By Lemma 2.3.2 we have tc(G) d" � +4 for all instances G of the Mathematical Induction
Scheme. Together with (2.4) we get
�+4
A i.e. tc(Ai) d" � +4 (2.5)
i
for all identity and non-logical axioms Ai of NT .
2.3.3 Definition For a finite set " of pseudo 1 sentences we define the semi formal provability
1
ą
relation " inductively by the following clauses
�
ą
(Ax ) sN = tN �! ", s " X, t " X
/
�
ą
ąG
( ) If F "  type )" " and ("G " CS (F )) ", G& ąG <ą then "
� �
ą
ąG
( ) If F "  type )" " and ("G " CS (F )) ", G& ąG <ą then "
� �
ą
ą0 ą0
(cut) If ", F; ", ŹF and rnk(F ) <� then " for all ą>ą0.
� � �
We call F the main formula of the clauses ( ) and ( ). The main formulas of an axiom (Ax )
are s " X and t " X. A cut possesses no main formula.
/
Observe that we have
ą ą
" �! " . (2.6)
0
Hence
m m
" �! " (2.7)
0
ą
by Theorem 2.1.6. There are some obvious properties of " which are proved by induction on
�
ą.
ą
2.3.4 Lemma (Soundness) If F1, . . . , Fn then N |=(F1 (" � � � (" Fn)[Ś] for every assign-
�
ment Ś of subsets of N to the set parameters in F1, . . . , Fn.
ą �
2.3.5 Lemma (Structural Lemma) If " then � holds for all � e" ą, � e" � and � �" ".
� �
ą ą
2.3.6 Lemma (Inversion Lemma) If F "  type and ", F then ", G for all G "
� �
CS (F ).
ą ą
2.3.7 Lemma ((" Exportation) If ", F1 (" � � � (" Fn then ", F1, . . . , Fn.
� �
ą ą
2.3.8 Lemma If F " D(N) and ", ŹF then ".
� �
2.3.9 Lemma (Reduction Lemma) Let � = rnk(F ) for F "  type, F a" (s " X) or F a"
ą � ą+�
(s " X). If ", F and �, ŹF then ", �.
/
� � �
30
2.3. The upper bound
�
Proof The proof is by induction on �. If ŹF is not the main formula in �, ŹF then we have
�
�ą
the premises �ą, F for ą " I. If I = " then � )" D(N) = " which entails ", � )" D(N) = " and

�
ą+�
we obtain ", � by an inference ( ) with empty premise. Otherwise we get
�
ą+�ą
", � (i)
�
ą+�
by the induction hypothesis and obtain ", � from (i) by the same inference.
�
Now assume that ŹF is the main formula. If � =0 then ŹF is atomic. If F "  type we have
ą+�
F " D(N) and obtain ", � by Lemma 2.3.8 and Lemma 2.3.4. If F a" (s " X) we show
�
ą
", � (ii)
�
by a side induction on ą. First we observe that there is a formula t " X with tN = sN in � since
� ą
�, ŹF holds by (Ax ) . If F is not the main formula of ", F then we have the premises
� �
ą
ąą
"ą, F for ą " I. If I = " we get ", � directly and for I = " from the induction hypothesis

� �
by the same inference. If F is the main formula we are in the case of (Ax ) which entails that
ą
there is a formula r " X in " with rN = sN = tN. But then we obtain ", � by (Ax). The
/
�
ą+�
case F a" (s " X) is symmetrical. From (ii) we get ", � by the Structural Lemma.
/
�
Now assume � >0. Then ŹF "  type and we have the premise
�0
�, ŹF, ŹG (iii)
�
for some G " CS (F ). Then we obtain
ą+�0
", �, ŹG (iv)
�
ą
by induction hypothesis. From ", F we obtain
�
ą+�0
", �, G (v)
�
by the Inversion and the Structural Lemma. Since rnk(G) < rnk(F ) =� we obtain the claim
from (iv) and (v) by (cut).
ą 2ą
2.3.10 Lemma (Basic Elimination Lemma) If " then ".
�
�+1
Proof Induction on ą. If the last inference is not a cut of complexity � we obtain the claim
immediately from the induction hypothesis and theąfact that � . 2� is order preserving. The
ą0
ą0
critical case is a cut ", F; ", ŹF �! " with rnk(F ) =�. By the induction
�+1 �+1 �+1
2ą0 +2ą0
0 0 0
hypothesis and the Reduction Lemma we obtain " and we have 2ą +2ą =2ą +1 d"
�
2ą.
Observe that our language so far only comprises formulas of finite rank. But we have designed
the semi formal calculus in such a way that it will also work for languages with formulas of
complexities e" �. The following results masters also this situation.
��(ą)
ą
2.3.11 Lemma (Predicative Elimination Lemma) If " then ".
�+�� �
2ą
Proof Induction on � with side induction on ą. For � = 0 we obtain " by the Basic
�
Elimination Lemma which, since 2ą d" �ą = �0(ą), entails the claim. Now assume � >0. If
31
2. The ordinal analysis for PA
the last clause was not a cut of rank e" � we obtain the claim from the induction hypotheses and
the fact that the functions �� are order preserving. Therefore assume that the last inference is
ą
ą0
ą0
", F ", ŹF �! "
�+�� �+�� �+��
such that � d" rnk(F ) <� + ��. But then there is an ordinal Ć such that rnk(F ) =� + Ć which,
1 n
writing Ć in CANTOR normal form, means rnk(F ) =�+�� +. . .+�� <�+��. Hence �1 <�
and, putting � := �1, weget rnk(F ) <� +�� �(n+1). By the side induction hypothesis we have
��(ą0
) ��(ą0
) ��(ą0
)+1
", F and ", ŹF . Byacut it follows ". If we define �0 (�) :=� and
�
� � �+���(n+1)
�n+1(�) :=��(�n(�)) we obtain from � <� by n +1 fold application of the main induction
� �
�n+1(��(ą0
)+1)
�
hypothesis ". Finally we show �n(��(ą0) +1) < ��(ą) by induction on n.
�
�
For n =0 we have �0 (��(ą0) +1) =��(ą0) +1<��(ą) since ą0 <ąand ��(ą) " Cr(0).
�
For the induction step we have �n+1(��(ą0)+1) = ��(�n(��(ą0)+1)) <��(ą) since � <�
� �
��(ą)
and �n(��(ą0) +1) <��(ą) by the induction hypothesis. Hence ".
�
�
By iterated application of the Predicative Elimination Lemma we obtain
ą
1 n
2.3.12 Theorem (Elimination Theorem) Let " such that � =NF �� + . . . + �� .
�
��1 (��2 (�����n (ą)���))
Then ".
0
2.3.13 Theorem (The upper bound for NT ) If NT F then tc(F ) <�0. Hence
||NT || = ||NT || 1 d" �0.
1
Proof If NT F we get by (2.3) and (2.5)
�+�
F (i)
r
for r := max{rnk(A1), . . . , rnk(An)} < �. By the Elimination Theorem (or just by iterated
application of the Basis Elimination Lemma) this entails
�r(�+�)
0
F. (ii)
0
�r(�+�)
0
Hence F and we get tc(F ) <�0 since �r(� + �) <�0 for all finite r.
0
2.4 The lower bound
We want to show that the bound given in Theorem 2.3.13 is the best possible one. By Theo-
rem 1.8.7 it suffices to have Theorem 2.4.1 below.
2.4.1 Theorem For every ordinal ą < �0 there is a primitive recursive well-order z" on the
natural numbers of order type ą such that NT TI (z", X).
The first step in proving Theorem 2.4.1 is to represent ordinals below �0 by primitive recursive
well-orders. This is done by an arithmetization. We simultaneously define a set On ą" N and a
relation a z" b for a, b " On together with an evaluation map | � |: On - On such that On and
z" become primitive recursive and a z" b �! |a| < |b|. We put
" 0 " On and |0| =0
1
" If z1, . . . , zn ą" On and z1 . . . zn then z1, . . . , zn "On and | z1, . . . , zn | = �|z | +
n
. . . + �|z |
32
2.4. The lower bound
and
" a z" b : �! a " On '" b " On '" [(a =0 '" b =0)

(" (lh(a) < lh(b) '" ("i (" ("i < min{lh(a), lh(b)})("j Observe that On and z" are defined by simultaneous course of values recursion and thence are
primitive recursive. It is also easy to check that a z" b �! |a| < |b|. The order On, z" is
a well-order of order type �0. We may therefore represent every ordinal ą < �0 by an initial
segment z"ą of the well-order z". Thus we can talk about ordinals <�0 in L(NT ). We will not
distinguish between ordinals and their representations in L(NT ) and regard formulas as ("ą)[. . .]
as abbreviations for ("x)[x " On . . .] as well as ("ą)[. . .] as abbreviation for ("x)[x "
On '" . . .]. We also write ą<�instead of ą z" �. We introduce the following formulas:
" ą ą" X :�! ("�)[� <ą � " X]
" Prog(X) :�! ("ą)[ą ą" X ą " X]
" TI(ą, X) :�! Prog(X) ą ą" X

Our aim is to show TI(ą, X) for all ą<�0. Since �0 =sup expn(�, 0) n " � and TI(0, X)
holds trivially we are done as soon as we succeed in proving
NT TI(ą, X) �! NT TI(�ą, X) (2.8)
because NT TI(ą, X) and � <ą obviously entails NT TI(�, X). The first observation is

NT F (X) �! NT F ( x G(x) ) (2.9)

for all L(NT )-formulas G. The formula F ( x G(x) ) is obtained from F (X) by replacing all
occurrences of t " X by G(t) and those of t " X by ŹG(t). To prove (2.9) assume
/
NT F (X) (i)
and let S be an arbitrary L(NT )-structure and Ś an assignment of subsets of N to the set variables
such that
S |= NT [Ś]. (ii)
We have to show

S |= F ( x G(x) )[Ś]. (iii)
Define a new assignment
Ś(Y ) if Y = X


�(Y ) :=
n " S S |= G(x)[n, Ś] otherwise.
Then

S |= F (X)[�] iff S |= F ( x G(x) )[Ś]. (iv)
We claim
S |= NT [�]. (v)
Then (v) together with (i) and (iv) prove (iii). To check (v) we have only to take care of formulas
in NT which contain the set variable X. This can only happen in instances of the scheme of
Mathematical Induction or in identity axioms. Let
I(X) :�! H(X, 0) '" ("x)[H(X, x) H(X, S(x))] ("x)H(X, x)
33
2. The ordinal analysis for PA
be an instance of Mathematical Induction. We have

S |= I(X)[�] iff S |= I( x G(x) )[Ś]. (vi)

The right formula in (vi), however, holds by (ii) since H( x G(x) , x) is also a formula in NT .
Instances of identity axioms are treated analogously.
The above proof shows the importance of formulating Mathematical Induction as a scheme.
Let

J (X) := ą ("�)[� ą" X � + �ą ą" X]
denote the jump of X. Then, if we assume
NT Prog(X) Prog(J (X)), (i)
we obtain
NT TI(ą, J (X)) TI(�ą, X). (ii)
To prove (ii) assume (working informally in NT ) TI(ą, J (X)), i.e.
Prog(J (X)) ą ą"J(X) (iii)
which entails
Prog(J (X)) ą "J(X). (iv)
Choosing � =0 in the definition of the jump turns (iv) into
Prog(J (X)) �ą ą" X, (v)
which, together with (i), gives
Prog(X) �ą ą" X, (vi)
which is TI(�ą, X). Once we have (ii) we also get (2.8) because TI(ą, X) implies TI(ą, J (X))
by (2.9).
It remains to prove (i). Again we work informally in NT . Assume
Prog(X). (vii)
We want to prove Prog(J (X)) i.e. ("ą)[ą ą"J (X) ą "J(X)]. Thus, assuming also
ą ą"J (X), (viii)
we have to show ą "J(X). i.e. ("�)[� ą" X � + �ą ą" X]. That means that we have to prove
� " X under the additional hypotheses
� ą" X (ix)
and
� <� + �ą. (x)
If � <� we obtain � " X by (ix). Let � d" � <� + �ą. If ą =0 the � = � and we obtain � " X
by (ix) and (vii). If ą >0 then there is a � < ą and a natural number (i.e. a numeral in NT ),
such that � < �� + . . . + �� =: �� � n (c.f. the proof of the Predicative Elimination Lemma).
n-fold
We show
� <ą � + �� � n ą" X (xi)
by induction on n. For n =0 this is (ix). For n := m +1we have
34
2.4. The lower bound
� + �� � m ą" X (xii)
by the induction hypothesis. From � <ą we obtain � " J (X) from (viii). This together with
(xii) entails � + �� � n = � + �� � m + �� " X. This finishes the proof of (i), hence also that of
(2.8) which in turn implies Theorem 2.4.1.
Summing up we have shown
2.4.2 Theorem (Ordinal Analysis of NT ) ||NT || = ||NT || 1 = �0.
1
As a consequence of Theorem 2.3.13 and Theorem 2.4.1 we get
2.4.3 Theorem There is a 1 sentence ("X)("x)F (X, x) which is true in the standard structure
1

N such that NT F (X, n) for all n " N but NT ("x)F (X, x) .
To prove the theorem choose F (X, x) :�! Prog(X) x " On x " X.
Theorem 2.4.3 is a weakened form of G�DEL s Theorem. G�DEL s Theorem says that Theo-
rem 2.4.3 holds already for a 0-sentence ("x)F (x).
1
35
2. The ordinal analysis for PA
36
3. Ordinal analysis of non iterated inductive
definitions
3.1 The theory ID1
We want to axiomatize the theory for positively definable inductive definitions over the natural
numbers. According to Theorem 1.7.7 we can express 1 relations by inductivley defined rela-
1
tions. Therefore we can dispend with set parameters in the theory and we will do so to save some
case distinctions (and also to give examples for some of the phenomena which are characteristic
for impredicative proof theory).
3.1.1 Definition The language L(ID1) comprises the language of NT . For every X positive
formula F (X, x) we introduce a new relation symbol IF whose arity is the length of the tuple x.
The theory ID1 comprises NT (but in the language without set parameters) together with the
defining axioms for the set constants
(ID11)("x)[F (IF , x) x " IF ]
and
(ID12)ClF (G) ("x)[x " IF G(x)],
where
ClF (G) a" ("x)[F (G, x) G(x)]

expresses that the  class x G(x) is closed under the operator �F induced by F (X, x). The
notion F (G, x) stands for the formula obtained from F (X, x) replacing all occurrences t " X
by G(t) and t " X by ŹG(t).
/
The standard interpretation for IF is of course the least fixed point IF as introduced in Definition
1.6.1. The following theorem is left as an exercise.
3.1.2 Theorem
N |= n " IF �! N |=("X)[ClF (X) n " X]
ID1 ("x)[F (IF , x) "! x " IF ]
3.2 The language L"(NT )
We extend the language of L(NT ) to an infinitary language containing infinitely long formulas.
3.2.1 Definition (The language L",�(NT )) We define the language L",�(NT ) as a TAIT
language parallel to Definition 1.3.1. It contains the same non logical symbols. The logical
symbols are augmented by the infinite boolean operations and . The atomic formulas are
unaltered. The language is closed under all first order operations and we have the additional
clause
37
3. Ordinal analysis of non iterated inductive definitions
" If F� | � " I is a infinite sequence of L",�(NT ) formulas containing at most finitely many
free variables then F� and F� are L",�(NT ) formulas.
�"I �"I
Again we are interested in the sentences of L",�(NT ). The set of sentences is denoted by
L"(NT ).
The semantics for L"(NT ) is defined in the obvious way. We get
|= F� :�! N |= F� for all � " I
�"I
and
|= F� :�! N |= F� for some � " I.
�"I
Then it is obvious that we have
" F� "  type
�"I
and
" F� "  type
�"I
and
" CS ( F�) =CS ( F�) = F� | � " I .
�"I �"I
The definition of the validity relation as given in Definition 1.3.10 now carries over to the language
L"(NT ). Observe that we can dipsense with rule (Ax) because we don t have set parameters.
By an easy induction on ą we get
3.2.2 Lemma For any finite set " of L"(NT ) sentences we have
ą
" �! N |= ".
Since we only deal with sentences the completeness of the validity relation is much easier to
show.
3.2.3 Definition For every formula F in L"(NT ) we define its rank rnk(F ) by

rnk(F ) :=sup rnk(G) +1 G " CS (F ) .
By an easy induction on rnk(F ) we obtain
3.2.4 Lemma For F "L"(NT ) we have
rnk(F )
N |= F �! F .
3.3 Inductive definitions and L"(NT )
The stages of an inductive definition over N can be easily expressed in L"(NT ).
38
3.4. The semi formal system for L"(NT )
3.3.1 Definition Let F (X, x) be a formula in L(NT ). By recursion on ą d" �1 we define
t " I<ą :a" F (I<�, t)
F F
�<ą
and dually
t " I<ą :a" ŹF (I<�, t).
/
F F
�<ą
As a shorthand we also use
t " Ią :a" F (I<ą, t)
F F
and
t " Ią :a"ŹF (I<ą, t).
/
F F
It it obvious that we have
ą
N |= t " Ią �! tN " IF (3.1)
F
ą
where IF denotes the stages of the inductive definiton induced by F in the sense of Definition
1.6.1.
For the rest of the lecture we will only regard the fragment of L"(NT ) which is obtained from
the sentences defined in Definition 3.3.1 by closing them under first order operations.
CK
If F (X, x) is an X positive L(NT ) formula, we know by Theorem 1.7.11 |F | d"�1 . Hence
CK
<�1 <�1
CK
IF = IF = IF . Let us use &! as a symbol for either �1 or �1. There is an obvious
embedding of the language L(ID1) into our fragment of L"(NT ).
3.3.2 Lemma If G is an L(ID1) sentence we obtain G" by replacing all occurrences of IF in G
by I<&!. Then
F
N |= G �! N |= G".
3.4 The semi formal system for L"(NT )
By Observation 1.7.10 we obtain an upper bound for ||ID1|| if we determine

1
�ID := sup |n|F F (X, x) is X positive '" ID1 n " IF .

CK
1
Since |n|F ID1 n " IF is a recursivley enumerable set we have �ID <�1 . Of course
we could have allowed set parameters in the language of ID1. Then it makes sense to talk about
pseudo 1 sentences provable in the extended theory ID1ext. One easily proves
1
ID1 t " IF �! ID1ext t " IF �! ID1ext ClF (X) t " X.
By the Boundedness Theorem 1.7.8 we then obtain
1
�ID e"||ID1ext|| 1
1
which confirms our decision not to include set parameters.
First we observe
3.4.1 Lemma We have
ą ą
" , t " I<&! �! " , I<ą
F F
which means
39
3. Ordinal analysis of non iterated inductive definitions
|n|F d" tc(n " I<&!).
F
The proof is a straightforward induction on ą which we omit since a similar property (Lemma
3.5.2) will be needed and proved for the semi formal calculus below.
1
It becomes clear from Lemma 3.4.1 that the computation of an upper bound for �ID can be
done analogously to that of an upper bound for ||NT || 1. Therfore the first step should be the
1
computation of the truth complexities for the axioms of ID1. Here we have even to be carful
in transfering Theorem 2.1.6. The sentence n " IF is an atomic sentence of L(ID1) but not an
atomic sentence of L"(NT ). But observe that because of rnk( t " I<&!) d" &! we obtain by the
F
Tautology Lemma (Lemma 2.3.1)
&!
" , t " I<&!, t " I<&!. (3.2)
/
F F
Thus Theorem 2.1.6 modifies to
m &!+m
3.4.2 Theorem If "(x) holds for a finite set of L(ID1) formulas then "(n) for all
tuples n of numerals.
The truth complexities of the defining axioms for primitive recursive functions and relations are of
course not altered. More caution is again needed for the identity axioms which of course include
the scheme
("x)("y)[x = y x " IF y " IF ].
But here we get
&!+n
("x)("y)[x = y x " I<&! y " I<&!]
F F
for some n<�. By the Induction Lemma (Lemma 2.3.2) we obtain
&!+�+4
G"
for all instances G of the scheme of Mathematical Induction in ID1. It remains to check the truth
complexities for the axioms ID11 and ID12. By Lemma 3.2.4 we obtain
&!+n
ClF (I<&!)
F
since rnk(ClF (I<&!)) = &! + n for some n<�.
F
The same is of course also true for all instances of the axiom ID12.
These observations show that the ordinal analysis for ID1 needs something new. The truth com-
1
plexities for the axioms of ID1 are above &!. The ordinal �ID , however, is an ordinal < &!
(regardless of the interpretation of &!). Since a validation proof for a sentence n " I<&! does not
F
contain &! branchings it is also clear that tc(n " I<&!) < &!. So we need additional conditions
F
which allow us to collapse the ordinal assigned to the infinitary derivations for sentences of the
form n " I<&! into ordinals below &!.
F
But there is still another reason why cut elimination alone cannot solve our problem. We define
the semi formal system for the language L"(NT ) as in Definition 2.3.3. Again we can dispense
with the rule (Ax) because we do not have set parameters. But now we obtain the following
theorem.
3.4.3 Theorem Let � be a finite sets of L"(NT ) sentences. Then
ą ą
� �! � .
�
Proof We prove
ą
ą
�, " and N |= F for all F " " �! � (i)
�
40
3.4. The semi formal system for L"(NT )
by induction on ą. The proof depends heavily on the fact that we only have sentences in L"(NT ).
In the case of a cut we have the premises
ą0
", �, F (ii)
�
and
ą0
", �, ŹF (iii)
�
and either N |= F or N |= ŹF . Using the induction hypothesis on the corresponding premise we
get the claim. The remaining cases are obvious.
It follows from Theorem 3.4.3 that cut elimination cannot be the crucial point in the ordinal anal-
ysis of ID1. The same is of course also true for stronger theories. The hallmark for impredicative
proof theory is not longer cut elimination but collapsing. Since ordinals above &! are in general
not collapsable into ordinal below &! we have to control the ordinals assigned to the derivations.
We follow the concept of operator controlled derivations which was introduced in [3] as a sim-
plification of the method of local predicativity introduced in [10]. However, we will not copy
BUCHHOLZ proof but introduce a variant which even sharper pinpoints the role of collapsing.
3.4.4 Definition A Skolem hull operator is a function H which maps sets of ordinals on sets of
ordinals satisfying the conditions
" For all X ą" On it is X ą"H(X)
" If Y ą"H(X) then H(Y ) ą"H(X).
3.4.5 Definition For a sentence G in our fragment of L"(NT ) we define

par (G) := ą I<ą occurs in G .
F
For a finite set " of sentences of our fragment of L"(NT ) we define
par (") := par (F ).
F ""
ą
3.4.6 Definition For a Skolem hull operator we define the relation H " by the clauses ( ),
�
( ) and (cut) of Definition 2.3.3 with the additional conditions that we always have
" ą "H(par ("))
and for an inference
ą
ąi
H "i �!H "
� �
different from ( ) also
" par ("i) ą"H(par (")).
We define
H1 ą"H2 :�! ("X)ą"On[H1(X) ą"H2(X)].
A Skolem hull operator H is Cantorian closed iff
" {0, &!} ą"H("),
and it satisfies
41
3. Ordinal analysis of non iterated inductive definitions
" ą "H(") �! SC (ą) ą"H(").
For a set X ą" On andanoperator H let
" H[X] :=ś. H(X *" ś).
ą
When writing H " we tacitly assume that H is a Cantorian closed Skolem hull operator. The
�
Structural Lemma of Section 2.3 extents to
ą �
3.4.7 Lemma If H1 ą"H2, ą d" �, � d" �, " ą" �, � "H2(par (�)) and H1 � " then H2 � �.
The remaining facts of Section 2.3 carry over to controlled semi formal derivations.
ą ą
3.4.8 Lemma (Inversion Lemma) If F "  type and H ", F then H[par (F )] ", G for
� �
all G " CS (F ).
ą ą
3.4.9 Lemma ((" Exportation) If H ", F1 (" � � � (" Fn then H ", F1, . . . , Fn.
� �
ą ą
3.4.10 Lemma If F " D(N) and H ", ŹF then H ".
� �
3.4.11 Lemma (Reduction Lemma) Let � = rnk(F ) and par (F ) ą" H(par (", �)) for F "
ą � ą+�
 type. If H ", F and H �, ŹF then H ", �.
� � �
This is the only place where the proof needs some extra care. First it becomes simpler than
that of Lemma 2.3.9 since we do not have set parameters. But we need to put extra care on the
controlling operator. Let us redo the critical case that ŹF is the main formula of the last inference
� �0
in H �, ŹF . Then we have the premise H ", ŹF, ŹG for some G " CS (F ) with
� �
par (", F, G) ą"H(par (", F)) (i)
ą+�0
and obtain H ", �, ŹG by the induction hypothesis. By inversion, the Structural Lemma
�
ą+�0
and the hypothesis par (F ) ą" H(par (", �)) we also have H ", �, G. It is rnk(G) < �
�
but toapplya cut we alsohave tocheck
par (", �, G) ą"H(par (", �)). (ii)
But this is secured by (i) and the hypothesis par(F ) ą"H(par (", �)).
3.4.12 Theorem (Cut elimination for controlled derivations) Let H be a Cantorian closed Skolem
hull operator. Then
ą 2ą
(i) H " �! H "
�
�+1
and
��(ą)
ą
(ii) H " and � "H(par (")) �! H ".
�+�� �
The easy adaption of the proofs given for Lemma 2.3.10 and Lemma 2.3.11 are left as an exercise.
Notice that for the proof of (ii) it is essential the H is Cantorian closed.
42
3.5. Controlling operators for ID1
3.5 Controlling operators for ID1
We introduce a family of operators Bą which suffice to interpret the sentences t " IF provable in
ID1 as operator controlled derivations of lengths < &!.
3.5.1 Definition For X ą" On let Bą(X) be the least set of ordinals containing X *"{0, &!} which
is closed under the functions �, � . � + � , �� . ��(�) and the collapsing function � ą where

�(ą) :=min � � "Bą(") .
/
We need a few facts about the operators Bą. Here it is comfortable to think on &! as the first
CK
uncountable cardinal. Interpreting &! as �1 makes the following considerations much harder.
First we observe
|Bą(X)| =max{|X|, �} (3.3)
which implies
�(ą) < &! (3.4)
showing that � is in fact collapsing. Clearly the operators are Cantorian closed and cumulative,
i.e.
ą d" � �! Bą ą"B� and �(ą) d" �(�). (3.5)
Since for ą "B�(") )" � we get �(ą) "B�(") we have
ą "B�(") )" � �! �(ą) <�(�). (3.6)
From (3.6) we get
Bą(") )" &!=�(ą). (3.7)
The  �"  direction follows from the definition of �(ą) and (3.4). For the opposite inclusion
observe that �(ą) is strongly critial and show
� "Bą(") )" &! �! � <�(ą)
by induction on the definition of � "Bą("). In case that � = �(�) we have � "Bą(") )" ą which
by (3.6) implies � = �(�) <�(ą).
There are two properties of controlled derivations which are crucial.
ą ą
3.5.2 Lemma (Boundedness) If H "( t " I<�) for � " H(") then H "( t " I<ł) holds for
� F � F
all ł such that ą d" ł d" � and ą "H(par ("( t " I<ł))).
F
Proof We induct on ą. In the cases that t " I<� is not the main formula of the last inference
F
ą
ąą
H "ą( t " I<�) �! H "( t " I<�) (i)
� F � F
we have ąą " H(par ("ą( t " I<�))) ą" H(par("ą( t " I<ł))) because � " H(par("( t "
F F
I<ł))). Hence
F
ąą
H "ą( t " I<ł) (ii)
� F
by induction hypothesis and
ą
H "( t " I<ł) (iii)
� F
from (ii) by the same inference.
43
3. Ordinal analysis of non iterated inductive definitions
If t " I<� is the main formula we are in the case of an ( ) inference with the premise
F
ą0
H "0, t " I<�, t " I� (iv)
� F F
for some � <�. Applying the induction hypothesis twice we obtain
ą0
0
H "0, t " I<ł, t " Ią . (v)
� F F
Since ą0 " H(par ("0, t " I<�, t " I� )) ą"H(par ("0, I<�)) ą" H(par ("0, I<ł)) and ą0 <
F F F F
ą d" ł we can apply an inference ( ) to obtain
ą
H "0, t " I<ł.
� F
&!
3.5.3 Definition We say that a sentence in our fragment of L"(NT ) is in  type if it does not
contain subformulas of the shape t " I<&!.
/
F
&!
3.5.4 Lemma (Collapsing Lemma) Let " ą"  type such that par(") *"{ą} ą" Bą+1(")
� �(ą+��)
and Bą+1 &! ŹCl (I<&!), . . . , ŹCl (I<&!), ". Then Bą+�� ".
F1 F1 Fk Fk
+1
&!
The proof is by induction on ą. The key property is
ą, � "Bą+1(") and ą + �� <ł �! �(ą + ��) <�(ł) (i)
which is obvious by (3.6) since we have ą + �� "Bą+1(") )" ł ą"Bł(") )" ł. Other observations
are
Bą+1(par (")) = Bą+1(") (ii)
because par (") ą"Bą+1(") and
ą, � "Bą+1(") �! ą + �� "Bą+�� (") and �(ą + ��) "Bą+�� (") (iii)
+1 +1
which is clear by (3.5) and definition.
Let us first assume that the main part of the last inference belongs to a sentence in ". Observe
that par(ŹCl (I<&!), . . . , ŹClF (I<&!)) = {&!}. So we only have to bother about the parameters
F1 F1
k Fk
of ". We run through the cases. If the last inference
�0 �
Bą+1 &! ŹClF (I<&!), . . . , ŹClF (I<&!), ", G �! Bą+1 &! ŹCl (I<&!), . . . , ŹCl (I<&!), " (iv)
F1 F1 Fk Fk
1 F1 k Fk
is according to ( ) we have par (", G) ą"Bą+1(par (")) ą"Bą+1(") and obtain by the induc-
tion hypothesis
�(ą+��0 )
Bą+��0 ", G. (v)
+1
&!
0
From ą, �0 "Bą+1(") we obtain �(ą + �� ) <�(ą + �) by (i) and from ą, � "Bą+1(") also
�(ą + ��) "Bą+�� ("). Since also par (", G) ą"Bą+1(") ą"Bą+�� (") we obtain
+1 +1
�(ą+��)
Bą+�� " (vi)
+1
&!
from (v) by an inference ( ).
Assume that the last inference is a cut
�ł
�0
żł
Bą+1 &! ŹClF (I<&!), . . . , ŹClF (I<&!), ", F
�
1 F1 k Fk
�!Bą+1 &! ŹCl (I<&!), . . . , ŹCl (I<&!), ". (vii)
F1 F1 Fk Fk
�0
�ł
Bą+1 &! ŹClF (I<&!), . . . , ŹClF (I<&!)", ŹF
1 k Fk
F1
44
3.5. Controlling operators for ID1
&!
Because rnk(F ) < &! we have that both F and ŹF are in  type. Since par(", F) ą"Bą+1(")
we can apply the induction hypothesis to the premises and obtain
�(ą+��0 ) �(ą+��0 )
Bą+��0 ", F and Bą+��0 ", ŹF. (viii)
+1 +1
&! &!
0
As in the previous case we obtain �(ą + �� ) <�(ą + ��) and �(ą + ��) "Bą+�� (") and
+1
infer
�(ą+�� )
Bą+�� "
+1
&!
from (viii) by (cut).
The real interesting case is that of an inference
�ł
żł
F "  type )" "
�
�! Bą+1 &! " (ix)
�G
Bą+1 &! ŹClF (I<&!), . . . , ŹClF (I<&!), ", G for all G " CS (F )�ł
1 k Fk
F1
&!
according to ( ). Since " ą"  type there is a  " &! )"Bą+1(") such that par (G) ą"
. According to (3.7) &! )"Bą+1(") is a segment which entails par (G) ą" Bą+1("). Hence
par (", G) ą"Bą+1("). By the induction hypothesis we thus get
�(ą+�G)
Bą+� +1 &! ", G for all G " CS (F ). (x)
G
Because ą, �G " Bą+1(par (", G)) = Bą+1(") we get �(ą + �G) < �(ą + ��) and from
ą, � "Bą+1(") also �(ą + ��) "Bą+�� . Therefore we obtain
+1
�(ą+�� )
Bą+�� "
+1
&!
from (x) by an inference ( ).
Now assume that the main formula ot the last inference is
ŹCl (I<&!) a" ("x)[Fi(I<&!, x) '" x " I<&!]. (xi)
/
Fi Fi
Fi Fi
Then we have the premise
�0
Bą+1 &! ŹCl (I<&!), . . . , ŹCl (I<&!), Fi(I<&!, t) '" t " I<&!, " (xii)
/
F1 F1 Fk Fk Fi
Fi
with �0 "Bą+1(par (") *"{&!}) =Bą+1("). By inversion we obtain from (xii)
�0
Bą+1 &! ŹCl (I<&!), . . . , ŹCl (I<&!), Fi(I<&!, t), " (xiii)
F1 F1 Fk Fk Fi
and
�0
Bą+1 &! ŹCl (I<&!), . . . , ŹCl (I<&!), t " I<&!, ". (xiv)
/
F1 F1 Fk Fk Fi
Applying the induction hypothesis to (xiii) and then using boundedness gives
�0
�(ą+��0 )
Bą+��0 Fi(I<�(ą+� ), t), ", (xv)
+1
Fi
&!
i.e.
�0
�(ą+��0 )
Bą+��0 t " I�(ą+� ), ". (xvi)
+1
Fi
&!
From (xiv) we obtain by inversion
�0
�0
Bą+1 &! ŹCl (I<&!), . . . , ŹCl (I<&!), t " I�(ą+� ), " (xvii)
/
F1 F1 Fk Fk Fi
which entails
45
3. Ordinal analysis of non iterated inductive definitions
�0
�0
Bą+��0 ŹCl (I<&!), . . . , ŹClF (I<&!), t " I�(ą+� ), ". (xviii)
/
F1 F1
+1 k Fk Fi
&!
0
Since �(ą + �� ) "Bą+��0 (") the induction hypothesis applies to (xviii) and we obtain
+1
�0
�(ą+��0 +��0 )
Bą+��0 t " I�(ą+� ), ". (xix)
/
+��0 +1
Fi
&!
Now we obtain
�(ą+��)
Bą+�� "
+1
&!
from (xvi) and (xix) by the Structural Lemma and (cut).
3.5.5 Remark Although we will not need it for the ordinal analysis of ID1 we want to remark
that the Collapsing Lemma may be strengthened to
� �(ą+��)
Bą+1 &!+1 ŹCl (I<&!), . . . , ŹClF (I<&!), " �! Bą+�� ".
F1 F1
+1
k Fk
�(ą+��)
For k =0 it can be modified to
� �(ą+�)
Bą+1 &! " �! Bą+�+1 �(ą) "
Proof We have to do three things. First we observe that in the case of a cut of rank < &! we
have par(F ) ą"Bą(") )" &!=�(ą) <�(ą + ��). Since rnk(F ) < max par(F ) +� we obtain
rnk(F ) <�(ą + �). If the cut rank is &!+1 we have the additional case of a cut of rank &!. Then
the cut sentence is t " I<&! and we have the premises
F
�0
Bą+1 &!+1 ŹCl (I<&!), . . . , ŹClF (I<&!), ", t " I<&! (i)
F1 F1
k Fk F
and
�0
Bą+1 &!+1 ŹCl (I<&!), . . . , ŹClF (I<&!), ", t " I<&!. (ii)
/
F1 F1
k Fk F
But then we may apply the induction hypothesis to (i) and then proceed as in the last case in the
�0
proof of the Collapsing Lemma. The resulting cut sentence is t " I<�(ą+� ) which shows that
F
the cut sentence has rank <�(ą + ��).
Finally we observe that only in this case we needed the fact that �� is additively indecomposable.
This case is not needed if k =0 and we may replace ą + �� by ą + �.
3.6 The upper bound
1
In order to get an upper bound for �ID Theorem 3.4.2 is not longer sufficient. What we need is
m &!+m
3.6.1 Theorem If "(x) holds for a finite set of L(ID1) formulas then H "(n) for all
0
tuples n of numerals and all Cantorian closed Skolem hull operators H.
The key here is
3.6.2 Lemma (Controlled Tautology) For every L"(NT )-sentence and Cantorian closed Skolem
2�rnk(F )
hull operator H we have H ", ŹF, F .
0
The proof by induction on rnk(F ) is easy. First observe that 2 � rnk(F ) "H(par (F )) for every
Cantorian closed Skolem hull operator because rnk(F ) = max par (F ) +n for some n < �.
Assume without loss of generality that F "  type. By induction hypothesis we have
46
3.6. The upper bound
2�rnk(G)
H ", ŹF, F, G, ŹG (i)
0
for all G " CS (F ). Since par (", ŹF, F, G, ŹG) ą"H(par(", ŹF, F, G)) we obtain from (i)
2�rnk(G)+1
H ", ŹF, F, G, (ii)
0
for all G " CS (F ) by an inference ( ). From (ii) and 2 � rnk(G) +1 < 2 � (rnk(G) +1) d"
2 � rnk(F ), however, we immediately get
2�rnk(F )
H ", ŹF, F
0
by an inference ( ).
Now it is an easy exercise to prove Theorem 3.6.1 by induction on m using Lemma 3.6.2 in case
m
that ", t " IF , Ź t " IF holds by (AxL).
It is obvious that all defining axioms and also all identity axioms are controlled derivable with a
derivation depth below �. Ruminating the proof of the Induction Lemma (Lemma 2.3.2) shows
that this proof is controlled by any Cantorian closed Skolem hull operator. Summing up we get
&!+�+4
"
H F (3.8)
0
for every axiom G of NT in the language L(ID1) where H may be an aribtrary Cantorian closed
Skolem hull operator.
So it remains to check the schemes ID11 and ID12. By the Collapsing Lemma (Lemma 3.5.4)
we have only to deal with ID12.
3.6.3 Lemma (Generalized Induction) Let F (X, x) be an X positive NT formula. Then
2�rnk(G)+��(ą+1)
H ŹClF (G), n " Ią , G(n)
/
F
0
holds for any sentence G(n) in our fragment of L"(NT ) and for any Cantorian closed Skolem
hull operator H.
From the Generalized Induction Lemma we obtain
&!�2+3
H ŹClF (G), ("x)[x " I<&! G(x)] (3.9)
F
0
which is the translation of the scheme ID12.
The proof of Lemma 3.6.3 still needs a preparing lemma.
3.6.4 Lemma (Monotonicity Lemma) Let F (X, x) be an X positive L(NT ) formula. Then
ą ą+2�rnk(F )
H ", ŹG(n), H(n) for all n �! H ", ŹF (G, n), F(H, n)
� �
for all n.
Proof Induction on rnk(F ). In the case that X does not occur in F (X, x) we have
2�rnk(F )
H ", ŹF, F
0
by the Tautology Lemma (Lemma 3.6.2). In the case that F a" (x " X) we obtain the claim from
ą
the hypothesis H ", ŹG(n), H(n). The remaining cases are as in the proof of the controlled
�
Tautology Lemma.
Proof of the Generalized Induction Lemma. We have
2�rnk(G)+��ą
H ŹClF (G), n " I<ą, G(n) (i)
/
F
0
47
3. Ordinal analysis of non iterated inductive definitions
by an inference ( ) with empty premises if ą = 0 or by induction hypothesis. From (i) we
obtain
2�rnk(G)+��ą+2�rnk(F )
/
H ŹCl (G), n " Ią , F(G, n) (ii)
F
F
0
by the Monotonicity Lemma. By controlled Tautology we have
2�rnk(G)
H ŹClF (G), n " Ią , ŹG(n), G(n). (iii)
/
F
0
From (ii) and (iii) we get
2�rnk(G)+��ą+(2�rnk(F ))+1
H ŹCl (G), n " Ią , F(G, n) '"ŹG(n), G(n) (iv)
/
F
F
0
by an inference ( ). From (iv) we finally obtain
2�rnk(G)+��ą+2�rnk(F )+2
H ŹCl (G), n " Ią , G(n)
/
F
F
0
by an inference ( ). Since 2 � rnk(G) +� � ą +2� rnk(F ) +2< 2 � rnk(G) +� � (ą +1) we
are done.
3.6.5 Theorem If ID1 F (x) then there are finitely many axioms ClF (I<&!), . . . , ClF (I<&!)
1 F1 k Fk
and an n<�such that
&!�2+�
H ŹClF (I<&!), . . . , ŹClF (I<&!), F(m)
1 F1 k Fk
&!+n
holds for any tuple m of the length of x and for any Cantorian closed Skolem hull operator.
Proof If ID1 F (x) then there are finitely many axioms A1, . . . , Ar and a natural number p
p
such that ŹA1, . . . , ŹAr, F(x). By Theorem 3.6.1 this implies
&!+p
"
H ŹA", . . . , ŹA", F (m) (i)
1 r
0
for any Cantorian closed Skolem hull operator H. From (i), (3.8) and (3.9) we obtain the claim
by some cuts.
1
3.6.6 Theorem (The Upper Bound for ID1) It is �ID d" �(�&!+1).
Proof If ID1 m " IF we obtain by Theorem 3.6.5
&!�2+�
B0 &!+n ŹClF (I<&!), . . . , ŹCl (I<&!), m " I<&!. (i)
Fk Fk F
1 F1
By Theorem 3.4.12 we obtain an ą<�&!+1 such that
ą
B0 &! ŹClF (I<&!), . . . , ŹClF (I<&!), m " I<&!. (ii)
1 F1 k Fk F
From (ii) and the Collapsing Lemma (Lemma 3.5.4) it follows
�(�ą)
B�ą m " I<&!
+1
F
&!
which by Theorem 3.4.3 implies tc(m " I<&!) d" �(�ą) <�(�&!+1). By Lemma 3.4.1 the claim
F
follows.
48
3.7. The lower bound
3.7 The lower bound
3.7.1 Coding ordinals in L(NT )
It follows from the previous sections that B� (") is the set of ordinals which turned out to be
&!+1
1
relevant in the computation of an upper bound for �ID . To prove that �(�&!+1) is the exact bound
it suffices to prove n " Accą(z") for some arithmetical definable relation z" and all ą<�(�&!+1).
If we succeed in showing that for a primitive recursive relation z" we have by Observation 1.7.10
that ||ID1|| = �(�&!+1).
Since we cannot talk about ordinals in L(ID1) we need codes for the ordinals in B� ("). The
&!+1
only parameters occurring on B� (") are 0 and &!. Therefore every ordinal in B� (") pos-
&!+1 &!+1
sesses a term notation which is built up from 0,&! by the functions +, � and �. This term notation,
however, is not unique. In order to show that the set of term notations together with the induced
< relation on the terms is primitive recursive we need a unique term notation. This forces us to
inspect the set Bą(") more closely.
We define
ą =NF �(�) :�! ą = �(�) '" � "B�(").
Then
ą =NF �(�1) '" ą =NF �(�2) �! �1 = �2 (3.10)
since �1 <�2 would imply �(�1) <�(�2) by (3.6) because �1 " B� (") ą"B� ("). Now we
1 2
define a set of ordinal terms T by the clauses
(T0) {0, &!} ą"T
(T1) ą " S '" SC (ą) ą" T �! ą " T
/
(T2) � " T '" ą =NF �(�) �! ą " T .
We want to prove
T = B&!�(") (3.11)

for &!� := min ą " SC &! <ą .
The inclusion ą" in (3.11) is obvious. Troublesome is the converse inclusion. The idea is of course
to prove
� "B&!�(") �! � " T (3.12)
by induction on the definition of � " B&!�("). We will therefore redefine the sets Bą(") more
carefully by the following clauses.
n
(B0) {0, &!} ą"Bą
n-1 n
(B1) � " SC '" SC (�) ą" Bą �! � " Bą
/
n-1 n
(B2) � " Bą )" ą �! �(�) " Bą

n
(B3) Bą := Bą '" �(ą) :=min � � " Bą .
/
n"�
It is easy to check that Bą = Bą(") for all ą d" &!� which justifies the use of the same symbol �

/ /
for the functions min � � "Bą(") and min � � " Bą . So (3.12) can be shown by proving
n
� " Bą �! � " T (3.13)
for all ą<&!� by induction on n. What is still troublesome in pursuing this strategy is case (B2).
In this case we don t know if �(�) is in normal form, i.e. if � " B�. Therefore we show first
49
3. Ordinal analysis of non iterated inductive definitions

3.7.1 Lemma For every ordinal ą<&!� the ordinal ąnf := min � ą d" � " Bą exists and it
is �(ą) =NF �(ąnf).
Proof Since &!� = supn"� �n (0) and �n (0) " Bą for any ą it follows that ąnf exists. By
&! &!
definition [ą, ąnf) )" Bą = " which implies Bą = Bą and thus also �(ą) = �(ąnf). Since
nf
ąnf " Bą = Bą we have �(ą) =NF �(ąnf).
nf
Our troubles are solved as soon as we can show
n n
� " Bą �! �nf " Bą . (3.14)
n-1 n-1
Then we may argue in case (B2) that for � " Bą we also have �nf " Bą and thus �nf " T
which entails �(�) =NF �(�nf) " T .
We obtain (3.14) as a special case of the following lemma whose proof is admittedly tedious.
Also we cannot learn much from its proof. Therefore one commonly includes the normal form
condition into clause (B2) which then becomes
n-1 n
(B2) � " Bą )" ą '" � " B� �! �(�) " Bą .
The proof of (3.13) then becomes trivial.

n n
3.7.2 Lemma Let �(ą) := min � ą d" � " B� . Then ą " B� implies �(ą) " B� for all
ą<&!�.
Proof We show the lemma by induction on n. First observe that by the miminality of �(ą) we
get
ą " H �! �(ą) " H and ą " SC �! �(ą) " SC . (i)
The lemma is trivial if ą " B�. Then �(ą) =ą. Therefore we assume
ą " B�. (ii)
/
n
Then ą <�(ą) and for ą <&! we get by (3.7) �(ą) =&! " B� for any n. Therefore we may
also assume
&! d" ą. (iii)
We have
n n-1
� " SC '" � " B� �! SC (�) ą" B� . (iv)
/
Since (&!, &!�) )" SC = " we obtain by induction hypothesis

n-1
�(SC ą) := �(�) � " SC (ą) ą" B� )" B�. (v)
We are done if we can prove
n-1
SC (�(ą)) ą" B� )" B�. (vi)
We prove (vi) by induction on the number of ordinals in SC (ą). First assume ą =NF ą1 + � � � +
ąk. Since ąj d" �(ąj) " H we obtain ą d" �(ą1)+� � � + �(ąk) and because �(ą1)+� � � �(ąn) "

B� even ą<�(ą1) +� � � �(ąk). Let i := min j d" k ąj <�(ąj) . We claim
�(ą) =ą1 + � � � + ąi-1 + �(ąi) =�(ą1) +� � � + �(ąi-1) +�(ąi). (vii)
From (vii) we obtain (vi) by induction hypothesis. Let � := ą1 + � � � + ąi-1. We have ą <
� + �(ąi). Hence �(ą) d" � + �(ąi). If we assume �(ą) <� + �(ąi) there is an � " B� such that
�+ąi d" ą<� <�+�(ąi). But then we obtain an �1 such that � = �+�1 and ąi <�1 <�(ąi).
But � " B� entails �1 " B� which contradicts the definition of �(ą1).
50
3.7. The lower bound
Next assume ą =NF �ą (ą2). If �(ą1) =ą1 we immediately obtain �(�ą (ą2)) = �ą (�(ą2)) =
1 1 1
��(ą )(�(ą2)) which entails (vi) byinduction hypothesis. If ą1 <�(ą1) and ą d" �(ą2) we ob-
1
tain �(ą) d" �(ą2) d" �(ą) and (vi) follows by induction hypothesis. So assume ą1 <�(ą1) and
�(ą2) <ą. Let

ą3 := min � ą d" ��(ą )(�) . (viii)
1
We claim
n-1
ą3 " B� )" B�. (ix)
From (ix) we get �(ą) d" ��(ą )(ą3). If we assume �(ą) <��(ą )(ą3) we have ą = �ą (ą2) <
1 1 1
��(ą )(ą3). Since �(ą) " H we obtain �(ą) =NF �� (�2). The assumption �1 = �(ą1) yields
1 1
ą < �(ą) = ��(ą )(�2) < ��(ą )(ą3) and thus �2 < ą3 conctradicting the minimality of ą3.
1 1
Assuming �(ą1) <�1 yields �(ą) <ą3 and ą <�(ą) =��(ą )(�(ą)) again contradicting the
1
minimality of ą3. So it remains �1 <�(ą1). But since �1 " Bą this implies �1 <ą1 which in
turn entails ą<�2 " B� )" �(ą) contradiction the definition of �(ą). Therefore we have
�(ą) =��(ą )(ą3) (x)
1
and obtain (vi) from (x) by induction hypothesis and (ix).
It remains to prove (ix). We are done if ą3 = 0. If we assume ą3 " Lim we get ą =NF
�ą (ą2) =��(ą )(ą3) by the continuity of ��(ą ). Because ą1 <�(ą1) we then obtain ą2 = ą
1 1 1
contradicting ą2 d" �(ą2) <ą. It remains the case that ą3 = � +1. Then ��(ą )(�) <ą=NF
1
�ą (ą2) < ��(ą )(� +1). Because of ą1 < �(ą1) this implies ��(ą )(�) d" ą2 d" �(ą2) <
1 1 1
ą = ��(ą )(� +1). But ą2 = ��(ą )(�) is excluded because otherwise we get �ą (ą2) =ą2 <
1 1 1
n-1
�ą (ą2). Since �(ą2) " B� )" B� we have shown
1
n-1
B� )" B� )" (��(ą )(�), ��(ą )(� +1)) = ". (xi)

1 1
To finish the proof we show that in general we have
n n
B� )" (��(�), ��(� +1)) = " �! � +1" B� . (3.15)

n-1
From (xi) and (3.15) we then obtain ą3 " B� )" B� , i.e. (ix).
To prove (3.15) we first show
ł " [��(�), ��(� +1)) �! SC (�) ą" SC (ł) (xii)
by induction on the number of elements in SC (ł).
If ł =NF ł1 +� � �+łk we have ł1 " [��(�), ��(� +1)) and obtain SC (�) ą" SC (ł1) ą" SC (ł).
If ł =NF �ł (ł2) then ł1 d" � because � <ł1 entails ł d" � +1 <��(�). If � = ł1 then � = ł2
1
and SC (�) =SC (ł2) ą" SC (ł). If ł1 <� then ��(�) d" ł2 <ł <��(� +1) and we obtain
SC (�) ą" SC (ł2) ą" SC (ł) by induction hypothesis. If finally ł " SC then ł = ��(�) =� and
the claim is obvious.
n
We prove (3.15) by induction on n. Let � " B� )" (��(�), ��(� +1)). Then � " SC and we
/
n-1 n-1 n-1
have SC (�) ą" B� . By (xii) we get SC (�) ą" SC (�) ą" B� . Since 0 " B� we also have
n-1
n
SC (� +1) ą" B� and thus obtain � +1" B� .
Having established B&!�(") =B&!� = T we want to develop a primitive recursive notation system
for the ordinals in T . What is still annoying is the normal form condition in clause (T2). In order
to define a set On of notions for ordinals in T together with a < relation in On by simultaneous
course of values recursion we should try to replace the condition � " B� in ą =NF �(�) by a
condition which refers only to proper subterms of �. We observe that we have
51
3. Ordinal analysis of non iterated inductive definitions
� " B� �! � =0 (" � =&!("
(� " SC '" SC (�) ą" B�) (" (3.16)
/
(� = �(�) '" � " B� )" �).
From (3.16) we read off the following definition.
3.7.3 Definition Let
ńł
" if � =0 or � =&!
�ł

/
K (�) := K (�) � " SC (�) if � " SC
ół
{�}*"K (�) if � = �(�).
From (3.16) and Definition 3.7.3 we immediately get
3.7.4 Lemma It is � " B� iff K (�) ą" �.
3.7.5 Corollary We have ą =NF �(�) iff ą = �(�) and K (�) ą" �.
3.7.6 Definition We use the facts about ordinals in T to define sets SC ą" H ą" On ą" N
of ordinal notations together with a finite set K(a) ą" On of subterms of a " On, relations
z"ą" On � On and a"ą" On � On and an evaluation function | |O: On - T by the following
clauses.
Definition of SC, H and On.
" 0 "On, 1 "SC, | 0 |O := 0 and | 1 |O := �1
" If a1, . . . , an " Hand a1 � � � an then 1, a1, . . . , an " On and | 1, a1, . . . , an |O :=
|a1|O + � � � + |an|O
" If a, b " On then 2, a, b "H and | 2, a, b |O = �|a| (|b|O)
O
" If a " On and b z" a for all b " K(a) then 3, a "SC and | 3, a |O := �(|a|O)
Definition of K(a).
" K( 0 ) =K( 1 ) ="
" K( 1, a1, . . . , an ) =K(a1) *"� � � *"K(an)
" If b z" 2, a, b then K( 2, a, b ) =K(a) *" K(b)
" K( 3, a ) ={a}*"K(a)
Let a, b " On. Then a z" b iff one of the following conditions is satisfied.
" a = 0 and b = 0

" a = 1, a1, . . . , am , b = 1, b1, . . . , bn and ("i ("j d" m)[aj a" bj] '" m" a = 1, a1, . . . , an , b " H and a1 z" b
" a " H, b = 1, b1, . . . , bn and a b1
" a = 2, a1, a2 , b = 2, b1, b2 and one of the following conditions is satisfied
a1 z" b1 and a2 z" b
a1 = b1 and a2 z" b2
b1 z" a1 and a z" b2
52
3.7. The lower bound
" a = 2, a1, a2 , a2 z" a, b " SC and a1, a2 z" b
" a " SC, b = 2, b1, b2 , b2 z" b and a b1 or a b2
" a = 3, a1 , b = 3, b1 and a1 z" b1
" a = 3, a1 and b = 1
For a, b " On we define a a" b if one of the following conditions is satisfied
" (a)0 =2 and (b)0 =2 and a = b

" a " SC, b1 z" a and b = 2, b1, a
" b " SC, a1 z" b and a = 2, a1, b
" a = 2, a1, a2 , b = 2, b1, b2 and one of the following conditions is satisfied
a1 z" b1 and a2 a" b
a1 = b2 and a2 a" b2
b1 z" a1 and a a" b2.
" The relation a" is transitive, reflexive and symmetrical.
Collecting all the known facts about T and observing that On, SC, H, K (a), z" and a" are defined
by simultaneous course of values recursion we obtain the following theorem.
3.7.7 Theorem The sets On, H and SC as well as the relations z" and a" are primitive recursive.
The map | |O: On - T is onto such that a z" b iff |a|O < |b|O and a a" b iff |a|O = |b|O.
CK
3.7.8 Corollary �(�&!+1) <�1 .
3.7.2 The well ordering proof
In view of Theorem 3.7.7 we may talk about the ordinals in B&!�(") in L(NT ) and thus also in
L(ID1). For the sake of better readability we will, however, not use the codes but identify ordinals
in B&!�(") and their codes. We will denote (codes of ) ordinals by lower case greek letters and
write ą<� instead of ą z" �. We use the abbreviations introduced in Section 2.4.
The aim of this section is to show that there is a primitive recursiv relation <0 such that for every
ą<�(�&!+1) we get ID1 ą " Acc(<0). The strategy of the proof will be the following.
" We first define a relation <1 which is not longer arithmetical definable but needs a fixed point
in its definition such that TI1(&!, X) holds trivially and then use the well ordering proof of
Section 2.4 to obtain TI1(ą, X) porvable in ID1ext for all ą<1 �&!+1.
" Then we use a condensing argument to show that TI1(ą, X) implies �(ą) " Acc(<0).
3.7.9 Definition For ordinals ą, � we define
" ą<0 � :�! ą<� <&!.
By � ą"0 X we denote the formula ("�<0 �)[� " X].
Let Acc be the fixed point of the operator induced by � ą"0 X, i.e. Acc a" Acc(<0).
For ą, � " On we define
" ą<1 � :�! ą<� '" SC (ą) )" &! ą" Acc.
� ą"1 X stands for ("�<1 �)[� " X].
53
3. Ordinal analysis of non iterated inductive definitions
Let
" Progi(F ) :a" ("� " field(" TIi(ą, F ) :a" ą " field(Observe that by the axioms of ID1 and Theorem 3.1.2 we have
ID1 ą " Acc "! ą<&! '" ą ą" Acc (3.17)
ID1 Prog0(Acc) (3.18)
ID1 Prog0(F ) ("�)[� " Acc F (�)] (3.19)
3.7.10 Lemma ID1 Acc ą" &!.

Proof Since Prog0(field(<0)) holds trivially we get Acc ą" field(<0) = ą ą<&! by
(3.19).
3.7.11 Lemma Let Prog(F ) :a" ("ą)[("� <ą)F (�) F (ą)]. Then ID1 Prog(F )
Prog0(F ) and thus also ID1 Prog(F ) ("� " Acc)F (�).
Proof ("�<0 ą)F (�) implies ("� <ą)F (�) for ą <&!. Together with Prog(F ) we therefore
get F (ą), i.e. we have Prog0(F ). Together with (3.19) we obtain the second claim, too,
3.7.12 Lemma (ID1) The class Acc is closed under ordinal addition.

Proof Let Acc+ := � ("� " Acc)[� + � " Acc] . We claim
Prog0(Acc+). (i)
To prove (i) we have the hypothesis
ą<&! '" ("� <ą)[� " Acc+] (ii)
andhave toshową " Acc+ i.e.
("� " Acc)[� + ą " Acc]. (iii)
By (3.17) it suffices to have
� + ą ą" Acc (iv)
to get (iii). Let � <�+ą. If � <� then we get � " Acc from � " Acc by (3.17). If � d" � <� +ą
there is a � <ąsuch that � = � + �. Then we obtain � + � " Acc by (ii).
From (i) we obtain
("� " Acc)[� " Acc+] (v)
by (3.19) which means
("� " Acc)("� " Acc)[� + � " Acc].
3.7.13 Lemma ID1 Prog1(F ) Prog0(F ).
Proof We have the premises Prog1(F ), ą <&! and ("�<0 ą)F (�) and have to show F (ą). If
� <1 ą we get � <0 ą by ą<&! and thus F (�) by ("�<0 ą)F (�). Hence ("�<1 ą)F (�) which
entails F (ą) by Prog1(F ).
54
3.7. The lower bound
3.7.14 Lemma (ID1) The class Acc is closed under �, � . ��(�).

Let M := ą SC (ą) )" &! ą" Acc and define

Acc� := ą ("� " Acc)[� <�ą(�) �ą(�) " Acc] (" ą " M (" &! d" ą . (i)
/
We claim
Prog1(Acc�). (ii)
To prove (ii) we have the hypothesis
("�<1 ą)[� " Acc�] (iii)
and have to show
ą " Acc�. (iv)
For ą " M or &! d" ą (iii) is obvious. Therefore assume
/
ą " M )" &!. (v)
we have to show
("� " Acc)[� <�ą(�) �ą(�) " Acc]. (vi)
According to Lemma 3.7.11 we may assume that we have
("�<�)[� <�ą(�) �ą(�) " Acc] (vii)
and have to show
�ą(�) " Acc (viii)
for which by (3.17) ist suffices to prove
� <�ą(�) � " Acc. (ix)
We show (ix) by Mathematical Induction on the length of the term notation of �. If � =NF
�1 + � � � + �n we have �i " Acc by induction hypothesis and obtain � " Acc by Lemma 3.7.12.
If � " SC then we have � d" ą or � d" �. If � d" � we get � " Acc from � " Acc. If � d" ą we
have � d" � for some � " SC (ą). Since ą " M we have � " Acc and thence also � " Acc.
Now assume � " H \ SC. Then � =NF �� (�2). There are the following cases.
1
1. �1 = ą and �2 <�. Then we obtain �� (�2) " Acc by (vii).
1
2. ą<�1 and � <�. Then � " Acc follows from � " Acc.
3. �1 <ą and �2 <�ą(�). Then SC (�1) )" &! is majorized by some � " SC (ą) )" &! ą" Acc
which means SC (�1) )" &! ą" Acc and therefore �1 <1 ą. By (ii) we obtain �1 " Acc�. By
induction hypothesis we have �2 " Acc and which entails �� (�2) " Acc. This finishes the proof
1
of (ii). We have to show
ą, � " Acc �! �ą(�) " Acc. (x)
From ą, � " Acc we get ą, � < &!. Therefore SC (ą) ą" ą which implies SC (ą) )" &! ą" Acc.
Hence ą " M )" &!. From (ii) and Lemma 3.7.13 we obtain Prog0(Acc�) and thence Acc� ą" Acc
by (3.19). Together with � " Acc this implies �ą(�) " Acc.

3.7.15 Lemma (ID1) Define Acc&! := ą ą " M (" ("� " K (ą))[ą d" �] (" �(ą) " Acc .
/
Then we obtain Prog1(Acc&!).
Proof Assume
55
3. Ordinal analysis of non iterated inductive definitions
ą " field(<1) and ("�<1 ą)[� " Acc&!]. (i)
We have to show
ą " Acc&!. (ii)
For ą " M or ("� " K (ą))[ą d" �] (ii) is obvious. Therefore assume ą " M and K (ą) ą" ą. To
/
prove (ii) it remains to show
�(ą) " Acc. (iii)
For (iii) in turn it suffices to have
� <�(ą) � " Acc. (iv)
We prove (iv) by Mathematical Induction on the length of the term notation of �. If � " SC we get
/
SC (�) ą" Acc by induction hypothesis and thence � " Acc by Lemma 3.7.12 and Lemma 3.7.14.
If � " SC then there is a �0 such that K(�0) ą" �0 <ąand � = �(�0). For � " SC (�0) )" &! we
either have � =0 or � =NF �(�) for some �. In the second case we get � " K(�) ą" K(�0) ą" ą
which implies � = �(�) < �(ą). Hence SC (�0) )" &! ą" �(ą). By induction hypothesis we
therefore obtain SC (�0) )" &! ą" Acc. Hence �0 <1 ą and therefore �0 " Acc&! by (i). Since we
have K(�0) ą" �0 and just showed �0 " M this implies � = �(�0) " Acc.
3.7.16 Lemma (Condensation Lemma) If K(ą) ą" ą and ą " M then ID1 TI1(ą, F ), im-
plies ID1 �(ą) " Acc.
Proof We especially have
ID1 TI1(ą, Acc&!). (i)
From (i) and Lemma 3.7.15 we obtain
("�<1 ą)[� " Acc&!] (ii)
and from (ii) and Lemma 3.7.15
ą " Acc&!. (iii)
But (iii) together with the other hypotheses yield �(ą) " Acc.
3.7.17 Lemma ID1 TI1(&! + 1, F) '" K(&! + 1) ą" &!+1'" &!+1" M.
Proof Since SC (&!+1) = {0} and K(&!+1) = " we obviously have K(&!+1) ą" &!+1 '" &!+1 "
M. Assuming Prog1(F ) we have to show ("�<1 &!+1)[F (�)]. If � <1 &! we obtain SC (�) ą" Acc
and thus � " Acc by Lemma 3.7.12 and Lemma 3.7.14. By Lemma 3.7.13 we get Prog0(F )
which then by (3.19) entails F (�). So we have ("�<1 &!)[F (�)] which by Prog1(F ) also implies
F (&!).
3.7.18 Lemma
ID1 TI1(ą, F ) '" K(ą) ą" ą '" ą " M �! ID1 TI1(�ą, F) '" K(�ą) ą" �ą '" �ą " M.
Proof We show ID1 TI1(ą, F ) �! ID1 TI1(�ą, F) literally as (2.8). Because of SC (�ą))"
&!=SC (ą) )" &! *"{0} and K(�ą) =K(ą) the remaining claims follow trivially.
3.7.19 Theorem (The lower bound for ID1) For every ordinal ą<�(�&!+1) there is a primitiv
recursive ordering z" such that ID1 n " Acc(z") and ą d"|n|Acc(z").
56
3.7. The lower bound
Proof We have outlined in Theorem 3.7.7 that <0 is primitive recursive. Defining a sequence
n
ś0 =&!+1 and śn+1 = �ś we obtain by Lemma 3.7.17 and Lemma 3.7.18
ID1 TI1(śn, F) '" K(śn) ą" śn '" śn " M
for all n. Hence �(śn) " Acc = Acc(<0) by the Condensation Lemma (Lemma 3.7.16). By
Observation 1.7.10 we have |n|Acc(< ) = otyp< (n) = |n|O. Hence |�(śn)|Acc(< ) = �(śn)
0 0
0
and the claim follows because supn śn = �(�&!+1).
ext
1 1
3.7.20 Corollary We have ||ID1|| = �ID = �(�&!+1) and ||ID1ext|| = ||ID1ext|| 1 = �ID =
1
�(�&!+1).
57
Index
Index
Notations
EA, 5 tc(F ), 15
"0 formula, 5 I�, 17
PRA, 5 M�, 17
Prf (i, v), 5 �ą, 17
Ax
�<ą(S), 17
, 5
Ax
ą
I� , 17
PRWO(z"), 5
<ą
I� , 17
TI (z"), 5
CK
|�|, 17
�1 , 6
|n|�, 18
TI (z", X), 8
��, 18
||Ax||, 8
I�, 18
On, 8
|�|, 18
ą<�, 8
|x|�, 18
Lim, 8
�S, 19
R, 9
otypT (s), 19
sup M, 9
otyp(T ), 19
�, 9
�T (X, x), 19
enM, 9
T s, 20
otyp(M), 9
�z"(X, x), 22
H, 10
Acc(z"), 22
ą =NF ą1 + . . . + ąn, 10
Accą(z"), 22
-number, 10
||Ax|| 1, 22
, 11
0 1
m
�ą(�), 11 ", 27
L(NT ), 28
Cr (ą), 11
n
Ck , 28
ą =NF ��(�), 11
n
Pk , 28
SC , 11
S, 28
�0, 11
Sub, 28
SC (ą), 11
Rec, 28
otypz"(x), 12
NT , 28
otyp(z"), 12
ą
", 30
<"F , 12
�
On, 32
D(N), 12
a z" b, 32
 type, 13
ą ą" X, 33
 type, 13
Prog(X), 33
CS (F ), 13
TI(ą, X), 33
ą
F , 13 J (X), 34
ą
" , 14 L(ID1), 37
S", 14 IF , 37
� completeness, 15 ID1, 37
58
Index
(ID11), 37
(ID12), 37
ClF (G), 37
L",�(NT ), 37
L"(NT ), 38
t " I<ą, 39
F
1
�ID , 39
par (G), 41
par ("), 41
ą
H ", 41
�
Bą, 43
�(ą), 43
&!
 type, 44
Bą, 49
n
Bą , 49
ąnf, 50
�(ą), 50
K (�), 52
SC, 52
H, 52
On, 52
K(a), 52
a z" b, 52
a a" b, 52
|a|O, 52
ą<0 �, 53
Acc, 53
ą<1 �, 53
Progi(F ), 54
TIi(ą, F ), 54
M, 55
Acc&!, 55
59
Index
Key words
(" Exporation, 42 epsilon0, 11
BEKLEMISHEV, 6 exponentiation
GENTZEN, 5 ordinal, 10
G�DEL, 5
fixed point, 16
KREISEL, 5
the, 16
MOSTOWSKI, 9
the, 18
TAIT, 12
formula
TAIT language, 12
X positive, 19
accessible part, 22
Gamma zero, 11
additive components, 10
Generalized Induction, 47
additive normal form, 10
additively indecomposable ordinal, 10
identity axiom, 28
incompleteness, 35
Basic Elimination Lemma, 31
induction, 28
bounded set, 9
transfinite, 8, 9
Boundedness Lemma, 43
Induction Lemma, 29
Boundedness Theorem, 21
inductive definition, 16
generalized, 18
Cantor normal form, 10, 11
generalized monotone, 16
cardinal, 8
inductively defined
cardinality, 8
by a set of clauses, 16
characteristic sequence, 13
Inversion Lemma, 42
clause
of an inductive definition, 16
jump, 34
closed, 9
in a regular ordinal, 9
Kleene-Brouwer ordering, 23
under an operator, 16
closure ordinal
limit ordinal, 8
of a structure, 19
limit ordinal (Lim), 8
of an operator, 18
club, 9
Mathematical Induction, 5
Collapsing Lemma, 44
Monotonicity Lemma, 47
conclusion
node, 19
of a clause, 16
normal function, 9
Condensation Lemma, 56
Number Theory NT , 28
continuous, 9
Controlled Tautology, 46
operator
critical ordinal, 11
F definable, 18
elementarily definable, 18
defining axioms
elementary definable, 18
for IF , 37
first order definable, 18
for primitive recursive functions, 28
monotone, 16
derivative, 11
positive, 19
diagram, 12
order type, otyp, 9
elementary Arithmetic, 5 ordinal, 8
Elimination Theorem, 32 ordinal analysis
enumerating function, 9 of NT, 35
epsilon number, 10 ordinal sum, 9
60
Index
path, 19
Predicative Elimination Lemma, 31
premise
of a clause, 16
proof by induction on the definition, 16
proof theoretic ordinal, 8
pseudo 1 sentence, 14
1
recursor, 28
Reducion Lemma, 42
regular ordinal, 9
relation
positively F inductive, 19
positively inductive, 19
restriction
of a tree above a node, 20
satisfaction
of a clause, 16
scheme
of Mathematical Induction, 28
search tree, 14, 23
semi formal provability, 30
Skolem hull operator, 41
strongly critical, 11
SC , 11
Structural Lemma, 30
substitution operator, 28
successor, 28
successor ordinal, 8
supremum, 9
symbols for primitive recursive functions, 28
symmetric sum, 10
Tautology Lemma, 29
transfinite recursion, 8, 9
tree, 19
well founded, 19
truth complexity
for arithmetical sentences, 13
for a (pseudo) +11 sentence, 15
unbounded set, 8, 9
validity relation, 13
validity relation, 14
Veblen function, 11
Veblen normal form, 11
61
Index
62
Bibliography
Bibliography
[1] P. ACZEL, H. SIMMONS AND S. S. WAINER (editors), Proof theory (Leeds 1990), Cam-
bridge University Press, Cambridge, 1992.
[2] A. BECKMANN AND W. POHLERS, Application of cut free infinitary derivations to gener-
alized recursion theory, Annals of Pure and Applied Logic, vol. 94 (1998), pp. 1 19.
[3] W. BUCHHOLZ, A simplified version of local predicativity, Proof theory (P. Aczel et al.,
editors), Cambridge University Press, Cambridge, 1992, pp. 115 147.
[4] S. R. BUSS (editor), Handbook of Proof Theory, Studies in Logic and the Foundations of
Mathematics, North-Holland Publishing Company, 1998.
[5] G. GENTZEN, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische An-
nalen, vol. 112 (1936), pp. 493 565.
[6] , Neue Fassung des Widerspruchsfreiheitsbeweises f�r die reine Zahlentheorie,
Forschungen zur Logik und Grundlegung der exakten Wissenschaften, vol. 4 (1938),
pp. 19 44.
[7] , Beweisbarkeit und Unbeweisbarkeit von Anfangsf�llen der transfiniten Induktion in
der reinen Zahlentheorie, Mathematische Annalen, vol. 119 (1943), pp. 140 161.
[8] J.-Y. GIRARD, Proof theory and logical complexity, vol. 1, Bibliopolis, Naples, 1987.
[9] Y. N. MOSCHOVAKIS, Elementary induction on abstract structures, Studies in Logic and
the Foundations of Mathematics, vol. 77, North-Holland Publishing Company, Amsterdam,
1974.
[10] W. POHLERS, Cut-elimination for impredicative infinitary systems I. Ordinal analysis
for ID1, Archiv f�r Mathematische Logik und Grundlagenforschung, vol. 21 (1981),
pp. 113 129.
[11] , Proof theory. An introduction, Lecture Notes in Mathematics, vol. 1407, Springer-
Verlag, Berlin/Heidelberg/New York, 1989.
[12] , A short course in ordinal analysis, Proof theory (P. Aczel et al., editors), Cambridge
University Press, Cambridge, 1992, pp. 27 78.
[13] , Subsystems of set theory and second order number theory, Handbook of Proof
Theory (S. R. Buss, editor), Studies in Logic and the Foundations of Mathematics, North-
Holland Publishing Company, 1998, pp. 209 335.
[14] K. SCH�TTE, Proof theory, Grundlehren der mathematischen Wissenschaften, vol. 225,
Springer-Verlag, Heidelberg/New York, 1977.
63
Bibliography
[15] G. TAKEUTI, Proof theory, 2. ed., Studies in Logic and the Foundations of Mathematics,
vol. 81, North-Holland Publishing Company, Amsterdam, 1987.
64