ファイル置き場 Sendai Logic Homepage

(1)

Nonstandard counterparts of

several weak axioms

Keita Yokoyama (joint work with Kojiro Higuchi)

Mathematical Institute, Tohoku University

July 23, 2010

(2)

Outline

1 Introduction Related topics

Nonstandard second-order arithmetic Axioms for nonstandard arithmetic

2 Weak nonstandard axioms from recursion A nonstandard approach for recursion MLR^∗and DNR^∗

Nonstandard extension

3 Conservativity

r-extension and d-extension Proof of conservation results

4 Future work

(3)

Outline

3 Conservativity

4 Future work

(4)

Nonstandard analysis and arithmetic

(Model theoretic) nonstandard arguments for reverse mathematics in WKL₀and ACA₀(Tanaka, Yamzaki, Sakamoto, Y).

Comparing axioms of nonstandard arithmetic and

second-order arithmetic (Keisler, Henson, Kaufmann,. . . ). Formalizing analysis and nonstandard analysis within nonstandard arithmetic, and doing Reverse Mathematics (Impens, Sanders, Y).

⇐Motivated by Prof. Fuchino’s question.

Searching nonstandard counterparts of systems of second-order arithmetic (Keisler, Y).

Comparing axioms of nonstandard arithmetic and weak axioms of arithmetic (Impens, Sanders).

(5)

Nonstandard analysis and arithmetic

(6)

Nonstandard analysis and arithmetic

(7)

Nonstandard analysis and arithmetic

(8)

Nonstandard analysis and arithmetic

(9)

Nonstandard analysis and arithmetic

Searching nonstandard counterparts of systems of second-order arithmetic(Keisler, Y).

(10)

Language of nonstandard second order arithmetic

Language of second-order arithmetic:_L₂_{= {}0,1,=, +, ·, <, ∈}^. We expand_L₂to_L^∗₂.

Definition (Language_L^∗₂)

Language of nonstandard second-order arithmetic (_L^∗₂) consists of snumber variables: x^s,y^s, . . .,

∗number variables: x^∗,y^∗, . . ., sset variables: X^s,Y^s, . . .,

∗set variables: X^∗,Y^∗, . . ., ssymbols: 0^s,1^s,=^s,+^s,_·^s, <^s,_∈^s,

∗^{symbols: 0}^∗^,¹^∗^,⁼^∗^,⁺^∗^,·^∗^{, <}^∗^,∈^∗^, function symbol: ^√.

(11)

s -structure and _∗ -structure

M^s: range of x^s,y^s, . . ., N, the standard numbers M^∗: range of x^∗,y^∗, . . ., N^∗, the nonstandard numbers S^s: range of X^s,Y^s, . . ., subsets ofN

S^∗: range of X^∗,Y^∗, . . . subsets ofN^∗. V^s= (M^s,S^s;0^s,1^s, . . .):s-_L₂ structure. V^∗= (M^∗,S^∗;0^∗,1^∗, . . .):_∗-_L₂ structure.

√:M^s_∪S^s_→M^∗_∪S^∗: embedding. We usually regard M^sis a subset of M^∗.

(12)

Notations:

Letϕbe an_L₂-formula.

ϕ^s_{: L}^∗₂formula constructed by adding^sto_L₂symbols inϕ. ϕ^∗_{: L}^∗₂formula constructed by adding^∗to_L₂ symbols inϕ. xˇ^s:=^√(x^s).

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

We usually omit^sand^∗of relations_{=, ≤, ∈}.

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

(13)

Systems of nonstandard arithmetic

Definition (base system)

RCA₀^nsconsists of the following: (RCA₀)^s.

√:V^s_→V^∗is an injective homomorphism. M^∗is an end extension of M^s.

finite standard part principle:

∀^X^∗^(card(^X^∗) ∈^M^s→ ∃^Y^s∀^x^s⁽^x^s∈^Y^s↔ ˇ^x^s∈^X^∗⁾^. Σ⁰₁saturation: for anyϕ_{∈ Σ}⁰₁,

(∀^x^s∃^y^∗^{ϕ( ˇ}^x^s^,^y^∗⁾^∗→ ∃^y^∗∀^x^s^{ϕ( ˇ}^x^s^,^y^∗⁾^∗⁾^. Σ⁰₀transfer principle: for anyϕ_{∈ Σ}⁰₀,

∀^x^s∀^X^s^(ϕ(^x^s^,^X^s⁾^s↔ ϕ( ˇ^x^s^{, ˇ}^X^s⁾^∗⁾^.

Σ¹₁equivalence: for any sentenceϕ_{∈ Σ}¹₁, (ϕ^s_{↔ ϕ}^∗).

(14)

Systems of nonstandard arithmetic

In short,

RCA₀^nsconsists of the following:

(RCA₀)^s: base theory of Reverse Mathematics plus

innocent nonstandard axioms.

RCA₀^nsis a weak nonstandard theory that can still define real numbers, continuous functions, . . . .

Theorem

RCA₀^nsis a conservative extension of RCA₀.

(15)

Systems of nonstandard arithmetic

In short,

Theorem

(16)

Systems of nonstandard arithmetic

In short,

Theorem

(17)

Systems of nonstandard arithmetic

Definition

WKL₀^nsconsists of RCA₀^nsplus the standard part principle (STP) which asserts that

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

WKL₀^nsis a conservative extension of WKL₀.

(18)

Systems of nonstandard arithmetic

Definition

ACA₀^nsconsists of WKL₀^nsplusΣ¹₁ transfer principle (Σ¹₁TP) Σ¹₁TP_{: ∀}x^s_∀X^s(ϕ(x^s,X^s)^s_{↔ ϕ( ˇ}x^s, ˇX^s)^∗) for any for anyϕ_{∈ Σ}¹₁.

Theorem

ACA₀^nsis a conservative extension of ACA₀.

(19)

Systems of nonstandard arithmetic

Definition

WWKL₀^nsconsists of RCA₀^nsplus the Loeb measure principle (LMP) which asserts that

LMP_{: ∀}H^∗_{∈ N}^∗_{\ N}^s_∀T^∗_⊆2^<H^∗ st^{( card({σ}

∗_∈_T∗_{| lh(σ}∗_{) =}_H∗_})

2^H^∗

)

>0

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

LMP:an NS-tree which has a positive measure has a standard path. Theorem (Simpson, Y)

WWKL₀^nsis a conservative extension of WWKL₀.

(20)

Nonstandard reverse mathematics

Within RCA₀^ns, we can develop basic part of nonstandard analysis. Moreover, within RCA₀^ns,

“Lebesgue measure is the standard part of Loeb measure”

⇔^WWKL⁰^ns^.

“Riemann integral can be infinitesimally approximated by hyperfinite Riemann sum”

⇔^WWKL0^ns^.

Every continuous function can be infinitesimally approximated by hyperfinite broken line.

⇔^WKL⁰^ns^.

Every compact separable metric space is a standard part of a nonstandard metric space whose points are all standard.

⇔^WKL0^ns^.

(21)

Nonstandard reverse mathematics

“If_{a_n^s_}is a bounded sequence of real numbers, then for some nonstandardω,st(a_ω^∗)is an accumulation value of_{a_n^s_}” (nonstandard Bolzano-Weierstraß theorem)

⇐^ACA⁰^ns^.

“If_{f_n_}is a normal family of holomorphic functions on a bounded domain, then for some nonstandardω,st(f_ω^∗)is an accumulation value of_{f_n^s_}”

⇐^ACA0^ns^.

These Reverse Mathematics phenomena show that

WWKL₀^ns,WKL₀^ns, . . . are nice nonstandard counterparts of second-order arithmetic.

⇒Can we find nonstandard counterparts of other systems such asDNR,MLR,COH,. . . ?

(22)

Nonstandard reverse mathematics

⇐^ACA⁰^ns^.

⇐^ACA0^ns^.

(23)

Nonstandard reverse mathematics

⇐^ACA⁰^ns^.

⇐^ACA0^ns^.

(24)

Outline

3 Conservativity

4 Future work

(25)

Nonstandard Turing Machine

Can we expand recursive notion into nonstandard analysis? Let_{e_}^A_s(x)be the result of the calculation of e-th Turing machine with an input x and an oracle A by s steps.

For a (standard or nonstandard) natural numberα,code(α)

denotes the finite set coded byα. Ifαis nonstandard,code(α)may be a hyperfinite set.

Definition

For a nonstandard natural numberα

{^e}^α⁽^x^{) =}^y⇔ ∃^s ∈ N^s{^e}^α↾ss ⁽^x^{) =}^y

whereα ↾s= code(α) ↾s.

By this definition, we can use the notionα-recursive for a nonstandard natural numberα.

(26)

Nonstandard Turing Machine

Definition

{^e}^α⁽^x^{) =}^y⇔ ∃^s ∈ N^s{^e}^α↾ss ⁽^x^{) =}^y

(27)

Nonstandard Turing Machine

Definition

{^e}^α⁽^x^{) =}^y⇔ ∃^s ∈ N^s{^e}^α↾ss ⁽^x^{) =}^y

(28)

MLR

^∗

and DNR

^∗

Using the notion ofα-recursive for a nonstandard natural number α, we define nonstandard axioms for some recursive notions.

MLR: for any set A , there exists X such that X is Martin-L ¨of random relative to A .

MLR^∗: for any nonstandard numberα, there exists X such that X is Martin-L ¨of random relative toα.

DNR: for any set A , there exists X such that X is diagonally non-recursive relative to A .

DNR^∗: for any nonstandard numberα, there exists X such that X is diagonally non-recursive relative toα.

(29)

MLR

^∗

and DNR

^∗

MLR: for any set A , there exists X such that X is Martin-L ¨of random relative to A .

MLR^∗: for any nonstandard numberα, there exists X such that X is Martin-L ¨of random relative toα.

DNR: for any set A , there exists X such that X is diagonally non-recursive relative to A .

DNR^∗: for any nonstandard numberα, there exists X such that X is diagonally non-recursive relative toα.

(30)

MLR

^∗

and DNR

^∗

MLR: for anyset A, there exists X such that X is Martin-L ¨of random relative to A .

MLR^∗: for anynonstandard numberα, there exists X such that X is Martin-L ¨of random relative toα.

DNR: for anyset A, there exists X such that X is diagonally non-recursive relative to A .

DNR^∗: for anynonstandard numberα, there exists X such that X is diagonally non-recursive relative toα.

(31)

Main theorems

IsDNR^∗(MLR^∗) a nonstandard counterpart ofDNR(MLR)?

⇒^Yes. Theorem

DNR^∗is a nonstandard counterpart ofDNR.

Theorem (Simpson, Y)

MLR^∗is a nonstandard counterpart ofMLR.

Here, “nonstandard counterpart” means that it is a ‘nonstandard extension’ and a ‘conservative extension (w.r.t. standard

formulas)’.

(32)

Main theorems

⇒^Yes. Theorem

formulas)’.

(33)

Main theorems

⇒^Yes. Theorem

formulas)’.

(34)

WWKL

₀^ns

and MLR

^∗

Note that Fact

1 _MLRis equivalent to weak weak K ¨onig’s lemma over RCA₀.

2 _MLR∗is equivalent toLMPover RCA₀^ns. Thus,

‘MLR^∗is a nonstandard counterpart ofMLR’ is just a restatement of

‘WWKL₀^ns=RCA₀^ns+ LMPis a nonstandard counterpart of WWKL₀’.

(35)

Nonstandard extension

Within RCA₀^ns, we can code subsets ofNwith nonstandard numbers.

Lemma

For any set A , there existsα_{∈ N}^∗such that

∀ⁿ∈ N^sⁿ∈^A ↔ⁿ∈ code(α). Thus, we have the following:

Proposition

RCA₀^ns+ DNR^∗provesDNR. Proposition

RCA₀^ns+ MLR^∗provesMLR.

(36)

MLR

^∗

and MLR

Is MLR^∗strictly stronger than MLR?

⇒^Yes. Fact

RCA₀^ns+ MLR^∗+ Σ⁰₁TPproves that there exists a 2-random real.

RCA₀^ns+ MLR + Σ⁰₁TPdoes not prove that there exists a 2-random real.

Thus, Proposition

RCA₀^ns+ MLRdoes not proveMLR^∗.

(37)

MLR

^∗

and MLR

⇒^Yes. Fact

Thus, Proposition

(38)

MLR

^∗

and MLR

⇒^Yes. Fact

Thus, Proposition

(39)

DNR

^∗

and DNR

Is DNR^∗strictly stronger than DNR?

⇒^Yes. Fact

RCA₀^ns+ DNR^∗+ Σ⁰₁TPproves that there exists a diagonally non-recursive set relative to 0^′.

RCA₀^ns+ DNR + Σ⁰₁TPdoes not prove that there exists a diagonally non-recursive set relative to 0^′.

Thus, Proposition

RCA₀^ns+ DNRdoes not proveDNR^∗.

(40)

DNR

^∗

and DNR

⇒^Yes. Fact

Thus, Proposition

(41)

DNR

^∗

and DNR

⇒^Yes. Fact

Thus, Proposition

(42)

Outline

3 Conservativity

4 Future work

(43)

Conservativity

Now, we prove the conservation results. Theorem (review)

RCA₀^ns+ MLR^∗is a conservative extension of RCA₀+ MLR.

Theorem

RCA₀^ns+ DNR^∗is a conservative extension of RCA₀+ DNR. We use the similar way to prove these theorems.

We first prepare ‘r-extension’ and ‘d-extension’.

(44)

randomness and r-extension

For S_⊆S^′ _{⊆ P(N)},

S _⊆_r S^′ _⇔ for any A _∈S^′there exists X _∈S such that X is random relative to A .

Proposition (Downey et. el. 2005, Reiman and Slaman 2010) If X _∈2^ωis Martin-L ¨of random, then for any nonemptyΠ⁰₁-class P _⊆2^ω there exists A_∈P such that X is Martin-L ¨of random relative to A .

Combining Harrington’s forcing with the previous proposition, we have the following.

Lemma (r-extension)

Let(M,S_{) |=}RCA₀+ MLRbe a countable model. Then, there exists anω-extensionS^¯ _⊇_r S such that(M, ¯S_{) |=}WKL₀.

(45)

randomness and r-extension

For S_⊆S^′ _{⊆ P(N)},

S _⊆_r S^′ _⇔ for any A _∈S^′there exists X _∈S such that X is random relative to A .

Proposition (Downey et. el. 2005, Reiman and Slaman 2010) If X _∈2^ωis Martin-L ¨of random, then for any nonemptyΠ⁰₁-class P _⊆2^ω there exists A_∈P such that X is Martin-L ¨of random relative to A .

Lemma (r-extension)

Let(M,S_{) |=}RCA₀+ MLRbe a countable model. Then, there exists anω-extensionS^¯ _⊇_r S such that(M, ¯S_{) |=}WKL₀.

(46)

DNR and _Π

⁰₁

-class

To prove conservativity forDNR^∗, we first prepare the following proposition for DNR-functions.

Proposition

If f is diagonally non-recursive, then for any nonemptyΠ⁰₁-class P _⊆2^ω there exists A_∈P such that there exists g_≤_T f which is diagonally non-recursive relative to A .

(47)

DNR and _Π

⁰₁

-class

Sketch of the proof.

For anyσ_∈2^<ωand for any T _⊆2^<ω, we define T(σ)by T_{(σ) = {τ ∈}T _{| (∀}e<lh_(σ))[{e_}^τ

lh(τ)⁽ê^{) ↓=⇒ σ(}ê^{) , {}ê^} τ

lh(τ)⁽^e^)]}.

Choose a recursive binary tree T such that[T] =P and a recursive function q_∈S such that

{^q⁽^s^{, σ})}(^x) := (leastz_)[(∃y_{)(∀τ ∈}T_{(σ) ∩}2^y)[z_{= {}s_}^τ_lh(τ)(s_{) ↓]].} Let g(s) =f(q(s,g↾s))and Q = ∩_s[T(g↾s)]. Then g_≤_T f and Q^,_∅.

(^∩_s[T(g↾s_{)] , ∅}can be proved by induction on s.)

Take A _∈Q arbitrary, then g is diagonally non-recursive relative to A sinceτ_∈T(g↾e+1)implies g(e_{) , {}e_}^τ(e).

(48)

DNR and d-extension

For S_⊆S^′ _{⊆ P(N)},

S _⊆_d S^′ _⇔ for any A _∈S^′there exists g_∈S such that g is diagonally non-recursive relative to A .

Proposition (review)

Lemma (d-extension)

Let(M,S_{) |=}RCA₀+ DNRbe a countable model. Then, there exists anω-extensionS^¯ _⊇_d S such that(M, ¯S_{) |=}WKL₀.

(49)

DNR and d-extension

For S_⊆S^′ _{⊆ P(N)},

S _⊆_d S^′ _⇔ for any A _∈S^′there exists g_∈S such that g is diagonally non-recursive relative to A .

Proposition (review)

Lemma (d-extension)

Let(M,S_{) |=}RCA₀+ DNRbe a countable model. Then, there exists anω-extensionS^¯ _⊇_d S such that(M, ¯S_{) |=}WKL₀.

(50)

MLR

^∗

is conservative over MLR

By the r-extension lemma and Tanaka’s self-embedding theorem for WKL₀, any coutable model of RCA₀+ MLRcan be expanded into a model of RCA₀^ns+ MLR^∗as follows.

✓

✒

✏

✑

(M,S) _⊆r (M, ¯S)

η ^{(I, ¯}^S ^↾^I) ⁽^e ^{(M, ¯}^S)

|= MLR ^(*) |=^WKL⁰ ^(**)

(*) r-extension

(**) Tanaka’s self-embedding theorem

Then,(M,S), (M, ¯S), η ↾ (M,S)is a model of RCA₀^ns+ MLR^∗. Thus, RCA₀^ns+ MLR^∗is a conservative extension of

RCA₀+ MLR.

(51)

MLR

^∗

is conservative over MLR

✓

✒

✏

✑

(M,S) _⊆r (M, ¯S)

η ^{(I, ¯}^S ^↾^I) ⁽^e ^{(M, ¯}^S)

|= MLR ^(*) |=^WKL⁰ ^(**)

(*) r-extension

RCA₀+ MLR.

(52)

MLR

^∗

is conservative over MLR

✓

✒

✏

✑

(M,S) _⊆r (M, ¯S)

η ^{(I, ¯}^S ^↾^I) ⁽^e ^{(M, ¯}^S)

|= MLR ^(*) |=^WKL⁰ ^(**)

(*) r-extension

RCA₀+ MLR.

(53)

DNR

^∗

is conservative over DNR

By the d-extension lemma and Tanaka’s self-embedding theorem for WKL₀, any coutable model of RCA₀+ DNRcan be expanded into a model of RCA₀^ns+ DNR^∗as follows.

✓

✒

✏

✑

(M,S) _⊆d (M, ¯S)

η ^{(I, ¯}^S ^↾^{I) (}^e ^{(M, ¯}^S⁾

|= DNR ^(*) |=^WKL0 ^(**) (*) d-extension

Then,(M,S), (M, ¯S), η ↾ (M,S)is a model of RCA₀^ns+ DNR^∗. Thus, RCA₀^ns+ DNR^∗is a conservative extension of

RCA₀+ DNR.

(54)

DNR

^∗

is conservative over DNR

✓

✒

✏

✑

(M,S) _⊆d (M, ¯S)

η ^{(I, ¯}^S ^↾^{I) (}^e ^{(M, ¯}^S⁾

RCA₀+ DNR.

(55)

DNR

^∗

is conservative over DNR

✓

✒

✏

✑

(M,S) _⊆d (M, ¯S)

η ^{(I, ¯}^S ^↾^{I) (}^e ^{(M, ¯}^S⁾

RCA₀+ DNR.

(56)

Nonstandard counterparts of second-order arithmetic

We have the following nonstandard counterparts of systems of second-order arithmetic.

second-order arithmetic nonstandard second-order arithmetic

RCA₀ RCA₀^ns

RCA₀+ DNR RCA₀^ns+ DNR^∗ RCA₀+ MLR RCA₀^ns+ MLR^∗

=WWKL₀ =WWKL₀^ns WKL₀ RCA₀^ns+ STP =WKL₀^ns ACA₀ RCA₀^ns+ STP + Σ¹₁TP=ACA₀^ns

(57)

Outline

3 Conservativity

4 Future work

(58)

Questions

Since RCA₀^ns+ MLR^∗is equivalent to WWKL₀^ns, there are some nice Reverse Mathematics phenomena forMLR^∗.

Question

Is there some nice Reverse Mathematics phenomena for DNR or DNR^∗?

(59)

Future work

Does the same argument work for other recursive notions? For example, does this argument work for the cohesive axiom?

COH: for any sequence_⟨A_n _|n_{∈ N⟩}, there exists an infinite set X such that X is_⟨A_n_⟩cohesive.

COH^∗: for any nonstandard sequence_⟨α_n _|n< β_⟩, there exists an infinite set X such that X is_⟨code(α_n_{) |}n_{∈ N⟩} cohesive.

(60)

Future work

Question

Is RCA₀^ns+ COH^∗a conservative extension of RCA₀+ COH? If the following question is true, we may apply the previous argument and answer this question.

Question

Let X is a recursive cohesive set, and let P be a non-empty Π⁰₁-class. Then, is there a set A _∈P such that X is A -recursive cohesive?

(61)

Future work

Theorem (folklore?)

IΣ₁+ Σ_nTP is a conservative extension of BΣ_n+1. Theorem

RCA₀^ns−+WKL₀+ Σ⁰₁TP is a conservative extension of WKL₀+BΣ₂.

Fact

RCA₀^ns+ Σ⁰₁TP+COH^∗_{⊢ RT}²₂.

Can we use these nonstandard arguments to analyze Ramsey theory for pairs?

(62)

Future work

Theorem (folklore?)

IΣ₁+ Σ_nTP is a conservative extension of BΣ_n+1. Theorem

RCA₀^ns−+WKL₀+ Σ⁰₁TP is a conservative extension of WKL₀+BΣ₂.

Fact

RCA₀^ns+ Σ⁰₁TP+COH^∗_{⊢ RT}²₂.

Can we use these nonstandard arguments to analyze Ramsey theory for pairs?

(63)

References.

Chris Impens and Sam Sanders, Transfer and a supremum principle for ERNA. J. Symbolic Logic 73 (2):689–710, 2008.

H. Jerome Keisler, Nonstandard arithmetic and reverse mathematics, The Bulletin of Symbolic Logic, 12(1):100–125, 2006.

Sam Sanders, A copy of several Reverse Mathematics, Logic Colloquium 2010.

Stephen Simpson and Y, A nonstandard counterpart of WWKL, preprint. Kazuyuki Tanaka, The self-embedding theorem of WKL0and a

non-standard method, Annals of Pure and Applied Logic 84:41–49, 1997. Y, Formalizing non-standard arguments in second order arithmetic, preprint.

(64)

It remains to show that T(g↾s)is infinite. Clearly, T(g↾0) =T is infinite. Assume that T(g↾s)is infinite. By definition,

T(g↾s+1_{) = {τ ∈}T(g↾s_{) | {}s_}^τ_lh(τ)(s_{) ↓⇒}B^′(s_{) , {}s_}^τ_lh(τ)(s_)}. Take y _{∈ ω}arbitrary. If

(∀τ ∈^T⁽^g^↾^s) ∩²^y^[^g⁽^s) = {^s}^τ_lh(τ)⁽^s) ↓],

then_(∀x_{) {}q(s,g↾s_)}(x) =g(s). But f _{∈ DNR}and, therefore, f(q(s,g↾s_{)) , {}q(s,g↾s_)}(q(s,g↾s)) =g(s) =f(q(s,g↾s)). A contradiction. Hence for any y _{∈ ω},

¬(∀τ ∈^T⁽^g^↾^s) ∩²^y^)[^g⁽^s) = {^s}^τ_lh(τ)⁽^s) ↓]. So T(g↾s+1)is infinite since T(g↾s)is infinite.

ファイル置き場 Sendai Logic Homepage

Nonstandard counterparts of

several weak axioms

Outline

Outline

Nonstandard analysis and arithmetic

Nonstandard analysis and arithmetic

Nonstandard analysis and arithmetic

Nonstandard analysis and arithmetic

Nonstandard analysis and arithmetic

Nonstandard analysis and arithmetic

Language of nonstandard second order arithmetic

s -structure and ∗ -structure

Systems of nonstandard arithmetic

Systems of nonstandard arithmetic

Systems of nonstandard arithmetic

Systems of nonstandard arithmetic

Systems of nonstandard arithmetic

Systems of nonstandard arithmetic

Systems of nonstandard arithmetic

Nonstandard reverse mathematics

Nonstandard reverse mathematics

Nonstandard reverse mathematics

Nonstandard reverse mathematics

Outline

Nonstandard Turing Machine

Nonstandard Turing Machine

Nonstandard Turing Machine

MLR

and DNR

MLR

and DNR

MLR

and DNR

Main theorems

Main theorems

Main theorems

WWKL

and MLR

Nonstandard extension

MLR

and MLR

MLR

and MLR

MLR

and MLR

DNR

and DNR

DNR

and DNR

DNR

and DNR

Outline

Conservativity

randomness and r-extension

randomness and r-extension

DNR and Π

-class

DNR and Π

-class

DNR and d-extension

DNR and d-extension

MLR

is conservative over MLR

MLR

is conservative over MLR

MLR

is conservative over MLR

DNR

is conservative over DNR

DNR

is conservative over DNR

DNR

is conservative over DNR

Nonstandard counterparts of second-order arithmetic

Outline

Questions

Future work

Future work

Future work

s -structure and _∗ -structure

DNR and _Π

DNR and _Π