ファイル置き場 Sendai Logic Homepage

(1)

Systems

Ryota Akiyoshi

Department of Philosophy Keio University

4 June 2010

(2)

Introduction

Aim of this talk: to explain some basic ideas of proof theory (esp. cut-elimination theorems) for impredicative systems like_Π¹₁-analysis.

Ryota Akiyoshi Introduction to Proof Theory for Impredicative Systems

(3)

Plan of this talk:

1

Cut-elimination theorem for PA

^∞

2

Cut-elimination theorem for BI

^Ω

3

Relationship between finitary proof theory

and infinitary proof theory

(4)

Introduction

Some history of proof theory (ordinal analysis):

The birth of proof theory (consistency proof) by D. Hilbert (ε-substitution).

(5)

The founder of ordinal analysis via cut-elimination: G. Gentzen (consistency proof by c.e. theorem for empty sequent).

(6)

Introduction

Takeuti succeeded ordinal analysis for impredicative subsystems of analysis likeΠ¹₁-CA and∆¹₂-CA.

(7)

Takeuti succeeded ordinal analysis for impredicative subsystems of analysis likeΠ¹₁-CA and∆¹₂-CA. German school (Sch ¨utte, Buchholz, Pohlers, J ¨ager) developed “infinitary proof theory” by proving Takeuti’s results using more perspicuous method (_ω-rule,Ω-rule, local predicativity).

(8)

Introduction

Takeuti succeeded ordinal analysis for impredicative subsystems of analysis likeΠ¹₁-CA and∆¹₂-CA. German school (Sch ¨utte, Buchholz, Pohlers, J ¨ager) developed “infinitary proof theory” by proving Takeuti’s results using more perspicuous method (_ω-rule,Ω-rule, local predicativity).

The recent breakthrough of ordinal analysis up toΠ¹₂-CA by Rathjen and Arai: proof theory of set theory, especially KPM, KP +Π³-Reflection, ...

(9)

Finitary proof theory by Gentzen-Takeuti-Arai and infinitary proof theory by Sch ¨utte-Buchholz-Pohlers-Rathjen.

Advantages of infinitary proof theory:

1 it is easy to understand cut-elimination theorems,

2 ordinal notations are “read off” from cut-elimination procedures.

In this talk we explain two major methods: _ω-rule (Sch ¨utte) and_Ω-rule (Buchholz).

(10)

Idea of_ω-rule

ω-arithmeticPA^∞is obtained by replacing induction axiom by the followinginfinitaryrule:

A(0), A(1), ...for all n ∈ω

∀xA

The point is that every natural number has its canonical name (numeral) unlike sets.

ω-rule satisfies thesubformula property, so the full cut-elimination theorem will hold forPA^∞while Gentzen proved the partial cut-elimination theorem forPAin 1938. G. Gentzen, “Neue Fassung des Widerspruchsfreiheitsbeweises fuer die reine Zahlentheorie”, 1938.

(11)

Definition

LetLbe the language for first-order arithmetic containing

¬,^V,^W, ∀, ∃.

SincePA^∞contains_ω-rule, we considerLwithout free number variables.

Negation is defined by de Morgan’s laws:

¬(A ∧ B) := ¬A ∨ ¬B,¬(A ∨ B) := ¬A ∧ ¬B,¬∀xA := ∃x¬A,

¬∃xA := ∀x¬A.

(12)

Infinitary SystemPA^∞

Definition

¬,^V,^W, ∀, ∃.

¬(A ∧ B) := ¬A ∨ ¬B,¬(A ∨ B) := ¬A ∧ ¬B,¬∀xA := ∃x¬A,

¬∃xA := ∀x¬A.

All systems in this talk are defined in the style of Tait’s calculus (one-sided sequent calculus).

Γ(or∆, . . .) denotes a set of formulas.

Only principal and minor formulas are explicitly shown, and weakning and contraction are implicitly assumed.

(13)

Definition

¬,^V,^W, ∀, ∃.

¬(A ∧ B) := ¬A ∨ ¬B,¬(A ∨ B) := ¬A ∧ ¬B,¬∀xA := ∃x¬A,

¬∃xA := ∀x¬A.

All systems in this talk are defined in the style of Tait’s calculus (one-sided sequent calculus).

Γ(or∆, . . .) denotes a set of formulas.

Only principal and minor formulas are explicitly shown, and weakning and contraction are implicitly assumed.

FormulaAor¬AwhereAis atomic is called a literal, TRUE := the set of all true literals.

(14)

Infinitary SystemPA^∞

Definition

Inference rules ofPA^∞:

(Ax_∆)∆where∆= {A} ⊆ TRUE or ∆= {C, ¬C}

(^V_A₀_∧A₁)^A⁰ ^A¹ A₀∧ A₁ ⁽

W_k

A0∧A1⁾

A_k

A₀∨ A₁ ^{where k}^{∈ {0, 1}}

(^V_∀xA). . . A(x/n) . . . for all n ∈ω

∀xA ⁽

W_k

∃xA⁾

A(x/k)

∃xA ^{where k}^∈^ω

(Cut_A)^A _/0^¬A

(15)

Definition

rk(A)is defined as follows.

1 _{rk(A) := 0}_if_Ais a literal.

2 rk(A ∧ B) := rk(A ∨ B) = max(rk(A), rk(B)) + 1.

3 rk(∀xA(x)) := rk(∃xA(x)) = rk(A(0)) + 1.

Definition

LetI be an inference symbol andda derivation inPA^∞. Then dg(I)anddg(d)are defined as follows.

1 dg(I) := rk(C) + 1ifI= Cut_C.

2 _{dg(I) := 0}_otherwise. 3 _dg(I(d_τ₎_τ

∈I) := sup({dg(I)} ∪ {dg(d_τ)|τ ∈ I}).

(16)

Cut-Elimination Theorem forPA^∞

We writed⊢mΓ^ifd is a derivation whose end-sequent is_Γand cut-rank is≤ m.

Theorem

We define an operator^R_Csuch that

ifd0⊢mΓ,C,d1⊢mΓ, ¬C^andrk(C) ≤ m, then^RC(d0, d1) ⊢mΓ^.

Proof. By induction ond0^andd1. Consider only the crucial cases:

Case 1.

Ifd₀= Ax_C,¬C, thend₀⊢_mΓ^′, ¬C,C. Thus¬C ∈Γ. We define R_C_(d₀_{, d}₁_{) := d}₁_⊢_m_Γ.

Case 2.

Assume thatd0=^V_∀xA(d0i)_i∈_ω andd1=^W^k_∃xA(d10).

(17)

Thend_0i⊢_mΓ, A(i), ∀xA(x)for alli∈_ω andd₁₀⊢_mΓ, ¬A(k), ∃x¬A. By IH, we have^R_C(d0k, d1) ⊢mΓ, A(k)and

R_C_(d₀_{, d}₁₀_{) ⊢}_mΓ, ¬A(k). Thus we obtain the required derivation by applying a new cut with its cut-formulaA(k).

R_C_(d₀_{, d}₁_{) := Cut}_A(k)_(R_C_(d_0k_{, d}₁_{), R}_C_(d₀_{, d}₁₀_{)) ⊢}_m_Γ. Note thatrk(A(k)) < rk(∀xA) ≤ m.

(18)

Cut-Elimination Theorem forPA^∞ We can define an operator^E reducing cut-rank by 1. Theorem

We can define an operator^E on derivations inPA^∞such that Ifd⊢_m+1Γ, then^E(d) ⊢_mΓ.

Proof. Letd beCutC(d0, d1). Then^E(d)is defined using^R. E_{(d) := R}_C_{(E (d}₀_{), E (d}₁_)).

Moreover we can eliminate all cuts if we want. Theorem

We can define an operator^E_ω on derivations inPA^∞such that Ifd⊢_ωΓ^{, then}^Eω^{(d) ⊢}0Γ^.

Proof. By induction ond. Note that^E_ω is defined byarbitrary finite applications of^E.

(19)

As Sch ¨utte proved, we can define an embedding map()^∞from PAintoPA^∞such that

Theorem

Ifd⊢Γ^whered∈ PAand_Γ: closed, thend^∞⊢^<_m^ω⁺^ωΓ^{for some} m∈_ω.

Moreover, ifd₀⊢^α_mΓ,C,d₁⊢^β_mΓ, ¬C andrk(C) ≤ m, then R_C_(d₀_{, d}₁_{) ⊢}^α_m^♯^β _Γ.

So, ifd⊢^α_m+1, then^E ⊢²_m^α Γ.

Thus we can understand why Gentzen used transfinite induction up to_ε₀ because

ε0= sup(2n(ω+ω)) where20(α) :=α ^and2_m+1(α) = 2²^m⁽^α⁾.

(20)

Plan of this talk:

1 Cut-elimination theorem forPA^∞

2

Cut-elimination theorem for BI

^Ω

3 Relationship between finitary proof theory and infinitary proof theory

(21)

Consider the parameter-free_Π¹₁-CA for the sake of simplicity(BI) : if∀XA(X), ∃XA(X)are formulas, thenA(X) contains no second-order quantifier (arithmetical) and no free predicate variable other thanX.

The systemBIcontains rules for first-order logical

connectives, arithmetical axiom,Cut and the following rules for second-order quantifiers^：

A(Y )

∀XA(X) V

∀XA(X)

¬A(T )

∃X¬A(X) WT

∃X¬A(X)

WT

∃X¬A(X)is just a parameter-freeΠ¹₁-CA.

(22)

Problem of Impredicativity and Cut-Elimination

Consider the following derivationd : the typical case of impredicative cut whereΓis a set of restricted formulas like 1=1:

... Γ, A(X), ∀XA(X)

Γ, ∀XA(X) V

∀XA(X)

...

Γ, ¬A(T ), ∃X¬A(X) Γ, ∃X¬A(X)

W_T

∃X¬A(X)

Γ ^Cut

(23)

For example, Takeuti transformsdintored(d)by replacing Π¹₁-CA by the substitution ruleSub^X_T and newCut:

... Γ, A(X), ∀XA(X)

Γ, ∀XA(X)

... Γ, A(X), ∀XA(X)

... Γ, ∃X¬A(X) Γ, A(X)

Γ,A(T ) ^Sub

X T

...

Γ,¬A(T ), ∃X¬A(X) Γ, ∃X¬A(X) ^Cut

Γ ^Cut

(24)

Question : why this cut-elimination process terminates ? In what sense the transformed derivationred(d)is simpler than the original derivationd?

cf. T. Arai, “A subsystem of classical analysis proper to Takeuti’s reduction method forΠ¹₁-Analysis”, RIMS Kokyuroku, 1984. Obvious idea 1 : the number of cut-rules

(25)

=⇒No: new cuts are inserted inred(d).

(26)

Obvious idea 2 : the length (or height) of derivation

(27)

Obvious idea 2 : the length (or height) of derivation

=⇒No: the length ofred(d)seems to be longer thand.

(28)

Obvious idea 3: how about logical complexity of cut-formulas ?

cf. Gentzen’s proof of the cut-elimination theorem for first-order logic or predicative system or the definition of R_C_for_PA^∞_.

(29)

=⇒No: the logical complexity of the new cut formulaA(T ) may be bigger than one of∀XA(X)(impredicativity of comprehension axiom).

(30)

How about Takeuti’s answer to this question ?

(31)

How about Takeuti’s answer to this question ?

=⇒The ordinal diagram assigned tored(d)is smaller (in some sense) than one assigned tod.

(32)

But the system of ordinal diagrams is very complicated. So it is not so easy to answer to this question in the case of Takeuti’s reduction.

(33)

But the system of ordinal diagrams is very complicated. So it is not so easy to answer to this question in the case of Takeuti’s reduction.

Ω-rule is a more perspicuous method.

(34)

Ω-rule

Buchholz introduced hisΩ-rule in his Habilitationschrift (1977).

He (and Sch ¨utte) usedΩ-rule for ordinal analysis of iterated inductive definition and subsystem of analysis up to_∆¹₂-CA +BR:

1 W. Buchholz, “TheΩ_µ+1-rule”, Iterated Inductive Definitions and Subsystems of Analysis, S. Feferman, W. Pohlers and W. Sieg (editors), LNM 897, Springer-Verlag.

2 W. Buchholz and K.Sch ¨utte, Proof Theory of Impredicative Subsystems of Analysis, Bibliopolis, 1988.

(35)

Pohlers introduced another method of “local predicativity”, which has been used for ordinal analysis ofID_<_µ,_Π¹₁-CA, Π³-Reflection,...

Ω-rule is very intuitive and the cut-elimination procedure can be defined independently of ordinal notations although the method of local predicativity is more uniform.

(36)

Ω-rule

Idea ofΩ_¬∀XA(X)^：

1 _{Γ, ¬∀XA}is equivalent to∀XA →Γ.

2 _{Proof of}_{∀XA →}_Γ_：a function from any proof of∀XAinto a proof ofΓ(BHK-reading).

3 Thus, when we have a proof ofΓ,∆for any cut-free proof of

∀XA,∆, we can assertΓ, ¬∀XA.

(37)

Idea ofΩ_¬∀XA(X)^：

1 _{Γ, ¬∀XA}is equivalent to∀XA →Γ.

2 _{Proof of}_{∀XA →}_Γ_：a function from any proof of∀XAinto a proof ofΓ(BHK-reading).

3 Thus, when we have a proof ofΓ,∆for any cut-free proof of

∀XA,∆, we can assertΓ, ¬∀XA.

The definition of_Ω-rule proceeds by iterated inductive definition:

1 First we define the set of cut-free arithmetical proofs: cut-free_ω-arithmetic.

2 Ω-rule is defined by quantifying over such cut-free arithmetical proofs.

This construction is similar to Kleene’s constructive ordinals.

(38)

Ω-rule

Our formulation ofΩ-rule is due to Buchholz:

W. Buchholz, “Explaining the Gentzen-Takeuti reduction steps”, AML, 2001.

Our formulation ofΩ-rule corresponds toΩ1-rule in the book by Sch ¨utte and Buchholz.

(39)

Our formulation ofΩ-rule is due to Buchholz:

W. Buchholz, “Explaining the Gentzen-Takeuti reduction steps”, AML, 2001.

Our formulation ofΩ-rule corresponds toΩ1-rule in the book by Sch ¨utte and Buchholz.

Assume that we have defined the set of arithmetical proofs (PA^∞without cut).

The systemBI^Ωis defined by adding_Ωand_Ωe-rules. In what follows, let

...

∆, A(X)

be a cut-free proof withoutΩ,Ω^e of the sequent∆, A(X) where_∆is arithmetical andX does not occur free in_∆.

(40)

Ω-rule

(Ω¬∀XA) ( _..

∆, A(X). )

... . . .∆. . .

¬∀XA ^{( e}^Ω^¬∀XA⁾ A(X)

( _..

∆, A(X). )

... . . .∆. . .

/0 ^{!X !}

(41)

(Ω¬∀XA) ( _..

∆, A(X). )

... . . .∆. . .

¬∀XA ^{( e}^Ω^¬∀XA⁾ A(X)

( _..

∆, A(X). )

... . . .∆. . .

/0 ^{!X !}

Ω-rule is used to interpret_Π¹₁-CA.

Ωe_¬∀XAis a combination ofΩ_¬∀XA(X),^V_∀XA,Cut_∀XA(X): hidden impredicative cut.

The other inference rules ofBI^Ωare ones for first-order connectives, arithmetical axiom,Cut, and a rule for second-order universal quantifier:

A(Y )

∀XA(X) V

∀XA(X)

(42)

Cut-Elimination Theorem forBI^Ω rk(C): the logical complexity of a formulaCso that rk(∀XA(X)) = rk(∃XA(X)) = 0.

dg(d): the maximal logical complexity of cut-formulas occurring ind.

We write⊢mΓif there is a derivationdsuch that its end-sequent isΓanddg(d) ≤ m.

Theorem

There is an operator^R_Csuch that

Ifd₀⊢_mΓ,C,d₁⊢_mΓ, ¬Candrk(C) ≤ m, then^R_C(d₀, d₁) ⊢_mΓ. Proof. By double induction ond₀andd₁.

R_Celiminates cuts other than impredicative cut in the standard way.

(43)

rk(C): the logical complexity of a formulaCso that rk(∀XA(X)) = rk(∃XA(X)) = 0.

dg(d): the maximal logical complexity of cut-formulas occurring ind.

We write⊢mΓif there is a derivationdsuch that its end-sequent isΓanddg(d) ≤ m.

Theorem

There is an operator^R_Csuch that

Ifd₀⊢_mΓ,C,d₁⊢_mΓ, ¬Candrk(C) ≤ m, then^R_C(d₀, d₁) ⊢_mΓ. Proof. By double induction ond₀andd₁.

R_Celiminates cuts other than impredicative cut in the standard way. The crucial case is impredicative cut in which the

cut-formula is second-order and introduced by^V_∀XAandΩ. Then^R replaces it by “hidden” impredicative cut_Ω.e

(44)

Cut-Elimination Theorem forBI^Ω

Π¹₁-CA inBIis of the form whered₀is the subderivation of Γ, ¬A(T ), ¬∀XA(X).

...

Γ, ¬A(T ), ¬∀XA(X) Γ, ¬∀XA(X)

This derivation is embedded intoBI^Ωin the following way: ...

∆, A(X)

∆, A(T ) ^S^T^X

...

Γ, ¬A(T ), ¬∀XA . . .Γ,∆, ¬∀XA . . . ^R^{A(T )}

Γ, ¬∀XA ^Ω

(45)

As before we can define the operation reducing cut-rank by 1 is defined inBI^Ω using the one-step reduction operator^R_C. Theorem

Ifd⊢_m+1Γ, then^E(d) ⊢_mΓ(Cut-Reduction Theorem). Proof.^E(CutC(d0, d1)) := RC(E (d0), E (d1)).

Again we can eliminate all cuts if we want. Theorem

We can define an operator^E_ω on derivations inBI^Ωsuch that Ifd⊢_ωΓ, then^E_ω(d) ⊢₀Γ.

(46)

Cut-Elimination forBI^Ω

Letd∈ BI^Ω, thendg(E_ω(d)) = 0. But^E_ω(d)may contain_Ωe !

(47)

Letd∈ BI^Ω, thendg(E_ω(d)) = 0. But^E_ω(d)may contain_Ωe ! In fact we can eliminate_Ωe (collapsing theorem).

(48)

Finally, we can define the operator^D eliminating hidden cutΩ^e as Buchholz did.

Theorem

Ifd⊢₀ΓandΓis arithmetical, then^D(d)is a derivation without Ω, eΩof the sequentΓ(Collapsing Theorem).

Proof. By induction ond.

The only crucial case islast(d) = eΩ. For the sake of simplicity we assume thatdcontains only the indicated_Ωe :

( eΩ¬∀XA⁾

... Γ, A(X)

( _..

∆, A(X). )

... . . .Γ,∆. . . Γ ^{!X !}

(49)

Since_Γis arithmetical andd0⊢0Γis cut-free, let’s take_Γas_∆. In other words,d₀can be regarded as “input” ofΩ. Then we^e can find the following subderivationdd0 ^of^d:

( _.. Γ, A(X).

)

... Γ,∆ Note thatΓ,∆=Γ. Thus we define

D_{(d) := d}_d

0^.

In general case, subderivationsd0, d_d₀ may contain_Ωe. So, using IH, we define

D_{(d) := D(d}_D_(d

0^)).

(50)

Combining these results, we have the cut-elimination theorem for arithmetical sequents:

Corollary

Letd∈ BI^Ω and whose end-sequent is arithmetical. Then there isd^′⊢0Γ^{such that}d^′ does not contain_{Ω, e}_Ω.

By replacingΠ¹₁-CA byΩ-rule, we can extend the embedding map toBI.

Theorem

Ifd⊢Γwhered∈ BIandΓ: closed, thend^∞⊢_mΓfor some m∈_ω.

The proof theoretic strength ofBIis equal to one ofID₁ (the Howard ordinal):

|BI| = |ID₁| =_ψ_ε_Ω+1(0).

(51)

1 Cut-elimination theorem forPA^∞

2 Cut-elimination theorem forBI^Ω

3

Relationship between finitary proof theory

and infinitary proof theory

(52)

Embedding function fromBItoBI^Ω Now we explain the relationship between finitary proof theory and infinitary proof theory.

Wilfried Buchholz, “Explaining the Gentzen-Takeuti reduction steps”, AML, 2001.

Two rulesE, Dcorresponding to^E, D are added toBI. ΓΓ ^E ^ΓΓ ^D

The embedding function()^∞fromBItoBI^Ωis extended such that^：

1 _Π¹

1^-CA^=⇒^Ω-rule

2 impredicative cut=⇒ eΩ

3 _E_{=⇒ E}

4 _D_{=⇒ D}

5 _SubX

T^{=⇒ S}T^X

(53)

Recall the transformed derivationred(d). We add the rules E, Dcorresponding^E, D tored(d)whenSub^X_T is used.

... Γ, A(X), ∀XA(X)

Γ, ∀XA(X) V

∀XA(X)

... Γ, A(X), ∀XA(X)

... Γ, ∃X¬A(X) Γ, A(X)

Γ, A(X) ^E^m+1 Γ, A(X) ^D Γ, A(T ) ^Sub^X^T

...

Γ, ¬A(T ), ∃X¬A(X) Γ, ∃X¬A(X)

Γ

(54)

Interpretation of Takeuti’s Reduction

In the embedded derivationd^∞∈ BI^Ωwe have a proof of Γ,∆foranycut-free proof of∆, A(X).

... Γ, A(X), ∀XA(X)

... Γ, ∃X¬A(X) Γ, A(X)

... Γ, ∀XA(X)

...

∆, A(X)

∆, A(T ) ^S^T^X

...

Γ, ¬A(T ), ∃X¬A(X) Γ,∆, ∃X¬A(X)

. . .Γ,∆, . . .

Γ ^Ω^e

(55)

In the embedded derivationd^∞∈ BI^Ωwe have a proof of Γ,∆foranycut-free proof of∆, A(X).

... Γ, A(X), ∀XA(X)

... Γ, ∃X¬A(X) Γ, A(X)

... Γ, ∀XA(X)

...

∆, A(X)

∆, A(T ) ^S^T^X

...

Γ, ¬A(T ), ∃X¬A(X) Γ,∆, ∃X¬A(X)

. . .Γ,∆, . . .

Γ ^Ω^e

Let the following subderivation ofred(d)beh. ...

Γ, A(X), ∀XA(X)

... Γ, ∃X¬A(X) Γ, A(X)

Γ, A(X) ^E^m+1 Γ, A(X) ^D

(56)

Theorem

red(d)^∗is one of the immediate subderivations ofd^∗, which is indexed byh^∗.

Proof.

We show thath^∗is one of given derivations of_{∆, A(X).} Ind^∗,

...

∆, A(X) is

1 _cut-free, 2 _without_{Ω, e}_Ω_,

3 _∆is arithmetical andX does not occur free in∆. We check thath^∗satisfies these conditions.

(57)

1 _First,_h∗ does not contain cut,Ω, eΩbecause ofE, Dinh.

(58)

2 Next, we take (arithmetical)Γas∆.

(59)

2 Next, we take (arithmetical)Γas∆.

3 _Finally,_X does not occur free in∆becauseX is the eigenvariable in the original derivationd.

Thusred(d)^∗is a subderivation ofd^∗, which is indexed byh^∗.

(60)

... Γ, ∀XA(X)

... Γ, A(X), ∀XA(X)

... Γ^{, ∃X¬A(X)} Γ, A(X)

Γ, A(X) ^E^m+1 Γ, A(X) ^D Γ, A(T ) ^S^T^X

...

Γ, ¬A(T ), ∃X¬A(X) Γ, ∃X¬A(X)

Γ

... Γ, A(X), ∀XA(X)

... Γ, ∃X¬A(X) Γ, A(X)

... Γ, ∀XA(X)

...

∆, A(X)

∆, A(T ) ^S^T^X

...

Γ, ¬A(T ), ∃X¬A(X) Γ,∆, ∃X¬A(X)

. . .Γ,∆, . . .

Γ ^Ω^e