Non-standard proof for standard theorem I
Example 1.
Theorem (WWKL 0 )
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 1
0
f n s ( x ) dx = Z 1
0
f s ( x ) dx .
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 Σ 0 1 - WSAT 0 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 Σ 0 1 - WSAT 0 ,
∀ k ∈ N s ∃ l ∈ N s ∀ n ≥ l | S ( f n ∗ ; ∆ ω ) − S ( f ∗ ; ∆ ω ) | ≤ 2 −k . Again by 2, we have lim n →∞ R 1
0 f n s ( x ) dx = R 1
0 f s ( x ) dx.
Non-standard proof for standard theorem III
Example 2.
Theorem (WKL 0 )
Let f : R 2 → 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 0 )
Let f : [ 0 , 1 ] 2 → [ − 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 0 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
s( 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 0 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 0 ns ,
“Lebesgue measure is the standard part of Loeb measure”
⇔ WWKL
0ns.
“Riemann integral can be infinitesimally approximated by hyperfinite Riemann sum”
⇔ WWKL
0ns.
This means that LMP is equivalent to “approximation for measure
and integral”.
Reverse Mathematics for non-standard analysis
Within RCA 0 ns ,
“Lebesgue measure is the standard part of Loeb measure”
⇔ WWKL
0ns.
“Riemann integral can be infinitesimally approximated by hyperfinite Riemann sum”
⇔ WWKL
0ns.
This means that LMP is equivalent to “approximation for measure
and integral”.
Reverse Mathematics for non-standard analysis
WKL 0 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 0 ns ,
Every continuous function can be infinitesimally approximated by hyperfinite broken line.
⇔ WKL
0ns.
Every compact separable metric space is a standard part of a non-standard metric space whose points are all standard.
⇔ WKL
0ns.
This means that ST is equivalent to “approximation for continuous
functions”.
Reverse Mathematics for non-standard analysis
Within RCA 0 ns ,
Every continuous function can be infinitesimally approximated by hyperfinite broken line.
⇔ WKL
0ns.
Every compact separable metric space is a standard part of a non-standard metric space whose points are all standard.
⇔ WKL
0ns.
This means that ST is equivalent to “approximation for continuous
functions”.
Reverse Mathematics for non-standard analysis
ACA 0 ns proves:
If { a
ns} is a bounded sequence of standard real numbers, then for some non-standard ω, st(a
ω∗) is an accumulation value of { a
ns} .
If { f
n} is a normal family of holomorphic functions on a bounded domain, then for some non-standard ω, st(f
ω∗) is an
accumulation value of { f
ns} . Π 1 1 CA 0 ns proves:
For every closed set C of a complete separable metric space,
there exists a non-standard sequence { c
n∗} such that for any
non-standard ω, st( { c
i∗| i < ω } ) = C.
Reverse Mathematics for non-standard analysis?
Within RCA 0 ns ,
“If { a
ns} is a bounded sequence of standard real numbers, then for some non-standard ω, st(a
ω∗) is an accumulation value of { a
ns} ”
; ACA
0ns.
“If { f
n} is a normal family of holomorphic functions on a bounded domain, then for some non-standard ω, st(f
ω∗) is an accumulation value of { f
ns} ”
; ACA
0ns. Within RCA 0 ns ,
For every closed set C of a complete separable metric space, there exists a non-standard sequence { c
n∗} such that for any non-standard ω, st( { c
i∗| i < ω } ) = C.
; Π
11CA
0ns.
Reverse Mathematics for non-standard analysis?
Within RCA 0 ns ,
“If { a
ns} is a bounded sequence of standard real numbers, then for some non-standard ω, st(a
ω∗) is an accumulation value of { a
ns} ”
; ACA
0ns.
“If { f
n} is a normal family of holomorphic functions on a bounded domain, then for some non-standard ω, st(f
ω∗) is an accumulation value of { f
ns} ”
; ACA
0ns. Why?
⇒ These are provable within WKL 0 ns + Σ 1 0 TP, but Σ 1 1 TP is not provable from WKL 0 ns + Σ 1 0 TP.
In fact, Σ 1 1 TP is non-standard over WKL 0 ns + Σ 1 0 TP, i.e.,
WKL 0 ns + Σ 1 0 TP +( TA 2 ) s does not prove Σ 1 1 TP.
Reverse Mathematics for non-standard analysis?
Within RCA 0 ns ,
“If { a
ns} is a bounded sequence of standard real numbers, then for some non-standard ω, st(a
ω∗) is an accumulation value of { a
ns} ”
; ACA
0ns.
“If { f
n} is a normal family of holomorphic functions on a bounded domain, then for some non-standard ω, st(f
ω∗) is an accumulation value of { f
ns} ”
; ACA
0ns. Why?
⇒ These are provable within WKL 0 ns + Σ 1 0 TP, but Σ 1 1 TP is not provable from WKL 0 ns + Σ 1 0 TP.
In fact, Σ 1 1 TP is non-standard over WKL 0 ns + Σ 1 0 TP, i.e.,
WKL 0 ns + Σ 1 0 TP +( TA 2 ) s does not prove Σ 1 1 TP.
Reverse Mathematics for non-standard analysis?
Within RCA 0 ns ,
“If { a
ns} is a bounded sequence of standard real numbers, then for some non-standard ω, st(a
ω∗) is an accumulation value of { a
ns} ”
; ACA
0ns.
“If { f
n} is a normal family of holomorphic functions on a bounded domain, then for some non-standard ω, st(f
ω∗) is an accumulation value of { f
ns} ”
; ACA
0ns. Why?
⇒ These are provable within WKL 0 ns + Σ 1 0 TP, but Σ 1 1 TP is not provable from WKL 0 ns + Σ 1 0 TP.
In fact, Σ 1 1 TP is non-standard over WKL 0 ns + Σ 1 0 TP, i.e.,
WKL 0 ns + Σ 1 0 TP +( TA 2 ) s does not prove Σ 1 1 TP.
Transfer principle
We need to compare TP with axioms of second-order arithmetic.
However, . . . Theorem
WKL 0 ns + Σ 1 0 TP + (TA 2 ) s does not prove Σ 1 1 TP .
Theorem
1
(Impense, Sanders) PRA ⊢ Con(ERNA + ˇ Σ 0 2 TP) . ( ERNA : Elementary Recursive Non-standard Analysis)
2
RCA 0 ns + ST + Σ 0 2 TP ⊢ ACA 0 .
The strengh of transfer principle
On the other hand, Theorem
1
Σ 1 0 TP < Σ 1 1 TP < Σ 1 2 TP over RCA 0 ns + ST .
2
RCA 0 ns + ST + Σ 1 2 TP ≡ Π
1
ドキュメント内
ファイル置き場 Sendai Logic Homepage
(ページ 47-66)