ファイル置き場 Sendai Logic Homepage 110520higuchi

A Nonstandard Counterpart of DNR

Kojiro Higuchi

joint work with

Keita Yokoyama ^,

Diagonally Non-Recursive function

Kleene’s recursion theorem (1938)

For any recursive function f, we can find e such that {e}={f(e)}. Arslanov’s completeness criterion (1981)

For any r.e. set A,

A is complete _{⇐⇒ (∃g≤T} A)(∀e)[{e}6={g(e)}]. In fact, _{⇐⇒ (∃h≤T} A)(∀e)[{e}(e)6=h(e)]. Definition f is d.n.r. ⇐⇒ (∀e)[{e}(e)6=f(e)].

Definition f is d.n.r.(A) ⇐⇒ (∀e)[{e}^A(e)6=f(e)]. On this concept, I was asked by Yokoyama-san...

Question (Yokoyama, March 2010)

Given any infinite recursive binary tree T and dnr function f, (_∃f^′ _≤T f)(_{∃A∈[T])[f}^′ is dnr(A)] ??

→^Yes In fact,

(_∃f^′ _≤T f)(∃inf f-rec tree T^′ ⊂T)(∀A∈[T^′])[f′ is dnr(A)]. Let us prove this!

Theorem Given any inf. rec. binary tree T and f:dnr,

(_∃f^′ _≤T f)(∃inf f-rec tree T^′ ⊂T)(∀A∈[T^′])[f′ is dnr(A)]. Proof. For x_{∈ N}^<N and k,e∈ N, define

T(_{∅):=T and}

T(x*k):={y ∈T(x):k6={|x|}^y_|y|⁽|x|) if the righthand is defined}, f^′(e)=f(q(e,f^′[e])), where

{q(e,x)}(n)= a if (∃a,b)(∀y∈T(x)∩2^b)[a={|x|}^y_|y|⁽|x|)↓],

= ↑ otherwise.

Theorem Given any inf. rec. binary tree T and f:dnr,

(_∃f^′ _≤T f)(∃inf f-rec tree T^′ ⊂T)(∀A∈[T^′])[f′ is dnr(A)]. Proof. For x_{∈ N}^<N and k,e∈ N, define

T(_{∅):=T and}

T(x*k):={y ∈T(x):k6={|x|}^y_|y|⁽|x|) if the righthand is defined}, f^′(e)=f(q(e,f^′[e])), where

{q(e,x)}(n)= a if (∃a,b)(∀y∈T(x)∩2^b)[a={|x|}^y_|y|⁽|x|)↓],

= ↑ otherwise.

Note f(q(e,f^′[e]))6={q(e,x)}(q(e,x)).

Hence, T(f^′[e]) is infinite for all e by induction. Let T^′=^T_eT(f^′[e]).

Note (_∀A∈T(f^′[e]*f^′(e)))[f^′(e)_6={e}^A(e)]. Hence, f^′ is dnr(A).

Theorem Given any inf. rec. binary tree T and f:dnr,

(_∃f^′ _≤T f)(∃inf f-rec tree T^′ ⊂T)(∀A∈[T^′])[f′ is dnr(A)]. The above theorem can be used to show some theorem

concerning on reverse mathematics of second order arithmetic.

Reverse mathematics of second order arithmetic

Reverse mathematics is a study to classify “natural”

mathematical statements according to equivalence over a base system.

Many mathematical concepts and theorems can be formalized in second order arithmetic.

We can also formalize “f is dnr(A)” in second order arithmetic.

The strength of DNR

Theorems non-provable in RCA⁰ are quite often equivalent to one of the statements WWKL, WKL, ACA, ATR and Π^11-CA over RCA⁰.

But the statement DNR is neither provable in RCA⁰ nor equivalent to one of these statements.

Here, DNR = (∀A)(∃f)(∀y)[f(y)6={y}^A(y)]. It is known that DNR<WWKL<WKL< _{· · · .}

Although many mathematical concepts and statements can be formalized in second order arithmetic,

sometimes they will become too complicated.

Nonstandard arithmetic and analysis

In nonstandard arithmetic and analysis, many concepts and theorems can be formalized by a simple notation or formula and can be proved in a simple way.

Example

f is continuous _{⇐⇒ (∀x}^∗,y^∗)[x^∗ _≈y^∗ _{⇒ f}^∗(x^∗)_≈f^∗(y^∗)].

Example of nonstandard argument

Theorem (_∀{xn}_{n∈N ⊂[0,1])[{xn}}_n has an accumulating point].

Sketch of Proof.

Let n^{∗ >} _{N and a}∈ R such that a≈x^∗_n∗ ^. By Transfer Principle,

(∀k∈ N)(∃m>k)[|x^m-a| <1/k]

since (_∀k^∗ _{∈ N)(∃m}^{∗ >}k^∗)[_|x^∗_m∗-a_{| <1/k}^∗].

How about doing reverse mathematics with nonstandard argument??

Review of RCA⁰

L :={0,1,=,+,·,<,∈}

There are two sorts for natural numbers and for sets of natural number.

• x,y,· · · for natural numbers,

• X,Y,· · · for sets of natural numbers. The axioms of RCA⁰ consists of

BASIC axioms + IΣ⁰1 + ∆⁰1^-CA.

L^ns

L :={0,1,=,+,·,<,∈}

L^{∗:={0∗,1∗,=∗,+∗,}·^∗,<∗,∈^∗} L^ns:=L ∪ L^∗∪{^√}

• x,y,· · · for standard natural numbers,

• X,Y,· · · for sets of standard natural numbers.

• x^∗,y∗,· · · for nonstandard natural numbers,

• X^∗,Y∗,· · · for sets of nonstandard natural numbers.

Structures for _L^ns=_{L ∪ L}^∗_∪{^√}

N =(N,S^{N ,0N ,1N ,+N ,}·^{N ,<N ) is an} L-structure is defined in a natural way.

N ^ns=(N ,N ^∗,√_{N ns}^{) is an} L^ns-structure ⇐⇒

• N is an L-structure,

• N ^{∗ is an} L^∗-structure,

• ^√ is a function mapping N (resp. _SN ) into N^{∗ (resp.} _{SN ∗}^).

Terms and Formulas for _L^ns=_{L ∪ L}^∗_∪{^√}

I hope you can imagine what are _L^ns-terms and _L^ns-formulas. Example.

1. “x^∗ is a bigger than any standard natural number (x^{∗ >} _N)”

≡ (∀y)[^{√(y)<∗x∗].}

2. “If A is unbounded, then ^√(A) has an infinitely large number”

≡ (∀A)[(∃^∞x)[x∈A]⇒(∃y^{∗ > N)[y∗} ∈ ^√(A)]]. 3. “_{N ⊂e N} ^∗”

≡ (∀x)(∀y^{∗ <∗ √(x))(}∃z)[y^{∗=∗√(z)].}

Notations

Given an L-formula F,

F^∗: an _L^ns-formula obtained by adding * to all L-symbols in F.

RCA^ns₀ =RCA⁰ +

• ^√ : N ֒→ N ^{∗ and} N ⊂^e N ^∗.

• N ≡Σ1

1 ^N

∗: for any sentence F in Σ¹1⁽_L)

F _{⇐⇒ F}^∗

• N ≺Σ0

0 ^N

∗: for any F(x,X) in Σ⁰⁰⁽_L) (∀x)(∀X)[F(x,X) ⇐⇒ F^{∗(√(x),√(X))]}

• Σ⁰¹ overspill: for any F(x,y) in Σ⁰¹⁽L)

(∀x)(∃y>x)[F(x,y)]⇒(∃y^{∗ > N)(}∀x)[F^{∗(√(x),y∗)]}

• Finite standard part principle:

(_∀X^∗)[card(X^∗)∈ N ⇒(∃Y)(∀x)[x∈Y ⇐⇒ ^√(x)∈X^∗]]

WKL^ns₀ =WKL⁰ +

• ^√ : N ֒→ N ^{∗ and} N ⊂^e N ^∗.

• N ≡Σ1

1 ^N

∗: for any sentence F in Σ¹1⁽_L)

F _{⇐⇒ F}^∗

• N ≺Σ0

0 ^N

∗: for any F(x,X) in Σ⁰⁰⁽_L) (∀x)(∀X)[F(x,X) ⇐⇒ F^{∗(√(x),√(X))]}

• Σ⁰¹ overspill: for any F(x,y) in Σ⁰¹⁽L)

(∀x)(∃y>x)[F(x,y)]⇒(∃y^{∗ > N)(}∀x)[F^{∗(√(x),y∗)]}

• Standard part principle:

(_∀X^∗)(∃Y)(∀x)[x∈Y ⇐⇒ ^√(x)∈X^∗]

RCA and WKL

It is known that

• RCA^ns0 is a conservative extension of RCA⁰.

• WKL^ns0 is a conservative extension of WKL⁰.

WKL⁰ _⊂^conWKL^ns₀

It is clear that every theorem in WKL⁰ is a theorem in WKL^ns₀ . To see the converse, note that it suffices to prove:

(∀cntb nonst M |=WKL⁰⁾⁽∃N |=WKL^{ns0 )[}N ↾ L ∼= M].

(∀cntb nonst M |=WKL⁰⁾⁽∃N |=WKL^{ns0 )[}N ↾ L ∼= M] Theorem (Tanaka, 1997)

(∀cntb nonst M |=WKL⁰⁾⁽∃I (^e M)[I ∼_{= M and} S^I=Code(I/M)].

Given cntb nonst _{M |=WKL}⁰, take _{I (}^e M as in the above theorem.

Consider N =(I,M,Id(-like)).

(∀cntb nonst M |=WKL⁰⁾⁽∃N |=WKL^{ns0 )[}N ↾ L ∼= M] Theorem (Tanaka, 1997)

(∀cntb nonst M |=WKL⁰⁾⁽∃I (^e M)[I ∼_{= M and} S^I=Code(I/M)].

Given cntb nonst _{M |=WKL}⁰, take _{I (}^e M as in the above theorem.

Consider N =(I,M,Id(-like)). N satisfies:

• I ≡Σ1

1 M since I ∼_{= M;}

• I ≺Σ0

0 M since I ⊂^e M;

• Σ⁰¹ overspill since _{I (}^e _{M |=IΣ}⁰₁;

• (∀X^∗)(∃Y)(∀x)[x∈Y⇔ ^√(x)∈X^{∗] since} S^I=Code(I/M).

DNR and DNR^ns

DNR⁰ = RCA⁰ + (∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

DNR^ns₀ = RCA^ns₀ + (_∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)]. Main Theorem DNR⁰ _⊂^conDNR^ns₀ .

We see an idea of proof and end this talk.

DNR⁰ _⊂^conDNR^ns₀ .

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)].

It is easy to see that every theorem in DNR⁰ is a theorem in DNR^ns₀ .

To show the converse, note that it suffices to prove:

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)].

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)]. Definition _M⁰ _{⊂d M}¹ iff _M⁰ _{⊂ω M}¹ and

(_∀A∈SM1)(_∃f∈SM0)[_M¹ |=f is dnr(A)].

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)]. Definition _M⁰ _{⊂d M}¹ iff _M⁰ _{⊂ω M}¹ and

(_∀A∈SM1)(_∃f∈SM0)[_M¹ |=f is dnr(A)]. Recall the following theorem holds,

Given any inf. rec. binary tree T and f:dnr,

(_∃f^′ _≤T f)(∃inf f-rec tree T^′ ⊂T)(∀A∈[T^′])[f′ is dnr(A)]. By the same argument of proof, we can modify the above theorem to...

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)]. Definition _M⁰ _{⊂d M}¹ iff _M⁰ _{⊂ω M}¹ and

(_∀A∈SM1)(_∃f∈SM0)[_M¹ |=f is dnr(A)].

Given any inf. binary tree T_∈SM1 and A_∈SM1,

(∃inf tree T^′ ⊂T in SM1⁾⁽∀B∈[T^′])(∃f∈SM1^)[M¹ |=f is dnr(A_⊕B)].

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)]. Definition _M⁰ _{⊂d M}¹ iff _M⁰ _{⊂ω M}¹ and

(_∀A∈SM1)(_∃f∈SM0)[_M¹ |=f is dnr(A)].

Given any inf. binary tree T_∈SM1 and A_∈SM1,

(∃inf tree T^′ ⊂T in SM1⁾⁽∀B∈[T^′])(∃f∈SM1^)[M¹ |=f is dnr(A_⊕B)].

Theorem (Harrington, 1977)

(_{∀cntb M}⁰ _|=RCA⁰)(_∃M¹ _{⊃ω M}⁰)[_M¹ _|=WKL⁰]. Combining the technique of these theorems, we have...

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)]. Definition _M⁰ _{⊂d M}¹ iff _M⁰ _{⊂ω M}¹ and

(_∀A∈SM1)(_∃f∈SM0)[_M¹ |=f is dnr(A)].

Theorem (∀cntb M |=DNR⁰⁾⁽∃M^′ ⊃^d M)[M^′ |=WKL^0].

(∀cntb nonst M |=DNR⁰⁾⁽∃N |=DNR^{ns0 )[}N ↾ L ∼= M].

• DNR^{0 = RCA0 + (}∀A)(∃f)(∀y)[f(y)6={y}(A;y)].

• DNR^{ns0 = RCAns0 + (}∀x^∗)(∃f)(∀y)[f(y)6={y}(Code(x^∗);y)]. Definition _M⁰ _{⊂d M}¹ iff _M⁰ _{⊂ω M}¹ and

(_∀A∈SM1)(_∃f∈SM0)[_M¹ |=f is dnr(A)].

Theorem (∀cntb M |=DNR⁰⁾⁽∃M^′ ⊃^d M)[M^′ |=WKL^0]. From this theorem, we can conclude our claim by the same

argument for WKL⁰ _⊂^conWKL^ns₀ .

fin.