Samuel R. Buss (UCSD)

Bounded Arithmetic, Expanders, and Monotone Propositional Logic

This talk discusses a weak theory of Bounded Arithmetic, $VNC^1$, which corresponds to alternating logarithmic time computation. We show that this theory can formalize the construction of expander graphs. This in turn implies that the monotone propositional sequent calculus can polynomially simulate the full (non-monotone) propositional sequent calculus with respect to monotone sequents. 

Jean-Yves Girard (Marseille)

ON SECOND ORDER LOGIC

In 1953, Takeuti introduced G^1LC, a second order sequent calculus. Both proofs of cut-elimination (weak form: Tait 1965, strong form: Girard 1970) shed a light on the very nature of logic — second order or not.

Kanji Namba (Prof. Emeritus, U. of Tokyo)

$\eta$ function, Gauss-AGM and computational complexity

$\eta$ function is defined by

$\eta(x) = x^{1/24}\cdot\Pi_{n\in N}(1-x^n) = \Sigma_{n\in Z}(-a)^n x^{1/24\cdot(6n+1)^2} = x^{1/24}\cdot\Sigma_{n\in N}(-x)^{n(3n+1)/2}$. 

Gauss-AGM, ehich, temporarily denoted as $a\diamond b$, is the common limit of recursion: 

$a = (a+b)/2, b=\sqrt{(a*b)}$, begin with $a, b$. 

For computational complexity, notion expressible in both form, for example, 

Recursive $(\exists n=\forall n)$, Borel $(\exists\alpha = \forall\alpha)$

Are very fundamental ones. In pure number theory, we concern in, both form, especially for cyclic continued exponential products (ccep): 

$\Pi_{n\in N} = \Sigma{n\in Z}$

Talk contains some notions of elliptic curves, modular functions $E_4(x), E_6(x)$ and AGM as for example. 

Masanao Ozawa

From Boolean-Valued Analysis to Quantum Set Theory

In 1978 Takeuti introduced Boolean-valued analysis, a systematic method to apply Boolean-valued models to problems of analysis. He subsequently constructed models of set theory based on a quantum logic, the full lattice of projections on a Hilbert space, showing how axioms of the ZFC set theory can be modified to hold in the models. In this talk, we review successful developments of Takeuti’s two attempts above, particularly with emphasis on what forcing meets an open problem in functional analysis and how quantum set theory naturally extends the standard interpretation of quantum mechanics. 

Wilfried Sieg (CMU)

Proofs and objects: Hilbert’s pivotal thought

The rigor of mathematics lies in its systematic organization that makes for conclusive proofs of assertions on the basis of assumed principles. Proofs are constructed through thinking, but can also be taken as objects of mathematical investigation; that was the key insight underlying Hilbert’s call a theory of the “specifically mathematical proof” in 1917. This pivotal idea was rooted in revolutionary developments of mathematics and logic, but it also shaped the new field of mathematical logic. IT grounded, in particular, Hilbert’s proof theory. The emerging investigations led over time to computability theory, artificial intelligence and cognitive science. Within this broad framework, I will describe first the pursuit of Hilbert’s proof theory with “reductive” foundational goals and then some recent, tentative steps towards a theory of the “specifically mathematical proof”. Those steps have been made possible by a confluence of proof theoretic investigations in the tradition of Gentzen’s work on natural deduction and computer implementation of mechanisms in which proofs can be (automatically) constructed. Here, at the intersection of automated proof search and interactive verification, is a promising avenue for exploring the structure of mathematical thought. 

Mariko Yasugi

(Tentative Title) A reflection on Takeuti's finitist standpoint 

The talk is composed of the framework of the so-called consistency proofs, Takeuti's finitist stand point therein and a proposal to give mathematical expressions to it in terms of extended terms with bar recursion.

Sakae Fuchino

Reflection principles and continuum hypothesis

It is known that some reflection statements impose restrictions on the size of the continuum (e.g. this is the case with the reflection of the stationarity of a set of countable subsets of an arbitrary underlying set down to a subset of cardinality $<\aleph_2$. This statement namely implies $2^{\aleph_0}\leq\aleph_2$, see [millennium book, Theorem 37.22]). 

Some very strong reflection down to $<\aleph_2$ even implies CH. Strong reflection down to $<2^{\aleph_0}$ implies $2^{\aleph_0}=\aleph_2$ while many strong statements about reflection down to $\leq2^{\aleph_0}$ are consistent with almost any size of the continuum (under some large large cardinal axiom). 

Daichi Hayashi

On upper bounds for some complete and consistent theories of truth

The proof-theoretic strengths of nine truth theories A to I presented by Friedman and Sheard (1987) are determined by Cantini (1990), Halbach (1994) and Leigh and Rathjen (2010). Especially, Leigh and Rathjen gave infinitary cut elimination arguments to establish upper bounds on the proof-theoretic strengths of E, F, G and I. In this talk, we show that upper bounds for A, B, C and D are also obtained by using infinitary cut elimination. Moreover, the same method can be applied to the analysis of the typed theories of truth.

Daisuke Ikegami

On large cardinal properties of $\omega_1$.

In the presence of the Axiom of Choice (AC), the least uncountable cardinal $\omega_1$ is very small compared to any large cardinal while without AC, $\omega_1$ may enjoy some properties of large cardinals. Jech and Takeuti independently proved that $\omega_1$ could be a measurable cardinal without AC. Takeuti went on to prove that $\omega_1$ could be strongly compact / supercompact / huge as well without AC. In this talk, we summarize recent development of large cardinal properties of $\omega_1$ and their influence on the real line. This is joint work with Nam Trang.

Sohei Iwata

Interpolation properties for fragments of Gödel-Löb logic GL

In 2001 Sacchetti introduced the modal logics wGL_n = K + □(□^nφ→φ)→φ (n≧2) which are fragments of the Gödel-Löb logic GL. He showed that these logics have the Craig interpolation property, and also proved the fixed-point theorem for wGL_n. The proofs are purely semantical, based on Smoryński's separation argument.

Sacchetti asked the existence of a provability predicate for PA whose provability logic is wGL_n, and the existence an effective procedure to construct fixed points for wGL_n. In recent years these problems are settled affirmatively by Kurahashi and Okawa.

In this talk, we formulate the sequent calculus for wGL_n, and give the syntactical proof of the Craig interpolation property. Moreover, we prove the Lyndon interpolation property for wGL_n by adapting Smoryński's semantical argument.

Mamoru Kaneko

Small Infinitary Epistemic Logics (with Tai-wei Hu and Nobu-Yuki Suzuki)

We develop a series of small infinitary epistemic logics to study deductive inference involving intra/inter-personal beliefs/knowledge such as common knowledge, common beliefs, and infinite regress of beliefs. Specifically, propositional epistemic logics GL(L_{α}) are presented for ordinal α up to a given ordinal so that GL(L₀) is finitary KDⁿ with n agents and GL(L_{α}) (α≥1) allows conjunctions of certain countably infinite formulae. GL(L_{α}) is small in that the language is countable and can be constructive. The set of formulae L_{α} is increasing up to α = ω but stops at ω. We present Kripke-completeness for GL(L_{α}) for each α ≤ ω, which is proved using the Rasiowa-Sikorski lemma and Tanaka-Ono lemma. GL(L_{α}) has a sufficient expressive power to discuss intra/inter-personal beliefs with infinite lengths. As applications, we discuss the explicit definabilities of Axioms T (truthfulness), 4 (positive introspection), 5 (negative introspection), and of common knowledge in GL(L_{α}). Also, we discuss the rationalizability concept in game theory in our framework. We evaluate where these discussions are done in the series GL(L_{α}), α ≤ ω. 

Takayuki Kihara

Computability-theoretic methods in descriptive set theory

We will survey our recent work on applications of computability theory to descriptive set theory and related areas. Our method ranges over the studies on decomposability of Borel functions, Borel isomorphism problems related to infinite dimensional topology, the Wadge degree structures of BQO-valued Borel functions, and so on. We will explain how computability-theoretic methods are involved in these studies.

Taishi Kurahashi

Rosser provability and the second incompleteness theorem

G\"odel's famous second incompleteness theorem states that if $T$ is recursively axiomatized consistent extension of Peano Arithmetic, then formal consistency statement of $T$ cannot be proved in $T$. This statement of the second incompleteness theorem is somewhat ambiguous because the unprovability of a formal consistency statement is dependent on the choice of a provability predicate. It is well-known that for $\Sigma_1$ provability predicates, the Hilbert-Bernays-L\"ob Derivability Conditions are sufficient for a proof of the second incompleteness theorem. Other sets of sufficient conditions for the second incompleteness theorem are also found by Jeroslow (1973), Montagna (1979), Rautenberg (2002?) and so on. 

On the other hand, Arai (1990) proved that some sets of conditions are not sufficient for the second incompleteness theorem by showing the existence of Rosser provability predicates satisfying such conditions. In this talk, I improve Arai's results and show that several sets of conditions are not sufficient for the second incompleteness theorem. 

Hidenori Kurokawa

On Takeuti's view of the concept of set

Gaisi Takeuti occasionally talked about the concept of set. Based on these remarks, we can easily see that Takeuti had a highly original view of the concept of set. However, although some of his views may be adopted inhis theory NTT, Takeuti gave no sufficiently systematic development of his own view (or philosophy) of the concept of set in its entirety. In this talk, we try to put together Takeuti's scattered remarks on the concept of set, most of which are currently available only in Japanese, and to reconstruct Takeuti's view of the concept of set in a manner as systematic as possible.  In particular, we will focus on the following two aspects of Takeuti's view of the concept of set: i) the relationship between logic and the concept of set; ii) the notion of growing universe. 

Yo Matsubara

Precipitousness of Countable Stationary Towers

H. Woodin introduced the concept of stationary tower forcing.  Using stationary tower forcing, he proved that the existence of some large cardinals implies various properties of L(R).

We present a characterization of precipitousness of countable stationary towers. Then we show that precipitousness of some countable stationary towers, without explicit use of strong large cardinals such as Woodin cardinals, implies some regularity properties of sets of reals in L(R).

Tadatoshi Miyamoto

Partitioning the Tripes of the Countable Ordinals and Morasses

We provide a new proof of a negative partition relation with the triples orginally established by Erdos and Rado in 1956. We make use of a simplified morass that was found by Velleman in 1984. It is known that the morass exists in ZFC. Hence the negative partition relation holds in ZFC.

NingNing Peng, Weiguang Peng, Kazuyuki Tanaka

The eigen-distribution for weighted trees on various kinds of distributions

n this talk, we survey recent results on the eigen-distributions that achieve the distributional complexity for AND-OR trees. Liu and Tanaka (2007) launched a study program to calibrate them on different kinds of distributions (CD for correlated, ID for independent, or IID for independent and identical) under different classes of algorithms (e.g., directional or non-directional). Recently, Suzuki and Niida (2015) made a prominent work on uniform binary trees on ID and IID, and then Peng et al. (2017) generalized it to balanced multi-branching trees. On the other hand, it had remained open whether the eigen-distribution is unique or not for a balanced multi-branching tree on CD. To this end, Okisaka et al. (2017) introduced the weighted trees, namely, trees with weights depending on the value of a leaf. In this talk, we show some new results on weighted trees on ID and IID.

Norbert Preining (joint work with Matthias Baaz)

First Order Gödel Logics with Propositional Quantifiers

First order Gödel logics form a well established class of many-valued logics with good proof-theoretic properties and extensive theory. Quantified Propositional Gödel Logics have been studied only a few times, and not much is known about these logics besides a few results for specific logics. Propositional quantifiers allow for quantification of propositions, which in the setting of Gödel logics boils down to quantification over all truth values of the underlying truth-value set. Thus, they are somewhere between first order and second order quantifiers. It has already been shown that there are uncountably many quantified propositional Gödel logics (without first order quantifiers), which is in stark contrast to the fact that there are only countably many first order Gödel logics. For three cases, namely V∞ = [0, 1], V↓ = {0} ∪ {1/n : n > 0}, and V↑ = {1} ∪ {1 − 1/n : n > 0}, quantifier elimination has been shown for the propositional quantified Gödel logics, in later two cases by extension of the language with an additional operator.

In this paper we initiate the research program to study the combination of propositional and first-order quantifieres with respect to Gödel logics.

Toshimichi Usuba

Multiverse and large cardinals

H. Woodin introduced the notion of generic multiverse, which is a minimal collection $F$ of transitive models of ZFC such that $F$ is closed under taking ground models and generic extensions. In this talk, we prove that large cardinal axioms strongly affect the structure of generic multiverse, namely, if a generic multiverse has a model with extendible cardinal, then a generic multiverese has a minimum element.

Mariko Yasugi, Yoshiki Tsujii and Takakazu Mori

Irrational based computability of functions

A theory of relatively irrationally (RelIrr-) computable real functions will be developed.  RelIrr-computability of a real function, continuous or discontinuous, means, roughly speaking, an effectivization of almost everywhere continuity. It gives a unifying computability principle to the functions we have so far made computable with various methods. We also discuss the virtue of this principle as a natural extension of the computability notion of continuous functions.

Keita Yokoyama

Ekeland's variational principle in reverse mathematics

Ekeland's variational principle is a key theorem used in various areas of analysis such as continuous optimization, fixed point theory and functional analysis. It guarantees the existence of pseudo minimal solutions of optimization problems on complete metric spaces. Let f be a positive real valued continuous (or lower semi-continuous) function on a complete metric space (X,d). Then, a point x in X is said to be a pseudo minimum if f(x)=f(y)+d(x,y) implies x=y. Now, Ekeland's variational principle says that for any point a in X, there exists a pseudo minimum x such that f(x)<=f(a)-d(a,x). In reverse mathematics, it is observed that many theorems for continuous optimization problems are provable within the system of arithmetical comprehension (ACA_0), and thus most such problems have arithmetical solutions. However, this is not the case for pseudo minima. We will see that Ekeland's variational principle or its restriction to the space of continuous functions C([0,1]) are both equivalent to Pi^1_1-comprehenstion. This is a joint work with Paul Shafer and David Fernandez-Duque.

Yasuo Yoshinobu

Indestructible and absolute properness

We say a poset P is indestructibly proper if any product of P with a \sigma-closed poset is proper. On the other hand, we say P is absolutely proper if P remains proper in any generic extension obtained by forcing over a \sigma-closed poset. We argue how different these two strengthenings of the properness are.