2023年度のセミナー

2024.3.5 Leonardo Pacheco (TU Wien)

Title: High-order feedback computation 

Time: 13:00-15:00.

Abstract: Feedback Turing machines are Turing machines which can query a halting oracle $h:\subseteq \omega\times\omega\to \{\downarrow,\uparrow\}$, which has information on the convergence or divergence of \emph{feedback} computations. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A natural question to ask is: what if we iterate the feedback construction? We define $\alpha$th order feedback Turing machines for each computable ordinal $\alpha$ and describe the feedback semi-computable sets using inductive definitions and Gale--Stewart games. 

2024.3.5 Juan P. Aguilera (TU Wien)

Title: The Logic of Correct Models 

Time: 13:00-15:00.

Abstract: We study the collection of valid formulas built from expressions of the form “\phi holds in all Sigma_n-correct models.” This is joint work with F. Pakhomov. 

2024.3.1 William Mance (University of Adam Mickiewicz in Poznan)

Title: Descriptive complexity in number theory and dynamics 

Time: 15:00-16:30.

       Abstract: Informally, a real number is normal in base b if in its b-ary expansion, all digits and blocks of digits occur as           often as one would expect them to, uniformly at random. We will denote the set of numbers normal in base b by N             (b). Kechris asked several questions involving descriptive complexity of sets of normal numbers. The first of these              was resolved in 1994 when Ki and Linton proved that N (b) is Π0 3 -complete. Further questions were resolved by             Becher, Heiber, and Slaman who showed that T∞ b=2 N (b) is Π0 3 -complete and that S∞ b=2 N (b) is Σ 04

        complete. Many of the techniques used in these proofs can be used elsewhere. We will discuss recent results where          similar techniques were applied to solve a problem of Sharkovsky and Sivak and a question of Kolyada, Misiurewicz,         and Snoha. Furthermore, we will discuss a recent result where the set of numbers that are continued fraction                       normal,  but not normal in any base b, was shown to be complete at the expected level of D2(Π0 3 ). An immediate              corollary is that this set is uncountable, a result (due to Vandehey) only known previously assuming the generalized          Riemann hypothesis. 

2024.2.15 Oto Araki (Tohoku University)

Title: ML-randomnessとWWKL0のωモデルについて

Time: 15:00-16:30.

Abstract: WWKL0とWKL0のωモデルによる分離(Xiaokang Yu and Stephen G. Simpson)を, ML-randomnessを用いて説明します.

2024.1.26 Yuto Takeda (Tohoku University)

Title: 逆数学および計算可能性理論におけるラムゼイ型定理の研究  

Time: 15:00-16:30.

Abstract: ラムゼイの定理は長きにわたり逆数学・計算可能性理論の研究の主要テーマのひとつであった. その研究成果として, ラムゼイ型と称されるラムゼイの定理のバリエーションである, 無限組み合わせ論の定理の分析も近年進展を見せている. 今回, ラムゼイ型定理のひとつであるTree Theoremについて, 逆数学および計算可能性理論の観点による分析を修論の内容を基に発表する. 具体的には, 逆数学はTT^1_{<\infty}と帰納法公理の関係について, 計算可能性理論はCTT^2_2の彩色とlow_2 basis theoremについて概説する. 

2024.1.26 Naoyuki Hakuta (Tohoku University)

Title: 証明可能性論理とその分類について  

Time: 15:00-16:30.

Abstract: 証明可能性論理とは様相演算子$\Box$を「証明可能性」と解釈するような様相論理である．アルテモフやヴィッサーによるトレースという概念を用いた手法と，ベクレミシェフによるモデルを用いた手法により，証明可能性論理は4つの形の論理に分類されることが示されている．今回はその分類手法の概要を説明し，実際にその手法を用いて具体的な理論における証明可能性論理について調べた結果を紹介する． 

2024.1.26 Masataka Taguchi (Tohoku University)

Title: 証明可能性論理の多様総論理への拡張について  

      Time: 15:00-16:30.

Abstract: 命題論理の言語に 1 つの様相記号 P を加えたものが様相論理の言語であり, 無限個の様相記号を 加えたものが多様相論理の言語である. 様相論理の 1 つに GL があり, 様相記号を証明可能性述語と解釈 して得られるものである. GL の自然な多様相論理への拡張が GLP であり, クリプキ意味論を適切に経由することで, GL の算術的完全性の証明に用いられた Solovay の手法の拡張から, 多様相論理 GLP の算術的完全性が示される. 

2023.12.27 Kazuyuki Tanaka (BMSA/Tohoku University)

Title: ゲームの決定性に関する逆数学の再考 

Time: 15:00-16:30.

Abstract: Σ2の差階層におけるゲーム決定性に関するこれまでの多くの結果と最近の階層崩壊について述べます． 

2023.12.22 Kaito Ichikura (Shizuoka University)

Title: Subintuitionistic logicsの間の非可算濃度の論理の存在

Time: 15:00-16:30.

Abstract: Jankovは1968年に古典論理と直観主義論理の間に非可算濃度の論理の存在を示している. このJankovの結果は, その間に存在する論理の濃度が大きいという意味で, 古典論理と直観主義論理との間に大きな隔たりがあることを表現していると考えられる. Bezhanishvili-Colacito-de Jongは, 2020年に幾つかのsubminimal logics の間における非可算濃度の論理の存在を近傍意味論を用いて示した. この結果は, subintuitionistic logicsの間にも多くの大きな隔たりがあることを示唆している. 今回は2020年の結果を出した方法とは別の1974年のWro\’{n}skiによる代数的手法を工夫した方法を用いて, 上記の2020年の結果も含めて多くのsubintuitionistic logicsの間に非可算濃度の論理が存在することが分かったので, これを概説する.

2023.12.1 Keita Yokoyama (Tohoku University)

Title: A few recent topics in reverse mathematics 

Time: 15:00-16:30.

Abstract: In this talk, I will report on recent topics from the discussions at the Oberwalfach proof theory workshop this month and my current studies.

2023.11.3 Takako Nemoto (Tohoku University)

Title: Recent results in constructive reverse mathematics around WKL 

Time: 15:00-16:30.

Abstract: Constructive reverse mathematics aims to characterize mathematical theorems with some combination of a fragment of choice axioms and logical principles. In this talk, we consider several variations of K\H{o}nig’s lemma and related principles and observe some examples of the following phenomena.

- Logical principle raises up the consistency strength of systems.

- Induction principles and choice principles act similarly. 

2023.10.31 Yuto Takeda (Tohoku University)

Title:  CTT^2_2 のインスタンスに対する low_2 解の構成について 

Time: 15:00-16:30.

Abstract:  ラムゼイの定理のバリエーションのひとつである tree theorem には, そのインスタン スに対する解の計算論的な複雑さにおいて, 幾つかのケースに対してラムゼイの定理と同様 の結果が得られることが知られている. 一方, ペアに対する tree theorem について, その弱い バージョンである cohesive tree theorem for pairs (CTT^2_2) においてすら, インスタンスに対 する low_2 解を構成するには, ラムゼイの定理の場合と異なる難しさが存在する. 今回は CTT^2_2 に関して, そのインスタンスの low_2 解の構成について概説する. 

2023.10.20, 10.31 Masataka Taguchi (Tohoku University)

Title:  多様相論理 GLP, J の健全性と完全性  

Time: 15:00-16:30.

Abstract: 多様相論理は様相記号が 2 個以上となるように拡張された様相論理であり, その中でも 通常の正規様相論理 GL と同様に健全性, 完全性を持つものを興味の対象としている. 中でも 多様相論理 GLP の算術的健全性・完全性について成立することが, Japaridze により示され, さらに Becklemishev によって簡略化された証明手法も確立されている. 今回は Becklemishev による多様相論理 J を経由した証明方法について紹介する. 

2023.10.20 Naoyuki Hakuta (Tohoku University)

Title:  証明可能性論理の分類

Time: 15:00-16:30.

Abstract: 理論 T の証明可能性述語を様相演算子 □ と解釈したときに，理論 U において証明可能 な様相論理式全体の集合を U における T の証明可能性論理という．ソロヴェイやヴィッサー により T = U のときの証明可能性論理は GL および GL{□n⊥} という形の論理で尽くされる ことが知られている．さらにベクレミシェフにより一般に証明可能性論理は α, β ⊆ ω（β は 補有限）について GLα，GL− β ，Dβ，Sβ という 4 つの形の論理に分類されることが示されて いる．今回はその分類方法について紹介する． 

2023.10.13 Makoto Fujiwara (Tokyo University of Science)

Title:  Weihrauch and constructive reducibility between existence statements

Time: 16:00-17:30.

Abstract: We formalize the primitive recursive variants of Weihrauch reduction between existence statements in finite-type arithmetic and show a meta-theorem stating that the primitive recursive Weihrauch reducibility verifiably in a classical finite-type arithmetic is identical with the normal reducibility in the corresponding (nearly) intuitionistic finite-type arithmetic for all existence statements formalized with existential free formulas. In addition, we demonstrate that our meta-theorem is applicable to some concrete examples from Weihrauch and constructive reverse mathematics. 

2023.8.29 Satoru Niki (Ruhr University Bochum)

Title: How can an intuitionistic logician understand connexive constructible falsity?   

Time: 15:00-16:30.

Abstract: Constructivists have usually understood negation as an implication to absurdity. Nonetheless, there have also been dissenting voices to this conception, one of the most notable among which are ones who advocate an alternative notion called constructible falsity. Nels David Nelson (1918-2003) introduced this notion as a `strong’ form of negation, which provides a direct counter-example to its negand. This `strongness’ is however often eschewed in favour of paraconsistency, making the resulting negation, severed of its relationship with intuitionistic negation, harder for intuitionistic logicians to comprehend. The issue is more serious in a variant of constructible falsity introduced by Heinrich Wansing, which validates so-called `connexive’ principles. This is due to the provability of a contradictory pair of formulas, which prohibits an interpretation of it as a `strong’ negation without bringing triviality. As a result, Wansingian negation should appear even more mysterious to the eyes of intuitionistic logicians. Another way to relate intuitionistic and Wansingian negations is to accept the law of excluded middle for the latter, as studied by Wansing and Hitoshi Omori. This move, however, compromises constructivity, and therefore is perhaps not so preferable either. In this talk, I will try to shed some lights on this issue, by discussing other ways to introduce an interaction between intuitionistic and Wansing negations. I will compare relative advantages of the interactions, which may enable intuitionistic logicians to better understand Wansingian negation and its connexivity. 

2023.8.4 Fuki Ito (Tokyo Metropolitan University)

Title: AND-OR木探索の乱択アルゴリズムとその均衡値 

Time: 16:00-17:30.

Abstract: AND-OR木は同じ変数が1度のみ現れるようなブール関数の計算モデルであり、その計算コストは変数のクエリー回数によって定義される。本講演では主に乱択アルゴリズムを興味の対象とする。乱択アルゴリズムによるコスト均衡値、すなわち最小化された最悪計算量は、ランダムでないアルゴリズムのみを用いる場合に比べて真に小さくなることがSaksとWigderson(1986)により示されている。Saksらの手法をベースとして、最適な乱択アルゴリズムの一意性や、乱択アルゴリズムを深さ優先(depth-first)・一方向性(directional)などの条件で制限した場合の均衡値の大小関係について解説する。本研究の一部は鈴木登志雄氏との共同研究である。 

2023.7.21 Hajime Ishihara (Japan Advanced Institute of Science and Technology)

Title: A constructive integration theory: a topological approach  

Time: 15:00-16:30.

Abstract: We present a development of a constructive integration theory from a topological point of view, and constructively prove several convergence theorems in integration theory including Fatou’s lemma, and the monotone and dominated convergence theorems of Lebesgue in the totally topological framework.

2023.6.23 Quentin Le Houérou (École normale supérieure de Lyon)

Title: \Pi^1_1 conservation of Ramsey theorem for pairs over B\Sigma^0_2+WF(\epsilon_0).  

Time: 15:00-16:30.

Abstract: Finding the first-order part of Ramsey theorem for pairs and two colors (RT^2_2) has been a long-standing question in the field of reverse mathematics. In their 2017 article, Chong, Slaman and Yang showed that RT^2_2 does not imply \Sigma_2 induction. We present here another proof of that result, by showing the \Pi^1_1 conservation of RT^2_2 over the base theory B\Sigma^0_2 + WF(\epsilon_0) where B\Sigma^0_2 denotes the bounded collection scheme for \Sigma_2 formulas and WF(\epsilon_0) the well-foundedness of the ordinal \epsilon_0.

The statement WF(\epsilon_0) is a strange base theory to consider, as it is at the same time a very strong assumption (not provable in ACA_0) but also quite weak (does not imply \Sigma_2 induction). Nevertheless, the well-foundedness of certain ordinals has been shown to be a robust and natural statement to study (see Kreuzer and Yokoyama 2013) and has already been used in various forms in the past to study Ramsey-like statements (see Chong, Slaman and Yang 2014).

This is a joint work with Ludovic Levy Patey and Keita Yokoyama. 

2023.6.16 Yudai Suzuki (Tohoku University)

Title: A \Pi^1_2 approximation of \Pi^1_1- CA_0.  

Time: 15:00-16:30.

Abstract: In the typical study of reverse mathematics, theorems are classified into five levels: RCA_0, WKL_0, ACA_0, ATR_0 and \Pi^1_1-CA_0. On the other hand, recent studies of this area focus on the intermediate levels: theorems they are not equivalent to any of those five systems.

In this talk, we consider the intermediate structure between ATR_0 and \Pi^1_1-CA_0.

It is known that the gap of \Pi^1_1-CA_0 is very large.

More precisely, \Pi^1_1-CA_0 is not provable from any consistent \Pi^1_2 statement, and ATR_0 is axiomatizable by a \Pi^1_2 sentence.

Moreover, there are a lot of \Pi^1_2 statements  provable from \Pi^1_1-CA_0 but stronger than ATR_0.

So a question arises: Can we clarify the structure of the \Pi^1_2 part of \Pi^1_1-CA_0? That is, is there a useful axiomatization of \Pi^1_2 part of \Pi^1_1-CA_0?

In this talk, we introduce a hierarchy of \Pi^1_2 statements such that  it captures the \Pi^1_2 part of \Pi^1_1-CA_0. That is, any \Pi^1_2 statement provable from \Pi^1_1-CA_0 is already provable from one of the statements in the hierarchy.

2023.6.9 Paul Shafer (University of Leeds)

Title: The Rival--Sands theorem for partial orders, ascending/descending sequences, and \Sigma_2 induction

Time: 15:00-16:30.

Abstract: In their 1980 article, Rival and Sands proved two theorems inspired by Ramsey’s theorem for pairs. The second of these theorems states that every infinite partial order P of finite width contains an infinite chain C with the property that every element of P is comparable either with no element of C or with infinitely many elements of C. We show that this theorem is equivalent to the ascending/descending sequence principle plus the \Sigma_2 induction scheme over RCA_0. This work is joint with Marta Fiori-Carones, Alberto Marcone, and Giovanni Soldà.

2023.6.2 Hiroyuki Ikari (Tohoku University)

Title:  A conservation result for RT^2 and B\Sigma^0_3. 

Time: 15:00-16:30.

Abstract: It's well known that COH+D^2 is equivalent to RT^2 (over RCA_0). Some basis theorems for RT^2 are proved by this decomposition. Carrying out this proof within a model of WKL_0+B\Sigma^0_3, we can prove a conservation result. In this talk, we see a proof of \ll^2-basis theorem for D^2, using effective coded \omega-models of WKL_0. These discussions and results can give a new view point to conservation results, with help of a view point of some types of basis theorem. The contents are joint work with Keita Yokoyama.


References

[1] Hirschfeldt, Denis R. Slicing the truth: On the computable and reverse mathematics of combinatorial principles. 2015.

[2] Fiori-Carones, M., Kołodziejczyk, L. A., Wong, T. L., Yokoyama, K. "An isomorphism theorem for models of Weak Kőnig's Lemma without primitive recursion." (2022).


2023.5.26 Yuto Takeda (Tohoku University)

Title:  The computability theoretic and reverse mathematical analysis of Ramsey's Theorem. 

2023.5.9 Antonio Montalban (University of California, Berkeley)

Title:  The game metatheorem.

2023.4.28 Masaya Taniguchi (Tohoku University)

Title:  Proof-theoretic linguistics: the formal approach to natural language. 

2023.4.21 Makoto Fuziwara (Tokyo University of Science)

Title:  On the embedding of Kripke models into Beth models

 Following [2, Chapter 13], we revisit the embedding from modern perspectives.

 [1] S. A. Kripke, Semantical Analysis of Intuitionistic Logic I, Studies in Logic and the Foundations of Mathematics, Vol.40, pp. 92-130, 1965.

 [2] A. S. Troelstra and D. van Dalen, Constructivism in Mathematics, Vol 2, Elsevier, 1988. 

2023.4.14 Hitoshi Omori (Tohoku University)

Title:  Negation and modality in view of non-deterministic semantics