Pohlers Infinitary Proof Theory (1999)

Infinitary Proof Theory

Wolfram Pohlers

Westf¨alische Wilhems–Universit¨at M¨unster

August 20, 1999

Contents

Proof theoretic ordinals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1.1

Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1.2

Some basic facts about ordinals . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1.3

Truth complexity for

–sentences . . . . . . . . . . . . . . . . . . . . . . . . . . .

1.4

Inductive definitions

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1.5

The stages of an inductive definition . . . . . . . . . . . . . . . . . . . . . . . . . .

1.6

Positively definable inductive definitions . . . . . . . . . . . . . . . . . . . . . . . .

1.7

Well–founded trees and positive inductive definitions . . . . . . . . . . . . . . . . .

1.8

The

–ordinal of an axiom system . . . . . . . . . . . . . . . . . . . . . . . . . .

The ordinal analysis for PA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2.1

Logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2.2

The theory NT . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2.3

The upper bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2.4

The lower bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Ordinal analysis of non iterated inductive definitions . . . . . . . . . . . . . . . .

3.1

The theory ID

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3.2

The language

∞

(NT) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37

3.3

Inductive definitions and

∞

(NT) . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

3.4

The semi–formal system for

∞

(NT) . . . . . . . . . . . . . . . . . . . . . . . . . 39

3.5

Controlling operators for ID

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3.6

The upper bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3.7

The lower bound . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3.7.1

Coding ordinals in

L(NT) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

3.7.2

The well–ordering proof . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

Contents

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 ¨

ODEL

’s second incompleteness

theorem, finitary consistency proofs are impossible for axiom systems which allow sufficiently
much coding machinery.
Ordinals entered the stage when G

ENTZEN

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 K

REISEL

there is a serious obstacle.

To state K

REISEL

’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, +, ·, 2

, =, ≤)

together with their defining axioms among them

(exp)

= 1 and 2

x+1

= 2

+ 2

(

≤)

x ≤ 0 ↔ x = 0 and

x ≤ y + 1 ↔ x ≤ y ∨ x = y + 1.

The scheme

(Ind)

ϕ(0) ∧ (∀x)[ϕ(x) → ϕ(x + 1)] → (∀x)ϕ(x)

of Mathematical Induction is restricted to

∆

–formulas ϕ. A formula is

∆

iff it only contains

bounded quantifiers

(∀x < a) or (∃x < a). Mostly we use the system PRA which has constants

for all primitive recursive functions and in which the scheme of mathematical induction is re-
stricted to

–formulas. By

⊥ we denote the false sentence 0 = 1. We assume that there is an

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”.

For an axiom system Ax we obtain the provability predicate as

x :⇔ (∃y)Prf

(y, x).

By PRWO

(≺) we denote that there are no primitive recursive infinite descending sequences in

field

≺. By TI (≺) we denote the scheme of induction along ≺.

1.1.1 Theorem (Kreisel)

For any consistent axiom system Ax there is a primitive recursive

well–ordering

≺

of order type ω such that

PRA

+ PRWO(≺

) Con(Ax)

1. Proof theoretic ordinals

Sketch of the proof of Theorem 1.1.1

Define

x ≺

y :⇔

x < y if (∀i < x)[¬Prf

(i, ⊥ )]

y < x otherwise

(i)

and let

F (x) :⇔ (∀i ≤ x)[¬Prf

(i, ⊥ )].

(ii)

Now we obtain

PRA

(∀x≺

y)F (x) → F (y)

(iii)

since if we assume

¬F (x) we have (∃i ≤ x)[Prf

(i, ⊥ )] and get x + 1 ≺

x and thus

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(≺

) (∀x)F (x)

(iv)

and thus

PRA

+ PRWO(≺

) Con(Ax).

(v)

Since Con

(Ax) is true we have otyp(≺

) = ω.

Recall that ω

denotes the first ordinal which cannot be represented as the order–type of a

recursive well–ordering. It is well-known that for every ordinal λ < ω

there is a primitive

recursive (even elementary) well–ordering of order–type λ. There is a theorem recently observed
by B

EKLEMISHEV

which points exactly in the opposite direction of Theorem 1.1.1.

1.1.2 Theorem (Beklemishev)

For any λ < ω

there is a primitive recursive well–ordering

of order–type λ such that

PRA

+ PRWO(≺) 6

Con

(PA).

To show Theorem 1.1.2 we first observes two other facts.

1.1.3 Theorem (Beklemishev) For every ordinal λ < ω

there is a primitive recursive well–

ordering E of order type λ such that

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

x R

y :⇔ x + y ≤ z ∧ x R y.

(ii)

Then R

is a finite ordering and we get a proof of TI

) primitive recursively from z. Hence

PRA

(∀z)

PRA

z·

(iii)

By the arithmetical fixed-point theorem we define a formula

x E y :⇔ x R y ∧ (∀u < x + y)¬C(u, (x E y) )

(iv)

where C

(u, v) is the primitive recursive predicate saying that v is a code for x E y and u codes a

proof of a contradiction from PRA

+ TI (E). Then

1.1. Preliminaries

PRA

C(z, (x E y) ) ∧ (∀u < z)¬C(u, (x E y) )

→ (x E y ↔ x R

→ (∀z)

PRA

(x E y ↔ xR

z·

→

PRA

(E)

(v)

by (iii). Since PA proves Con

(PRA) and the least number principle we get from (v)

(∃z)C(z, (x E y) ) → Con(PRA + TI (E)).

(vi)

But (vi) means

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 Ax

be theories which comprise PRA (either directly or via in-

terpretation). Then Ax

Con

(Ax

) implies Ax

⊆

, i.e. Ax

–conservative over

Sketch of the proof of Thm.1.1.4

By formalized

completeness we get for a

formula P

PRA

¬P →

¬P

(i)

and thus

PRA

¬P → P.

(ii)

If Ax

P we get PRA

P and thus also

PRA

¬¬P.

(iii)

Hence

PRA

⊥ → ¬

¬P

(iv)

which is

PRA

Con

(Ax

) → ¬

¬P.

(v)

Because of

Con

(Ax

)

(vi)

we obtain from (vi),(v) and (ii)

and are done.

Now we obtain Theorem 1.1.2 from Theorems 1.1.4 and 1.1.3 by choosing

≺ 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 G

ENTZEN

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.

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

≺ can be expressed by the formula

(≺, X) :⇔ (∀x)[(∀y ≺ x)(y ∈ X) → x ∈ X] → (∀x)[x ∈ X].

Let PR denote the collection of primitive recursive relations. According to G

ENTZEN

’s observa-

tion we define

||Ax|| := sup

otyp

(≺) ≺∈ PR ∧ Ax

(≺, 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 Π

–ordinal of Ax and will later indicate that

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:

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

(On4)

The class

R is unbounded, i.e., (∀ξ ∈ On)(∃η ∈ R)[ξ ≤ η].

We define

sup M := min

ξ ∈ On (∀η ∈ M)(η ≤ ξ)

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 ω

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

order preserving function en

: otyp(M)

onto

−→ M. The function en

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 M

OSTOWSKI

collapse of

M and en

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 α ≤ f(α) for all

α ∈ M.
A class 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 en

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 α ≤ ξ

1. Proof theoretic ordinals

which is club in all regular κ > α. Hence λξ . α

+ ξ is a κ-normal function for all regular κ > α.

We define

H :=

α ∈ On α 6= 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 en

(0) = 1 and en

(1) = ω which are the first

two examples of the fact that

(∀ξ ∈ On)[en

(ξ) = ω

(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

{α

, . . . , α

} ⊆ H we get

+ . . . + α

= α

+ . . . + α

for

, . . . , k

} ⊆ {1, . . . , n} such that k

< k

i+1

and α

≥ α

i+1

. By induction on α we

obtain thus ordinals

{α

, . . . , α

} ⊆ H such that for α 6= 0 we have

α = α

+ . . . + α

and α

≥ . . . ≥ α

(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 α

, . . . , α

in (1.3) are

uniquely determined. We therefore define an additive normal form

α =

N F

+ . . . + α

: ⇔ α = α

+ . . . + α

, {α

, . . . , α

} ⊆ H and α

≥ . . . ≥ α

We call

{α

, . . . , α

} the set of additive components of α if α =

N F

+ . . . + α

We use the additive components to define the symmetric sum of ordinals α

N F

+ . . . + α

and β

N F

n+1

+ . . . + α

β := α

π(1)

+ . . . + α

π(m)

where π is a permutation of the numbers

{1, . . . , m} such that

1 ≤ i < j ≤ m ⇒ α

π(i)

≥ α

π(j)

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 C

ANTOR

normal form for ordinals for the basis ω,

which says that for every ordinal α

6= 0 there are ordinals ξ

, . . . , ξ

such that

α =

N F

+ . . . + ω

Since λξ . ω

is a normal function we have α

≤ ω

for all ordinals α. We call α an ε-number if

= α and define

:= min

α ω

= α

more generally let λξ . ε

enumerate the fixed points of λξ . ω

. If we put

exp

(α, β) := β and exp

n+1

(α, β) := α

exp

(α,β)

1.2. Some basic facts about ordinals

we obtain

:= sup

n<ω

exp

(ω, 0).

For

0 < α < ε

we have α < ω

and obtain by the C

ANTOR

Normal Form Theorem uniquely

determined ordinals α

, . . . , α

< α such that α =

N F

+ . . . + ω

For a class M

⊆ On we define its derivative

ξ ∈ On en

(ξ) = ξ

The derivative f

of a function f is defined by f

:= en

Fix (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 f is a normal function f

is a normal function, too.

ι ∈ I

is a collections of classes club (in some regular κ) and

|I| ∈ On (|I| ∈ κ) then

ι∈I

is also club (in κ).

These facts give raise to a hierarchy of club classes. We define

(0) := H

(α

) := Cr(α)

(λ) :=

ξ<λ

(ξ) for λ ∈ Lim.

If we put

:= en

Cr(α),

then all ϕ

are normal functions and we have by definition

α < β ⇒ ϕ

(ϕ

(γ)) = ϕ

(γ).

(1.4)

The function ϕ is commonly called V

EBLEN

function. From (1.4) we obtain immediately

(β

) ≤ ϕ

(β

) iff

< α

and β

≤ ϕ

(β

)

= α

and β

≤ β

< α

and ϕ

(β

) ≤ β

(1.5)

We define the V

EBLEN

normal form for ordinals ϕ

(η) by

α =

N F

(η) : ⇔ α = ϕ

(η) and η < α.

Then α

N F

(η

) and α =

N F

(η

) ⇒ ξ

= ξ

and η

= η

. Since ξ < α and

η < β ∈ 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

α ∈ 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

α ϕ

(0) = α

If we define γ

:= 0 and γ

n+1

:= ϕ

(0) then we obtain

= sup

n < ω

We define the set of strongly critical components SC

(α) of an ordinal α by

1. Proof theoretic ordinals

(α) :=










{0}

if α

= 0

{α}

if α

∈ SC

(ξ) ∪ SC (η)

if α

N F

(η)

(α

) ∪ . . . SC (α

) if α =

N F

+ . . . + α

(1.6)

For every α <

there are uniquely determined ordinals ξ

, . . . , ξ

< α and η

, . . . , η

< α

such that

α =

N F

(η

) + . . . + ϕ

(η

) and η

< ϕ

(η

) for i ∈ {1, . . . , n}.

(1.7)

Recall that a relation

≺ is well–founded if there is no infinite descending sequence · · · x

n+1

≺

≺ · · · in field(≺). For x ∈ field(≺) we define

otyp

≺

(x) := sup

otyp

≺

(y) y ≺ x

and

otyp

(≺) := sup

otyp

≺

(x) x ∈ field(≺)

We call otyp

(≺) the ordertype of ≺. It is easy to see that otyp

≺

(x) and otyp(≺) 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

–sentences

1.3.1 Definition The T

AIT

–language for arithmetic contains the following symbols

• Set variables X, Y , X

,. . .

• The logical symbols ∧, ∨, ∀, ∃
• The binary relation symbols ∈,/∈, =,6=.
• 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) :≡ s 6= t; ∼(s 6= t) :≡ s = t
• ∼(s ∈ X) :≡ s /∈ X; ∼(s /∈ X) :≡ s ∈ X
• ∼(A ∧ B) :≡ ∼A ∨ ∼B; ∼(A ∨ B) :≡ ∼A ∧ ∼B
• ∼(∀x)F (x) :≡ (∃x)∼F (x); ∼(∃x)F (x) :≡ (∀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 (F

∨ F

) or (∃x)F (x) where F

and F

(k) is true for some i ∈

{0, 1} or k ∈ ω respectively

1.3. Truth complexity for

–sentences

• the sentences of the form (F

∧ F

) or (∀x)F (x) where F

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 (F

∧ F

)}∪

{sentences of the form (∀x)F (x)}

–type

¬F F ∈

–type

¬D(N) ∪ {sentences of the form (F

∨ F

)}

∪{sentences of the form (∃x)F (x)}

and define a characteristic sequence CS

(F ) of sub–sentences of F by

1.3.4 Definition

(F ) :=






∅

if F is atomic

, F

)

if F

≡ (F

◦ F

)

(F (k)| k ∈ ω) if F ≡ (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

(

) If F ∈

–type and

(∀G ∈ CS(F ))[

G & α

< α] then

(

) If F ∈

–type und

(∃G ∈ CS(F ))[

G & α

< α] then

F .

Finally we put

(F ) := min

∪ {ω}

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 ) ≤ rnk(F )

and

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

–sentence. For pseudo

–sentences F

( ~

X) we

define

N |= F ( ~

X) :⇔ N |= (∀ ~

X)F ( ~

X).

For pseudo

–sentences there is a third type of open atomic pseudo sentences which are the

sentences of the form

(t ∈ X) and (s /∈ X).

1.3.10 Definition For a finite set

∆ of pseudo Π

–sentences we define the validity relation

∆

inductively by the following clauses

(Ax) s

= t

⇒

∆ , s ∈ X, t /∈ X

(

) If F ∈

–type

∩ ∆ and (∀G ∈ CS(F ))

∆ , G & α

< α

then

∆

(

) If F ∈

–type

∩ ∆ and (∃G ∈ CS(F ))

∆ , G & α

< α

then

∆

Observe that for finite sets of formulas we always write F

, . . . , F

instead of

, . . . , F

}. 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 S

UTTE

. Therefore

we regard for the moment finite sequences

∆ of pseudo Π

–sentences. The leftmost non atomic

formula in a sequence

∆ is its redex R(∆). The sequence ∆

is obtained from

∆ by canceling its

redex R

(∆). We put

(∆) :⇔ ∃s, t, X[s

= t

∧ {t ∈ X, s /∈ X} ⊆ ∆].

For the definition of a tree cf. Definition 1.7.1. Two pseudo

–sentences are numerical equiva-

lent if they only differ in terms whose evaluation yield the same value.

1.3.11 Definition For a finite sequence

∆ of pseudo Π

-sentences we define its search tree S

∆

together with a label function

δ: S

∆

−→ finite sequences of pseudo Π

–sentences

inductively by the following clauses

)

hi ∈ S

∆

∧ δ(hi) = ∆

For the following clauses assume s

∈ S

∆

and

¬Ax(δ(s))

)

R(δ(s)) = ∅ ⇒ s

h0i ∈ S

∆

∧ δ(s

h0i) = δ(s)

)

R(δ(s)) ∈

–type

⇒ (∀F

∈ CS(R(δ(s))))[s

hii ∈ S

∆

] ∧ δ(s

hii) = ∆

, F

)

R(δ(s)) ∈

–type

⇒ s

h0i ∈ S

∆

∧ δ(s

h0i) = ∆

, F

, R(δ(s)), where F

is the

first formula in CS

(F ) which is not numerical equivalent to a formula in

[

⊆s

δ(s

1.3. Truth complexity for

–sentences

1.3.12 Remark The search tree S

∆

and δ are primitive recursively constructed from

∆.

1.3.13 Lemma (Syntactical Main Lemma)

If S

∆

is well–founded then

otyp(s)

∆ 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 S

, . . . , S

to the set variables occurring in

∆ such that N 6|= F [S

, . . . , S

] for all F ∈ ∆.

Sketch of the proof of Lemma 1.3.14.

Pick an infinite path f in S

∆

and let

f[n] := hf(0), . . . , f(n − 1)i.

Observe

F atomic ∧ F ∈ δ(f[n]) ⇒ (∀m≥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) :=

(∃m)[(t /∈ X) ∈ δ(f[m])]

and show by induction on rnk

(F ) that N 6|= F [Φ] for all F ∈

[

m∈ω

δ(f[m]) using (ii) and (iii).

1.3.15 Theorem (ω–completeness Theorem)

For a

–sentence

(∀X

) . . . (∀X

)F (X

, . . . , X

)

we have

N |= (∀X

) . . . (∀X

)F (X

, . . . , X

) ⇔ (∃a < ω

)

F (X

, . . . , X

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 (X

, . . . , X

)

(ii)

for all α < ω

. Then S

F (X

,...,X

)

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 X

, . . . , X

such that

N 6|= F (X

, . . . , X

)[Φ].

1.3.16 Definition Let

(∀ ~

X)F ( ~

X) be a Π

sentence. We put

((∀ ~

X)F ( ~

X)) := min

F ( ~

∪ ω

and call tc

(F ) the truth complexity of F . For a pseudo Π

–sentence G

( ~

X) containing the free

set parameters ~

X we define

(G( ~

X)) := tc((∀ ~

X)G( ~

X)).

1. Proof theoretic ordinals

1.3.17 Theorem For any (pseudo)

–sentence F we have

N |= F ⇔ tc(F ) < ω

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

⊆ N

is the set of premises and c

∈ N

is the conclusion of the clause (C).

A set S

⊆ N

satisfies (C) if P

⊆ S implies c ∈ S.

An inductive definition on N s a set

Φ :=

−→ c

ι ∈ I

of clauses on N .

The least (with respect to set inclusion) set I

⊆ N

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

⊆ N

is inductively defined by an inductive definition

Φ and ϕ is a “prop-

erty” which is preserved by all clauses in

Φ, i.e.

−→ 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

: P ow(N

) −→ P ow(N

)

by defining

(S) :=

c (∃P )[P −→ c ∈ Φ ∧ P ⊆ S]

which is monotonic, i.e.

S ⊆ T ⊆ N

⇒ Γ

(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

Γ: P ow(N

) −→ P ow(N

A set S

⊆ N

is closed under

Γ, if Γ(S) ⊆ S.

A set F

⊆ N

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

Γ.

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

S Γ(S) ⊆ S

and

For S

∈ M

we have I

⊆ S and thus Γ(I

) ⊆ Γ(S) ⊆ S by monotonicity. Thus

Γ(I

) ⊆

= I

(i)

From (i) we obtain

Γ(Γ(I

)) ⊆ Γ(I

)

(ii)

again by monotonicity. Hence

Γ(I

) ∈ M

which entails

⊆ Γ(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

Γ: P ow(N

) −→ P ow(N

) we define its α–th iter-

ation

(S) := S

α+1

(S) := Γ(Γ

(S))

(S) := Γ(

[

(S) ξ < λ

) for λ ∈ Lim.

We will frequently use the shorthand

<α

(S) :=

[

ξ<α

(S).

We define

:= Γ

<α

(∅) ∪ Γ(Γ

<α

(∅))

and use the shorthand

<α

[

ξ<α

1.5.2 Lemma For a monotone operator

Γ we have

:= Γ(I

<α

1.5.3 Lemma Let

Γ: P ow(N

) −→ P ow(N

) be an operator. Then there is a least ordinal

|Γ| < |N|

such that

|Γ|

= I

<|Γ|

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

<|Γ|

Proof

Since

Γ(I

<|Γ|

) = I

|Γ|

= I

<|Γ|

we have I

|Γ|

∈ M

and thus I

⊆ I

|Γ|

. For the opposite

inclusion we prove

⊆ I

(i)

by induction on ξ

≤ |Γ|. 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

Γ: P ow(N

) −→ P ow(N

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

≤ |Γ|.

(i)

Assuming σ <

|Γ| we get I

<σ

$ I

and find some x

∈ I

such that σ

≤ |x|

< |x|

+ 1 ≤ σ.

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

Γ: S

−→ S

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 ∈ S

S |= ϕ[~y, M,~a]

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|

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 ∈ S

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 ⊆ S

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 ∈ S

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 Π

-definable.

Proof

This follows immediately from Observations 1.6.3 and 1.4.5.

1.6.6 Definition The ordinal

:= sup

|ϕ| ϕ(X, ~x) is an X–positive elementary L(S)–formula

is called the closure ordinal of the structure

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) ≤ lh(t) ∧ (∀i < lh(s))[(s)

= (t)

A path in a 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

otyp

(s) := sup

otyp

hyi) s

hyi ∈ T

and

otyp

(T ) := otyp

(h i).

1.7.2 Definition Let T be a tree. We define the X–positive formula

(X, x) :⇔ (∀y)[x

hyi ∈ T → x

hyi ∈ X].

1.7.3 Lemma Let T be a well–founded tree and s

∈ T . Then s ∈ I

otyp

(s)

1. Proof theoretic ordinals

Proof

We induct on otyp

(s). If otyp

(s) = 0 then there is no x ∈ S such that s

hxi ∈ T .

Hence ϕ

(∅, s) which entails s ∈ I

. Now let otyp

(s) > 0. For every s

hxi ∈ T we have

α := otyp

hxi) < otyp

(s). By induction hypothesis we therefore obtain s

hxi ∈ I

⊆

<otyp

(s)

. Hence ϕ

<otyp

(s)

, s) which entails s ∈ I

otyp

(s)

1.7.4 Corollary For a well–founded tree T we have

|s|

≤ otyp

(s) for all s ∈ T . Hence

|ϕ

| ≤ 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

hyi ∈ T

such that the tail of P above s belongs to T

hyi. This shows that T s is well-founded if

T s

hyi is well–founded for all s

hyi ∈ 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) ≤

|s|

Proof

The proof is by induction on

|s|

. If

|s|

= 0 then we have ϕ

(∅, s), i.e. (∀x)[s

hxi /∈

T ]. Hence T s = h i and otyp(T s) = 0. If |s|

> 0 we have (∀x)[s

hxi ∈ T ⇒

hxi ∈ I

<|s|

ϕT

]. Then by induction hypothesis T s

hxi is well–founded for all s

hxi ∈ T

and otyp

(T s

hxi) < |s|

. This implies that T s is well-founded, too and otyp(T s) ≤ |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

h i ∈ I

and for well-founded trees T we have

otyp

(T ) + 1 = |ϕ|.

Proof

Let T be well–founded. Then

h i ∈ I

by Lemma 1.7.3. If conversely

h i ∈ I

then

T = T h i 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

otyp

(s) = otyp(T s) ≤ |s|

≤ otyp

(s).

Hence

T well–founded ∧ s ∈ T ⇒ otyp

(s) = |s|

(1.9)

and

otyp

(T ) = otyp(T h i) = |h i|

< |s|

for all s

∈ T . But |ϕ

| = sup

|s|

+ 1 s ∈ I

= |h i|

+ 1 = otyp(T ) + 1.

1.7.7 Theorem The

–relations on

N are exactly the positively inductive relations .

Proof

By Theorem 1.6.5 we know that all positively inductive relations are

definable. Con-

versely let R be a

–relation. Then there is a

–formula

(∀ ~

X)φ( ~

X, ~x) such that by Theorem

1.7.6

~s ∈ R ⇔ N |= (∀ ~

X)φ( ~

X, ~s)

⇔ S

φ( ~

X,~

is well–founded

⇔ h i ∈ I

φ( ~

X,~

(i)

1.7. Well–founded trees and positive inductive definitions

1.7.8 Theorem (Boundedness Theorem)

(∃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 ⊆ N

and an X–positive formula ϕ

(X, ~x) we introduce the formula

(X, ~x) :⇔ ϕ(X, ~x) ∨ ~x ∈ M.

(i)

If M

= {~t

, . . . ,~t

} we write ϕ

,...,~t

instead of ϕ

. We claim

M∪{~

⊆ I

α+1

∪ {~s}.

(ii)

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}. Therefore we obtain
~x ∈ I

M∪{~

⇔ ϕ(I

<α

M∪{~

, ~x) ∨ ~x ∈ I

<α

M∪{~

⇒ ϕ(I

∪ {~s}, ~x) ∨ ~x ∈ I

∨ ~x = ~s

⇒ ϕ(I

, ~x) ∨ ~x ∈ I

∨ ~x = ~s

⇒ ~x ∈ I

α+1

∨ ~x ∈ {~s}.

Let S be an arbitrary subset of

N. We show

(∃x)[ϕ(X, ~x) ∧ ~x /∈ X],~t

∈ X, . . . ,~t

∈ X, ∆[X, Y ] ⇒ N |= ∆[I

t1,...,~tn

, S] (iii)

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 ~s

= ~t

for some i

∈ {1, . . . , n}. Since ~t

∈

t1,...,~tn

we obtain

N |=

∆[I

t1,...,~tn

, S].

If the last inference is

(∃x)[ϕ(X, ~x) ∧ ~x /∈ X],~t

∈ X, . . . ,~t

∈ X, ∆

[X, Y ] ι ∈ J

⇒

(∃x)[ϕ(X, ~x) ∧ ~x /∈ X],~t

∈ X, . . . ,~t

∈ X, ∆[X, Y ]

then we have by induction hypothesis

N |=

∆

t1,...,~tn

, S]

(iv)

for all ι

∈ J. Hence N |=

∆ι[I

t1,...,~tn

, S] for all ι ∈ J which entails N |=

∆[I

t1,...,~tn

, S]

by the soundness of the inferences of the infinitary calculus.
The really interesting case is

(∃x)[ϕ(X, ~x) ∧ ~x /∈ X],~t

∈ X, . . . ,~t

∈ X, ϕ(X, ~s) ∧ ~s /∈ X, ∆[X, Y ] ⇒

(∃x)[ϕ(X, ~x) ∧ ~x /∈ X],~t

∈ X, . . . ,~t

∈ X, ∆[X, Y ].

(v)

From the premise in (v) we obtain

(∃x)[ϕ(X, ~x) ∧ ~x /∈ X],~t

∈ X, . . . ,~t

∈ X, ϕ(X, ~s), ∆[X, Y ]

(vi)

and

(∃x)[ϕ(X, ~x) ∧ ~x /∈ X],~t

∈ X, . . . ,~t

∈ X, ~s /∈ X, ∆[X, Y ].

(vii)

From the induction hypothesis for (vii) we obtain

N |=

∆[I

t1,...,~tn,~s

, S]

(viii)

1. Proof theoretic ordinals

which together with (ii) imply

N |=

∆[I

t1,...,~tn

∪ {~s}, S].

(ix)

Assuming

N 6|=

∆[I

t1,...,~tn

, S]

(x)

we also have

N 6|=

∆[I

t1,...,~tn

, S]

(xi)

which together with the induction hypothesis for (vi) imply

N |= ϕ(I

t1,...,~tn

, ~s).

(xii)

Hence

~s ∈ I

t1,...,~tn

⊆ I

t1,...,~tn

(xiii)

By (xiii) and (ix) we finally obtain

N |=

∆[I

t1,...,~tn

, S].

So we have (iii). The theorem, however, is a special case of (iii).

1.7.9 Definition For an order relation

≺ let

≺

(X, x) :⇔ (∀y ≺ x)[y ∈ X]

(1.11)

and Acc

(≺) := I

≺

. We call Acc

(≺) the accessible part of ≺. By Acc

(≺) := I

≺

we denote

the αth stage of the accessible part.

1.7.10 Observation For a well-founded relation

≺ we have

x ∈ Acc

(≺) ⇔ otyp

≺

(x) = α.

1.7.11 Theorem It is κ

= ω

Proof

≺ is a recursive well–ordering then by Observation 1.7.10 we obtain otyp(≺) ≤

|ϕ

≺

| ≤ κ

. Since ω

= sup

otyp

(≺) ≺ is recursive

this implies ω

≤ κ

For an X– positive formula ϕ

(X, ~x) we have

~s ∈ I

⇔ N |= (∀X)[(∀~x)(ϕ(X, ~x) → ~x ∈ X) → ~s ∈ X]

⇔ (∃α < ω

)

¬ (∀~x)(ϕ(X, ~x) → ~x ∈ X), ~s ∈ X

⇒ (∃α < ω

)

N |= ~s ∈ I

(i)

|ϕ| ≤ ω

holds for all positive elementary inductive definitions which entails κ

≤ ω

1.8

The

–ordinal of an axiom system

1.8.1 Definition For a theory Ax in the language of (

–order) arithmetic we define

||Ax||

:= sup

(F ) F ∈ Π

∧ Ax

We call

||Ax||

the

–ordinal of Ax .

1.8. The

–ordinal of an axiom system

We are going to show that the

–ordinal and the proof theoretic ordinal defined in (1.1) coincide.

1.8.2 Lemma For a well–ordering

≺ we have

otyp

(≺) ≤ tc(TI (≺, X)).

Proof

Apply the Boundedness Theorem (Theorem 1.7.8) to the formula ϕ

≺

(X, x) defined in

(1.11) and then apply Observation 1.7.10.

For a primitive recursive well-ordering

≺ and s ∈ field(≺) we obtain by an easy induction on

otyp

≺

(s)

5·(otyp

≺

(s)+1)

¬ (∀x)[(∀y ≺ 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

≺ we have

otyp

(≺) = tc(TI (≺, X)).

We just want to remark that this can be extended to

–definable well–orderings. Details are in [2].

1.8.4 Lemma For any axiom system Ax in the language of (

–order) arithmetic we have

||Ax|| ≤ ||Ax||

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||

Sketch of the proof

Assume that Ax is a theory comprising PA and let

(∀~Y )F (~Y ) be a Π

sentence. Denote by

≺

F (~

Y )

the K

LEENE

–B

ROUWER

ordering in the search tree S

F (~

Y )

for F

(~Y )

and assume that Ax

(≺

F (~

Y )

, X) . Then there is a model M |= Ax and an assignment

T ⊆ M for X such that M 6|= TI (≺

F (~

Y )

, X)[T ]. Therefore there is an infinite path, say P ⊆ M,

through S

F (~

Y )

which is definable by an first order formula with parameter T . According to the

Semantical Main Lemma we get assignments

Φ(Y

) ⊆ M for all Y

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 6|= F (~Y )[Φ] as in the proof of the Semantical Main Lemma using a local

truth predicate. Hence Ax

F (~Y ) and we have shown

F (~Y ) ⇒ Ax

(≺

F (~

Y )

, X).

Since

≺

F (~

Y )

is primitive recursively definable and we have tc

(F (~Y )) ≤ otyp(≺

F (~

Y )

) ≤ ||Ax||

for Ax

F (~Y ) this implies ||Ax||

≤ ||Ax||.

1.8.6 Theorem Let Ax be a

–set of arithmetical sentences. The theory Ax is

–sound iff

||Ax|| < ω

Proof

||Ax|| < ω

we have

||Ax||

< ω

and thus

N |= F for all F such that Ax

by Theorem 1.3.17. If conversely Ax is

–sound then

(F ) Ax

is a

–definable

subset of ω

. Hence

||Ax|| = ||Ax||

= sup

(F ) Ax

< ω

The following theorem is an immediate consequence of Theorem 1.8.3.

1. Proof theoretic ordinals

1.8.7 Theorem

||Ax|| ≤ sup

otyp

(≺) ≺∈ PR ∧ Ax

(≺)

≤ sup

otyp

(≺) ≺∈ Π

∞

∧ Ax

(≺)

≤ sup

otyp

(≺) ≺∈ Σ

∧ Ax

(≺)

≤ ||Ax||

= ||Ax||

1.8.8 Theorem (Kreisel)

Let Ax be a theory which contains PA. Then

||Ax||

= ||Ax + F ||

holds for every true

–sentence F .

Proof

Assume

+ F

(≺, X)

(i)

for a primitive recursive ordering

≺. Then

¬F ∨ TI (≺, X)

(ii)

which implies

¬ F, TI (≺, X)

(iii)

for some α <

||Ax||

. Let

Prog

(≺, X) :⇔ (∀x)[(∀y ≺ x)(y ∈ X) → x ∈ X].

(iv)

Then

(≺, X) ≡ Prog(≺, X) → (∀x ∈ field(≺))[x ∈ X].

(v)

For F

≡ (∃Y )F

(Y ) we obtain from (iii)

¬ Prog(≺, X), ¬F

(Y ), (∀x ∈ field(≺))[x ∈ X]

(vi)

which by the Boundedness Theorem (Theorem 1.7.8) implies

N |= ¬F

[S] ∨ (∀x ∈ field(≺))[x ∈ Acc

(≺)]

(vii)

for every set S

⊆ N. Since N |= (∃Y )F

(Y ) there is a set S ⊆ N such that N |= F

[S] and we

obtain from (vii)

N |= (∀x ∈ field(≺))[otyp

≺

(x) ≤ α].

(viii)

Hence

||Ax + F ||

= ||Ax + F || ≤ ||Ax||

The opposite inequality holds obviously.

It follows from K

REISEL

’s theorem that the

–ordinal of an axiom system does not characterize

its arithmetical power. Therefore more refined notions of proof theoretic ordinals have been
developed (e.g. in [13]). Most recently B

EKLEMISHEV

could define the

–ordinal of a theory

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.

1.8. The

–ordinal of an axiom system

In this lecture we will concentrate on the computation of the

ordinals. In the second part

Weierman will say something about the

–ordinal of PA which characterizes its provably recur-

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

ordinals. But we don’t want to give details about that here.

1. Proof theoretic ordinals

2. The ordinal analysis for

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 `a la T

AIT

2.1.1 Definition

(AxL)

∆, A, ¬A for any m, if A is an atomic formula

(∨)

∆, A

for some i

∈ {1, 2}, then

∆, A

∨ A

for all m > m

(∧)

∆, A

and m

< m for all i ∈ {1, 2}, then

∆, A

∧ A

(∃)

∆, A(t), then

∆, (∃x)A(x) for all m > m

(∀)

∆, A(u) and u not free in ∆, (∀x)A(x), then

∆, (∀x)A(x) for all m > m

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

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
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 T

AIT

–calculus is the admissibility

of the cut rule. We obtain

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

(Cut) If rnk

(F ) < r,

m
r

∆, F and

m
r

, ∆¬F then

n
r

∆ for all n > m

and replaces

∆, . . . in all clauses by

m
r

∆, . . .. The subscript r is thus a measure for the

complexity of all cut formulas occurring in the derivation. Obviously we have

∆ ⇔

m
0

∆.

2.1.5 Theorem (Gentzen’s Hauptsatz)

m
r

∆ then

(m)

∆ where 2

(x) is defined by 2

(x) =

x and 2

n+1

(x) = 2

(x)

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

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

= t

and

∆ (s) ⇒

∆ (t).

(2.1)

2.2

The theory

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, X

, . . . 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
C

for the constant function, P

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

, . . . , x

) = k

, . . . , x

) = x

Sub

(g, h

, . . . , h

)(x

, . . . , x

) = g(h

, . . . , x

)) . . . (h

, . . . , x

))

Rec

(g, h)(0, x

, . . . , x

) = g(x

, . . . , x

)

Rec

(g, h)(Sy, x

, . . . , x

) = h(y, Rec(g, h)(y, x

, . . . , x

), x

, . . . , x

)

, . . . , x

) ∈ R ↔ χ

, . . . , x

) = 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)[x

= y

∧ . . . ∧ x

= y

→ f(x

, . . . , x

) = f(y

, . . . , y

)]

(∀~x)(∀~y)[x

= y

∧ . . . ∧ x

= y

→ (R(x

, . . . , x

) → R(y

, . . . , y

))]

(∀x)(∀y)[x = y → (x ∈ X → y ∈ X)].

If NT

F there are finitely many axioms A

, . . . , A

of NT such that

¬A

∨ · · · ∨ ¬A

∨ F

is logically valid. Due to the completeness of the T

AIT

–calculus (cf. Theorem 2.1.3) we therefore

have the following theorem.

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
A

, . . . , A

and an m < ω such that

¬A

, . . . , ¬A

, F .

2.3

The upper bound

It follows from Theorems 2.1.3 and 2.1.6 that we have

¬A

, . . . , ¬A

, F

(2.2)

for the provable pseudo

–sentences of NT . In order to determine the

–ordinal of NT we

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

(2.3)

for all axioms A

. 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

(∀x)(∀y)[x = y → (x ∈ X → y ∈ X)] .

So we have

(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.3.1 Lemma (Tautology Lemma) For every

L(NT )-formula we have

2·rnk(F )

∆, ¬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)

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) ≤ ω + 4 for all instances G of the Mathematical Induction

Scheme. Together with (2.4) we get

ω+4

i.e. tc

) ≤ ω + 4

(2.5)

for all identity and non-logical axioms A

of NT .

2.3.3 Definition For a finite set

∆ of pseudo Π

–sentences we define the semi–formal provability

relation

α
ρ

∆ inductively by the following clauses

(Ax) s

= t

⇒

α
ρ

∆, s ∈ X, t /∈ X

(

) If F ∈

–type

∩ ∆ and (∀G ∈ CS(F ))

∆, G & α

< α

then

α
ρ

∆

(

) If F ∈

–type

∩ ∆ and (∃G ∈ CS(F ))

∆, G & α

< α

then

α
ρ

∆

(cut)

∆, F ;

∆, ¬F and rnk(F ) < ρ then

α
ρ

∆ for all α > α

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

α
0

∆ ⇔

∆ .

(2.6)

Hence

∆ ⇒

m
0

∆

(2.7)

by Theorem 2.1.6. There are some obvious properties of

α
ρ

∆ which are proved by induction on

α.

2.3.4 Lemma (Soundness)

α
ρ

, . . . , F

then

N |= (F

∨ · · · ∨ F

)[Φ] for every assign-

ment

Φ of subsets of N to the set parameters in F

, . . . , F

2.3.5 Lemma (Structural Lemma)

α
ρ

∆ then

β
σ

Γ holds for all β ≥ α, σ ≥ ρ and Γ ⊇ ∆.

2.3.6 Lemma (Inversion Lemma)

If F

∈

–type and

α
ρ

∆, F then

α
ρ

∆, G for all G ∈

(F ).

2.3.7 Lemma (

∨–Exportation) If

α
ρ

∆, F

∨ · · · ∨ F

then

α
ρ

∆, F

, . . . , F

2.3.8 Lemma If F

∈ D(N) and

α
ρ

∆, ¬F then

α
ρ

∆.

2.3.9 Lemma (Reduction Lemma)

Let ρ

= rnk(F ) for F ∈

–type, F

≡ (s ∈ X) or F ≡

(s /∈ X). If

α
ρ

∆, F and

β
ρ

Γ, ¬F then

α+β
ρ

∆, Γ.

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) 6= ∅ which entails ∆, Γ ∩ D(N) 6= ∅ 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 ≡ (s ∈ X) we show

α
ρ

∆, Γ

(ii)

by a side induction on α. First we observe that there is a formula t

∈ X with t

= s

Γ 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 6= ∅ 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 r

= s

= t

. But then we obtain

α
ρ

∆, Γ by (Ax). The

case F

≡ (s /∈ X) is symmetrical. From (ii) we get

α+β
ρ

∆, Γ by the Structural Lemma.

Now assume ρ >

0. Then ¬F ∈

–type and we have the premise

Γ, ¬F, ¬G

(iii)

for some G

∈ CS(F ). Then we obtain

α+β

∆, Γ, ¬G

(iv)

by induction hypothesis. From

α
ρ

∆, F we obtain

α+β

∆, Γ, 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.3.10 Lemma (Basic Elimination Lemma)

ρ+1

∆ then

∆.

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 λξ .

is order preserving. The

critical case is a cut

ρ+1

∆, F ;

ρ+1

∆, ¬F ⇒

ρ+1

∆ with rnk(F ) = ρ. By the induction

hypothesis and the Reduction Lemma we obtain

α0

∆ and we have 2

+ 2

= 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

≥ ω. The following results masters also this situation.

2.3.11 Lemma (Predicative Elimination Lemma)

β+ω

∆ then

(α)

∆.

Proof

Induction on ρ with side induction on α. For ρ

= 0 we obtain

∆ by the Basic

Elimination Lemma which, since

≤ ω

= ϕ

(α), entails the claim. Now assume ρ > 0. If

2. The ordinal analysis for PA

the last clause was not a cut of rank

≥ β we obtain the claim from the induction hypotheses and

the fact that the functions ϕ

are order preserving. Therefore assume that the last inference is

β+ω

∆, F

β+ω

∆, ¬F ⇒

β+ω

∆

such that β

≤ rnk(F ) < β + ω

. But then there is an ordinal φ such that rnk

(F ) = β + φ which,

writing φ in C

ANTOR

normal form, means rnk

(F ) = β+ω

+. . .+ω

< β+ω

. Hence σ

< ρ

and, putting σ

:= σ

, we get rnk

(F ) < β+ω

·(n+1). By the side induction hypothesis we have

(α

)

∆, F and

(α

)

∆, ¬F . By a cut it follows

(α

)+1

β+ω

·(n+1)

∆. If we define ϕ

(ξ) := ξ and

n+1

(ξ) := ϕ

(ϕ

(ξ)) we obtain from σ < ρ by n + 1–fold application of the main induction

hypothesis

n+1

(ϕ

(α

)+1)

∆. Finally we show ϕ

(ϕ

(α

) + 1) < ϕ

(α) by induction on n.

For n

= 0 we have ϕ

(ϕ

(α

) + 1) = ϕ

(α

) + 1 < ϕ

(α) since α

< α and ϕ

(α) ∈ Cr(0).

For the induction step we have ϕ

n+1

(ϕ

(α

) + 1) = ϕ

(ϕ

(α

) + 1)) < ϕ

(α) since σ < ρ

and ϕ

(ϕ

(α

) + 1) < ϕ

(α) by the induction hypothesis. Hence

(α)

∆.

By iterated application of the Predicative Elimination Lemma we obtain

2.3.12 Theorem (Elimination Theorem)

Let

α
ρ

∆ such that ρ =

N F

+ . . . + ω

Then

ρ1

(ϕ

ρ2

(···ϕ

ρn

(α)···))

∆.

2.3.13 Theorem (The upper bound for NT )

If NT

F then tc(F ) < ε

. Hence

||NT|| = ||NT||

≤ ε

Proof

If NT

F we get by (2.3) and (2.5)

ω+ω
r

(i)

for r

:= max{rnk(A

), . . . , rnk(A

)} < ω. By the Elimination Theorem (or just by iterated

application of the Basis Elimination Lemma) this entails

(ω+ω)

(ii)

Hence

(ω+ω)

F and we get tc(F ) < ε

since ϕ

(ω + ω) < ε

for all finite r.

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 α < ε

there is a primitive recursive well-order

≺ on the

natural numbers of order type α such that NT

(≺, X).

The first step in proving Theorem 2.4.1 is to represent ordinals below ε

by primitive recursive

well-orders. This is done by an arithmetization. We simultaneously define a set On

⊆ N and a

relation a

≺ b for a, b ∈ On together with an evaluation map | · |: On −→ On such that On and

≺ become primitive recursive and a ≺ b ⇔ |a| < |b|. We put

• 0 ∈ On and |0| = 0
• If z

, . . . , z

⊆ On and z

 . . . z

then

, . . . , z

i ∈ On and |hz

, . . . , z

i| = ω

. . . + ω

2.4. The lower bound

and

• a ≺ b : ⇔ a ∈ On ∧ b ∈ On ∧ [(a = 0 ∧ b 6= 0)

∨ (lh(a) < lh(b) ∧ (∀i < lh(a))((a)

= (b)

))

∨ (∃i < min{lh(a), lh(b)})(∀j < i)((a)

= (b)

∧ (a)

≺ (b)

)].

Observe that On and

≺ are defined by simultaneous course of values recursion and thence are

primitive recursive. It is also easy to check that a

≺ b ⇔ |a| < |b|. The order hOn, ≺i is

a well-order of order type ε

. We may therefore represent every ordinal α < ε

by an initial

segment

≺

of the well-order

≺. Thus we can talk about ordinals < ε

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 α ≺ β. 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 α < ε

. Since ε

= sup

exp

(ω, 0) n ∈ ω

and TI

(0, X)

holds trivially we are done as soon as we succeed in proving

TI(α, X) ⇒ NT

TI(ω

, X)

(2.8)

because NT

TI(α, X) and β < α obviously entails NT

TI(β, X). The first observation is

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

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 ) :=

Φ(Y )

if Y

6= X

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)

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

Prog(X) → Prog(J (X)),

(i)

we obtain

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 ξ ≤ η < ξ + ω

. 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−fold

=: ω

· n (c.f. the proof of the Predicative Elimination Lemma).

We show

σ < α → ξ + ω

· n ⊆ X

(xi)

by induction on n. For n

= 0 this is (ix). For n := m + 1 we have

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||

= ε

As a consequence of Theorem 2.3.13 and Theorem 2.4.1 we get

2.4.3 Theorem There is a

–sentence

(∀X)(∀x)F (X, x) which is true in the standard structure

N such that NT

F (X, n) for all n ∈ N but NT 6

(∀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 ¨

ODEL

’s Theorem. G ¨

ODEL

’s Theorem says that Theo-

rem 2.4.3 holds already for a

-sentence

(∀x)F (x).

2. The ordinal analysis for PA

3. Ordinal analysis of non iterated inductive
definitions

3.1

The theory

We want to axiomatize the theory for positively definable inductive definitions over the natural
numbers. According to Theorem 1.7.7 we can express

–relations by inductivley defined rela-

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(ID

) comprises the language of NT. For every X–positive

formula F

(X, ~x) we introduce a new relation symbol I

whose arity is the length of the tuple ~

The theory ID

comprises NT (but in the language without set parameters) together with the

defining axioms for the set constants

(ID

)(∀x)[F (I

, ~x) → x ∈ I

]

and

(ID

)Cl

(G) → (∀x)[x ∈ I

→ G(x)],

where

(G) ≡ (∀x)[F (G, ~x) → G(~x)]

expresses that the “class”

~x G

(~x)

is closed under the operator

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 I

is of course the least fixed point I

as introduced in Definition

1.6.1. The following theorem is left as an exercise.

3.1.2 Theorem

N |= ~n ∈ I

⇔ N |= (∀X)[Cl

(X) → ~n ∈ X]

(∀x)[F (I

, ~x) ↔ ~x ∈ I

]

3.2

The language

∞

(NT)

We extend the language of

L(NT ) to an infinitary language containing infinitely long formulas.

3.2.1 Definition (The language

∞,ω

(NT )) We define the language L

∞,ω

(NT) as a T

AIT

–

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

3. Ordinal analysis of non iterated inductive definitions

• If hF

| ξ ∈ Ii is a infinite sequence of L

∞,ω

(NT)–formulas containing at most finitely many

free variables then

ξ∈I

and

ξ∈I

are

∞,ω

(NT )–formulas.

Again we are interested in the sentences of

∞,ω

(NT). The set of sentences is denoted by

∞

(NT).

The semantics for

∞

(NT) is defined in the obvious way. We get

ξ∈I

:⇔ N |= F

for all ξ

∈ I

and

ξ∈I

:⇔ N |= F

for some ξ

∈ I.

Then it is obvious that we have

•

ξ∈I

∈

–type

and

•

ξ∈I

∈

–type

and

• CS(

ξ∈I

) = CS (

ξ∈I

) = hF

| ξ ∈ Ii.

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

∞

(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

N |= F ⇒

rnk (F )

F .

3.3

Inductive definitions and

∞

(NT )

The stages of an inductive definition over

N can be easily expressed in L

∞

(NT ).

3.4. The semi–formal system for

∞

(NT)

3.3.1 Definition Let F

(X, ~x) be a formula in L(NT ). By recursion on α ≤ ω

we define

~t ∈ I

<α

:≡

ξ<α

F (I

<ξ
F

,~t)

and dually

~t /∈ I

<α

:≡

ξ<α

¬F (I

<ξ
F

,~t).

As a shorthand we also use

~t ∈ I

:≡ F (I

<α

,~t)

and

~t /∈ I

:≡ ¬F (I

<α

,~t).

It it obvious that we have

N |= ~t ∈ I

⇔ ~t

∈ I

(3.1)

where I

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

∞

(NT ) which is obtained from

the sentences defined in Definition 3.3.1 by closing them under first order operations.
If F

(X, ~x) is an X–positive L(NT)–formula, we know by Theorem 1.7.11 |F | ≤ ω

. Hence

= I

<ω

= I

<ω

. Let us use

Ω as a symbol for either ω

or ω

. There is an obvious

embedding of the language

L(ID

) into our fragment of L

∞

(NT ).

3.3.2 Lemma If G is an

L(ID

)–sentence we obtain G

∗

by replacing all occurrences of I

in G

by I

<Ω

. Then

N |= G ⇔ N |= G

∗

3.4

The semi–formal system for

∞

(NT)

By Observation 1.7.10 we obtain an upper bound for

||ID

|| if we determine

:= sup

|n|

F (X, x) is X–positive ∧ ID

n ∈ I

Since

|n|

n ∈ I

is a recursivley enumerable set we have κ

< ω

. Of course

we could have allowed set parameters in the language of ID

. Then it makes sense to talk about

pseudo

–sentences provable in the extended theory ID

ext

. One easily proves

~t ∈ I

⇔ ID

ext

~t ∈ I

⇔ ID

ext

(X) → ~t ∈ X.

By the Boundedness Theorem 1.7.8 we then obtain

≥ ||ID

ext

which confirms our decision not to include set parameters.
First we observe

3.4.1 Lemma We have

∆ ,~t ∈ I

<Ω

⇒

∆ , I

<α

which means

3. Ordinal analysis of non iterated inductive definitions

|n|

≤ tc(n ∈ I

<Ω

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.
It becomes clear from Lemma 3.4.1 that the computation of an upper bound for κ

can be

done analogously to that of an upper bound for

||NT||

. Therfore the first step should be the

computation of the truth complexities for the axioms of ID

. Here we have even to be carful

in transfering Theorem 2.1.6. The sentence n

∈ I

is an atomic sentence of

L(ID

) but not an

atomic sentence of

∞

(NT ). But observe that because of rnk(~t ∈ I

<Ω

) ≤ Ω we obtain by the

Tautology Lemma (Lemma 2.3.1)

Ω

∆ ,~t /∈ I

<Ω

,~t ∈ I

<Ω

(3.2)

Thus Theorem 2.1.6 modifies to

3.4.2 Theorem If

∆(~x) holds for a finite set of L(ID

)–formulas then

Ω+m

∆ (~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 ∈ I

→ ~y ∈ I

But here we get

Ω+n

(∀~x)(∀~y)[~x = ~y → ~x ∈ I

<Ω

→ ~y ∈ I

<Ω

]

for some n < ω. By the Induction Lemma (Lemma 2.3.2) we obtain

Ω+ω+4

∗

for all instances G of the scheme of Mathematical Induction in ID

. It remains to check the truth

complexities for the axioms ID

and ID

. By Lemma 3.2.4 we obtain

Ω+n

<Ω

)

since rnk

(Cl

<Ω

)) = Ω + n for some n < ω.

The same is of course also true for all instances of the axiom ID

These observations show that the ordinal analysis for ID

needs something new. The truth com-

plexities for the axioms of ID

are above

Ω. The ordinal κ

, however, is an ordinal <

Ω

(regardless of the interpretation of

Ω). Since a validation proof for a sentence ~n ∈ I

<Ω

does not

contain

Ω–branchings it is also clear that tc(~n ∈ I

<Ω

) < Ω. So we need additional conditions

which allow us to collapse the ordinal assigned to the infinitary derivations for sentences of the
form ~

n ∈ I

<Ω

into ordinals below

Ω.

But there is still another reason why cut–elimination alone cannot solve our problem. We define
the semi–formal system for the language

∞

(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 6|= F for all F ∈ ∆ ⇒

(i)

3.4. The semi–formal system for

∞

(NT)

by induction on α. The proof depends heavily on the fact that we only have sentences in

∞

(NT ).

In the case of a cut we have the premises

∆, Γ, F

(ii)

and

∆, Γ, ¬F

(iii)

and either

N 6|= F or N 6|= ¬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 ID

. 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
B

UCHHOLZ

’ 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

∞

(NT) we define

par

(G) :=

<α

occurs in G

For a finite set

∆ of sentences of our fragment of L

∞

(NT) we define

par

(∆) :=

[

F ∈∆

par

(F ).

3.4.6 Definition For a Skolem–hull operator we define the relation

α
ρ

∆ by the clauses (

(

) and (cut) of Definition 2.3.3 with the additional conditions that we always have

• α ∈ H(par(∆))

and for an inference

∆

⇒ H

α
ρ

∆

different from

(

) also

• par(∆

) ⊆ H(par(∆)).

We define

⊆ H

:⇔ (∀X)⊆On[H

(X) ⊆ H

(X)].

A Skolem–hull operator

H is Cantorian closed iff

• {0, Ω} ⊆ H(∅),

and it satisfies

3. Ordinal analysis of non iterated inductive definitions

• α ∈ H(∅) ⇔ SC (α) ⊆ H(∅).

For a set X

⊆ On and an operator H let

• H[X] := λΞ. H(X ∪ Ξ).

When writing

α
ρ

∆ 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

⊆ H

, α

≤ β, ρ ≤ σ, ∆ ⊆ Γ, β ∈ H

(par(Γ)) and H

α
ρ

∆ then H

β
σ

Γ.

The remaining facts of Section 2.3 carry over to controlled semi–formal derivations.

3.4.8 Lemma (Inversion Lemma) If F

∈

–type and

α
ρ

∆, F then H[par(F )]

α
ρ

∆, G for

all G

∈ CS(F ).

3.4.9 Lemma (

∨–Exportation) If H

α
ρ

∆, F

∨ · · · ∨ F

then

α
ρ

∆, F

, . . . , F

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

α
ρ

∆, 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

β
ρ

Γ, ¬F . Then we have the premise H

∆, ¬F, ¬G for some G ∈ CS(F ) with

par

(∆, F, G) ⊆ H(par(∆, F ))

(i)

and obtain

α+β

∆, Γ, ¬G by the induction hypothesis. By inversion, the Structural Lemma

and the hypothesis par

(F ) ⊆ H(par(∆, Γ)) we also have H

α+β

∆, Γ, G. It is rnk(G) < ρ

but to apply a cut we also have to check

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

(i)

ρ+1

∆ ⇒ H

∆

and

(ii)

β+ω

∆ 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.

3.5. Controlling operators for ID

3.5

Controlling operators for

We introduce a family of operators

which suffice to interpret the sentences ~t

∈ I

provable in

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

. Here it is comfortable to think on

Ω as the first

uncountable cardinal. Interpreting

Ω as ω

makes the following considerations much harder.

First we observe

(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.

α ≤ β ⇒ B

⊆ B

and ψ

(α) ≤ ψ(β).

(3.5)

Since for α

∈ B

(∅) ∩ β we get ψ(α) ∈ B

(∅) we have

α ∈ B

(∅) ∩ β ⇒ ψ(α) < ψ(β).

(3.6)

From (3.6) we get

(∅) ∩ Ω = ψ(α).

(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

α
ρ

∆(~t ∈ I

<β
F

) for β ∈ H(∅) then H

α
ρ

∆(~t ∈ I

<γ
F

) holds for

all γ such that α

≤ γ ≤ β and α ∈ H(par(∆(~t ∈ I

<γ
F

))).

Proof

We induct on α. In the cases that ~t

∈ I

<β
F

is not the main formula of the last inference

∆

(~t ∈ I

<β
F

) ⇒ H

α
ρ

∆(~t ∈ I

<β
F

)

(i)

we have α

∈ H(par(∆

(~t ∈ I

<β
F

))) ⊆ H(par(∆

(~t ∈ I

<γ
F

))) because β ∈ H(par(∆(~t ∈

<γ
F

))). Hence

∆

(~t ∈ I

<γ
F

)

(ii)

by induction hypothesis and

α
ρ

∆(~t ∈ I

<γ
F

)

(iii)

from (ii) by the same inference.

3. Ordinal analysis of non iterated inductive definitions

If ~t

∈ I

<β
F

is the main formula we are in the case of an

(

) inference with the premise

∆

,~t ∈ I

<β
F

,~t ∈ I

ξ
F

(iv)

for some ξ < β. Applying the induction hypothesis twice we obtain

∆

,~t ∈ I

<γ
F

,~t ∈ I

(v)

Since α

∈ H(par(∆

,~t ∈ I

<β
F

,~t ∈ I

ξ
F

)) ⊆ H(par(∆

, I

<β
F

)) ⊆ H(par(∆

, I

<γ
F

)) and α

α ≤ γ we can apply an inference (

) to obtain

α
ρ

∆

,~t ∈ I

<γ
F

3.5.3 Definition We say that a sentence in our fragment of

∞

(NT) is in

Ω

–type if it does not

contain subformulas of the shape ~t /

∈ I

<Ω

3.5.4 Lemma (Collapsing Lemma)

Let

∆ ⊆

Ω

–type such that par

(∆) ∪ {α} ⊆ B

α+1

(∅)

and

α+1

β
Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆. Then B

α+ω

ψ(α+ω

)

Ω

∆.

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

α+1

(par(∆)) = B

α+1

(∅)

(ii)

because par

(∆) ⊆ B

α+1

(∅) and

α, β ∈ B

α+1

(∅) ⇒ α + ω

∈ B

α+ω

(∅) and ψ(α + ω

) ∈ B

α+ω

(∅)

(iii)

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

<Ω

), . . . , ¬Cl

<Ω

)) = {Ω}. So we only have to bother about the parameters

∆. We run through the cases. If the last inference

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆, G ⇒ B

α+1

β
Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆ (iv)

is according to

(

) we have par(∆, G) ⊆ B

α+1

(par(∆)) ⊆ B

α+1

(∅) and obtain by the induc-

tion hypothesis

α+ω

β0

ψ(α+ω

β0

)

Ω

∆, G.

(v)

From α, β

∈ B

α+1

(∅) we obtain ψ(α + ω

) < ψ(α + β) by (i) and from α, β ∈ B

α+1

(∅) also

ψ(α + ω

) ∈ B

α+ω

(∅). Since also par(∆, G) ⊆ B

α+1

(∅) ⊆ B

α+ω

(∅) we obtain

α+ω

ψ(α+ω

)

Ω

∆

(vi)

from (v) by an inference

(

Assume that the last inference is a cut

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆, F

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

)∆, ¬F






⇒ B

α+1

β
Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆. (vii)

3.5. Controlling operators for ID

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

)

Ω

∆, F and B

α+ω

β0

ψ(α+ω

β0

)

Ω

∆, ¬F .

(viii)

As in the previous case we obtain ψ

(α + ω

) < ψ(α + ω

) and ψ(α + ω

) ∈ B

α+ω

(∅) and

infer

α+ω

ψ(α+ω

)

Ω

∆

from (viii) by (cut).
The real interesting case is that of an inference

F ∈

–type

∩ ∆

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆, G for all G ∈ CS(F )






⇒ B

α+1

β
Ω

∆ (ix)

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 for all G ∈ CS(F ).

(x)

Because α, β

∈ B

α+1

(par(∆, G)) = B

α+1

(∅) we get ψ(α + β

) < ψ(α + ω

) and from

α, β ∈ B

α+1

(∅) also ψ(α + ω

) ∈ B

α+ω

. Therefore we obtain

α+ω

ψ(α+ω

)

Ω

∆

from (x) by an inference

(

Now assume that the main formula ot the last inference is

¬Cl

<Ω

) ≡ (∃x)[F

<Ω

, x) ∧ x /∈ I

<Ω

(xi)

Then we have the premise

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), F

<Ω

, t) ∧ t /∈ I

<Ω

, ∆

(xii)

with β

∈ B

α+1

(par(∆) ∪ {Ω}) = B

α+1

(∅). By inversion we obtain from (xii)

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), F

<Ω

, t), ∆

(xiii)

and

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), t /∈ I

<Ω

, ∆.

(xiv)

Applying the induction hypothesis to (xiii) and then using boundedness gives

α+ω

β0

ψ(α+ω

β0

)

Ω

<ψ(α+ω

β0

)

, t), ∆,

(xv)

i.e.

α+ω

β0

ψ(α+ω

β0

)

Ω

t ∈ I

ψ(α+ω

β0

)

, ∆.

(xvi)

From (xiv) we obtain by inversion

α+1

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), t /∈ I

ψ(α+ω

β0

)

, ∆

(xvii)

which entails

3. Ordinal analysis of non iterated inductive definitions

α+ω

β0

Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), t /∈ I

ψ(α+ω

β0

)

, ∆.

(xviii)

Since ψ

(α + ω

) ∈ B

α+ω

β0

(∅) the induction hypothesis applies to (xviii) and we obtain

α+ω

β0

+ω

β0

ψ(α+ω

β0

+ω

β0

)

Ω

t /

∈ I

ψ(α+ω

β0

)

, ∆.

(xix)

Now we obtain

α+ω

ψ(α+ω

)

Ω

∆

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 ID

we want to remark

that the Collapsing Lemma may be strengthened to

α+1

β
Ω+1

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆ ⇒ B

α+ω

ψ(α+ω

)

ψ(α+ω

)

∆.

For k

= 0 it can be modified to

α+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

α+1

Ω+1

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆, t ∈ I

<Ω

(i)

and

α+1

Ω+1

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), ∆, t /∈ I

<Ω

(ii)

But then we may apply the induction hypothesis to (i) and then proceed as in the last case in the

proof of the Collapsing Lemma. The resulting cut sentence is t

∈ I

<ψ(α+ω

β0

)

which shows that

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

In order to get an upper bound for κ

Theorem 3.4.2 is not longer sufficient. What we need is

3.6.1 Theorem If

∆(~x) holds for a finite set of L(ID

)–formulas then H

Ω+m
0

∆(~n) for all

tuples ~

n of numerals and all Cantorian closed Skolem–hull operators

The key here is

3.6.2 Lemma (Controlled Tautology)

For every

∞

(NT)-sentence and Cantorian closed Skolem–

hull operator

H we have H

2·rnk(F )
0

∆, ¬F, F .

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

3.6. The upper bound

2·rnk(G)
0

∆, ¬F, F, G, ¬G

(i)

for all G

∈ CS(F ). Since par(∆, ¬F, F, G, ¬G) ⊆ H(par(∆, ¬F, F, G)) we obtain from (i)

2·rnk(G)+1
0

∆, ¬F, F, G,

(ii)

for all G

∈ CS(F ) by an inference (

). From (ii) and 2 · rnk(G) + 1 < 2 · (rnk(G) + 1) ≤

2 · rnk(F ), however, we immediately get

2·rnk(F )
0

∆, ¬F, F

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
that

∆,~t ∈ I

, ¬~t ∈ I

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
0

∗

(3.8)

for every axiom G of NT in the language

L(ID

) where H may be an aribtrary Cantorian closed

Skolem–hull operator.
So it remains to check the schemes ID

and ID

. By the Collapsing Lemma (Lemma 3.5.4)

we have only to deal with ID

3.6.3 Lemma (Generalized Induction) Let F

(X, ~x) be an X–positive NT formula. Then

2·rnk(G)+ω·(α+1)
0

¬Cl

(G), ~n /∈ I

, G(~n)

holds for any sentence G

(~n) in our fragment of L

∞

(NT ) and for any Cantorian closed Skolem–

hull operator

From the Generalized Induction Lemma we obtain

Ω·2+3
0

¬Cl

(G), (∀~x)[~x ∈ I

<Ω

→ G(~x)]

(3.9)

which is the translation of the scheme ID

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

α
ρ

∆, ¬G(~n), H(~n) for all ~n ⇒ H

α+2·rnk (F )
ρ

∆, ¬F (G, ~n), F (H, ~n)

for all ~

Proof

Induction on rnk

(F ). In the case that X does not occur in F (X, ~x) we have

2·rnk(F )
0

∆, ¬F, F

by the Tautology Lemma (Lemma 3.6.2). In the case that F

≡ (~x ∈ X) we obtain the claim from

the hypothesis

α
ρ

∆, ¬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)+ω·α
0

¬Cl

(G), ~n /∈ I

<α

, G(~n)

(i)

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 )
0

¬Cl

(G), ~n /∈ I

, F (G, ~n)

(ii)

by the Monotonicity Lemma. By controlled Tautology we have

2·rnk(G)
0

¬Cl

(G), ~n /∈ I

, ¬G(~n), G(~n).

(iii)

From (ii) and (iii) we get

2·rnk(G)+ω·α+(2·rnk(F ))+1
0

¬Cl

(G), ~n /∈ I

, F (G, ~n) ∧ ¬G(~n), G(~n)

(iv)

by an inference

(

). From (iv) we finally obtain

2·rnk(G)+ω·α+2·rnk(F )+2
0

¬Cl

(G), ~n /∈ I

, G(~n)

by an inference

(

). Since 2 · rnk(G) + ω · α + 2 · rnk(F ) + 2 < 2 · rnk(G) + ω · (α + 1) we

are done.

3.6.5 Theorem If ID

F (~x) then there are finitely many axioms Cl

<Ω

), . . . , Cl

<Ω

)

and an n < ω such that

Ω·2+ω
Ω+n

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), F (~m)

holds for any tuple ~

m of the length of ~x and for any Cantorian closed Skolem–hull operator.

Proof

If ID

F (~x) then there are finitely many axioms A

, . . . , A

and a natural number p

such that

¬A

, . . . , ¬A

, F (~x). By Theorem 3.6.1 this implies

Ω+p
0

¬A

∗

, . . . , ¬A

∗

, F

∗

(~m)

(i)

for any Cantorian closed Skolem–hull operator

H. From (i), (3.8) and (3.9) we obtain the claim

by some cuts.

3.6.6 Theorem (The Upper Bound for ID

)

It is κ

≤ ψ(ε

Ω+1

Proof

If ID

m ∈ I

we obtain by Theorem 3.6.5

Ω·2+ω
Ω+n

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), m ∈ I

<Ω

(i)

By Theorem 3.4.12 we obtain an α < ε

Ω+1

such that

α
Ω

¬Cl

<Ω

), . . . , ¬Cl

<Ω

), m ∈ I

<Ω

(ii)

From (ii) and the Collapsing Lemma (Lemma 3.5.4) it follows

ψ(ω

)

Ω

m ∈ I

<Ω

which by Theorem 3.4.3 implies tc

(m ∈ I

<Ω

) ≤ ψ(ω

) < ψ(ε

Ω+1

). By Lemma 3.4.1 the claim

follows.

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

Ω+1

(∅) is the set of ordinals which turned out to be

relevant in the computation of an upper bound for κ

. To prove that ψ

(ε

Ω+1

) is the exact bound

it suffices to prove n

∈ Acc

(≺) for some arithmetical definable relation ≺ and all α < ψ(ε

Ω+1

If we succeed in showing that for a primitive recursive relation

≺ we have by Observation 1.7.10

that

||ID

|| = ψ(ε

Ω+1

Since we cannot talk about ordinals in

L(ID

) we need codes for the ordinals in B

Ω+1

(∅). The

only parameters occurring on

Ω+1

(∅) are 0 and Ω. Therefore every ordinal in B

Ω+1

(∅) pos-

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

(∅) more closely.

We define

α =

N F

ψ(β) :⇔ α = ψ(β) ∧ β ∈ B

(∅).

Then

α =

N F

ψ(β

) ∧ α =

N F

ψ(β

) ⇒ β

= β

(3.10)

since β

< β

would imply ψ

(β

) < ψ(β

) by (3.6) because β

∈ B

(∅) ⊆ B

(∅). Now we

define a set of ordinal terms T by the clauses

) {0, Ω} ⊆ T

) α /∈ S ∧ SC (α) ⊆ T ⇒ α ∈ T

) β ∈ T ∧ α =

N F

ψ(β) ⇒ α ∈ T.

We want to prove

= 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.

) {0, Ω} ⊆ B

) ξ /∈ SC ∧ SC (ξ) ⊆ B

n−1

⇒ ξ ∈ B

) η ∈ B

n−1

∩ α ⇒ ψ(η) ∈ B

) B

n∈ω

∧ ψ(α) := min

ξ ξ /

∈ B

It is easy to check that B

= B

(∅) for all α ≤ Ω

which justifies the use of the same symbol ψ

for the functions

min

ξ ξ /

∈ B

(∅)

and

min

ξ ξ /

∈ B

. So (3.12) can be shown by proving

ξ ∈ B

⇒ ξ ∈ T

(3.13)

for all α <

Ω

by induction on n. What is still troublesome in pursuing this strategy is case

In this case we don’t know if ψ

(η) is in normal–form, i.e. if η ∈ B

. Therefore we show first

3. Ordinal analysis of non iterated inductive definitions

3.7.1 Lemma For every ordinal α <

Ω

the ordinal α

:= min

ξ α ≤ ξ ∈ B

exists and it

is ψ

(α) =

N F

ψ(α

Proof

Since

Ω

= sup

n∈ω

Ω

(0) and ϕ

Ω

(0) ∈ B

for any α it follows that α

exists. By

definition

[α, α

) ∩ B

= ∅ which implies B

= B

and thus also ψ

(α) = ψ(α

). Since

∈ B

= B

we have ψ

(α) =

N F

ψ(α

Our troubles are solved as soon as we can show

η ∈ B

⇒ η

∈ B

(3.14)

Then we may argue in case

) that for η ∈ B

n−1

we also have η

∈ B

n−1

and thus η

∈ T

which entails ψ

(η) =

N F

ψ(η

) ∈ 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

) which then becomes

)

η ∈ B

n−1

∩ α ∧ η ∈ B

⇒ ψ(η) ∈ B

The proof of (3.13) then becomes trivial.

3.7.2 Lemma Let δ

(α) := min

ξ α

≤ ξ ∈ 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)

Then α < δ

(α) and for α < Ω we get by (3.7) δ(α) = Ω ∈ B

for any n. Therefore we may

also assume

Ω ≤ α.

(iii)

We have

ξ /

∈ SC ∧ ξ ∈ B

⇒ SC (ξ) ⊆ B

n−1

(iv)

Since

(Ω, Ω

) ∩ SC = ∅ we obtain by induction hypothesis

δ(SC α) :=

δ(ξ) ξ ∈ SC (α)

⊆ B

n−1

∩ B

(v)

We are done if we can prove

(δ(α)) ⊆ B

n−1

∩ B

(vi)

We prove (vi) by induction on the number of ordinals in SC

(α). First assume α =

N F

+ · · · +

. Since α

≤ δ(α

) ∈ H we obtain α ≤ δ(α

) + · · · + δ(α

) and because δ(α

) + · · · δ(α

) ∈

even α < δ

(α

) + · · · δ(α

). Let i := min

j ≤ k α

< δ(α

)

. We claim

δ(α) = α

+ · · · + α

i−1

+ δ(α

) = δ(α

) + · · · + δ(α

i−1

) + δ(α

(vii)

From (vii) we obtain (vi) by induction hypothesis. Let η

:= α

+ · · · + α

i−1

. We have α <

η + δ(α

). Hence δ(α) ≤ η + δ(α

). If we assume δ(α) < η + δ(α

) there is an ε ∈ B

such that

η +α

≤ α < ε < η+δ(α

). But then we obtain an ε

such that ε

= η+ε

and α

< ε

< δ(α

But ε

∈ B

entails ε

∈ B

which contradicts the definition of δ

(α

3.7. The lower bound

Next assume α

N F

(α

). If δ(α

) = α

we immediately obtain δ

(ϕ

(α

)) = ϕ

(δ(α

)) =

δ(α

)

(δ(α

)) which entails (vi) byinduction hypothesis. If α

< δ(α

) and α ≤ δ(α

) we ob-

tain δ

(α) ≤ δ(α

) ≤ δ(α) and (vi) follows by induction hypothesis. So assume α

< δ(α

) and

δ(α

) < α. Let

:= min

ξ α ≤ ϕ

δ(α

)

(ξ)

(viii)

We claim

∈ B

n−1

∩ B

(ix)

From (ix) we get δ

(α) ≤ ϕ

δ(α

)

(α

). If we assume δ(α) < ϕ

δ(α

)

(α

) we have α = ϕ

(α

) <

δ(α

)

(α

). Since δ(α) ∈ H we obtain δ(α) =

N F

(ξ

). The assumption ξ

= δ(α

) yields

α < δ(α) = ϕ

δ(α

)

(ξ

) < ϕ

δ(α

)

(α

) and thus ξ

< α

conctradicting the minimality of α

Assuming δ

(α

) < ξ

yields δ

(α) < α

and α < δ

(α) = ϕ

δ(α

)

(δ(α)) again contradicting the

minimality of α

. So it remains ξ

< δ(α

). But since ξ

∈ B

this implies ξ

< α

which in

turn entails α < ξ

∈ B

∩ δ(α) contradiction the definition of δ(α). Therefore we have

δ(α) = ϕ

δ(α

)

(α

)

(x)

and obtain (vi) from (x) by induction hypothesis and (ix).

It remains to prove (ix). We are done if α

= 0. If we assume α

∈ Lim we get α =

N F

(α

) = ϕ

δ(α

)

(α

) by the continuity of ϕ

δ(α

)

. Because α

< δ(α

) we then obtain α

= α

contradicting α

≤ δ(α

) < α. It remains the case that α

= η + 1. Then ϕ

δ(α

)

(η) < α =

N F

(α

) < ϕ

δ(α

)

(η + 1). Because of α

< δ(α

) this implies ϕ

δ(α

)

(η) ≤ α

≤ δ(α

) <

α = ϕ

δ(α

)

(η + 1). But α

= ϕ

δ(α

)

(η) is excluded because otherwise we get ϕ

(α

) = α

(α

). Since δ(α

) ∈ B

n−1

∩ B

we have shown

∩ B

n−1

∩ (ϕ

δ(α

)

(η), ϕ

δ(α

)

(η + 1)) 6= ∅.

(xi)

To finish the proof we show that in general we have

∩ (ϕ

(η), ϕ

(η + 1)) 6= ∅ ⇒ η + 1 ∈ B

(3.15)

From (xi) and (3.15) we then obtain α

∈ B

∩ B

n−1

, i.e. (ix).

To prove (3.15) we first show

γ ∈ [ϕ

(η), ϕ

(η + 1)) ⇒ SC (η) ⊆ SC (γ)

(xii)

by induction on the number of elements in SC

(γ).

If γ

N F

+· · ·+γ

we have γ

∈ [ϕ

(η), ϕ

(η+1)) and obtain SC (η) ⊆ SC (γ

) ⊆ SC (γ).

If γ

N F

(γ

) then γ

≤ ξ because ξ < γ

entails γ

≤ η +1 < ϕ

(η). If ξ = γ

then η

= γ

and SC

(η) = SC (γ

) ⊆ SC (γ). If γ

< ξ then ϕ

(η) ≤ γ

< γ < ϕ

(η + 1) and we obtain

(η) ⊆ SC (γ

) ⊆ SC (γ) by induction hypothesis. If finally γ ∈ SC then γ = ϕ

(η) = η and

the claim is obvious.

We prove (3.15) by induction on n. Let σ

∈ B

∩ (ϕ

(η), ϕ

(η + 1)). Then σ /∈ SC and we

have SC

(σ) ⊆ B

n−1

. By (xii) we get SC

(η) ⊆ SC (σ) ⊆ B

n−1

. Since

0 ∈ B

n−1

we also have

(η + 1) ⊆ B

n−1

and thus obtain η

+ 1 ∈ B

Having established

Ω

(∅) = 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

). 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 α

N F

ψ(β) by a

condition which refers only to proper subterms of β. We observe that we have

3. Ordinal analysis of non iterated inductive definitions

ξ ∈ B

⇔ ξ = 0 ∨ ξ = Ω ∨

(ξ /∈ SC ∧ SC (ξ) ⊆ B

) ∨

(ξ = ψ(η) ∧ η ∈ B

∩ β).

(3.16)

From (3.16) we read off the following definition.

3.7.3 Definition Let

(ξ) :=






∅

if ξ

= 0 or ξ = Ω

[

(η) η ∈ 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 α

N F

ψ(β) 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

≺⊆ On × On and ≡⊆ On × On and an evaluation function | |

: On −→ T by the following

clauses.

Definition of SC, H and On.

• h0i ∈ On, h1i ∈ SC, |h0i|

:= 0 and |h1i|

:= ω

• If a

, . . . , a

∈ H and a

 · · · a

then

h1, a

, . . . , a

i ∈ On and |h1, a

, . . . , a

+ · · · + |a

• If a, b ∈ On then h2, a, bi ∈ H and |h2, a, bi|

= ϕ

|a|

(|b|

)

• If a ∈ On and b ≺ a for all b ∈ K(a) then h3, ai ∈ SC and |h3, ai|

:= ψ(|a|

)

Definition of K

(a).

• K(h0i) = K(h1i) = ∅
• K(h1, a

, . . . , a

i) = K(a

) ∪ · · · ∪ K(a

)

• If b ≺ h2, a, bi then K(h2, a, bi) = K(a) ∪ K(b)
• K(h3, ai) = {a} ∪ K(a)

Let a, b

∈ On. Then a ≺ b iff one of the following conditions is satisfied.

• a = h0i and b 6= h0i
• a = h1, a

, . . . , a

i, b = h1, b

, . . . , b

i and (∃i < m)(∀j ≤ i)[a

≡ b

∧ a

i+1

≺ b

i+1

] or

(∀j ≤ m)[a

≡ b

] ∧ m < n

• a = h1, a

, . . . , a

i, b ∈ H and a

≺ b

• a ∈ H, b = h1, b

, . . . , b

i and a b

• a = h2, a

, a

i, b = h2, b

, b

i and one of the following conditions is satisfied

≺ b

and a

≺ b

= b

and a

≺ b

≺ a

and a

≺ b

3.7. The lower bound

• a = h2, a

, a

i, a

≺ a, b ∈ SC and a

, a

≺ b

• a ∈ SC, b = h2, b

, b

i, b

≺ b and a b

or a

 b

• a = h3, a

i, b = h3, b

i and a

≺ b

• a = h3, a

i and b = h1i

For a, b

∈ On we define a ≡ b if one of the following conditions is satisfied

• (a)

6= 2 and (b)

6= 2 and a = b

• a ∈ SC, b

≺ a and b = h2, b

, ai

• b ∈ SC, a

≺ b and a = h2, a

, bi

• a = h2, a

, a

i, b = h2, b

, b

i and one of the following conditions is satisfied

≺ b

and a

≡ b

= b

and a

≡ b

≺ a

and a

≡ b

• The relation ≡ is transitive, reflexive and symmetrical.

Collecting all the known facts about T and observing that On, SC, H, K

(a), ≺ and ≡ 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

≺ and ≡ are primitive recursive.

The map

| |

: On −→ T is onto such that a ≺ b iff |a|

< |b|

and a

≡ b iff |a|

= |b|

3.7.8 Corollary ψ

(ε

Ω+1

) < ω

3.7.2

The well–ordering proof

In view of Theorem 3.7.7 we may talk about the ordinals in

Ω

(∅) in L(NT ) and thus also in

L(ID

). For the sake of better readability we will, however, not use the codes but identify ordinals

Ω

(∅) and their codes. We will denote (codes of ) ordinals by lower case greek letters and

write α < β instead of α

≺ β. We use the abbreviations introduced in Section 2.4.

The aim of this section is to show that there is a primitive recursiv relation <

such that for every

α < ψ(ε

Ω+1

) we get ID

α ∈ Acc(<

). The strategy of the proof will be the following.

• We first define a relation <

which is not longer arithmetical definable but needs a fixed point

in its definition such that TI

(Ω, X) holds trivially and then use the well–ordering proof of

Section 2.4 to obtain TI

(α, X) porvable in ID

ext

for all α <

Ω+1

• Then we use a condensing argument to show that TI

(α, X) implies ψ(α) ∈ Acc(<

3.7.9 Definition For ordinals α, β we define

• α <

β :⇔ α < β < Ω.

By ξ

⊆

X we denote the formula (∀η<

ξ)[η ∈ X].

Let Acc be the fixed point of the operator induced by ξ

⊆

X, i.e. Acc ≡ Acc(<

For α, β

∈ On we define

• α <

β :⇔ α < β ∧ SC (α) ∩ Ω ⊆ Acc.

ξ ⊆

X stands for (∀η<

ξ)[η ∈ X].

3. Ordinal analysis of non iterated inductive definitions

Let

• Prog

(F ) :≡ (∀ξ ∈ field(<

))[(∀η<

ξ)F (η) → F (ξ)]

• TI

(α, F ) :≡ α ∈ field(<

) ∧ Prog

(F ) → (∀ξ<

α)F (ξ).

Observe that by the axioms of ID

and Theorem 3.1.2 we have

α ∈ Acc ↔ α < Ω ∧ α ⊆ Acc

(3.17)

Prog

(Acc)

(3.18)

Prog

(F ) → (∀ξ)[ξ ∈ Acc → F (ξ)]

(3.19)

3.7.10 Lemma ID

Acc ⊆ Ω.

Proof

Since Prog

(field(<

)) holds trivially we get Acc ⊆ field(<

) =

α α < Ω

(3.19).

3.7.11 Lemma Let Prog

(F ) :≡ (∀α)[(∀ξ < α)F (ξ) → F (α)]. Then ID

Prog(F ) →

Prog

(F ) and thus also ID

Prog(F ) → (∀ξ ∈ Acc)F (ξ).

Proof

(∀ξ<

α)F (ξ) implies (∀ξ < α)F (ξ) for α < Ω. Together with Prog(F ) we therefore

get F

(α), i.e. we have Prog

(F ). Together with (3.19) we obtain the second claim, too,

3.7.12 Lemma

(ID

) The class Acc is closed under ordinal addition.

Proof

Let Acc

ξ (∀η ∈ Acc)[η + ξ ∈ Acc]

. We claim

Prog

(Acc

(i)

To prove (i) we have the hypothesis

α < Ω ∧ (∀ξ < α)[ξ ∈ Acc

]

(ii)

and have to show α

∈ 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 η ≤ ξ < η+α

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 ID

Prog

(F ) → Prog

(F ).

Proof

We have the premises Prog

(F ), α < Ω and (∀ξ<

α)F (ξ) and have to show F (α). If

ξ <

α we get ξ <

α by α < Ω and thus F (ξ) by (∀ξ<

α)F (ξ). Hence (∀ξ<

α)F (ξ) which

entails F

(α) by Prog

(F ).

3.7. The lower bound

3.7.14 Lemma

(ID

) The class Acc is closed under λξ, η . ϕ

(η).

Let M

α SC

(α) ∩ Ω ⊆ Acc

and define

Acc

α (∀ξ ∈ Acc)[ξ < ϕ

(ξ) → ϕ

(ξ) ∈ Acc] ∨ α /∈ M ∨ Ω ≤ α

(i)

We claim

Prog

(Acc

(ii)

To prove (ii) we have the hypothesis

(∀ξ<

α)[ξ ∈ Acc

]

(iii)

and have to show

α ∈ Acc

(iv)

For α /

∈ M or Ω ≤ α (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 ρ

N F

+ · · · + ρ

we have ρ

∈ Acc by induction hypothesis and obtain ρ ∈ Acc by Lemma 3.7.12.

If ρ

∈ SC then we have ρ ≤ α or ρ ≤ ξ. If ρ ≤ ξ we get ρ ∈ Acc from ξ ∈ Acc. If ρ ≤ α we

have ρ

≤ µ for some µ ∈ SC (α). Since α ∈ M we have µ ∈ Acc and thence also ρ ∈ Acc.

Now assume ρ

∈ H \ SC. Then ρ =

N F

(ρ

). There are the following cases.

= α and ρ

< ξ. Then we obtain ϕ

(ρ

) ∈ Acc by (vii).

α < ρ

and ρ < ξ. Then ρ

∈ Acc follows from ξ ∈ Acc.

< α and ρ

< ϕ

(ξ). Then SC (ρ

) ∩ Ω is majorized by some µ ∈ SC (α) ∩ Ω ⊆ Acc

which means SC

(ρ

) ∩ Ω ⊆ Acc and therefore ρ

α. By (ii) we obtain ρ

∈ Acc

. By

induction hypothesis we have ρ

∈ Acc and which entails ϕ

(ρ

) ∈ Acc. This finishes the proof

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 Prog

(Acc

) and thence Acc

⊆ Acc

by (3.19). Together with β

∈ Acc this implies ϕ

(β) ∈ Acc.

3.7.15 Lemma

(ID

) Define Acc

Ω

α α /

∈ M ∨ (∃ξ ∈ K (α))[α ≤ ξ] ∨ ψ(α) ∈ Acc

Then we obtain Prog

(Acc

Ω

Proof

Assume

3. Ordinal analysis of non iterated inductive definitions

α ∈ field(<

) and (∀η<

α)[η ∈ Acc

Ω

(i)

We have to show

α ∈ Acc

Ω

(ii)

For α /

∈ M or (∃ξ ∈ K (α))[α ≤ ξ] (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

(ρ) ⊆ Acc by induction hypothesis and thence ρ ∈ Acc by Lemma 3.7.12 and Lemma 3.7.14.

If ρ

∈ SC then there is a ρ

such that K

(ρ

) ⊆ ρ

< α and ρ = ψ(ρ

). For ξ ∈ SC (ρ

) ∩ Ω we

either have ξ

= 0 or ξ =

N F

ψ(η) for some η. In the second case we get η ∈ K(ξ) ⊆ K(ρ

) ⊆ α

which implies ξ

= ψ(η) < ψ(α). Hence SC (ρ

) ∩ Ω ⊆ ψ(α). By induction hypothesis we

therefore obtain SC

(ρ

) ∩ Ω ⊆ Acc. Hence ρ

α and therefore ρ

∈ Acc

Ω

by (i). Since we

have K

(ρ

) ⊆ ρ

and just showed ρ

∈ M this implies ρ = ψ(ρ

) ∈ Acc.

3.7.16 Lemma (Condensation Lemma)

If K

(α) ⊆ α and α ∈ M then ID

(α, F ), im-

plies ID

ψ(α) ∈ Acc.

Proof

We especially have

(α, Acc

Ω

(i)

From (i) and Lemma 3.7.15 we obtain

(∀ξ<

α)[ξ ∈ 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 ID

(Ω + 1, F ) ∧ K(Ω + 1) ⊆ Ω + 1 ∧ Ω + 1 ∈ M.

Proof

Since SC

(Ω+1) = {0} and K(Ω+1) = ∅ we obviously have K(Ω+1) ⊆ Ω+1 ∧ Ω+1 ∈

M. Assuming Prog

(F ) we have to show (∀ξ<

Ω+1)[F (ξ)]. If ξ <

Ω we obtain SC (ξ) ⊆ Acc

and thus ξ

∈ Acc by Lemma 3.7.12 and Lemma 3.7.14. By Lemma 3.7.13 we get Prog

(F )

which then by (3.19) entails F

(ξ). So we have (∀ξ<

Ω)[F (ξ)] which by Prog

(F ) also implies

F (Ω).

3.7.18 Lemma

(α, F ) ∧ K(α) ⊆ α ∧ α ∈ M ⇒ ID

(ω

, F ) ∧ K(ω

) ⊆ ω

∧ ω

∈ M.

Proof

We show ID

(α, F ) ⇒ ID

(ω

, 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 ID

)

For every ordinal α < ψ

(ε

Ω+1

) there is a primitiv

recursive ordering

≺ such that ID

n ∈ Acc(≺) and α ≤ |n|

Acc(≺)

3.7. The lower bound

Proof

We have outlined in Theorem 3.7.7 that <

is primitive recursive. Defining a sequence

= Ω + 1 and ζ

n+1

= ω

we obtain by Lemma 3.7.17 and Lemma 3.7.18

(ζ

, F ) ∧ K(ζ

) ⊆ ζ

∧ ζ

∈ M

for all n. Hence ψ

(ζ

) ∈ Acc = Acc(<

) by the Condensation Lemma (Lemma 3.7.16). By

Observation 1.7.10 we have

|n|

Acc(<

)

= otyp

(n) = |n|

. Hence

|ψ(ζ

Acc(<

)

= ψ(ζ

)

and the claim follows because

sup

= ψ(ε

Ω+1

3.7.20 Corollary We have

||ID

|| = κ

= ψ(ε

Ω+1

) and ||ID

ext

|| = ||ID

ext

= κ

ext

ψ(ε

Ω+1

Index

Notations

EA, 5
∆

–formula, 5

PRA, 5
Prf

(i, v), 5

, 5

PRWO

(≺), 5

, 6

(≺, X), 8

||Ax||, 8
On, 8
α < β, 8
Lim, 8
R, 9

sup M, 9

ω, 9
en

, 9

otyp

(M), 9

H, 10

α =

N F

+ . . . + α

, 10

-number, 10

, 11

(β), 11

(α), 11

α =

N F

(η), 11

SC , 11
Γ

, 11

(α), 11

otyp

≺

(x), 12

otyp

(≺), 12

∼F , 12

D(N), 12

–type, 13

(F ), 13

F , 13

∆ , 14

∆

, 14

ω–completeness, 15

(F ), 15

, 17

<α

(S), 17

, 17

<α

, 17

|Γ|, 17

|n|

, 18

|ϕ|, 18

|x|

, 18

, 19

otyp

(s), 19

otyp

(T ), 19

(X, x), 19

T s, 20

≺

(X, x), 22

Acc

(≺), 22

Acc

(≺), 22

||Ax||

, 22

∆, 27

L(NT ), 28

, 28

S, 28
Sub, 28
Rec, 28
NT , 28

α
ρ

∆, 30

On, 32
a ≺ b, 32

α ⊆ X, 33

Prog(X), 33

TI(α, X), 33

J (X), 34

L(ID

), 37

, 37

Index

(ID

), 37

(ID

), 37

(G), 37

∞,ω

(NT ), 37

∞

(NT), 38

~t ∈ I

<α

, 39

par

(G), 41

par

(∆), 41

α
ρ

∆, 41

, 43

ψ(α), 43

Ω

–type, 44

, 49

, 50

δ(α), 50
K

(ξ), 52

SC, 52
H, 52
On, 52
K(a), 52

a ≺ b, 52

a ≡ b, 52

|a|

, 52

α <

β, 53

Acc, 53
α <

β, 53

Prog

(F ), 54

(α, F ), 54

M, 55
Acc

Ω

, 55

Index

Key–words

∨–Exporation, 42
B

EKLEMISHEV

, 6

ENTZEN

, 5

G ¨

ODEL

, 5

REISEL

, 5

OSTOWSKI

, 9

AIT

, 12

AIT

–language, 12

accessible part, 22
additive components, 10
additive normal form, 10
additively indecomposable ordinal, 10

Basic Elimination Lemma, 31
bounded set, 9
Boundedness Lemma, 43
Boundedness Theorem, 21

Cantor normal form, 10, 11
cardinal, 8
cardinality, 8
characteristic sequence, 13
clause

of an inductive definition, 16

closed, 9

in a regular ordinal, 9
under an operator, 16

closure ordinal

of a structure, 19
of an operator, 18

club, 9
Collapsing Lemma, 44
conclusion

of a clause, 16

Condensation Lemma, 56
continuous, 9
Controlled Tautology, 46
critical ordinal, 11

defining axioms

for I

, 37

for primitive recursive functions, 28

derivative, 11
diagram, 12

elementary Arithmetic, 5
Elimination Theorem, 32
enumerating function, 9
epsilon number, 10

epsilon0, 11
exponentiation

ordinal, 10

fixed–point, 16

the, 16
the, 18

formula

X–positive, 19

Gamma zero, 11
Generalized Induction, 47

identity axiom, 28
incompleteness, 35
induction, 28

transfinite, 8, 9

Induction Lemma, 29
inductive definition, 16

generalized, 18
generalized monotone, 16

inductively defined

by a set of clauses, 16

Inversion Lemma, 42

jump, 34

Kleene-Brouwer ordering, 23

limit ordinal, 8
limit ordinal (Lim), 8

Mathematical Induction, 5
Monotonicity Lemma, 47

node, 19
normal function, 9
Number Theory NT , 28

operator

F–definable, 18
elementarily definable, 18
elementary definable, 18
first order definable, 18
monotone, 16
positive, 19

order type,

otyp

, 9

ordinal, 8
ordinal analysis

of NT, 35

ordinal sum, 9

Index

path, 19
Predicative Elimination Lemma, 31
premise

of a clause, 16

proof by induction on the definition, 16
proof–theoretic ordinal, 8
pseudo

–sentence, 14

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)

Π + 1

–sentence, 15

unbounded set, 8, 9

validity relation, 13
validity relation, 14
Veblen function, 11
Veblen normal form, 11

Index

Bibliography

[1] P. A

CZEL

, H. S

IMMONS AND

S. S. W

AINER

(editors), Proof theory (Leeds 1990), Cam-

bridge University Press, Cambridge, 1992.

[2] A. B

ECKMANN AND

W. P

OHLERS

, 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. B

UCHHOLZ

, A simplified version of local predicativity, Proof theory (P. Aczel et al.,

editors), Cambridge University Press, Cambridge, 1992, pp. 115–147.

[4] S. R. B

USS

(editor), Handbook of Proof Theory, Studies in Logic and the Foundations of

Mathematics, North-Holland Publishing Company, 1998.

[5] G. G

ENTZEN

, Die Widerspruchsfreiheit der reinen Zahlentheorie, Mathematische An-

nalen, vol. 112 (1936), pp. 493–565.

[6]

, Neue Fassung des Widerspruchsfreiheitsbeweises f¨ur die reine Zahlentheorie,

Forschungen zur Logik und Grundlegung der exakten Wissenschaften, vol. 4 (1938),
pp. 19–44.

[7]

, Beweisbarkeit und Unbeweisbarkeit von Anfangsf¨allen der transfiniten Induktion in

der reinen Zahlentheorie, Mathematische Annalen, vol. 119 (1943), pp. 140–161.

[8] J.-Y. G

IRARD

, Proof theory and logical complexity, vol. 1, Bibliopolis, Naples, 1987.

[9] Y. N. M

OSCHOVAKIS

, Elementary induction on abstract structures, Studies in Logic and

the Foundations of Mathematics, vol. 77, North-Holland Publishing Company, Amsterdam,
1974.

[10] W. P

OHLERS

, Cut-elimination for impredicative infinitary systems I. Ordinal analysis

for ID

, Archiv f ¨ur 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. S

UTTE

, Proof theory, Grundlehren der mathematischen Wissenschaften, vol. 225,

Springer-Verlag, Heidelberg/New York, 1977.

Bibliography

[15] G. T

AKEUTI

, Proof theory, 2. ed., Studies in Logic and the Foundations of Mathematics,

vol. 81, North-Holland Publishing Company, Amsterdam, 1987.

Wyszukiwarka

Podobne podstrony:
Matlab Tutorial for Systems and Control Theory (MIT) (1999) WW
An Introduction to Conformal Field Theory [jnl article] M Gaberdiel (1999) WW
Social Theory across Disciplinary Boundaries Cultural Studies and Sociology 1999 Orville Lee
Ustawa z dnia 25 06 1999 r o świadcz pien z ubezp społ w razie choroby i macierz
brzuch 1999 2000
chojnicki 1999 20 problemy GP
(ebook PDF)Shannon A Mathematical Theory Of Communication RXK2WIS2ZEJTDZ75G7VI3OC6ZO2P57GO3E27QNQ
Goertzel Theory
Porty morskie i żegluga morska w Polsce w latach 1999 2001
ABS Octawia 1999
NLP for Beginners An Idiot Proof Guide to Neuro Linguistic Programming
Hawking Theory Of Everything
1999 05 05 0953
ED 1999 1 41
Badanie wahadła skrętnego, Studia, Pracownie, I pracownia, 7 Badanie drgań wahadła skrętnego {torsyj
Okręgi wojskowe od roku 1999, wiedza o siłach zbrojnych

więcej podobnych podstron