ファイル置き場 Sendai Logic Homepage 100430tanaka
20
0
0
全文
(2) 1. Introduction . Reverse math classifies mathematical theorems, according to which set existence axioms are need to prove them.. Framework:.
(3) Classifying Formulas . Bounded formulas. . Arithmetical formulas. . Analytical formulas:. , only with. , with no set quantifiers.
(4) Big five subsystems Bishop's constructivism Computable math Hilbert's finitistic reductionism. Weyl's Predicativism Predicative reductionism. Impredicativism.
(5) Typical results of R. M..
(6) After five ….
(7) Recent Progress in Reverse Mathematics after the Big Five . . . . Mummert and Simpson found a metrization theorem of topology to be equivalent to -comprehension. Heinatsch and Moellerfeld show that the determinacy of boolean combinations of -sets has the same theorems as -comprehension. MedSalem and Tanaka studied the set existence axioms for -determinacy. Montalban and Shore prove that does not hold in Z2.. -determinacy.
(8) Infinite Games . . Let. due to Ulam-Gale-Stewart. Consider the following game: Player. wins A, if. Player. wins A, otherwise.. I has a winning strategy where.
(9) Determinacy of Infinite Games . A is determinate. either Rem. “A Borel game Note: Borel =. has a winning strategy in A. is determinate” is. ..
(10) . Which set existence axioms are needed to prove the determinacy of lower Borel games?.
(11) Recall Hintikka's Games (1973) Consider ∀-player：Take any >0. ∃-player：Choose a >0. ∀-player：Choose an x. ∃-player: Choose or If his chosen basic formula is true，then ∃-player wins． Thm． ∃-player has a win. strategy ⇔ the given formula is true．. ..
(12) Teacher & Student Games . . Player I ： Pose a formula φ． Player II ： Choose 0 (true) or 1 (false) ． If 0 is chosen，Player II is∃-player in the following Hintikka's game. If 1 is chosen，Player II is∀-player.. Thm． I has no winning strategy． Thm． From II's win. st.，the truth predicate can be defined..
(13) Proof: where. is recursive. Define a tree. Then T has no path. So, we have a formula decreasing along the K.-B. ordering of T s.t..
(14) Axiom of Inductive Definition.
(15) Iterative Combinations of Inductive Operators Richter-Aczel (1974). 1. Repeatedly apply 2. Apply. Define. as:. (from ) until a fixed point.. once. Go to 1 until a fixed point.. MedSalem-Tanaka (2007). Define. as:. 0. 1. Repeat. apply 2.. from. until a fixed point .. . Go to 1 until a fixed point..
(16) Axioms of Iterative Comb. of Ind. Operators. asserts that for any. , there exists. a (maximal) pre-wellordering constructed by iterative combination of. If. , we write. For any ordinal In particular,. and. .. for. .. is defined analogously..
(17) Some equivalences (with some induction).
(18) Combinations of Ind. Def. Theorem (T. 2010). means the set of arithmetical combinations of formulas..
(19) Ramsey property of partitions . P(X) is Ramsey there exists an infinite (homogeneous) set H s.t. either all infinite subsets X of H satisfies P(X) or all infinite sugsets X of H satisfies ￢P(X).. Remark: “A Borel partition. formula.. Note: Borel =. is Ramsey” is a.
(20) . Which set existence axioms are needed to prove the Ramsey property of partitions?.
(21)
関連したドキュメント
Projection of Differential Algebras and Elimination As was indicated in 5.23, Proposition 5.22 ensures that if we know how to resolve simple basic objects, then a sequence of
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
S.; On the Solvability of Boundary Value Problems with a Nonlocal Boundary Condition of Integral Form for Multidimentional Hyperbolic Equations, Differential Equations, 2006, vol..
In order to prove these theorems, we need rather technical results on local uniqueness and nonuniqueness (and existence, as well) of solutions to the initial value problem for
They are a monoidal version of the classical attribute grammars, and have the following advantages: i) we no longer need to stick to set-theoretic representation of attribute
We shall prove the completeness of the operational semantics with respect to Lq, which will establish a tight correspondence between logic (Lq sequent calculus) and computation
We study several choice principles for systems of finite character and prove their equivalence to the Prime Ideal Theorem in ZF set theory without Axiom of Choice, among them
