
IMSJSPS 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. 186195, 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 "nonuniformly computable" choice principles.
« Back... Reflection and the finestructure 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 wellknown $\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 wellfoundedness of $\omega^\omega$.)
Thus, one can view reflection as a generalization of induction. The finestructure theorem is a classical result relating different fragments of reflection. So far, there have been only prooftheoretic proofs of this theorem. We will present a new modeltheoretic proof of this result with an explicit modelconstruction.
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 Eigendistribution for multibranching 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 iset and E^idistribution (i=0,1).They showed that for any binary trees, the E^1distribution is the unique eigendistribution with respect to the closed set of deterministic algorithms.
In this talk, we will consider the equivalence of E^idistribution and eigendistribution for balanced multibranching trees.
« Back... An overview on recent results on semiautomatic groups and semigroups Frank Stephan, National University of Singapore
An automatic function is a function where a deterministic finite automaton verifies that the output belongs to the input, that is, it reads the input and output with the same speed (one symbol per cycle) and accepts iff the output is correct for the given input. Automatic functions can also be characterised as those which are computed by positionfaithful onetape Turing machines in linear time. A group is automatic iff its domain is regular and both, equality and the group operation, are automatic functions with two inputs (read at the same speed). A group is Cayley automatic iff the domain is regular and equality is automatic and multiplication with a fixed group element is an automatic function; furthermore, one might postulate that the group is finitely generated. A group is semiautomatic, iff the domain is regular, for each fixed group element the set of all representatives is regular and for each fixed group element the multiplication from either side is automatic. Note that Cayley automatic does not require that multiplication with constants from both sides is automatic but only from one side. The talk will give an overview on recent results on these three types of groups and automaticity.
« Back... Determinacy strength of infinite games in omegalanguages recognized by variations of automata Kazuyuki Tanaka, Tohoku University, Japan
Continuing my talk at the 2014 IMSJSPS workshop in Singapore, I will report on the progress of our study on determinacy strength of infinite games in omegalanguages recognized by variations of automata. For example, we downscale O. Finkel?s result on analytic determinacy in contextfree omegalanguages to the Borel hierarchy, so that we obtain some reversemathematical results on determinacy. This is a joint work with Wenjuan Li.
« Back... The downward directed grounds hypothesis Toshimichi Usuba, Kobe University, Japan
A ground is a transitive inner model of ZFC such that the universe is a forcing extension of the model. We show that, in ZFC, the intersection of any setindexed collection of grounds contains a ground. Consequently, we see that the mantle, the intersection of all grounds, is a forcing invariant model of ZFC.
« Back... A survey on Qdegrees Guohua Wu, Nanyang Technological University
In the talk, I will give a survey on recent research on Qdegrees, with the focus on the isolation phenomenon involved.
« Back... Thoughts on indicators and density notions Keita Yokoyama, Japan Advanced Institute of Science and Technology, Japan
The density notion for Ramsey's theorem was first introduced by Paris to give an independent statement from PA. This notion actually defines an indicator for PA. In this talk, we will generalize this situation.
We will consider a class of secondorder 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 prooftheoretic strength of Ramsey's theorem for pairs Keita Yokoyama, Japan Advanced Institute of Science and Technology, Japan
In this talk, we study the prooftheoretic strength of Ramsey's theorem for pairs and two colors. Bovykin and Weiermann pointed out that the prooftheoretic strength of RT^2_2 can be can be approximated by Paris's density notion. Here, a finite set is said to be ndense if one can apply Ramsey's theorem for pairs ntimes repeatedly and the result set is still relatively large. Then, the Pi^0_3part of RT^2_2+WKL_0 is the same as that of RCA_0+"any infinite set contains an ndense 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_3part 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...

