|
IMS-JSPS Joint Workshop on Mathematical Logic and the Foundations of Mathematics
(15 - 16 Jan 2016)
~ Abstracts ~
Characterizing uniform provability by intuitionistic provability
Makoto Fujiwara, Japan Advanced Institute of Science and Technology, Japan
Uniform provability of existence statements is closely related to the investigation of sequential versions in reverse mathematics as well as Weihrauch reducibility.
In [1], we have provided an exact formalization of uniform provability in RCA and have shown that for any existence statement of some syntactical form, it is intuitionistically provable if and only if it is uniformly provable in RCA.
In this talk, we discuss the possibility to extend this result to characterize uniform provability in further stronger systems by intuitionistic provability.
[1] M. Fujiwara, Intuitionistic provability versus uniform provability in RCA, Lecture Notes in Computer Science, vol. 9136, pp. 186-195, 2015.
« Back... Boolean valued second order logic
Daisuke Ikegami, Tokyo Denki University, Japan
In the research of second order predicate logic, the following two semantics are mainly considered; full semantics (or Tarski semantics) and Henkin semantics. Full semantics for second order logic can express much more things than the standard semantics for first order predicate logic, but it is very complicated and hard to analyze while Henkin semantics for second order logic is essentially the same as that for first order predicate logic.
In this talk, we propose another semantics for second order logic which is called "Boolean valued semantics", and we investigate the basic properties of this semantics and compare it with full semantics.
This is joint work with Jouko Väänänen.
« Back... Weak choice principles in the Weihrauch degrees
Takayuki Kihara, The University of California, Berkeley, USA
Various problems on the Weihrauch degrees have been proposed in the Dagstuhl seminar on "Measuring the Complexity of Computational Content: Weihrauch Reducibility and Reverse Analysis". We give solutions to some of the Dagstuhl problems, e.g., those on the strengths of sequential compositions and parallel products of several "non-uniformly computable" choice principles.
« Back... Reflection and the fine-structure theorem
Alexander P. Kreuzer, National University of Singapore
Reflection is the schema if a sentence $\phi$ is provable in a theory $T$, then $\phi$ is true. It is well-known $\Sigma_n$-induction is equivalent to the fragment of reflection for $\Pi_{n+2}$-formulas $\phi$ and $T=I\Delta_0+exp$. Since reflection is a more complex statement than induction, one can easily find fragments intermediate to the classical induction hierarchy. For instance, reflection for $\Pi_3$-formulas and $T=I\Sigma_1$ lies strictly between $I\Sigma_1$ and $I\Sigma_2$. (In fact, it is equivalent to the well-foundedness of $\omega^\omega$.)
Thus, one can view reflection as a generalization of induction. The fine-structure theorem is a classical result relating different fragments of reflection. So far, there have been only proof-theoretic proofs of this theorem. We will present a new model-theoretic proof of this result with an explicit model-construction.
Joint work with Chi Tat Chong, and Yang Yue.
« Back... Forcing with matrices of countable elementary submodels
Borisa Kuzeljevic, National University of Singapore
We analyze the forcing notion P of finite matrices whose rows consists of isomorphic countable elementary submodels of a given structure of the form H(k). We show that forcing with this poset adds a Kurepa tree T. Moreover, if Q is a suborder of P containing only continuous matrices, then the Kurepa tree T is almost Souslin, i.e. the level set of any antichain in T is not stationary. This is a joint work with Stevo Todorcevic.
« Back... The uniqueness of Eigen-distribution for multi-branching trees
Shohei Okisaka, Tohoku University, Japan
Game tree is a simple model to compute Boolean functions. To eliminate the reluctant assignments in computing the value of root, Liu and Tanaka (2009) defined the concepts of i-set and E^i-distribution (i=0,1).They showed that for any binary trees, the E^1-distribution is the unique eigen-distribution with respect to the closed set of deterministic algorithms.
We will consider a class of second-order theories and give density notions for those theories. Then, we will study several basic properties of density notions such as the existence of a certain cut, conservation result and the relation with provably recursive functions comparing with those properties of indicators.
« Back... The proof-theoretic strength of Ramsey's theorem for pairs
Keita Yokoyama, Japan Advanced Institute of Science and Technology, Japan
In this talk, we study the proof-theoretic strength of Ramsey's theorem for pairs and two colors. Bovykin and Weiermann pointed out that the proof-theoretic strength of RT^2_2 can be can be approximated by Paris's density notion. Here, a finite set is said to be n-dense if one can apply Ramsey's theorem for pairs n-times repeatedly and the result set is still relatively large. Then, the Pi^0_3-part of RT^2_2+WKL_0 is the same as that of RCA_0+"any infinite set contains an n-dense subset" for any standard n. In this talk, we introduce a new combinatorial principle called grouping principle, and with this, calculate the size of dense sets for RT^2_2. By this we will show that the Pi^0_3-part of RT^2_2+WKL_0 is the same as that of RCA_0, and thus RT^2_2 does not imply the totality of the Ackermann function, which answers the question posed by Cholak, Jockusch and Slaman. This is a joint work with Ludovic Patey.
« Back...
|
|