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

A copy of several Reverse Mathematics

Sam Sanders

Department of Pure Mathematics Ghent University

Belgium

April 23, 2010, Tohoku University

FACULTY OF SCIENCES

Outline

1 Introduction

2 A copy of the RM of WKL₀

3 A constructive copy

4 Big questions

5 Future research

Reverse Mathematics

Reverse Mathematics

= finding the minimal axioms A that prove a theorem T .

Reverse Mathematics

Reverse Mathematics

= finding the minimal axioms A that prove a theorem T . T is a theorem of ^ordinarymathematics

in many cases: A equivalent to T

Big Five: RCA0, WKL0, ACA0, ATR0 and Π¹₁-CA0

Reverse Mathematics

Reverse Mathematics

= finding the minimal axioms A that prove a theorem T . T is a theorem of ^ordinarymathematics

in many cases: A equivalent to T

Big Five: RCA0, WKL0, ACA0, ATR0 and Π¹₁-CA0

Most theorems of ‘everyday’ mathematics are either provable in RCA0 or equivalent to one of the ‘Big Five’ theories.

An example: Reverse Mathematics for WKL

Central principle:

Theorem (Weak K¨onig’s Lemma)

Every infinite binary tree has an infinite path.

An example: Reverse Mathematics for WKL

Central principle:

Theorem (Weak K¨onig’s Lemma)

Every infinite binary tree has an infinite path.

Assuming the base theory RCA₀, WKL is equivalent to

1 Heine-Borel: every countable covering of [0, 1] has a finite subcovering.

An example: Reverse Mathematics for WKL

Central principle:

Theorem (Weak K¨onig’s Lemma)

Every infinite binary tree has an infinite path.

Assuming the base theory RCA₀, WKL is equivalent to

1 Heine-Borel: every countable covering of [0, 1] has a finite subcovering.

2 A continuous function on [0, 1] is uniformly continuous.

3 A continuous function on [0, 1] is Riemann integrable.

4 Weierstrass’ theorem: a continuous function on [0, 1] attains its maximum.

5 Peano’s theorem for differential equations y^′ = f (x, y ).

7 _G¨odel’s completeness theorem.

7 _G¨odel’s completeness theorem.

8 A countable commutative ring has a prime ideal.

9 A countable formally real field is orderable.

10 A countable formally real field has a (unique) closure.

7 _G¨odel’s completeness theorem.

8 A countable commutative ring has a prime ideal.

9 A countable formally real field is orderable.

10 A countable formally real field has a (unique) closure.

11 Brouwer’s fixed point theorem: A continuous function from [0, 1]ⁿ to [0, 1]ⁿ has a fixed point.

12 The separable Hahn-Banach theorem.

7 _G¨odel’s completeness theorem.

8 A countable commutative ring has a prime ideal.

9 A countable formally real field is orderable.

10 A countable formally real field has a (unique) closure.

11 Brouwer’s fixed point theorem: A continuous function from [0, 1]ⁿ to [0, 1]ⁿ has a fixed point.

12 The separable Hahn-Banach theorem.

13 A continuous function on [0, 1] can be approximated by (Bernstein) polynomials.

14 And many more. . .

A ‘gap’ in Reverse Mathematics

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

✲

Weak Strong

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

✲

Weak Strong

IΣ₁IΣ₂. . . PA

| {z }

Big Five

RCA₀ WKL0

ACA₀ ATR₀ Π¹₁-CA0

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

✲

Weak Strong

IΣ₁IΣ₂. . . PA

| {z }

Big Five

RCA₀ WKL0

ACA₀ ATR₀ Π¹₁-CA0

Q S₂¹ S₂² . . . S₂

| {z }

Bounded Arithmetic

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

✲

Weak Strong

IΣ₁IΣ₂. . . PA

| {z }

Big Five

RCA₀ WKL0

ACA₀ ATR₀ Π¹₁-CA0

Q S₂¹ S₂² . . . S₂

| {z }

Bounded Arithmetic

Riemann integral isnotdefinable. . .

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

IΣ₁IΣ₂. . . PA ✲

| {z }

Big Five

RCA₀ WKL0

ACA₀ ATR₀ Π¹₁-CA0

Q S₂¹ S₂² . . . S₂

| {z }

Bounded Arithmetic

Riemann integral isnotdefinable. . .

GAP

z }| {

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

IΣ₁IΣ₂. . . PA ✲

| {z }

Big Five

RCA₀ WKL0

ACA₀ ATR₀ Π¹₁-CA0

Q S₂¹ S₂² . . . S₂

| {z }

Bounded Arithmetic

Riemann integral isnotdefinable. . .

GAP

z }| {

I∆₀+ exp

(and many others)

A ‘gap’ in Reverse Mathematics

The ’Big Five’ of RM have first-order strength at least I Σ₁ ([5]).

IΣ₁IΣ₂. . . PA ✲

| {z }

Big Five

RCA₀ WKL0

ACA₀ ATR₀ Π¹₁-CA0

Q S₂¹ S₂² . . . S₂

| {z }

Bounded Arithmetic

Riemann integral isnotdefinable. . .

GAP

z }| {

I∆₀+ exp

(and many others)

What about the RM of I ∆₀+ exp?

RM for I ∆

+ exp

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp.

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

new numbers, not in Q

z }| {

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

new numbers, not in Q

z }| {

ω

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

new numbers, not in Q

z }| {

ω ω/2

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

new numbers, not in Q

z }| {

ω

ω/2 2^ω

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

new numbers, not in Q

z }| {

ω

ω/2 2^ω

⌈^√ω⌉

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

infinitenumbers

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

−ω

−2^ω −⌈^√ω⌉

| {z }

negativeinfinitenumbers

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

Q,the rational numbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

−ω

−2^ω −⌈^√ω⌉

| {z }

negativeinfinitenumbers

x isinfinite iff |x| > q, for all q ∈ Q⁺

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

thefinitenumbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

−ω

−2^ω −⌈^√ω⌉

| {z }

negativeinfinitenumbers

x isinfinite iff |x| > q, for all q ∈ Q⁺

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

thefinitenumbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

−ω

−2^ω −⌈^√ω⌉

| {z }

negativeinfinitenumbers

x isinfinite iff |x| > q, for all q ∈ Q⁺

x isinfinitely smalliff |x| < q, for all q ∈ Q⁺

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

thefinitenumbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

−ω

−2^ω −⌈^√ω⌉

| {z }

negativeinfinitenumbers

x isinfinite iff |x| > q, for all q ∈ Q⁺

x isinfinitely smalliff |x| < q, for all q ∈ Q^{+ (e.g. 1/ω)} 1

ω

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

thefinitenumbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

−ω

−2^ω −⌈^√ω⌉

| {z }

negativeinfinitenumbers

x isinfinite iff |x| > q, for all q ∈ Q⁺

x isinfinitely smalliff |x| < q, for all q ∈ Q^{+ (e.g. 1/ω)} 1

ω

(also ‘x ≈ 0’ or ‘x is infinitesimal’)

RM for I ∆

+ exp

We work in ERNA, a nonstandard version of I ∆0+ exp. ERNA has a field^∗Q:

. . . −1 0 ^{12 1 53 2 . . .} ✲

| {z }

thefinitenumbers

ω

ω/2 2^ω

⌈^√ω⌉

| {z }

positiveinfinitenumbers

−ω

−2^ω −⌈^√ω⌉

| {z }

negativeinfinitenumbers

x isinfinite iff |x| > q, for all q ∈ Q⁺

∗_Q,the hyperrational numbers

z }| {

x isinfinitely smalliff |x| < q, for all q ∈ Q^{+ (e.g. 1/ω)} 1

ω

(also ‘x ≈ 0’ or ‘x is infinitesimal’)

Central principle for ERNA

The following principle, called ‘Π₁-transfer’, plays the role of WKL. Axiom schema (Π1-TRANS)

Central principle for ERNA

The following principle, called ‘Π₁-transfer’, plays the role of WKL. Axiom schema (Π1-TRANS)

For allstandard quantifier-free ϕ,

(∀x ∈ Q)ϕ(x) → (∀x ∈^∗Q)ϕ(x)

standard= no infinite numbers^†, no ‘x ≈ y’, no ‘x is (in)finite’.

Central principle for ERNA

The following principle, called ‘Π₁-transfer’, plays the role of WKL. Axiom schema (Π1-TRANS)

For allstandard quantifier-free ϕ,

(∀x ∈ Q)ϕ(x) → (∀x ∈^∗Q)ϕ(x)

standard= no infinite numbers^†, no ‘x ≈ y’, no ‘x is (in)finite’. (^†exceptin terms like^Pω_n=0 ^x_n!ⁿ,^Pω_n=0(−1)^{n x}_(2n)!²ⁿ , . . . )

Continuity

Continuity

A function f isstandardcontinuous (or ε-δ-continuous) if

(∀ε ∈ Q)(∃δ ∈ Q)(∀x, y ∈ Q)(|x − y| < δ → |f (x) − f (y)| < ε).

Continuity

A function f isstandardcontinuous if

(∀ε ∈ Q)(∃δ ∈ Q)(∀x, y ∈ Q)(|x − y| < δ → |f (x) − f (y)| < ε). A function f isnonstandard continuous if

(∀x, y ∈^∗Q)(x ≈ y → f (x) ≈ f (y)).

Continuity

A function f isstandardcontinuous if

(∀ε ∈ Q)(∃δ ∈ Q)(∀x, y ∈ Q)(|x − y| < δ → |f (x) − f (y)| < ε). A function f isnonstandard continuous if

(∀x, y ∈^∗Q)(x ≈ y → f (x) ≈ f (y)). ⁽¹⁾

Principle (Continuity principle)

Astandard function is standard cont. iff it is nonstandard cont. standard= no infinite numbers^†, no ‘x ≈ y’, no ‘x is (in)finite’.

Continuity

A function f isstandardcontinuous if

(∀ε ∈ Q)(∃δ ∈ Q)(∀x, y ∈ Q)(|x − y| < δ → |f (x) − f (y)| < ε). A function f isnonstandard continuous if

(∀x, y ∈^∗Q)(x ≈ y → f (x) ≈ f (y)). ⁽¹⁾

Principle (Continuity principle)

Astandard function is standard cont. iff it is nonstandard cont. The Continuity Principle is usedthroughoutPhysics:

While modeling reality, physicists use the intuitive definition (1) andnotε-δ-continuity.

Continuity

A function f isstandardcontinuous if

(∀ε ∈ Q)(∃δ ∈ Q)(∀x, y ∈ Q)(|x − y| < δ → |f (x) − f (y)| < ε). A function f isnonstandard continuous if

(∀x, y ∈^∗Q)(x ≈ y → f (x) ≈ f (y)). ⁽¹⁾

Principle (Continuity principle)

Astandard function is standard cont. iff it is nonstandard cont. Theorem (S.)

InERNA, the Continuity principle is equivalent to Π₁-transfer.

Weierstrass extremum principle

✲

✻

f(x)

a b

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x).

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define x_i = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define x_i = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

2) Every x ∈ [a, b] is in some [xj^{, x}j+1^].

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define x_i = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

2) Every x ∈ [a, b] is in some [xj^{, x}j+1^].

3) x ≈ x^j ≈ x^j+1 implies f (x) ≈ f (x^j)

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define x_i = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

2) Every x ∈ [a, b] is in some [xj^{, x}j+1^].

3) x ≈ x^j ≈ x^j+1 implies f (x) ≈ f (x^j) 4) Calculate M = maxi_≤ω^f(xi).

•^M

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define x_i = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

2) Every x ∈ [a, b] is in some [xj^{, x}j+1^].

3) x ≈ x^j ≈ x^j+1 implies f (x) ≈ f (x^j) 4) Calculate M = maxi_≤ω^f(xi).

•^M

5) We have (∀x ∈ [a, b])(f (x) / M).

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define x_i = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

2) Every x ∈ [a, b] is in some [xj^{, x}j+1^].

3) x ≈ x^j ≈ x^j+1 implies f (x) ≈ f (x^j) 4) Calculate M = maxi_≤ω^f(xi).

•^M

5) We have (∀x ∈ [a, b])(f (x) / M). Theorem (Weierstrass extremum principle)

A standard function which is standard continuous on[a, b] attains its maximum there,up to infinitesimals.

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define xi = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

2) Every x ∈ [a, b] is in some [x^{j, xj}+1^].

3) x ≈ x^j ≈ x^j+1 implies f (x) ≈ f (x^j) 4) Calculate M = maxi_≤ω^f(xi).

•^M

5) We have (∀x ∈ [a, b])(f (x) / M). Theorem (Weierstrass extremum principle)

A standard function which is standard continuous on[a, b] attains its maximum there,up to infinitesimals.

In Physics, results also holdup to a degree of accuracy.

Weierstrass extremum principle

✲

✻

f(x)

a b

We find the maximum over [a, b] of the continuous function f (x). 1) Define x_i = a + ε(b − a)i. (i ≤ ω)

x_i x_i+1

✲

✛ ε ≈ 0

2) Every x ∈ [a, b] is in some [xj^{, x}j+1^].

3) x ≈ x^j ≈ x^j+1 implies f (x) ≈ f (x^j) 4) Calculate M = maxi_≤ω^f(xi).

•^M

5) We have (∀x ∈ [a, b])(f (x) / M). Theorem (Weierstrass extremum principle)

A standard function which is standard continuous on[a, b] attains its maximum there,up to infinitesimals.

Theorem (S.)

InERNA, the Weierstrass ext. prin. is equivalent to Π1^-transfer.

Brouwer fixed point theorem

Theorem (Brouwer fixed point theorem)

A continuous[0, 1] → [0, 1]-function has a fixed point ?

Brouwer fixed point theorem

Theorem (Brouwer fixed point theorem)

A continuous[0, 1] → [0, 1]-function has a fixed point ?

X Y

y = 1 − x^{2 y = x}

• •

•

−1 +

√5 2

−1 +

√5 2

Brouwer fixed point theorem

Theorem (Brouwer fixed point theorem)

A continuous[0, 1] → [0, 1]-function has a fixed point ?

X Y

y = 1 − x^{2 y = x}

• •

•

−1 +

√5 2

−1 +

√5 2

But ⁻¹⁺₂^√5 _6∈^∗Qbecause ^√_{5 6∈}^∗Q!

Brouwer fixed point theorem

Theorem (Brouwer fixed point theorem)

A continuous[0, 1] → [0, 1]-function has a fixed point ?

X Y

y = 1 − x^{2 y = x}

• •

•

−1 +

√5 2

−1 +

√5 2

But ⁻¹⁺₂^√5 _6∈^∗Qbecause ^√_{5 6∈}^∗Q! There is β ∈^{∗Qwith β2} ≈ 5 and we have ^−1+β_{2 ≈ 1 − (}^−1+β₂ )².

Brouwer fixed point theorem

Theorem (Brouwer fixed point theorem)

A continuous[0, 1] → [0, 1]-function has a fixed point ?

X Y

y = 1 − x^{2 y = x}

• •

•

−1 +

√5 2

−1 +

√5 2

But ⁻¹⁺₂^√5 _6∈^∗Qbecause ^√_{5 6∈}^∗Q! There is β ∈^{∗Qwith β2} ≈ 5 and we have ^−1+β_{2 ≈ 1 − (}^−1+β₂ )².

−1+β2 is fixed point ‘up to infinitesimals’ for y = 1 − x^2.

Brouwer fixed point theorem

Definition

x₀ is a fixed pointup to infinitesimalsif f(x_{0) ≈ x0}.

Brouwer fixed point theorem

Definition

x₀ is a fixed pointup to infinitesimalsif f(x0_{) ≈ x}0^.

Theorem (Brouwer fixed point principle)

A standard continuous[0, 1]²_{→ [0, 1]}²-function has a fixed point up to infinitesimals.

Brouwer fixed point theorem

Definition

x₀ is a fixed pointup to infinitesimalsif f(x0_{) ≈ x}0^.

Theorem (Brouwer fixed point principle)

A standard continuous[0, 1]²_{→ [0, 1]}²-function has a fixed point up to infinitesimals.

As in Physics, we only haveapproximations(of e.g. fixed points).

Brouwer fixed point theorem

Definition

x₀ is a fixed pointup to infinitesimalsif f(x0_{) ≈ x}0^.

Theorem (Brouwer fixed point principle)

A standard continuous[0, 1]²_{→ [0, 1]}²-function has a fixed point up to infinitesimals.

As in Physics, we only haveapproximations(of e.g. fixed points). Theorem (S.)

InERNA, the Brouwer fixed point principle is equivalent to Π1^-transfer.

Riemann integration

✲

✻

f(x)

a b

Riemann integration

✲

✻

f(x)

a b

Rb

a ^f(x) dx = the surface under f (x)

Riemann integration

✲

✻

f(x)

a b

Rb

a ^f(x) dx = the surface under f (x)

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

ωintervals [xi, xi+1]

z }| {

✲

✛ ε_{i ≈ 0}

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0}

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

•

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

2) Surface of rectangle is f (x_i)ε_i

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

2) Surface of rectangle is f (x_i)ε_i 3) Construct all rectangles

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

2) Surface of rectangle is f (x_i)ε_i 3) Construct all rectangles

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

2) Surface of rectangle is f (x_i)ε_i 3) Construct all rectangles 4) Total surface is ^Pω_i=1f(x_i)ε_i

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

2) Surface of rectangle is f (x_i)ε_i 3) Construct all rectangles 4) Total surface is ^Pω_i=1f(x_i)ε_i

= Sπ, the Riemann sum of π

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

2) Surface of rectangle is f (x_i)ε_i 3) Construct all rectangles 4) Total surface is ^Pω_i=1f(x_i)ε_i

= Sπ, the Riemann sum of π

≈^R_a^{bf(x) dx}

Riemann integration

✲

✻

f(x)

a b

1) Hyperfine partition π of [a, b]

= set of ω subintervals [x_i, x_i+1] of length ε_{i ≈ 0}

✲

✛ ε_{i ≈ 0} x_i

• f(xi)

•

2) Surface of rectangle is f (x_i)ε_i 3) Construct all rectangles 4) Total surface is ^Pω_i=1f(x_i)ε_i

= Sπ, the Riemann sum of π

≈^R_a^{bf(x) dx}

f is integrable if S_{π ≈ q ≈ Sπ}^′, for all hyperfine π, π^′

(q ∈^∗Qis finite)

Riemann integration II

Riemann integration II

Principle (Integrability principle)

A standard continuous function is Riemann integrable.

Riemann integration II

Principle (Integrability principle)

A standard continuous function is Riemann integrable.

Theorem (S.)

InERNA, the Integrability principle is equivalent to Π₁-transfer.

Riemann integration II

Principle (Integrability principle)

A standard continuous function is Riemann integrable.

Theorem (S.)

InERNA, the Integrability principle is equivalent to Π₁-transfer. The integral^R_a^bf(x)dx is only defined up to infinitesimals, i.e. only approximately.

Peano existence theorem

Peano existence theorem

Principle (Peano existence principle)

Let f(x, y ) be standard continuous on [−a, a] × [−b, b] with maximum M. Then there existsφ(x), cont. differentiable for

|x| ≤ α such that

φ^′(x)_≈f(x, φ(x)), φ(0) = 0 (2) holds for|x| < α, with α = min(a, b/M).

Peano existence theorem

Principle (Peano existence principle)

Let f(x, y ) be standard continuous on [−a, a] × [−b, b] with maximum M. Then there existsφ(x), cont. differentiable for

|x| ≤ α such that

φ^′(x)_≈f(x, φ(x)), φ(0) = 0 (2) holds for|x| < α, with α = min(a, b/M).

= the ‘real’ Peano existence theorem,up to infinitesimals

Peano existence theorem

Principle (Peano existence principle)

Let f(x, y ) be standard continuous on [−a, a] × [−b, b] with maximum M. Then there existsφ(x), cont. differentiable for

|x| ≤ α such that

φ^′(x)_≈f(x, φ(x)), φ(0) = 0 (2) holds for|x| < α, with α = min(a, b/M).

= the ‘real’ Peano existence theorem,up to infinitesimals Theorem

InERNA, the Peano exist. princ. is equivalent to Π₁-transfer.

Isomorphism Theorem

(inspired by work of Sommer and Suppes [6]) Theorem (Isomorphism theorem)

Every ‘R-like’ model of a physical problem has an isomorphic

‘Q-like’ model.

Isomorphism Theorem

(inspired by work of Sommer and Suppes [6]) Theorem (Isomorphism theorem)

Every ‘R-like’ model of a physical problem has an isomorphic

‘Q-like’ model.

R-like model = irrationalobjects (e.g. π and e^x) are used Q-like model = onlyrational numbers and functions are used

Isomorphism Theorem

(inspired by work of Sommer and Suppes [6]) Theorem (Isomorphism theorem)

Every ‘R-like’ model of a physical problem has an isomorphic

‘Q-like’ model.

R-like model = irrationalobjects (e.g. π and e^x) are used Q-like model = onlyrational numbers and functions are used Theorem

InERNA, the Isomorphism theorem is equivalent to Π₁-transfer.

Isomorphism Theorem

(inspired by work of Sommer and Suppes [6]) Theorem (Isomorphism theorem)

Every ‘R-like’ model of a physical problem has an isomorphic

‘Q-like’ model.

R-like model = irrationalobjects (e.g. π and e^x) are used Q-like model = onlyrational numbers and functions are used Theorem

InERNA, the Isomorphism theorem is equivalent to Π₁-transfer. The Isomorphism theorem implies thatno physical experiment can decide whether reality is discrete or continuous.

And many more principles. . .

And many more principles. . .

In ERNA, the following are equivalent to Π1-transfer.

And many more principles. . .

In ERNA, the following are equivalent to Π1-transfer.

1 Continuity principle (NS-cont. is equivalent to S-cont. )

And many more principles. . .

In ERNA, the following are equivalent to Π1-transfer.

1 Continuity principle (NS-cont. is equivalent to S-cont. )

2 Weierstrass extremum theorem (‘up to infinitesimals’)

3 Brouwer fixpoint theorem (‘up to infinitesimals’)

4 Peano existence theorem (‘up to infinitesimals’)

5 Integrability principle

6 Isomorphism theorem

7 Completeness up to infinitesimals of^∗Q (Cauchy, Dedekind, Cantor)

8 Fundamental theorem of calculus.

9 And many more. . .

And many more principles. . .

In ERNA, the following are equivalent to Π1-transfer.

1 Continuity principle (NS-cont. is equivalent to S-cont. )

2 Weierstrass extremum theorem (‘up to infinitesimals’)

3 Brouwer fixpoint theorem (‘up to infinitesimals’)

4 Peano existence theorem (‘up to infinitesimals’)

5 Integrability principle

6 Isomorphism theorem

7 Completeness up to infinitesimals of^∗Q (Cauchy, Dedekind, Cantor)

8 Fundamental theorem of calculus.

9 And many more. . .

The RM of ERNA + Π₁-TRANS is a copy up to infinitesimalsof the RM of WKL₀.

And many more principles. . .

In ERNA, the following are equivalent to Π₁-transfer.

1 Continuity principle (NS-cont. is equivalent to S-cont. )

2 Weierstrass extremum theorem (‘up to infinitesimals’)

3 Brouwer fixpoint theorem (‘up to infinitesimals’)

4 Peano existence theorem (‘up to infinitesimals’)

5 Integrability principle

6 Isomorphism theorem

7 Completeness up to infinitesimals of^∗Q (Cauchy, Dedekind, Cantor)

8 Fundamental theorem of calculus.

9 And many more. . .

However,(7) belongs to the RM ofACA₀,NOTto that of WKL₀.

And many more principles. . .

In ERNA, the following are equivalent to Π₁-transfer.

1 Continuity principle (NS-cont. is equivalent to S-cont. )

2 Weierstrass extremum theorem (‘up to infinitesimals’)

3 Brouwer fixpoint theorem (‘up to infinitesimals’)

4 Peano existence theorem (‘up to infinitesimals’)

5 Integrability principle

6 Isomorphism theorem

7 Completeness up to infinitesimals of^∗Q (Cauchy, Dedekind, Cantor)

8 Fundamental theorem of calculus.

9 And many more. . .

However,(7) belongs to the RM ofACA₀,NOTto that of WKL₀. Why is this so?

Similarities between Constructivism and ERNA

Constructivism ERNA

Similarities between Constructivism and ERNA

Constructivism ERNA

√x is not always defined ^√x is not always defined

Similarities between Constructivism and ERNA

standard part function: st(x + ε) = x, with x standard and ε ≈ 0

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

Similarities between Constructivism and ERNA

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff.

Similarities between Constructivism and ERNA

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property

Similarities between Constructivism and ERNA

finite set property: not every subset of afiniteset is finite hyperfinite set property: not every subset of ahyperfiniteset is hyperfinite

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property

Similarities between Constructivism and ERNA

finite set property: not every subset of afiniteset is finite hyperfinite set property: not every subset of ahyperfiniteset is hyperfinite

(hyperfinitesets are of the form {0, 1, . . . , N} for (in)finite N.)

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property

Similarities between Constructivism and ERNA

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property computable witnesses computable witnesses

Similarities between Constructivism and ERNA

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property computable witnesses computable witnesses Constructivism

(∃n)ϕ(x) means ‘there is an algorithm to compute n₀ s.t. ϕ(n₀)’.

Similarities between Constructivism and ERNA

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property computable witnesses computable witnesses Constructivism

(∃n)ϕ(x) means ‘there is an algorithm to compute n₀ s.t. ϕ(n₀)’. ERNA

If (∃n ∈ N)ϕ(n), then n0 := (µn ≤ ω)ϕ(n) satisfies ϕ(n0^).

Similarities between Constructivism and ERNA

Constructivism ERNA

√x is not always defined ^√x is not always defined no standard part function no standard part function

uniform cont. and diff. uniform cont. and diff. finite set property hyperfinite set property computable witnesses computable witnesses Constructivism

(∃n)ϕ(x) means ‘there is an algorithm to compute n₀ s.t. ϕ(n₀)’. ERNA+ Π₁-transfer

If (∃n ∈^∗N)ϕ(n), then n₀ := (µn ≤ ω)ϕ(n) satisfies ϕ(n0^).

Constructive Reverse Mathematics (CRM)

Constructive Reverse Mathematics (CRM)

In CRM, an important principle (related to Completeness) is Principle (Σ₁-excluded middle)

For every q.f. formulaϕ, we have _(∃n)ϕ(n)∨ (∀n)¬ϕ(n).

Constructive Reverse Mathematics (CRM)

In CRM, an important principle (related to Completeness) is Principle (Σ₁-excluded middle)

For every q.f. formulaϕ, we have _(∃n)ϕ(n)∨ (∀n)¬ϕ(n).

In constructive math.,_(∃n)ϕ(n)means ‘we can compute a number n₀ s.t. ϕ(n₀)’.

Constructive Reverse Mathematics (CRM)

In CRM, an important principle (related to Completeness) is Principle (Σ₁-excluded middle)

For every q.f. formulaϕ, we have (∃n)ϕ(n) ∨ (∀n)¬ϕ(n).

In constructive math.,_(∃n)ϕ(n)means ‘we can compute a number n₀ s.t. ϕ(n₀)’.

Principle (Π1-transfer)

For every q.f. formulaϕ, we have(∃n ∈ N)ϕ(n)∨ (∀n ∈^∗N)¬ϕ(n).

Constructive Reverse Mathematics (CRM)

In CRM, an important principle (related to Completeness) is Principle (Σ₁-excluded middle)

For every q.f. formulaϕ, we have (∃n)ϕ(n) ∨ (∀n)¬ϕ(n).

In constructive math.,_(∃n)ϕ(n)means ‘we can compute a number n₀ s.t. ϕ(n₀)’.

Principle (Π1-transfer)

For every q.f. formulaϕ, we have(∃n ∈ N)ϕ(n)∨ (∀n ∈^∗N)¬ϕ(n). To find a witness for_{(∃n ∈}^∗N)ϕ(n), calculate (µn ≤ ω)ϕ(n).

Constructive Reverse Mathematics (CRM)

In CRM, an important principle (related to Completeness) is Principle (Σ₁-excluded middle)

For every q.f. formulaϕ, we have (∃n)ϕ(n) ∨ (∀n)¬ϕ(n).

In constructive math.,_(∃n)ϕ(n)means ‘we can compute a number n₀ s.t. ϕ(n₀)’.

Principle (Π1-transfer)

For every q.f. formulaϕ, we have (∃n ∈ N)ϕ(n) ∨ (∀n ∈^∗N)¬ϕ(n). To find a witness for_{(∃n ∈}^∗N)ϕ(n), calculate (µn ≤ ω)ϕ(n). Thus, Π₁-transfer is ‘hyperexcluded middle’: it excludes the possibility ‘(∀n ∈ N)¬ϕ(n) ∧ (∃n ∈^{∗N)ϕ(n)’.}

Constructive Reverse Mathematics

Conjecture:

CRM withΣ₁-PEM is similar to the RM of ERNA+ Π₁-TRANS.

Big Questions

Big Questions

(#1) Is physical reality continuous or discrete?

Big Questions

(#1) Is physical reality continuous or discrete? (#2) What are good foundations for Mathematics?

Big Questions

(#1) Is physical reality continuous or discrete? (#2) What are good foundations for Mathematics? (#3) Do infinitesimals exist?

Small answers (#2)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL₀.

Small answers (#2)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL₀.

Observation: RM is ‘robustfor infinitesimal error’.

Small answers (#2)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL₀.

Observation: RM is ‘robustfor infinitesimal error’.

‘Robuststatistics’ attempts to produce estimators that are not

particularly affected by small departures from model assumptions([1]).

Small answers (#2)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL₀.

Observation: RM is ‘robustfor infinitesimal error’.

‘Robuststatistics’ attempts to produce estimators that are not

particularly affected by small departures from model assumptions([1]). In CS,robustrefers to an algorithm that performs well not only under ordinary conditions but also under unusual conditions that stress its designers’ assumptions’([3]).

Small answers (#2)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL₀.

Observation: RM is ‘robustfor infinitesimal error’.

‘Robuststatistics’ attempts to produce estimators that are not

particularly affected by small departures from model assumptions([1]). In CS,robustrefers to an algorithm that performs well not only under ordinary conditions but also under unusual conditions that stress its designers’ assumptions’([3]).

Thus,‘robust’methods are reasonably resistant toerrors in the results, produced by deviations from assumptions. Robustness is important throughout the exact sciences.

Small answers (#2)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL₀.

Observation: RM is ‘robustfor infinitesimal error’.

‘Robuststatistics’ attempts to produce estimators that are not

particularly affected by small departures from model assumptions([1]). In CS,robustrefers to an algorithm that performs well not only under ordinary conditions but also under unusual conditions that stress its designers’ assumptions’([3]).

Thus,‘robust’methods are reasonably resistant toerrors in the results, produced by deviations from assumptions. Robustness is important throughout the exact sciences.

(#2)As RM is robust, it is a good foundation for Mathematics!

Small answers (#3)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL0.

Small answers (#3)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL0.

The RM of ERNA + Π₁-TRANS is ‘better’ because the base theory (I ∆₀+ exp) is weaker than that of WKL₀ (I Σ₁).

Small answers (#3)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL0.

The RM of ERNA + Π₁-TRANS is ‘better’ because the base theory (I ∆₀+ exp) is weaker than that of WKL₀ (I Σ₁).

(#3)ERNA+ Π1-TRANS is ‘more real’ than WKL0.

Small answers (#3)

The RM of ERNA + Π₁-TRANS is acopy up to infinitesimalsof the RM of WKL0.

The RM of ERNA + Π₁-TRANS is ‘better’ because the base theory (I ∆₀+ exp) is weaker than that of WKL₀ (I Σ₁).

(#3)ERNA+ Π1-TRANS is ‘more real’ than WKL0. Thus, infinitesimals are ‘more real’ than subsets of N.