ファイル置き場 Sendai Logic Homepage

The strength of transfer priciples

and Reverse Mathematics

Keita Yokoyama

Mathematical Institute, Tohoku University

April 9, 2010

Outline

1 Introduction

RM and subsystems of second-order arithmetic

Non-standard analysis

Related topics

2 Non-standard second-order arithmetic

Non-standard second-order arithmetic

Axioms for non-standard analysis

Non-standard analysis in NSOA

3 Non-standard axioms and Reverse Mathematics

Reverse Mathematics for non-standard analysis

The strengh of transfer principle

Standard part principle

Outline

1 Introduction

RM and subsystems of second-order arithmetic

Non-standard analysis

Related topics

2 Non-standard second-order arithmetic

Non-standard second-order arithmetic

Axioms for non-standard analysis

Non-standard analysis in NSOA

3 Non-standard axioms and Reverse Mathematics

Reverse Mathematics for non-standard analysis

The strengh of transfer principle

Standard part principle

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

Reverse Mathematics and

subsystems of second-order arithmetic

This part is a long introduction of Reverse Mathematics and

second-order arithmetic for new graduates.

What is Reverse Mathematics?

What are the appropriate axioms for mathematics?

Compare axioms and theorems of mathematics.

Find new axioms which are essencially needed for

mathematics.

. . .

Friedman, Simpson, Tanaka, Yamazaki, . . . have shown that

many theorems of mathematics are equivalent to some nice

subsystems of second-order arithmetic!

⇒ Let’s read Simpson’s book!

language of second order arithmetic ( _{L 2} )

Definition (language of second order arithmetic ( _{L 2} ))

number variables:x , y , z , . . . set variables:X , Y , Z , . . .

constant symbols:0 , 1 function symbols: _{+, ·}

relation symbols: _{=, <, ∈}

Classes of formulas

bounded formula: all quantifiers are of the form _∀ x < y, _∃ x < y.

“every thing is bounded.”

arithmetical formulas:( θ : bounded formula)

Σ ⁰ _n formula: _∃ x _{1 ∀} x ₂ . . . x _n θ

Π ⁰ _n formula: _∀ x _{1 ∃} x ₂ . . . x _n θ

“use only number quantifier.”

analytic formula:( ϕ : arithmetical formula)

Σ ¹ _n formula: _∃ X _{1 ∀} X ₂ . . . X _n ϕ

Π ¹ _n formula: _∀ X _{1 ∃} X ₂ . . . X _n ϕ

“very complex formulas.”

Classes of formulas

bounded formula: all quantifiers are of the form _∀ x < y, _∃ x < y.

“every thing is bounded.”

arithmetical formulas:( θ : bounded formula)

Σ ⁰ _n formula: _∃ x _{1 ∀} x ₂ . . . x _n θ

Π ⁰ _n formula: _∀ x _{1 ∃} x ₂ . . . x _n θ

“use only number quantifier.”

analytic formula:( ϕ : arithmetical formula)

Σ ¹ _n formula: _∃ X _{1 ∀} X ₂ . . . X _n ϕ

Π ¹ _n formula: _∀ X _{1 ∃} X ₂ . . . X _n ϕ

“very complex formulas.”

Subsystems of second-order arithmetic

RCA ₀ : “discrete ordered semi ring”+ Σ ⁰ ₁ induction+recursive

comprehension.

WWKL ₀ : RCA ₀ + weak weak K ¨onig’s lemma.

WKL ₀ : RCA ₀ + weak K ¨onig’s lemma.

ACA ₀ : RCA ₀ + arithmetical comprehension.

ATR ₀ : RCA ₀ + arithmetical transfinite recursion.

Π ¹ ₁ CA ₀ : RCA ₀ + Π ¹ ₁ comprehension.

Subsystems of second-order arithmetic

RCA ₀ : In this system, we need to prove everything

“recursively”.

WWKL ₀ : We can use the notion of measure for closed set.

WKL ₀ : We can use Hiene/Borel compactness.

ACA ₀ : We can use sequential compactness.

ATR ₀ : We can compare well orderings.

Π ¹ ₁ CA ₀ : We can check well-foundedness.

Basic notion for analysis in _{L 2}

real number: a Cauchy sequence _{ q _{n } n ∈N} of rational numbers

with _| q _{n −} q _{n+i | <} 2 ⁻ⁿ .

open set: coded by a sequence of open balls

U = S _{n ∈N} B ( a _n ; r _n ) .

continuous function: coded by a sequence of pairs of open

balls

f ( B ( a _n ; r _{n )) ⊆} B ( b _n ; s _n ) .

. . .

Mathematics in RCA ₀

Within RCA ₀ ,

we can define the notion of convergence,

we can find codes for polynomial functions,

we can define derivative (pointwise) and Riemann integral,

we can prove intermideate value theorem,

we can prove the existence of a Riemann integral of a

polynomial function on [ 0 , 1 ] ,

. . .

Mathematics in RCA ₀

However,

we cannot find the limit of a Cauchy sequence

(need sequential compactness),

we cannot prove the existence of a maximum of a continuous

function on [ 0 , 1 ]

(need Heine/Borel compactness),

we cannot prove the existence of a Riemann integral of a

continuous function on [ 0 , 1 ] ,

. . .

Question

Which axioms are exactly needed?

Mathematics in RCA ₀

However,

we cannot find the limit of a Cauchy sequence

(need sequential compactness),

we cannot prove the existence of a maximum of a continuous

function on [ 0 , 1 ]

(need Heine/Borel compactness),

we cannot prove the existence of a Riemann integral of a

continuous function on [ 0 , 1 ] ,

. . .

Question

Which axioms are exactly needed?

Reverse Mathematics

Which axioms are exactly needed?

Theorem

The following are provable within RCA ₀ .

1

Mean value theorem.

2

Implicit function theorem.

3

Taylor’s expansion theorem for holomorphic function.

4

The Jordan curve theorem for a piecewise linear Jordan

curve.

5

The Riemann mapping theorem for a polygonal region.

Reverse Mathematics

Which axioms are exactly needed?

Theorem

The following are provable within WWKL ₀ .

1

Every bounded continuous function on [ 0 , 1 ] is Riemann

integrable.

2

Every complex differentiable function (pointwisely) is

holomorphic, i.e., it has a continuous derivative.

3

Every bounded entire holomorphic function is a constant

function.

4

The Schwarz reflection principle.

5

The Casorati–Weierstraß theorem.

6

Picard’s little theorem.

Reverse Mathematics

Which axioms are exactly needed?

Theorem

The following are equivalent over RCA ₀ .

1

_{WKL 0} (Hiene Borel compactness for [ 0 , 1 ] ).

2

Every continuous function on [ 0 , 1 ] has a maximum.

3

The Jordan curve theorem.

4

The Jordan–Sch ¨onflies theorem.

5

The Cauchy integral theorem for a triangle.

6

The Cauchy integral theorem for a Jordan curve.

7

The Riemann mapping theorem for a Jordan region.

Reverse Mathematics

Which axioms are exactly needed?

Theorem

The following are equivalent over RCA ₀ .

1

_ACA

0 (sequential compactness [ 0 , 1 ] ).

2

Every continuous function on a bounded closed set D _{⊆ C} has

a maximum.

3

Every normal family _{F D} , i.e., _F is a family of uniformly

bounded holomorphic functions on a common domain D _{⊆ C} ,

has a uniformly convergent sub sequence.

4

For every normal family _{F D} and z _∈ D, max _{| f ^′ ( z _{)| :} f _{∈ F D }}

exists.

5

The Riemann mapping theorem.

Non-standard analysis

What is non-standard analysis?

If there were infinitely large natural numbers or infinitely small

real numbers, then . . .

Can we justify the infinitesimal calculus investigated by

Leibniz?

Non-standard analysis

What is non-standard analysis?

If there were infinitely large natural numbers or infinitely small

real numbers, then . . .

Can we justify the infinitesimal calculus investigated by

Leibniz?

Non-standard analysis

What is non-standard analysis?

If there were infinitely large natural numbers or infinitely small

real numbers, then . . .

Can we justify the infinitesimal calculus investigated by

Leibniz?

Non-standard analysis

Non-standard analysis was introduced by Abraham Robinson in

1960s (based on model theory).

Expanding the universe ( ^N _{⊆ N} ^∗ , ^R _{⊆ R} ^∗ ), we can use

infinitesimals (infinitely large and small numbers).

0 1

∗ R

R

α ^{− 1}

α

Non-standard analysis

Example. Let f be a continuous function, and f ^∗ be a non-standard

expansion of f . Let ω _{∈ N} ^∗ _{\ N} be a infinitely large number.

Then, the Riemann integral and the derivative are defined as

follows:

Riemann integral:

Z ₁

0

f ( x ) dx = st



 

 

 

ω

X

k=1

f ^∗ ( k /ω)

ω



 

 

 

.

derivative:

f ^′ ( a ) = st ^f

∗ _{( a + 1 /ω ) − f} ∗ _{( a )}

1 /ω

!

.

Non-standard analysis

Example (Bolzano Weierstraß theorem).

Let _h a _{n |} n _{∈ Ni} be a real sequence.

Let _h a _n ^∗ _| n _{∈ N} ^∗ _i be the non-standard expansion of _h a _{n |} n _{∈ Ni} .

Then, for any infinitely large number ω _{∈ N} ^∗ _{\ N} , there exists a

subsequence _h a _n

_| i _{∈ Ni} which converges to r := st( a _ω ^∗ ) .

We can do mathematics only by using bounded formulas or less

complicated ( Σ ⁰ _{1 ∪ Π} ⁰ ₁ ) formulas.

Related topics

Comparing axioms of non-standard arithmetic and

second-order arithmetic (Keisler, Henson, Kaufmann,. . . ).

Comparing axioms of non-standard arithmetic and weak

axioms of arithmetic (Inpense, Sanders).

(Model theoretic) non-standard arguments for reverse

mathematics in WKL ₀ and ACA ₀ (Tanaka, Yamzaki,

Sakamoto, Y).

Reverse Mathematics for analysis.

Question

Which axioms are essentially needed for non-standard analysis?

Outline

1 Introduction

RM and subsystems of second-order arithmetic

Non-standard analysis

Related topics

2 Non-standard second-order arithmetic

Non-standard second-order arithmetic

Axioms for non-standard analysis

Non-standard analysis in NSOA

3 Non-standard axioms and Reverse Mathematics

Reverse Mathematics for non-standard analysis

The strengh of transfer principle

Standard part principle

Language of non-standard second order arithmetic

Definition (Language _L ^∗ ₂ )

Language of non-standard second order arithmetic ( _L ^∗ ₂ ) are the

following:

s number variables: x ^s , y ^s , . . . ,

∗ number variables: x ^∗ , y ^∗ , . . . ,

s set variables: X ^s , Y ^s , . . . ,

∗ set variables: X ^∗ , Y ^∗ , . . . ,

s symbols: 0 ^s , 1 ^s , = ^s , + ^s , _· ^s , < ^s , _∈ ^s ,

∗ ^{symbols: 0 ∗ , 1 ∗ , = ∗ , + ∗ ,} · ^{∗ , < ∗ ,} ∈ ^{∗ ,}

function symbol: ^√ .

s -structure and _∗ -structure

M ^s : range of x ^s , y ^s , . . . ,

M ^∗ : range of x ^∗ , y ^∗ , . . . ,

S ^s : range of X ^s , Y ^s , . . . ,

S ^∗ : range of X ^∗ , Y ^∗ , . . . .

V ^s = ( M ^s , S ^s ; 0 ^s , 1 ^s , . . . ) : s - _{L 2} structure.

V ^∗ = ( M ^∗ , S ^∗ ; 0 ^∗ , 1 ^∗ , . . . ) : _∗ - _{L 2} structure.

√ : M ^s _∪ S ^s _→ M ^∗ _∪ S ^∗ : embedding.

We usually regard M ^s as a subset of M ^∗ .

Notations:

Let ϕ be an _{L 2} -formula.

ϕ ^s _{: L} ^∗ ₂ formula constructed by adding ^s to any _{L 2} symbols in

ϕ .

ϕ ^∗ _{: L} ^∗ ₂ formula constructed by adding ^∗ to any _{L 2} symbols in

ϕ .

x ˇ ^s := ^√ ( x ^s ) .

X ˇ ^s := ^√ ( X ^s ) .

We usually omit ^s and ^∗ of relations _{=, ≤, ∈} .

We often say “ ϕ holds in V ^s (in V ^∗ )” when ϕ ^s ( ϕ ^∗ ) holds.

classes of formulas

Σ ^S ₀ formula: all quantifiers are of the form _∀ x ^s < y ^s , _∃ x ^s < y ^s ,

∀ ^{x ∗ < y ∗ ,} ∃ ^{x ∗ < y ∗ .}

S formulas:( θ : Σ ^S ₀ formula)

Σ ^S _n formula: _∃ x ₁ ^s _∀ x ₂ ^s . . . x _n ^s θ

Π ^S _n formula: _∀ x ₁ ^s _∃ x ₂ ^s . . . x _n ^s θ

† ^{formula:( ϕ} : S formula)

Σ ^† _n formula: _∃ x ₁ ^∗ _∀ x ₂ ^∗ . . . x _n ^∗ ϕ

Π ^† _n formula: _∀ x ₁ ^∗ _∃ x ₂ ^∗ . . . x _n ^∗ ϕ

Axioms for non-standard analysis

Definition (Saturation principles)

Σ ⁱ _j WSAT ⁰ _{: (∀} x ^s _∃ y ^∗ ϕ( ˇ x ^s , y ^∗ ) ^∗ _{→ ∃} y ^∗ _∀ x ^s ϕ( ˇ x ^s , y ^∗ ) ^∗ )

for any Σ ⁱ _j formula ϕ( x , y ).

Σ ⁱ _j WSAT ¹ _{: (∀} x ^s _∃ Y ^∗ ϕ( ˇ x ^s , Y ^∗ ) ^∗ _{→ ∃} Y ^∗ _∀ x ^s ϕ( ˇ x ^s , Y ^∗ ) ^∗ )

for any Σ ⁱ _j formula ϕ( x , Y ).

Definition (Transfer principles)

Σ ⁱ _j EQ : (ϕ ^s _{↔ ϕ} ^∗ )

for any Σ ⁱ _j sentence ϕ.

Σ ⁱ _j TP _{: ∀} x ^s _∀ X ^s (ϕ( x ^s , X ^s ) ^s _{↔ ϕ( ˇ} x ^s , ˇ X ^s ) ^∗ )

for any Σ ⁱ formula ϕ( x , X ).

Definition (Standard part principles)

fst : _∀ X ^∗ (card( X ^∗ _{) ∈} M ^s

→ ∃ ^{Y s} ∀ ^{x s ( x s} ∈ ^{Y s} ↔ ˇ ^{x s} ∈ ^{X ∗ ).}

ST : _∀ X ^∗ _∃ Y ^s _∀ x ^s ( x ^s _∈ Y ^s _{↔ ˇ} x ^s _∈ X ^∗ ).

LMP _{: ∀} H ^∗ _{∈ N} ^∗ _{\ N} ^s _∀ T ^∗ _⊆ 2 ^<H

st ^card({σ

∗ _{∈ T} ∗ _{| lh(σ} ∗ _{) = H} ∗ _})

2 ^H

!

> 0

→ ∃σ ^∗ ∈ ^{T ∗ lh(σ ∗ ) = H ∗} ∧ σ ^∗ ∩ N ^s ∈ ^{V s .}

(An NS-tree which has a positive measure has a standard path.)

Definition (Basic axioms)

emb : “ ^√ is an injective homomorphism” .

e : _∀ x ^∗ _∀ y ^s ( x ^∗ < ˇ y ^s _{→ ∃} z ^s ( x ^∗ = ˇ z ^s )).

HKK transformation

Definition (Henson, Kaufmann, Keisler)

Let ϕ be an _{L 2} formula. Then, ϕ ^† is an _L ^∗ ₂ formula obtained by

replacing each x _i by x _i ^s , each X _i by x _i ^∗ , and

x _∈ Y _7→ x ^s _{∈ code(} y ^∗ )

where code( a ) is a finite set coded by a.

† ^{maps Σ 0} _j formulas to Σ _j ^S formulas, and Σ ¹ _j formulas to Σ ^† _j

formulas.

We define

Σ ^† _j - CA = (Σ ¹ _j - CA) ^† , Σ ^† _j - SEP = (Σ ¹ _j - SEP) ^† , . . .

Systems of non-standard second-order arithmetic

We define systems of non-standard second order arithmetic as

follows.

Definition

RCA ₀ ^ns =( RCA ₀ ) ^s + ( RCA ₀ ) ^∗ + emb + e + fst + Σ ⁰ ₁ WSAT ⁰

+ Σ ¹ ₁ EQ + Σ ⁰ ₀ TP.

WWKL ₀ ^ns = RCA ₀ ^ns + LMP.

WKL ₀ ^ns = RCA ₀ ^ns + ST.

ACA ₀ ^ns = RCA ₀ ^ns + ST + Σ ¹ ₁ TP + Σ ¹ ₀ WSAT ⁰ .

ATR ₀ ^ns = ACA ₀ ^ns + Σ ^† ₁ SEP + Σ ¹ ₂ TP.

Π ¹ ₁ CA ₀ ^ns = ACA ₀ ^ns + Σ ₁ ^† CA + Σ ¹ ₂ TP + Σ ¹ ₁ WSAT ¹ .

Non-standard analysis in NSOA

Within RCA ₀ ^ns , we can define real numbers, open sets,

continuous functions, complete separable metric spaces,. . . in

both s -structure and _∗ -structure.

We can also define ‘non-standard concepts’ such as standard

part, monad, s -continuous, . . .

Then, . . .

WWKL ₀ ^ns proves:

Lebesgue measure is the standard part of Loeb measure.

Riemann integral can be infinitesimally approximated by

hyperfinite Riemann sum.

WKL ₀ ^ns proves:

Every continuous function can be infinitesimally approximated

by hyperfinite broken line.

Every compact separable metric space is a standard part of a

non-standard metric space whose points are all standard.

.. .

ACA ₀ ^ns proves:

If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^.

If _{ f

_} is a normal family of holomorphic functions on a bounded

domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} .

Π ¹ ₁ CA ₀ ^ns proves:

For every closed set C of a complete separable metric space,

there exists a non-standard sequence _{ c

_} such that for any

non-standard ω, st _({ c

_| i < ω _{}) =} C.

.. .

Conservativity

Moreover,

Theorem

T ^ns is a conservative extension of T for

T _{∈ {} RCA ₀ , WWKL ₀ , WKL ₀ , ACA ₀ , ATR ₀ , Π ¹ ₁ CA _{0 }} ,

i.e., T ^ns _{⊢ ϕ} ^s implies T _{⊢ ϕ} for any _{L 2} sentence ϕ .

By this theorem, we can use non-standard analysis for standard

analysis in SOA.

Non-standard proof for standard theorem I

Example 1.

Theorem (WWKL ₀ )

If a monotone sequence of bounded continuous functions _{ f _n ^s _{} n ∈N}

on [ 0 , 1 ] converges to a continuous function f ^s pointwise, then,

each of f _n ^s and f ^s is integrable and

n lim _→∞

Z ₁

0

f _n ^s ( x ) dx =

Z ₁

0

f ^s ( x ) dx .

Proof.

Within WWKL ₀ ^ns ,

1

For every continuous function g ^s on [ 0 , 1 ] , there exists a

non-standard continuous function g ^∗ on [ 0 , 1 ] such that

g ^s ( x ^s ) = st( g ^∗ ( y ^∗ )) if x ^s = st( y ^∗ ) .

Non-standard proof for standard theorem II

2

_{If g} ^s _{and g} ∗ satisfy 1, then for any ω _{∈ N} ^∗ _{\ N} ^s ,

Z 1

0

g ^s ( x ) dx = st



 

 

 

X

i<2

g ^∗ ( i2 ^−ω )

2 ^ω



 

 

  ^.

Let _{ f _n ^∗ _{} n≤m} (m > N ^s ) and f ^∗ be non-standard continuous functions

taken by 1, and let ω _{∈ N} ^∗ _{\ N} ^s . Then, by Σ ⁰ ₁ - WSAT ⁰ and 2, there

exists H > N ^s such that for any ^{N s} < n < H,

st _(| S ( f _n ^∗ ; ∆ _{ω ) −} S ( f ^∗ ; ∆ _{ω )|) =} 0. Thus, again by Σ ⁰ ₁ - WSAT ⁰ ,

∀ ^k ∈ N ^s ∃ ^l ∈ N ^s ∀ ⁿ ≥ ^l | ^{S ( f} n ^{∗ ; ∆} ω ) − ^{S ( f ∗ ; ∆} ω )| ≤ ^{2 −k .}

Again by 2, we have lim _{n →∞} ^R ₀ ¹ f _n ^s ( x ) dx = ^R ₀ ¹ f ^s ( x ) dx. _

Non-standard proof for standard theorem III

Example 2.

Theorem (WKL ₀ )

Let f : R ² _{→ R} be a continuous function. Then, there exists a

maximal global solution x : D _{→ R} of the following initial value

problem.



 



 



x ( 0 ) = 0 ,

dx

dt ^{= f ( x ( t ), t ).}

Proof.

We use the following Cauchy/Peano theorem.

Non-standard proof for standard theorem IV

Lemma (WKL ₀ )

Let f : [ 0 , 1 ] ² _{→ [−} 1 , 1 ] be a continuous function. Then, there exists

a solution y : [ 0 , 1 _{] → R} of the following initial value problem.



 



 



x ( 0 ) = 0 ,

dy

dt ^{= f ( y ( t ), t ).}

Within WKL ₀ ^ns , we can expand f into a non-standard continuous

function ^¯ f such that st(¯ f ) = f and _|¯ f _{| <} M for some M > N ^s . Then,

apply the Cauchy/Peano theorem for an infinite interval _{[−ω, ω]}

( ω > N ^s ) for ^¯ f , and take a local solution y : [−ω, ω] → R ^{∗ .}

Non-standard proof for standard theorem V

By infinitesimal approximation, there exists a bloken line

¯

x : [−ω, ω] → R ^{∗ such that x ¯} ≈ y and satisfies the following:

¯

x ( t _{) ≈} S (¯ f (¯ x ( t ), t ); ∆) (1)

for any infinitesimal splittng ∆ of [ 0 , t ] .

For n _{∈ N} ^∗ , let

p _n = inf _{ t : t _≤ s _≤ 0 _{→ |¯} x ( s _{)| ≤} n _} ,

q _n = inf _{ t : 0 _≤ s _≤ t _{→ |¯} x ( s _{)| ≤} n _} .

Then, for any n _{∈ N} ^s , x is ¯ s -continuous on ( p _n , q _n ) by (1).

Thus, the standard part x = st(¯ x ) is a maximal global solution on

D _{= ∪ n ∈N}

( p _n , q _n ) . _

Outline

1 Introduction

RM and subsystems of second-order arithmetic

Non-standard analysis

Related topics

2 Non-standard second-order arithmetic

Non-standard second-order arithmetic

Axioms for non-standard analysis

Non-standard analysis in NSOA

3 Non-standard axioms and Reverse Mathematics

Reverse Mathematics for non-standard analysis

The strengh of transfer principle

Standard part principle

Question

Which axioms are essentially needed for non-standard analysis?

Reverse Mathematics for non-standard analysis

WWKL ₀ ^ns proves:

Lebesgue measure is the standard part of Loeb measure.

Riemann integral can be infinitesimally approximated by

hyperfinite Riemann sum.

Reverse Mathematics for non-standard analysis

Within RCA ₀ ^ns ,

“Lebesgue measure is the standard part of Loeb measure”

⇔ ^WWKL

^.

“Riemann integral can be infinitesimally approximated by

hyperfinite Riemann sum”

⇔ ^WWKL

^.

This means that LMP is equivalent to “approximation for measure

and integral”.

Reverse Mathematics for non-standard analysis

Within RCA ₀ ^ns ,

“Lebesgue measure is the standard part of Loeb measure”

⇔ ^WWKL

^.

“Riemann integral can be infinitesimally approximated by

hyperfinite Riemann sum”

⇔ ^WWKL

^.

This means that LMP is equivalent to “approximation for measure

and integral”.

Reverse Mathematics for non-standard analysis

WKL ₀ ^ns proves:

Every continuous function can be infinitesimally approximated

by hyperfinite broken line.

Every compact separable metric space is a standard part of a

non-standard metric space whose points are all standard.

Reverse Mathematics for non-standard analysis

Within RCA ₀ ^ns ,

Every continuous function can be infinitesimally approximated

by hyperfinite broken line.

⇔ ^WKL

^.

Every compact separable metric space is a standard part of a

non-standard metric space whose points are all standard.

⇔ ^WKL

^.

This means that ST is equivalent to “approximation for continuous

functions”.

Reverse Mathematics for non-standard analysis

Within RCA ₀ ^ns ,

Every continuous function can be infinitesimally approximated

by hyperfinite broken line.

⇔ ^WKL

^.

Every compact separable metric space is a standard part of a

non-standard metric space whose points are all standard.

⇔ ^WKL

^.

This means that ST is equivalent to “approximation for continuous

functions”.

Reverse Mathematics for non-standard analysis

ACA ₀ ^ns proves:

If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^.

If _{ f

_} is a normal family of holomorphic functions on a bounded

domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} .

Π ¹ ₁ CA ₀ ^ns proves:

For every closed set C of a complete separable metric space,

there exists a non-standard sequence _{ c

_} such that for any

non-standard ω, st _({ c

_| i < ω _{}) =} C.

Reverse Mathematics for non-standard analysis?

Within RCA ₀ ^ns ,

“If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^”

; _ACA

_.

“If _{ f

_} is a normal family of holomorphic functions on a

bounded domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} ”

; _ACA

_.

Within RCA ₀ ^ns ,

For every closed set C of a complete separable metric space,

there exists a non-standard sequence _{ c

_} such that for any

non-standard ω, st _({ c

_| i < ω _{}) =} C.

; _Π

1

^CA

_.

Reverse Mathematics for non-standard analysis?

Within RCA ₀ ^ns ,

“If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^”

; _ACA

_.

“If _{ f

_} is a normal family of holomorphic functions on a

bounded domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} ”

; _ACA

_.

Why?

⇒ These are provable within WKL ₀ ^ns + Σ ¹ ₀ TP, but Σ ¹ ₁ TP is not

provable from WKL ₀ ^ns + Σ ¹ ₀ TP.

In fact, Σ ¹ ₁ TP is non-standard over WKL ₀ ^ns + Σ ¹ ₀ TP, i.e.,

WKL ₀ ^ns + Σ ¹ ₀ TP +( TA ² ) ^s does not prove Σ ¹ ₁ TP.

Reverse Mathematics for non-standard analysis?

Within RCA ₀ ^ns ,

“If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^”

; _ACA

_.

“If _{ f

_} is a normal family of holomorphic functions on a

bounded domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} ”

; _ACA

_.

Why?

⇒ These are provable within WKL ₀ ^ns + Σ ¹ ₀ TP, but Σ ¹ ₁ TP is not

provable from WKL ₀ ^ns + Σ ¹ ₀ TP.

In fact, Σ ¹ ₁ TP is non-standard over WKL ₀ ^ns + Σ ¹ ₀ TP, i.e.,

WKL ₀ ^ns + Σ ¹ ₀ TP +( TA ² ) ^s does not prove Σ ¹ ₁ TP.

Reverse Mathematics for non-standard analysis?

Within RCA ₀ ^ns ,

“If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^”

; _ACA

_.

“If _{ f

_} is a normal family of holomorphic functions on a

bounded domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} ”

; _ACA

_.

Why?

⇒ These are provable within WKL ₀ ^ns + Σ ¹ ₀ TP, but Σ ¹ ₁ TP is not

provable from WKL ₀ ^ns + Σ ¹ ₀ TP.

In fact, Σ ¹ ₁ TP is non-standard over WKL ₀ ^ns + Σ ¹ ₀ TP, i.e.,

WKL ₀ ^ns + Σ ¹ ₀ TP +( TA ² ) ^s does not prove Σ ¹ ₁ TP.

Transfer principle

We need to compare TP with axioms of second-order arithmetic.

However, . . .

Theorem

WKL ₀ ^ns + Σ ¹ ₀ TP + (TA ² ) ^s does not prove Σ ¹ ₁ TP .

Theorem

1

(Impense, Sanders) PRA ⊢ Con(ERNA + ˇ ^{Σ 0} ₂ ^{TP) .}

( ERNA : Elementary Recursive Non-standard Analysis)

2

_{RCA 0} ^ns _{+ ST + Σ} ⁰

2 ^{TP ⊢ ACA 0 .}

The strengh of transfer principle

On the other hand,

Theorem

1

_Σ ¹

0 ^{TP < Σ}

1

1 ^{TP < Σ}

1

2 ^{TP over RCA 0}

ns _{+ ST .}

2

_{RCA 0} ^ns _{+ ST + Σ} ¹

2 ^{TP ≡ Π}

^{ACA 0 .}

3

_RCA

0 ^{ns + ST + Σ 1} ₂ ^{TP + (Σ 1} ₁ ^{-IND ) s} ⊢ Π ¹ ₁ ^CA 0 ^.

The strengh of transfer principle

Similarly,

Theorem

1

_{RCA 0} ^ns _{+ ST + Σ} ¹

n ⁺ 2 ^{TP ≡ Π}

^Π

1 n ^{-CA 0 ,}

and

Π ¹ _n -CA ₀ + Σ ¹ _n+1 -IND _{⊢ Con(} RCA ₀ ^ns + ST + Σ ¹ _n+2 TP) .

2

_RCA

0 ^{ns + ST + Σ 1} _n+2 ^{TP + (Σ 1} _n+1 ^{-IND ) s} ⊢ Π ¹ _n+1 ^-CA 0 ^.

The strength of TP is heavily depends on the base system of

second-order arithmetic.

(As far as I know,) there is no theorem in non-standard analysis

which implies some strong ( Σ ¹ ₁ , . . . ) transfer principle.

The strengh of transfer principle

Similarly,

Theorem

1

_{RCA 0} ^ns _{+ ST + Σ} ¹

n ⁺ 2 ^{TP ≡ Π}

^Π

1 n ^{-CA 0 ,}

and

Π ¹ _n -CA ₀ + Σ ¹ _n+1 -IND _{⊢ Con(} RCA ₀ ^ns + ST + Σ ¹ _n+2 TP) .

2

_RCA

0 ^{ns + ST + Σ 1} _n+2 ^{TP + (Σ 1} _n+1 ^{-IND ) s} ⊢ Π ¹ _n+1 ^-CA 0 ^.

The strength of TP is heavily depends on the base system of

second-order arithmetic.

(As far as I know,) there is no theorem in non-standard analysis

which implies some strong ( Σ ¹ ₁ , . . . ) transfer principle.

The strengh of transfer principle

Similarly,

Theorem

1

_{RCA 0} ^ns _{+ ST + Σ} ¹

n ⁺ 2 ^{TP ≡ Π}

^Π

1 n ^{-CA 0 ,}

and

Π ¹ _n -CA ₀ + Σ ¹ _n+1 -IND _{⊢ Con(} RCA ₀ ^ns + ST + Σ ¹ _n+2 TP) .

2

_RCA

0 ^{ns + ST + Σ 1} _n+2 ^{TP + (Σ 1} _n+1 ^{-IND ) s} ⊢ Π ¹ _n+1 ^-CA 0 ^.

The strength of TP is heavily depends on the base system of

second-order arithmetic.

(As far as I know,) there is no theorem in non-standard analysis

which implies some strong ( Σ ¹ ₁ , . . . ) transfer principle.

Reverse Mathematics for non-standard analysis?

Within RCA ₀ ^ns ,

“If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^”

; _ACA

_.

“If _{ f

_} is a normal family of holomorphic functions on a

bounded domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} ”

; _ACA

_.

What is essential?

Standard part principle

Definition (Standard part principles)

Σ ^† _i ST _{: ∃} Y ^s _∀ x ^s ( x ^s _∈ Y ^s _{↔ ϕ(} x ^s ))

for any Σ ^† _i formula ϕ( x ^s ).

Then,

Within RCA ₀ ^ns ,

“If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^”

⇔ Σ

^ST.

“If _{ f

_} is a normal family of holomorphic functions on a

bounded domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} ”

⇔ Σ

^ST.

†

Standard part principle

Definition (Standard part principles)

Σ ^† _i ST _{: ∃} Y ^s _∀ x ^s ( x ^s _∈ Y ^s _{↔ ϕ(} x ^s ))

for any Σ ^† _i formula ϕ( x ^s ).

Then,

Within RCA ₀ ^ns ,

“If _{ a

_} is a bounded sequence of standard real numbers, then

for some non-standard ω, st(a

) is an accumulation value of

{ ^a

} ^”

⇔ Σ

^ST.

“If _{ f

_} is a normal family of holomorphic functions on a

bounded domain, then for some non-standard ω, st(f

) is an

accumulation value of _{ f

_} ”

⇔ Σ

^ST.

†

Reverse Mathematics for non-standard analysis!

Similarly,

Within RCA ₀ ^ns ,

For every closed set C of a complete separable metric space,

there exists a non-standard sequence _{ c

_} such that for any

non-standard ω, st _({ c

_| i < ω _{}) =} C.

⇔ Σ

^ST.

This means that Σ ^† ₁ ST is equivalent to “approximation for closed

sets”.

Reverse Mathematics for non-standard analysis!

Similarly,

Within RCA ₀ ^ns ,

For every closed set C of a complete separable metric space,

there exists a non-standard sequence _{ c

_} such that for any

non-standard ω, st _({ c

_| i < ω _{}) =} C.

⇔ Σ

^ST.

This means that Σ ^† ₁ ST is equivalent to “approximation for closed

sets”.

Systems of non-standard second-order arithmetic

We should redefine systems of non-standard second order

arithmetic as follows(?)

Definition

RCA ₀ ^ns =( RCA ₀ ) ^s + ( RCA ₀ ) ^∗ + emb + e + fst + Σ ⁰ ₁ WSAT ⁰

+ Σ ¹ ₁ EQ + Σ ⁰ ₀ TP.

WWKL ₀ ^ns = RCA ₀ ^ns + LMP.

WKL ₀ ^ns = RCA ₀ ^ns + ST.

ACA ₀ ^ns = RCA ₀ ^ns + Σ ^† ₀ ST.

ATR ₀ ^ns = ACA ₀ ^ns + Σ ^† ₁ SEP(?).

Π ¹ ₁ CA ₀ ^ns = ACA ₀ ^ns + Σ ^† ₁ ST.

Conclusion

Standard part principles provide the infinitesimal

approximation principles.

Standard part principles correspond to the comprehension

axioms in SOA in the viewpoint of Reverse Mathematics.

The strength of transfer principles is unstable (it depends

heavily on the base system).

Propositions in non-standard analysis usually do NOT require

strong transfer principles.

Question

What is the role of transfer principle in non-standard analysis?

How can we measure the strength of transfer principle?