ファイル置き場 Sendai Logic Homepage speaker2
24
0
0
全文
(2) Reverse Mathematics I. ▶. Setting: Second order arithmetic.. ▶. Main Question: What axioms are necessary to prove the theorems of Mathematics?. ▶. Axiom systems(Big 5): RCA0 ≡ ∆11 -Comprehension + Σ01 -Induction + Semiring ax WKL0 ≡ RCA0 + Weak K¨onig’s lemma ACA0 ≡ RCA0 + Arithmetic Comprehension ATR0 1 Π1 -CA0. ≡ ACA0 + Arithmetic Transfinite recursion ≡ ACA0 + Π11 -Comprehension.
(3) Theories of Second-Order Arithmetic I ▶. ∪ A set is called arithmetical ( n<ω Σ0n (X )) if it is defined by a formula consisting of only number quantifiers(no set quantifiers).. ▶. ACA0 is a theory consists of RCA0 and arithmetical comprehension.. ▶. ACA0 is a Π11 -conservative extension of PA.. ▶. ACA0 satisfies good theorems about arithmetical properties.. Fact (examples of properties of ACA0 ) 1. ARITH(X ) ⊨ ACA0 for any X ⊆ ω. Where ARITH(X ) is a class of all sets which are arithmetical in X. 2. Every ω model M of ACA0 is arithmetically closed. That is, for any X ∈ M, ARITH(X ) ⊆ M..
(4) Theories of Second-Order Arithmetic II RCA0 WKL0. ∆01. Comprehension Weak K¨onig’s Lemma. ACA0. Arithmetical Comprehension. ? ATR0 Π11 -CA0. What axiom is placed here? Arithmetical Transfinite Recursion Π11 Comprehension. ∆01 Recursive, Computable Σ0n Arithmetical ∪ ∆11 , µ<ωCK Σ0µ ∪. n<ω. 1. Hyperarithmetical Π11. ▶. A set defined by transfinite induction of arithmetical definition. is called hyperarithmetical set.. ▶. A class of sets which hyperarithmetical in X is denoted by ∪ 1 0 µ<ω X Σµ . In fact, It is equivalent to ∆1 (X ).
(5) Theories of Second-Order Arithmetic III. ∆01 Comprehension Weak K¨onig’s lemma. RCA0 WKL0 ACA0. Arithmetical Comprehension. ? ATR0 Π11 -CA0. What axiom is placed here? Arithmetical Transfinite Recursion Π11 Comprehension. ∆01 Recursive, Computable Σ0n Arithmetical ∪ ∆11 , µ<ωCK Σ0µ ∪. n<ω. 1. Hyperarithmetical Π11. ▶. Question: What theory of second-order arithmetic corresponds to Hyperarithmetical?. ▶. ∆11 -CA0 ?.
(6) Theory of Hyperarithemetic Analysis I. Definition A theory T is called theory of hyperarithmetic analysis if it satisfies following: 1. HYP(X ) ⊨ T for any X ⊆ ω. Where HYP(X ) is a class of all sets which are hyperarithmetical in X. 2. Every ω model of T is hyperarithmetically closed. ▶. ∆11 -CA0 is a theory of hyperarithmetic analysis.. ▶. However, beside ∆11 -CA0 , there exists other various theories of hyperarithmetic..
(7) Theory of Hyperarithemetic Analysis II. ▶. the following are theories of hyperarithmetic analysis. Σ11 -AC0 ≡ ACA0 + Σ11 -Axiom of Choice Π11 -SEP0 ≡ ACA0 + Π11 -Separation ∆11 -CA0 ≡ ACA0 + ∆11 -Comprehension. weak-Σ11 -AC0 ≡ ACA0 + weak-Σ11 -Axiom of Choice INDEC ≡ ACA0 + Jullien’s Indecomposability Theorem ABW0 ≡ ACA0 + Arithmetical Bolzano-Weierstraß’s Theorem JI ≡ ACA0 + (∀X )(∀α){[(∀β < α)X (β) exists] → X (α) exists}.
(8) Theory of Hyperarithemetic Analysis III CDG-CA ≡ ACA0 + Given a sequence {Tn | n ∈ N} of completely determined trees, there exists a set X s.t. n ∈ X ⇔ I has a winning strategy in Tn CDG-AC ≡ ACA0 + Given a sequence {Tn | n ∈ N} of completely determined trees, Σn∈N Tn is also completely determined. DG-CA ≡ ACA0 + Given a sequence {Tn | n ∈ N} of determined trees, there exists a set X s.t. n ∈ X ⇔ I has a winning strategy in Tn DG-AC ≡ ACA0 + Given a sequence {Tn | n ∈ N} of determined trees, Σn∈N Tn is also completely determined. etc....
(9) Theory of Hyperarithemetic Analysis IV → is proved over RCA0. Σ11 -AC0. ⇒ is proved over RCA0 + Σ11 -IND ?. DG-AC H. . ×.
(10). Π11 -SEP0. ̸→ is proved by tagged tree forcing. J. ×. . ABW0 o. ×. ∆11 -CA0 o J. ×. / DG-CA. ×. '. INDEC H ×. ". . weak-Σ11 -AC0 K. . o × CDG-CA H ×. JI. / CDG-AC.
(11) Definition of Tagged Tree I We shall see how Π11 -SEP0 ̸→ Σ11 -AC0 is proved by Montalb´an.. Definition Σ11 -AC0 is ACA0 plus following scheme: (∀n)(∃X )ψ(n, X ) ⇒ (∃Z )(∀n)ψ(n, Zn ), where ψ(n, X ) is Σ11 .. Definition Π11 -SEP0 is ACA0 plus following scheme: ¬(∃n)[¬ψ(n) ∧ ¬φ(n)] ⇒ (∃Z )(∀n)[(¬ψ(n) → n ∈ Z ) ∧ (¬φ(n) → n ∈ / Z )], where ψ(n) and φ(n) are Σ11 formula..
(12) Definition of Tagged Tree II Definition p = (T p , f p , hp ) ∈ P if and only if ▶ T p ⊆ ω <ω is a finite tree. ▶. ▶. f p is a non-empty finite partial function such that dom(f p ) ⊆ ω, ran(f p ) ⊆ T p . ▶. ▶. T p grows to a infinite tree T G .. Every f p (i) grows to a path f G (i) of T G .. hp : T p → ω1CK ∪ {∞} s.t. ▶ ▶. ▶. (∀s, t ∈ T p )[s ⊊ t → hp (s) > hp (t)] (∀s ∈ T p )[(∃i)[s ⊆ f p (i)] → hp (s) = ∞] Every hp grows to a rank function hG of T G.
(13) Definition of Tagged Tree III. Definition For any P-generic G, we define objects as follows: ▶. T G := ∪p∈G T p. ▶. αiG = f G (i) := ∪p∈G ,i∈dom(f p ) f p (i). ▶. hG := ∪p∈G hp. ▶. ⊕ MFG := {X | (∃µ < ω1CK )[X is Σ0µ (T G ⊕ i∈F αG (i))]} ∪ G := G G G M∞ F ⊆fin ω MF = HYP({T } ∪ {α (i) | i ∈ F }). ▶. where, MFG ∩ [T G ] = {αiG | i ∈ F } holds..
(14) G M∞ ⊭ Σ11 -AC0. Theorem G ⊭ Σ1 -AC M∞ 0 1 ▶. If there finitely arbitrary many sets satisfy a Σ11 formula, Σ11 -AC0 certifies that it is possible to take infinitely many sets satisfying the formula.. ▶. ”X is an infinite path of T” is also Σ11 formula with argument X.. ▶. If F is large enough, MFG contains many paths, therefore it is G possible to take they from M∞. ▶. However, every MFG contains at most finitely many paths. Therefore it is impossible to take infinitely many paths from G. M∞.
(15) Forcing relation I. Definition For p ∈ P and a formula ψ, p ⊩ ψ is defined as follows: ▶. p ⊩ σ ∈ T ⇔def σ ∈ T p ∨ (1 ≤ hp (σ − ) ∧ σ − ∈ T p ). ▶. p ⊩ (¯ n, m) ¯ ∈ αi ⇔def i ∈ dom(f p ) ∧ f p (i)(n) = m. ▶. p ⊩ n ∈ Sν,F ,e ⇔def p ⊩ (∃x)θ(e, x, n, Hν,F ) (where (∃x)θ(e, x, y , X ) is a universal Σ01 formula for some θ Σ00 formula.). ▶. p ⊩ (e, n, ν) ∈ Hµ,F ⇔def ν < µ ∧ p ⊩ n ∈ Sν,F ,e.
(16) Forcing relation II Definition ▶. p ⊩ ∀XFµ φ(XFµ ) ⇔def (∀ν < µ)(∀e ∈ ω)p ⊩ φ(Sν,F ,e ). ▶. p ⊩ ∀X µ φ(X µ ) ⇔def (∀ν < µ)(∀e ∈ ω)(∀F ⊆fin ω)p ⊩ φ(Sν,F ,e ). ▶. p ⊩ ∀XF φ(XF ) ⇔def (∀ν < ω1CK )(∀e ∈ ω)p ⊩ φ(Sν,F ,e ). ▶. p ⊩ ∀X φ(X ) ⇔def (∀ν < ω1CK )(∀e ∈ ω)(∀F ⊆fin ω)p ⊩ φ(Sν,F ,e ). where a subscript F of the variable X means that values of X are in MFG , a superscript µ of the variable X means that values of X are Σ0µ set..
(17) Retagging I. Definition Ret(µ, F , p, p ∗ ) (p is a µ-F -absolute-retagging of p ∗ ) if and only if ▶. Tp = Tp. ▶. (∀i ∈ F )[f p (i) = f p (i)]. ▶. (∀s ∈ T p )[hp (s) ≥ µ → hp (s) ≥ µ]. ▶. (∀s ∈ T p )[hp (s) < µ → hp (s) = hp (s)]. ∗ ∗. ∗. ∗. Lemma Ret(ω · µ, F , p, p ∗ ) ∧ q ≤ p ∧ ν < µ ⇒ (∃q ∗ ≤ p ∗ )Ret(ω · ν, F , q, q ∗ ).
(18) Retagging II Definition A formula ψ is F -restricted if every subscript of variable of ψ is a subset of F .. Lemma Let a formula ψ be such that F-restricted and rk(ψ) < ω1CK . Let p, p ∗ ∈ P. Then Ret(ω · rk(ψ), F , p, p ∗ ) ⇒ (p ⊩ ψ ⇒ p ∗ ⊩ ψ) p⊩ψ. Ret. . p∗. q⊩ψ . Ret. q∗.
(19) Retagging III. Lemma For a formula ψ with rank µ, 0(µ) is able to decide whether p ⊩ ψ uniformly in p, ψ, and µ..
(20) Σ-over-L∞ Definition ▶. A formula ψ is F -restricted if every subscript of variable of ψ is a subset of F .. ▶. A formula ψ is ranked if every variable of ψ is ranked.. ▶. A formula is Σ-over-LF if it is built up from ranked and F -restricted formulas using ∧, (∀n), (∃X ).. Definition For any formula ψ and µ < ω1CK , ψ µ is a result of replacing of (∃X ) by (∃X µ ).. Lemma Let F ⊆fin ω, ψ be Σ-over-LF sentence, and µ < ω1CK . Then, Ret(ω · rk(ψ) + ω 2 + ω, F , p, p ∗ ) ∧ dom(f p ) ⊆ F ⇒ (p ⊩ ¬ψ µ ⇒ p ∗ ⊩ ¬ψ µ ).
(21) G M∞ ⊨ Π11 -SEP0 I. Theorem G ⊨ Π1 -SEP M∞ 0 1. Proof ▶. Let φ(n) and ψ(n) be a Σ-over-LF formulas(Σ11 formulas) with a free variable n such that G M∞ ⊨ (∀n)[ψ(n) ∨ φ(n)]. ▶. G will be constructed such that D ∈ M∞ G M∞ ⊨ (∀n)[(¬φ(n) → n ∈ D) ∧ (n ∈ D → ψ(n))]. ▶. Let p ∈ G be such that p ⊩ (∀n)[ψ(n) ∨ φ(n)].. ▶. Let µ < ω1CK be such that p ⊩ (∀n)[ψ µ (n) ∨ φµ (n)].. ▶. Let ν < ω1CK be large enough for p ∈ Pν ∧ (∀n ∈ ω)[rk(ψ µ (¯ n) ∨ φµ (¯ n)) < ν].
(22) G M∞ ⊨ Π11 -SEP0 II. ▶ ▶. D is defined as follows. d ∈ D if and only if there exists q ∈ P such that 1. 2. 3. 4. 5. 6.. q ⊩ ¬φν (d) Tq ⊆ TG (∀i ∈ F )[f q (i) = αiG ∩ T q ] ran(hq (s)) ⊆ (ων + ω 2 + 2ω) ∪ {∞} hG (s) < ων + ω 2 + 2ω → g (s) = hG (s) hG (s) ≥ ων + ω 2 + 2ω → g (s) ≥ ν. ▶. D is hyperarithmetical in T ⊕. ▶. G. Therefore D ∈ M∞. ⊕. i∈F. αiG .. (¬φ(n) → n ∈ D) and (n ∈ D → ψ(n)) will be proved in next page..
(23) G M∞ ⊨ Π11 -SEP0 III. ¬φ(n) → n ∈ D. ▶. G ⊨ ¬φµ (n) holds. Assume that M∞. ▶. Let q ∗ ∈ G be such that q ∗ ≤ p ∧ q ∗ ⊩ ¬φµ (n).. ▶. q ∗ satisfies almost every condition of D.. ▶. However, it is not necessarily true that ∗ ran(hq (s)) ⊆ (ων + ω 2 + 2ω) ∪ {∞}. Let retagging q of q ∗ as follows. Then q is a witness of d ∈ D.. ▶. ∗. 1. T q = T q ∗ 2. f q = f q { 3. hq (s) =. ∗. hq (s) ∞. ∗. (if hq (s) < ων + ω 2 + 2ω) (otherwise).
(24) G M∞ ⊨ Π11 -SEP0 IV. ¬ψ(n) → n ∈ /D ▶. Assume that ¬ψ(n) ∧ n ∈ D and we prove it by contradiction.. ▶. G ⊨ ¬ψ µ (n), there exists r ≤ p s.t. r ⊩ ¬ψ µ (n). Since M∞. ▶. G ⊨ n ∈ D, there exists q ≤ p such that q ⊩ ¬φµ (n). Since M∞. p ⊩ ψ µ (n) ∨ φµ (n) u. ). q ⊩ ¬φµ (n). r ⊩ ¬ψ µ (n). . q ∗ ⊩ ¬φµ (n). . Ret. s∗. Ret. . r ∗ ⊩ ¬ψ µ (n). Let q ∗ ≤ q, r ∗ ≤ r , s ∗ ≤ p be such that Ret(ων + ω 2 + ω, F , q ∗ , s ∗ ) ∧ Ret(ων + ω 2 + ω, F , r ∗ , s ∗ ). Then s ∗ ⊩ ¬φµ (n) ∧ ¬ψ µ (n) holds. It is contradiction. Q.E.D..
(25) Bibliography ▶. Antonio Montalb´an “Indecomposable linear ordering and hyperarithmetic analysis” Journal of Mathematical Logic, Vol.6, No.1, 89-120 2006.. ▶. Antonio Montalb´an “On the Π11 -separation principle” Mathematical Logic Quarterly 2008.. ▶. Itay Neeman “The strength of Jullien’s indecomposability theorem” Journal of Mathematical Logic 2008.. ▶. Chris J. Conidis “Comparing theorems of hyperarithmetic analysis with the arithmetical Bolzano-Weierstrass theorem” to appear.. Thank you for your attention..
(26)
関連したドキュメント
TOSHIKATSU KAKIMOTO Yonezawa Women's College The main purpose of this article is to give an overview of the social identity research: one of the principal approaches to the study
3.1, together with the result in (Barber and Plotkin 1997) (completeness via the term model construction), is that the term model of DCLL forms a model of DILL, i.e., a
Light linear logic ( LLL , Girard 1998): subsystem of linear logic corresponding to polynomial time complexity.. Proofs of LLL precisely captures the polynomial time functions via
Polarity, Girard’s test from Linear Logic Hypersequent calculus from Fuzzy Logic DM completion from Substructural Logic. to establish uniform cut-elimination for extensions of
pole placement, condition number, perturbation theory, Jordan form, explicit formulas, Cauchy matrix, Vandermonde matrix, stabilization, feedback gain, distance to
administrative behaviors and the usefulness of knowledge and skills after completing the Japanese Nursing Association’s certified nursing administration course and 2） to clarify
Shi, “Oscillation criteria for a class of second-order Emden-Fowler delay dynamic equations on time scales,” Journal of Mathematical Analysis and Applications, vol. Zhang,
in [Notes on an Integral Inequality, JIPAM, 7(4) (2006), Art.120] and give some answers which extend the results of Boukerrioua-Guezane-Lakoud [On an open question regarding an
