ファイル置き場 Sendai Logic Homepage 100430sanders slide

Unbounded Arithmetic

Sam Sanders & Andreas Weiermann

Department of Pure Mathematics, Ghent University, Belgium

Tohoku University, April 30, 2010

FACULTY OF SCIENCES

Bounded arithmetic vs. Peano arithmetic

Bounded arithmetic vs. Peano arithmetic

✲ . . . IΣn IΣn+1 . . . PA (=∪nIΣn)

IΣ1 IΣ2

IΣn= Q + Σn-IND

Bounded arithmetic vs. Peano arithmetic

✲ . . . IΣn IΣn+1 . . . PA (=∪nIΣn)

IΣ1 IΣ2

IΣn= Q + Σn-IND (base theory Q plus induction for Σn-formulas)

Bounded arithmetic vs. Peano arithmetic

✲ . . . IΣn IΣn+1 . . . PA (=∪nIΣn)

IΣ1 IΣ2

IΣn= Q + Σn-IND (base theory Q plus induction for Σn-formulas)

✲ . . . ^T2^{n T}2ⁿ⁺¹ . . . T^{2 (= ∪nT}2ⁿ⁾

T₂¹ T₂²

T₂ⁿ= BASIC + Σ^b_n-IND

Bounded arithmetic vs. Peano arithmetic

✲ . . . IΣn IΣn+1 . . . PA (=∪nIΣn)

IΣ1 IΣ2

IΣn= Q + Σn-IND (base theory Q plus induction for Σn-formulas)

✲ . . . ^T2^{n T}2ⁿ⁺¹ . . . T^{2 (= ∪nT}2ⁿ⁾

T₂¹ T₂²

T₂ⁿ= BASIC + Σ^b_n-IND (base theory plus induction for Σ^b_n-formulas)

Bounded arithmetic vs. Peano arithmetic

✲ . . . IΣn IΣn+1 . . . PA (=∪nIΣn)

IΣ1 IΣ2

IΣn= Q + Σn-IND (base theory Q plus induction for Σn-formulas)

✲ . . . ^T2^{n T}2ⁿ⁺¹ . . . T^{2 (= ∪nT}2ⁿ⁾

T₂¹ T₂²

T₂ⁿ= BASIC + Σ^b_n-IND (base theory plus induction for Σ^b_n-formulas) T₂= ∪n^T₂ⁿ= Bounded Arithmetic

A quote by Richard Kaye

Many authors have emphasized the analogies between the fragments Σ^b_n-IND of [Bounded Arithmetic] and the fragments

IΣn of Peano arithmetic. Sometimes this is helpful, but often one feels that the bounded hierarchy of theories is of a rather

different nature and new techniques must be developed to answer the key questions concerning them.

A quote by Richard Kaye

Many authors have emphasized the analogies between the fragments Σ^b_n-IND of [Bounded Arithmetic] and the fragments

IΣn of Peano arithmetic. Sometimes this is helpful, but often one feels that the bounded hierarchy of theories is of a rather

different nature and new techniques must be developed to answer the key questions concerning them.

We show that Bounded Arithmetic (BA) and Peano Arithmetic (PA) are indeedfundamentallydifferent.

We propose an axiomatization of PA inspired by BA.

Two questions about the logarithm

Two questions about the logarithm

1) Is the log function unbounded?

Two questions about the logarithm

1) Is the log function unbounded? Just look at the graph. . .

0 1 2 3 4 5 6 7 8 9 10

-1 -0,5 0,5 1

y= log x Yes!

Two questions about the logarithm

1) Is the log function unbounded? Yes!

2) Would you use this fact to prove P = NP or P 6= NP?

Two questions about the logarithm

1) Is the log function unbounded? Yes!

2) Would you use this fact to prove P = NP or P 6= NP? Come again?

Two questions about the logarithm

1) Is the log function unbounded? Yes!

2) Would you use this fact to prove P = NP or P 6= NP? Come again?

——

The log function can be bounded!

Two questions about the logarithm

1) Is the log function unbounded? Yes!

2) Would you use this fact to prove P = NP or P 6= NP? Come again?

——

The log function can be bounded!

Define |x| := ⌈log₂(x + 1)⌉ and T2 as usual. Then T2 6⊢(∀x)(∃y )^|y | > x^ (Parikh’s theorem).

Two questions about the logarithm

1) Is the log function unbounded? Yes!

2) Would you use this fact to prove P = NP or P 6= NP? Come again?

——

The log function can be bounded!

Define |x| := ⌈log₂(x + 1)⌉ and T2 as usual. Then T2 6⊢(∀x)(∃y )^|y | > x^ (Parikh’s theorem).

Thus, there is a model of BA where (∃x)(∀y )^|y | ≤ x^, i.e. |x| is bounded.

First difference between BA and PA

Despite this ‘strange’ property, the logarithm is essential to BA:

First difference between BA and PA

Despite this ‘strange’ property, the logarithm is essential to BA:

Σ^b_n-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|).

First difference between BA and PA

Despite this ‘strange’ property, the logarithm is essential to BA:

Σ^b_n-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|).

✲ . . . ^T2^{n T}

n+1

2 . . . T^{2 (= ∪nT}2ⁿ⁾

T₂¹ T₂²

First difference between BA and PA

Despite this ‘strange’ property, the logarithm is essential to BA:

Σ^b_n-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|).

✲ . . . ^T2^{n T}

n+1 2 . . . T₂¹ T₂²

S₂ⁿ= BASIC + Σ^b_n-LIND

S₂ⁿ S₂ⁿ⁺¹ S₂¹ S₂²

T₂ = S2 = ∪n^S₂ⁿ= ∪n^T₂ⁿ

First difference between BA and PA

Despite this ‘strange’ property, the logarithm is essential to BA:

Σ^b_n-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|).

✲ . . . ^T2^{n T}

n+1 2 . . . T₂¹ T₂²

S₂ⁿ= BASIC + Σ^b_n-LIND

S₂ⁿ S₂ⁿ⁺¹ S₂¹ S₂²

T₂ = S2 = ∪n^S₂ⁿ= ∪n^T₂ⁿ

Polynomial Time (Cobham): ‘Limited iteration on notation’ involves the condition|f (z, ~x)| ≤ p(|z|, |~x|).

First difference between BA and PA

Despite this ‘strange’ property, the logarithm is essential to BA:

Σ^b_n-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|).

✲ . . . ^T2^{n T}

n+1 2 . . . T₂¹ T₂²

S₂ⁿ= BASIC + Σ^b_n-LIND

S₂ⁿ S₂ⁿ⁺¹ S₂¹ S₂²

T₂ = S2 = ∪n^S₂ⁿ= ∪n^T₂ⁿ

Polynomial Time (Cobham): ‘Limited iteration on notation’ involves the condition|f (z, ~x)| ≤ p(|z|, |~x|).

Difference 1: there isNOanalog of |x| (or LIND or FP) in PA.

Second difference: BASIC is not very basic

Second difference: BASIC is not very basic

BASIC defines x#y = 2^{|x|.|y |}. (2^x isnotavailable in BA)

Second difference: BASIC is not very basic

BASIC defines x#y = 2^{|x|.|y |}. (2^x isnotavailable in BA)

x#y is essential for BA (G¨odel numbering, collection, hierarchy).

Second difference: BASIC is not very basic

BASIC defines x#y = 2^{|x|.|y |}. (2^x isnotavailable in BA)

x#y is essential for BA (G¨odel numbering, collection, hierarchy).

Difference 2: there isNOanalog of x#y in PA.

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA.

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit)

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . ,

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}),

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1,

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1, ω + 2, . . . , ω + n, . . . ,

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1, ω + 2, . . . , ω + n, . . . , ω+ ω

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1, ω + 2, . . . , ω + n, . . . , ω+ ω (= 2ω),

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1, ω + 2, . . . , ω + n, . . . , ω+ ω (= 2ω), 3ω, . . . , nω, . . . ,

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1, ω + 2, . . . , ω + n, . . . , ω+ ω (= 2ω), 3ω, . . . , nω, . . . , ω × ω (= ω²),

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1, ω + 2, . . . , ω + n, . . . , ω+ ω (= 2ω), 3ω, . . . , nω, . . . , ω × ω (= ω²), ω³, ω⁴, . . . , ωⁿ, ω^ω,

Introducing Unbounded Arithmetic

Unbounded Arithmeticis an axiomatization of PA which overcomes these differences. Thus, it is very close to BA. Definition (Ordinals)

(≈ generalization of natural numbers)

1 _{0 ∈ ORD.}

2 If α ∈ ORD, then α + 1 ∈ ORD.

3 _{If λ}

n∈ ORD, then λ := ∪n{λn} ∈ ORD. (limit) The following are in ORD:

0, 1, 2, . . . , n, . . . , ω (= ∪_n{n}), ω + 1, ω + 2, . . . , ω + n, . . . , ω+ ω (= 2ω), 3ω, . . . , nω, . . . , ω × ω (= ω²), ω³, ω⁴, . . . , ωⁿ, ω^ω, ω^ωω, ω^ωω

ω

, . . . , ε0 (=limit of ω^ω...

ω

), . . .

Hardy Hierarchy

Hardy Hierarchy (describes functions using ordinals) H0(x) := x,

Hα₊₁(x) := Hα(x + 1), Hλ(x) := Hλ_x(x).

Hardy Hierarchy

Hardy Hierarchy (describes functions using ordinals) H0(x) := x,

Hα₊₁(x) := Hα(x + 1), Hλ(x) := Hλ_x(x).

Define the inverse Hα⁻¹(x) := (µm ≤ x)(Hα(m) ≥ x).

Hardy Hierarchy

Hardy Hierarchy (describes functions using ordinals) H0(x) := x,

Hα₊₁(x) := Hα(x + 1), Hλ(x) := Hλ_x(x).

Define the inverse Hα⁻¹(x) := (µm ≤ x)(Hα(m) ≥ x). For short, denote the inverse Hα⁻¹(x) as |x|α.

Hardy Hierarchy

Hardy Hierarchy (describes functions using ordinals) H0(x) := x,

Hα₊₁(x) := Hα(x + 1), Hλ(x) := Hλ_x(x).

Define the inverse Hα⁻¹(x) := (µm ≤ x)(Hα(m) ≥ x). For short, denote the inverse Hα⁻¹(x) as |x|α.

Examples: Hω(x) = 2x,

Hardy Hierarchy

Hardy Hierarchy (describes functions using ordinals) H0(x) := x,

Hα₊₁(x) := Hα(x + 1), Hλ(x) := Hλ_x(x).

Define the inverse Hα⁻¹(x) := (µm ≤ x)(Hα(m) ≥ x). For short, denote the inverse Hα⁻¹(x) as |x|α.

Examples: Hω(x) = 2x, Hω²(x) ≈ 2^x,

Hardy Hierarchy

Hardy Hierarchy (describes functions using ordinals) H0(x) := x,

Hα₊₁(x) := Hα(x + 1), Hλ(x) := Hλ_x(x).

Define the inverse Hα⁻¹(x) := (µm ≤ x)(Hα(m) ≥ x). For short, denote the inverse Hα⁻¹(x) as |x|α.

Examples: Hω(x) = 2x, Hω²(x) ≈ 2^x, Hω^ω(x) ≈ A(x), . . .

Going through great lengths

PA6⊢(∀x)(∃y )(Hε⁻¹₀ (y ) > x). (Wainer-Schwichtenberg-Kreisel)

Going through great lengths

PA6⊢(∀x)(∃y )(Hε⁻¹₀ (y ) > x). (Wainer-Schwichtenberg-Kreisel) (Recall that |PA| = ε0 and that T26⊢(∀x)(∃y )^|y | > x^)

Going through great lengths

PA6⊢(∀x)(∃y )(Hε⁻¹₀ (y ) > x). (Wainer-Schwichtenberg-Kreisel) (Recall that |PA| = ε0 and that T26⊢(∀x)(∃y )^|y | > x^) Thus, Hε⁻¹₀ (x) = |x|ε₀ is a good analog of |x| for PA.

Going through great lengths

PA6⊢(∀x)(∃y )(Hε⁻¹₀ (y ) > x). (Wainer-Schwichtenberg-Kreisel) (Recall that |PA| = ε0 and that T26⊢(∀x)(∃y )^|y | > x^) Thus, Hε⁻¹₀ (x) = |x|ε₀ is a good analog of |x| for PA. Axiom schema (Σn-LIND)

For ϕ∈ Σ_n,^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|ε₀)

Going through great lengths

PA6⊢(∀x)(∃y )(Hε⁻¹₀ (y ) > x). (Wainer-Schwichtenberg-Kreisel) (Recall that |PA| = ε0 and that T26⊢(∀x)(∃y )^|y | > x^) Thus, Hε⁻¹₀ (x) = |x|ε₀ is a good analog of |x| for PA.

Axiom schema (Σn-LIND)

For ϕ∈ Σ_n,^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|ε₀) Thus, Σ_n-LIND is a good analog of Σ^b_n-LIND for PA.

Where it’s at

Recall that BASIC defines x#y = 2^{|x|.|y |}.

Where it’s at

Recall that BASIC defines x#y = 2^{|x|.|y |}.

The axiom BASIC defines x@y := Hε₀ |x|ε₀.|y |ε₀

.

Where it’s at

Recall that BASIC defines x#y = 2^{|x|.|y |}.

The axiom BASIC defines x@y := Hε₀ |x|ε₀.|y |ε₀

.

Thus, x@y is a good analog of x#y for PA.

Where it’s at

Recall that BASIC defines x#y = 2^{|x|.|y |}.

The axiom BASIC defines x@y := Hε₀ |x|ε₀.|y |ε₀

.

Thus, x@y is a good analog of x#y for PA. (Hε₀(x) isnotavailable in PA)

( 2^x isnotavailable in BA)

The hierarchy of Unbounded Arithmetic

The hierarchy of Unbounded Arithmetic

BASICdefines x@y := Hε₀ |x|ε₀.|y |ε₀

.

✲ . . . ^Tn2 ^Tn+12 . . . T^{2 (= ∪nTn}2^{) ≈ PA}

T¹

2 ^T22

Tⁿ₂ = BASIC + Σn-IND

≈ I Σn

The hierarchy of Unbounded Arithmetic

Σn-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|ε₀).

✲ . . . ^Tn2 ^Tn+12 . . .

T¹

2 ^T22

Tⁿ₂ = BASIC + Σn-IND

≈ I Σn

Sⁿ₂ = BASIC + Σn-LIND S_{2= ∪n}Sⁿ₂

Sⁿ

2 ^S

n+1

S¹ 2 2 ^S22

T_{2= S2≈ PA}

The hierarchy of Unbounded Arithmetic

Σn-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|ε₀).

✲ . . . ^Tn2 ^Tn+12 . . .

T¹

2 ^T22

Tⁿ₂ = BASIC + Σn-IND

≈ I Σn

Sⁿ₂ = BASIC + Σn-LIND S_{2= ∪n}Sⁿ₂

Sⁿ

2 ^S

n+1

S¹ 2 2 ^S22

T_{2= S2≈ PA}

Σ^b_n-LIND : ^ϕ(0) ∧ (∀n)(ϕ(n) → ϕ(n + 1))^→ (∀n)ϕ(|n|).

✲ . . . ^T2^{n T}

n+1

2 . . . T^{2 = S2} T₂¹ T₂²

S₂ⁿ= BASIC + Σ^b_n-LIND T₂ⁿ= BASIC + Σ^b_n-IND S₂= ∪_nS₂ⁿ T₂= ∪_nT₂ⁿ

S₂ⁿ S₂ⁿ⁺¹ S₂¹ S₂²

Some time functions

Some time functions

(Roughly speaking)

FP is the class of primitive recursive functions f (z, ~x) satisfying

|f (z, ~x)| ≤ p(|z|, |~x|), for a polynomial p

Some time functions

(Roughly speaking)

FP is the class of primitive recursive functions f (z, ~x) satisfying

|f (z, ~x)| ≤ p(|z|, |~x|), for a polynomial p What about. . .

FP, the class of recursive functions f (z, ~x) satisfying

|f (z, ~x)|ε₀ ≤ g (|z|ε₀,|~x|ε₀), for a primitive recursive g

Some time functions

(Roughly speaking)

FP is the class of primitive recursive functions f (z, ~x) satisfying

|f (z, ~x)| ≤ p(|z|, |~x|), for a polynomial p What about. . .

FP, the class of recursive functions f (z, ~x) satisfying

|f (z, ~x)|ε₀ ≤ g (|z|ε₀,|~x|ε₀), for a primitive recursive g What about the above for (ε0)n= ω^ω...

ω

| {z }

ntimes

instead of ε0?

Final Thought

Many authors have emphasized the analogies between the fragments Σ^b_n-IND of [Bounded Arithmetic] and the fragments

IΣn of Peano arithmetic. Sometimes this is helpful, but often one feels that the bounded hierarchy of theories is of a rather

different nature and new techniques must be developed to answer the key questions concerning them. Richard Kaye

Final Thought

Many authors have emphasized the analogies between the fragments Σ^b_n-IND of [Bounded Arithmetic] and the fragments

IΣn of Peano arithmetic. Sometimes this is helpful, but often one feels that the bounded hierarchy of theories is of a rather

different nature and new techniques must be developed to answer the key questions concerning them. Richard Kaye

Thanks for you attention!

Any questions?