ファイル置き場 Sendai Logic Homepage speaker8

(1)

Florian Pelupessy

Department of Mathematics, Ghent University, Belgium

FACULTY OF SCIENCES

(2)

Overview

1 Introduction

What are phase transitions for unprovability?

2 Small examples

Ackermann function, Growing trees

3 _Orders

Monomial ideals

4 _Colours

unordered regressive Ramsey numbers, adjacent Ramsey

5 Concluding remarks

Florian Pelupessy Phase transitions for unprovability 2 / 49

(3)

✲

✻

Pressure

Temperature Liquid

Solid

Gas q

Figure: Phase transitions in physics

(4)

Phase transition:

at a threshold point a small change has a big consequence.

(5)

Phase transition:

at a threshold point a small change has a big consequence. Phase transition in logic:

1 Take an interesting theorem with a parameter.

(6)

Phase transition:

2 Find values of that parameter for which the theorem is provable and values for which it is unprovable.

(7)

Phase transition:

2 Find values of that parameter for which the theorem is provable and values for which it is unprovable.

3 Determine a threshold for that parameter where the theorem changes from unprovable to provable.

(8)

Peano Arithmetic

Take language L = {+, ×, <, 0, 1}. The first order theory of Peano Arithmetic consists of some ordinary rules for arithmetic:

Distributivity, associativity and commutativity of + and × with neutral elements 0 and 1 respectively.

<is a discrete linear order, with minimal element 0, 1 is the successor of 0.

x < y → x + z < y + z. And the axiom scheme for induction:

(9)

Peano Arithmetic

Take language L = {+, ×, <, 0, 1}. The first order theory of Peano Arithmetic consists of some ordinary rules for arithmetic:

Distributivity, associativity and commutativity of + and × with neutral elements 0 and 1 respectively.

<is a discrete linear order, with minimal element 0, 1 is the successor of 0.

x < y → x + z < y + z.

And the axiom scheme for induction: for every L-formula ϕ : [ϕ(0, ¯y) ∧ ∀x(ϕ(x, ¯y) → ϕ(x + 1, ¯y))] → ∀xϕ(x, ¯y).

(10)

fragments

Σn-formulas are formulas of the form:

∃x¹^{. . . x}ⁱ1∀y¹^{. . . y}ⁱ2∃ . . . ϕ

where there are n quantifiers and ϕ contains only bounded quantifiers. IΣnis PA with the induction scheme restricted to Σn-formulas.

(11)

Unprovability

G¨odel (1931): There exist L-theorems which are unprovable in PA. Since then interesting PA-unprovable theorems have been found, among them: Paris-Harrington strong Ramsey theorem, Paris and Kirby Hydra battles, Goodstein sequences, miniaturised Kruskal theorem and the Kanamori-McAloon principle (regressive Ramsey).

(12)

ordinals below ε

₀

Intuitive description of the ordinals below ε0: 0, 1, 2, 3, . . .

(13)

ordinals below ε

₀

Intuitive description of the ordinals below ε0: 0, 1, 2, 3, . . . , ω

(14)

ordinals below ε

₀

Intuitive description of the ordinals below ε0: 0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . .

(15)

ordinals below ε

₀

Intuitive description of the ordinals below ε0:

0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . . , ω + ω = ω · 2,

(16)

ordinals below ε

₀

0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . . , ω + ω = ω · 2,

ω· 3, ω · 4, . . . , ω · ω = ω²^,

(17)

ordinals below ε

₀

0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . . , ω + ω = ω · 2,

ω· 3, ω · 4, . . . , ω · ω = ω²^{, ω}³^{, ω}⁴^{, . . .}

(18)

ordinals below ε

₀

0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . . , ω + ω = ω · 2,

ω· 3, ω · 4, . . . , ω · ω = ω²^{, ω}³^{, ω}⁴^{, . . .}

ω^ω= ω1,

(19)

ordinals below ε

₀

0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . . , ω + ω = ω · 2,

ω· 3, ω · 4, . . . , ω · ω = ω²^{, ω}³^{, ω}⁴^{, . . .}

ω^ω= ω1, ω^ω

ω = ω2,

(20)

ordinals below ε

₀

0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . . , ω + ω = ω · 2,

ω· 3, ω · 4, . . . , ω · ω = ω²^{, ω}³^{, ω}⁴^{, . . .}

ω^ω= ω1, ω^ω

ω = ω2, ω^ω

ω^ω

= ω3, . . . ,

(21)

ordinals below ε

₀

0, 1, 2, 3, . . . , ω, ω + 1, ω + 2, . . . , ω + ω = ω · 2,

ω· 3, ω · 4, . . . , ω · ω = ω²^{, ω}³^{, ω}⁴^{, . . .}

ω^ω= ω1, ω^ω

ω = ω2, ω^ω

ω^ω

= ω3, . . . , ω_ω= ε0

(22)

ordinals below ε

₀

Important properties of these ordinals: They are well ordered.

Any ordinal α can be written in the Cantor Normal Form: α= ω^α¹_{· m}1+ · · · + ω^αⁿ· mⁿ^, where α > α1^>· · · > αⁿ ^{and the m}ⁱ^>^0.

(23)

ordinals below ε

₀

Important properties of these ordinals: They are well ordered.

Any ordinal α can be written in the Cantor Normal Form: α= ω^α¹_{· m}1+ · · · + ω^αⁿ· mⁿ^, where α > α1^>· · · > αⁿ ^{and the m}ⁱ^>^0.

They are used as a way to measure the logical strength of a theory.

(24)

Fast growing hierarchy

Define:

ω^α+1[x] = ω^α_{· x} ω^γ[x] = ω^γ[x] (α + ω^β)[x] = α+ (ω^β[x])

(25)

Fast growing hierarchy

Define:

ω^α+1[x] = ω^α_{· x} ω^γ[x] = ω^γ[x] (α + ω^β)[x] = α+ (ω^β[x]) and

F0(i) = i+ 1 Fα+1(i) = F_αⁱ(i)

F_γ(i) = F_γ[i](i) Where F_αⁱ denotes the i-times iteration of Fα.

(26)

Important fact

If a computable function is provably total in IΣn then it can be bounded by some function Fαwith α < ω_n−1.

If such a function is provably total in PA then it can be bounded by some function Fαwith α < ε0.

(27)

Ackermann

A0(i) = i+ 1 An+1(i) = Aⁱ_n(i)

A(i) = Ai(i)

Where Aⁱ_ndenotes the i-times iteration of An.

(28)

Ackermann

A0(i) = i+ 1 An+1(i) = Aⁱ_n(i)

A(i) = Ai(i)

Where Aⁱ_ndenotes the i-times iteration of An.

Ais total, but not provably so in IΣ1(notice that A = Fω).

(29)

Ackermann with parameter

Af,0(i) = i+ 1 Af,n+1(i) = A^f_f⁽ⁱ⁾_,n(i)

Af(i) = Af,i(i)

(30)

Ackermann with parameter

Af,0(i) = i+ 1 Af,n+1(i) = A^f_f⁽ⁱ⁾_,n(i)

Af(i) = Af,i(i)

Theorem (Kojman, Lee, Omri, Weiermann) Take fc(i) =^√^ci :

Afc is not provably total in IΣ1, but Alog is provably total in IΣ1

(31)

Growing trees

Examine the following process for l:

(32)

Growing trees

l+1 new leaves

z }| {

Step 1

(33)

Growing trees

l+2 new leaves

z }| {

(34)

Growing trees

l+3 new leaves

z }| {

Step 3

(35)

Growing trees

l+4 new leaves

z }| {

(36)

Growing trees

l+5 new leaves

z }| {

Step 5

(37)

Growing trees

l+6 new leaves

z }| {

(38)

Growing trees

l+7 new leaves

z }| {

Step 7

(39)

Growing trees

l+8 new leaves

z }| {

(40)

Growing trees

Step i: select a leaf

(41)

Growing trees

l+i new leaves

z }| {

(42)

Growing trees

Lemma (MKL)

For every h and l there exists a K such that every growing tree reaches height h within K steps.

Intuition: Every growing tree reaches any height.

(43)

Growing trees

Lemma (MKL)

For every h and l there exists a K such that every growing tree reaches height h within K steps.

Intuition: Every growing tree reaches any height. Theorem

MKL is unprovable in IΣ1.

(44)

Growing trees with parameter

Examine the following process for l and f :

Step i: select a leaf

(45)

Growing trees with parameter

Examine the following process for l and f :

f(l+i) new leaves

z }| {

(46)

Growing trees with parameter

Lemma (MKL^f)

For every f , h and l there exists a K such that every growing tree reaches height h within K steps.

(47)

Growing trees with parameter

Lemma (MKL^f)

For every f , h and l there exists a K such that every growing tree reaches height h within K steps.

Theorem

1 _MKL_id is unprovable in IΣ1,

2 _MKL_c is provable in IΣ1for constant function c.

(48)

Growing trees with parameter

Theorem Take fc(i) =^√^ci :

1 _MKL_f

c is unprovable in IΣ1, but

2 _MKL

log is provable in IΣ1.

(49)

Monomial ideals

Given field K and polynomial ring K [Xd, . . . , X₀, Y]. A monomial ideal is an ideal that is generated by monomials.

The degree of a monomial is the total degree.

The degree of a set of generators is the maximum of the degrees of its elements.

deg(I ) is the minimum of the degrees of the sets that generate I . Intuition: the degree of an ideal is the minimum degree necessary to be able to generate it.

(50)

Monomial ideals

Theorem (Maclagan 2001)

For every l , d there exists M such that for every sequence I1, . . . , IM of monomial ideals in K[Xd, . . . , X0, Y] with deg(In) ≤ l + n there are i < j with Ii_{⊇ I}j.

Intuition: Any sufficiently long linearly bounded sequence contains an ideal that is a subset of an earlier one.

(51)

Maclagan with parameter

Theorem (MMf)

For every f , l , d there exists M such that for every sequence I1, . . . , IM of monomial ideals in K[Xd, . . . , X0, Y] with deg(In) ≤ l + f (n) there are i < j with Ii_{⊇ I}j.

(52)

Maclagan with parameter

Theorem (MMf)

For every f , l , d there exists M such that for every sequence I1, . . . , IM of monomial ideals in K[Xd, . . . , X0, Y] with deg(In) ≤ l + f (n) there are i < j with Ii_{⊇ I}j.

Take fc(i) =^p^c log(i): Theorem (Pelupessy) MMf is

1 unprovable in IΣ2for f = fc, but

2 provable for f = log log.

(53)

Proof sketch:

First show that MMidis unprovable in the following manner: Associate with each ordinal < ω^ωmonomials in variables Xi.

(54)

Proof sketch:

Define Mα(l) as the maximal length of a bad sequence of ideals with generators from monomials that are associated with ordinals ≤ α.

(55)

Proof sketch:

Define Mα(l) as the maximal length of a bad sequence of ideals with generators from monomials that are associated with ordinals ≤ α. Notice, using induction, that Mα(h(l)) ≥ Fα(l) for some primitive recursive function h.

(56)

Proof sketch:

Then use this result to show that MM^√^c_logis unprovable: Take bad sequence I1, . . . IM from previously,

(57)

Proof sketch:

Define new sequence:

If_c(1), . . . , If_c(M)^.

(58)

Proof sketch:

Define new sequence:

If_c(1), . . . , If_c(M)^.

Use extra variables to ensure that the sequence becomes a bad sequence. (2c + 3 extra variables suffice).

(59)

Kanamori McAloon

Identify R with the set of its predecessors: R = {0, . . . , R − 1}. [R]^d is the set of d-element subsets of R.

(60)

Kanamori McAloon

For a colouring C : [R]²→ N a set H ⊆ R is homogeneous if C is constant on [H]²,

(61)

Kanamori McAloon

min-homogeneous if C (x, y ) = C (x, z) for all x, y , z ∈ H with x < y , x < z,

(62)

Kanamori McAloon

min-homogeneous if C (x, y ) = C (x, z) for all x, y , z ∈ H with x < y , x < z,

min_≺-homogeneous for a linear order ≺ on H if C (x, y) = C (x, z) for all x, y , z ∈ H with x ≺ y, x ≺ z.

(63)

Kanamori McAloon

Theorem (Ramsey)

For all l , c there exists R such that for any colouring C: [R]²_{→ c there} exists H of size l that is homogeneous for C .

(64)

Kanamori McAloon

Theorem (Ramsey)

For all l , c there exists R such that for any colouring C: [R]²_{→ c there} exists H of size l that is homogeneous for C .

Theorem (KM²)

For all l there exists R such that for any colouring C: [R]²_{→ N with} C(x, y ) ≤ min(x, y) there exists H of size l that is min-homogeneous for C .

(65)

unordered Kanamori McAloon

Theorem (uKM²)

For all l there exists R such that for any colouring C: [R]²_{→ N with} C(x, y ) ≤ min(x, y) there exists H of size l with linear order ≺ that is min_≺-homogeneous for C .

(66)

unordered Kanamori McAloon

Theorem (uKM²)

For all l there exists R such that for any colouring C: [R]²_{→ N with} C(x, y ) ≤ min(x, y) there exists H of size l with linear order ≺ that is min_≺-homogeneous for C .

Theorem

uKM²is unprovable in IΣ1.

(67)

unordered Kanamori McAloon with parameter

Theorem (uKM²f)

For all f , l there exists R such that for any colouring C : [R]²_{→ N with} C(x, y ) ≤ f (min(x, y)) there exists H of size l with linear order ≺ that is min_≺-homogeneous for C .

(68)

unordered Kanamori McAloon with parameter

Theorem (uKM²f)

For all f , l there exists R such that for any colouring C : [R]²_{→ N with} C(x, y ) ≤ f (min(x, y)) there exists H of size l with linear order ≺ that is min_≺-homogeneous for C .

Theorem (Pelupessy, Weiermann) Take f(i) = log i and fd(i) = ^√^di :

1 _uKM²

f_d is unprovable in IΣ1, but

2 _uKM²

f is provable in IΣ1.

(69)

Proof sketch

Show:

uKM^√d (Rc(m + 4)) _{≥ A}_c+1^√^d (m)

(70)

Proof sketch

Show:

uKM^√d (Rc(m + 4)) _{≥ A}_c+1^√^d (m)

↓ ↓ ↓

fast _{⇐ slow} fast

(71)

Proof sketch

uKM^√d (Rc(m + 4)) _{≥ A}_c+1^√^d (m)

Get two nice colourings C , D involving A_c+1^√^d .

Take the H of size m + 4 that is min_≺-homogeneous for C and homogeneous for D

Use the nice properties to see that one of the four <-largest elements of H is larger than A_c+1^√^d (m).

(72)

unordered Kanamori McAloon with parameter

Theorem (uKMf)

For all f , d , l there exists R such that for any colouring C : [R]^d_{→ N} with C(x, y ) ≤ f (min(x, y)) there exists H of size l with linear order ≺ that is min_≺-homogeneous for C .

(73)

unordered Kanamori McAloon with parameter

Theorem (uKMf)

For all f , d , l there exists R such that for any colouring C : [R]^d_{→ N} with C(x, y ) ≤ f (min(x, y)) there exists H of size l with linear order ≺ that is min_≺-homogeneous for C .

Define log^∗ to be the inverse of the tower function. Theorem (Pelupessy, Bovykin)

1 _uKM

log^k is unprovable in PA, but

2 _uKM

log^∗ is provable in PA.

(74)

Proof sketch

Construct a model of PA + ¬uKMlog^k^.

(75)

We call a colouring C : [R]^d _{→ N}^r limitedif max C (x) ≤ max x. Theorem (AR)

For every d , r there exists R such that for every limited colouring C: [R]^d_{→ N}^r there exist x1^<· · · < xd+1 with

C(x1, . . . , xd_{) ≤ C (x}2, . . . , x_d+1).

(76)

We call a colouring C : [R]^d _{→ N}^r limitedif max C (x) ≤ max x. Theorem (AR)

For every d , r there exists R such that for every limited colouring C: [R]^d_{→ N}^r there exist x1^<· · · < xd+1 with

C(x1, . . . , xd_{) ≤ C (x}2, . . . , x_d+1).

Theorem (Friedman)

Adjacent Ramsey is unprovable in PA.

(77)

We call a colouring C : [R]^d _{→ N}^r f -limitedif max C (x) ≤ f (max x). Theorem (AR^f)

For every d , r there exists R such that for every f -limited colouring C: [R]^d_{→ N}^r there exist x1<· · · < xd+1 with

C(x1, . . . , xd_{) ≤ C (x}2, . . . , xd+1).

(78)

We call a colouring C : [R]^d _{→ N}^r f -limitedif max C (x) ≤ f (max x). Theorem (AR^f)

For every d , r there exists R such that for every f -limited colouring C: [R]^d_{→ N}^r there exist x1<· · · < xd+1 with

C(x1, . . . , xd_{) ≤ C (x}2, . . . , xd+1).

Theorem (Pelupessy)

1 _AR

log^k is unprovable in PA, but

2 _AR_log_∗ is provable in PA.

(79)

Proof sketch

Take a limited colouring C : [R]^d_{→ N}^r (d > k). Define a new colouring D(x) = C (log^kx1, . . . ,log^kxd). This colouring will be log^k-limited, but may contain undesired identical elements. This can be solved by adding an extra coordinate, using estimates for ARc (roughly a tower of exponentials of height k).

(80)

Some of these results have been sharpened: Theorem

1 _MKL_f is unprovable in IΣ1 if f(i) = ^A−1(i)^√i , but

2 _MKL_f is provable in IΣ1if f(i) = ^A−^c¹⁽ⁱ⁾^√i .

(81)

2 _MKL_f is provable in IΣ1if f(i) = ^A−^c¹⁽ⁱ⁾^√i . Theorem

Take f_α(i) = ^{F −1}^α ⁽ⁱ⁾^plog(i), then MMfα is

1 unprovable in IΣ2for α= ω^ω, but

2 provable for α < ω^ω.

(82)

2 _MKL_f is provable in IΣ1if f(i) = ^A−^c¹⁽ⁱ⁾^√i . Theorem

Take f_α(i) = ^{F −1}^α ⁽ⁱ⁾^plog(i), then MMfα is

1 unprovable in IΣ2for α= ω^ω, but

2 provable for α < ω^ω.

Theorem

1 _uKM²

f is unprovable in IΣ1for f(i) = ^A−1(i)^√i , but

2 _uKM²

f is provable in IΣ1for f(i) = ^A−^c¹⁽ⁱ⁾^√i .

(83)

Take fα(i) = log^F^α⁻¹⁽ⁱ⁾(i). Conjecture

1 _uKM_f

ε0 is unprovable in PA, but

2 _uKM_f

α is provable in PA if for α < ε0.

(84)

Take fα(i) = log^F^α⁻¹⁽ⁱ⁾(i). Conjecture

1 _uKM_f

ε0 is unprovable in PA, but

2 _uKM_f

α is provable in PA if for α < ε0.

Motivation: this would correspond with existing results for Kanamori McAloon.

(85)

The proof of PA-unprovability of adjacent Ramsey can be adapted into showing that for fixed k > 1 this theorem is unprovable in IΣ_k−1. What are the corresponding phase transitions?

(86)

Thank you for listening.