Title: 二階算術における様相論理の完全性について
Venue: Complex A 801
Time: 15:00-
Abstract: TBA
Title: 2階算術における特異積分論
Venue: Complex A 801
Time: 15:00-
Abstract: TBA
Title: 確率計算木論理とその周辺
Venue: Complex A 801
Time: 15:00-
Abstract: TBA
Title: 二階算術における様相論理の完全性について
Venue: Complex A 801
Time: 15:00-
Abstract: TBA
Title: 2階算術における特異積分論
Venue: Complex A 801
Time: 15:00-
Abstract: The motivation of this research is to formalize some basic theories concerning singular integrals in a weak subsystem of second-order arithmetic called RCA_0. Especially, we focus on the theorem which states the L^p boundedness of convolution operators with a singular kernel satisfying certain conditions. WWKL_0 is usually required when dealing with analysis in second-order arithmetic, since its lack would mean that even the basic properties of measure theory, such as the countable additivity of measure, cannot be justified. However, most part of this research is carried out in RCA_0 by limiting the calculation of integrals on a class of compactly supported smooth functions that are effectively integrable on any cube in R^d.
Title: A proof of Nash-Williams theorem in ATR0
Venue: online via zoom
Time: 16:00-
Abstract: In [1], Crispin Nash-Williams proved that if (Q, ≤_Q) is a well quasi-order (henceforth wqo), then so is the set of transfinite sequences over Q with finite range, ordered by embeddability. In this talk, we will show that this result is provable in the subsystem of second-order arithmetic ATR_0: together with previous results by Shore [2], this determines the reverse mathematical strength of Nash-Williams’ result. In order to do this, we will go via the notion of better quasi-order, which makes it possible to develop an equivalence between the iterated powerset of a qo Q and the iterated powerset over Q. This is joint work with Fedor Pakhomov.
[1] C. Nash-Williams, On well-quasi-ordering transfinite sequences, Mathematical Proceedings of the Cambridge Philosophical Society 61 (1965), no. 1, 33–39.
[2] R. A. Shore, On the strength of Fraïssé’s conjecture, Logical methods: In honor of Anil Nerode’s sixtieth birthday, 1993, pp. 782–813.
Title: Leanを用いたGödelの第一・第二不完全性定理の形式化
Venue: Complex A 801 (and online via zoom)
Time: 15:00-16:30
Abstract: I report on the formalization of Gödel's famous incompleteness theorems in the Lean 4 proof assistant. While formalizations of the incompleteness theorems have been conducted multiple times since the 1980s, this study formalizes stronger versions than those in previous works: the first incompleteness theorem over Cobham's R₀ and the second incompleteness theorem over IΣ₁.
Title: On some restricted variants of the leftmost path principle
Venue: Complex A 801 (and online via zoom)
Time: 14:30-16:00
Abstract: In the studies of reverse mathematics and problem reductions, principles stating the existence of a path through a given tree play a central role. For example, WKL, KL, C_{ω^ω} and LPP are widely studied in those contexts. Here, WKL is the assertion that any infinite binary tree has a path, KL is the assertion that any finitely branching infinite tree has a path, C_{ω^ω} is the principle to find a path from an ill-founded tree, and LPP is the assertion that any ill-founded tree has a leftmost path. Recently, Towsner[Tow] introduced a new principle called the relative leftmost path principle stating the existence of a pseudo leftmost path. It is known that the proof-theoretic strength of relative LPP is strictly between ATR_0 and Pi^1_1-CA_0, and relative LPP is useful to study the complexity of some theorems which are stronger than ATR_0[FDSTY]. In this talk, I will present my contribution[SuY, Suz] to the studies of relative LPP, and consider LPP and relative LPP restricted to WKL or KL. A part of this talk is joint work with Keita Yokoyama.
[Tow] Henry Towsner. Partial impredicativity in reverse mathematics. J. Symb. Log., 78(2):459–488, 2013
[FDSTY] David Fern´andez-Duque, Paul Shafer, Henry Towsner, and Keita Yokoyama. Metric fixed point theory and partial impredicativity. Philosophical Transactions of the Royal Society A, 381(2248):20220012, 2023.
[SuY] Yudai Suzuki and Keita Yokoyama. Ann. Pure Appl. Logic 175, No. 10, Article ID 103488, 31 p. (2024; Zbl 07894021)
[Suz] Yudai Suzuki Relative leftmost path principles and omega-model reflections of transfinite inductions’, Preprint, arXiv:2407.13504 [math.LO] (2024)
Title: 直観主義論理の部分体系上の算術の分類
Venue: Complex A 801
Time: 15:00-16:30
Abstract: 爆発律を subminimal logics (Minimal logic の否定を弱めた部分体系を subminimal logic と呼ぶ) 上で観察することから始め、そうすることで得られる論理上の算術を証明される論理式の多さに対する関係について調べる。
Title: 鳩ノ巣原理の階層とTree Theorem
Venue: Complex A 801
Time: 15:00-16:30
Abstract: 逆数学における鳩ノ巣原理はラムゼイの定理の最もシンプルなバージョンとして 計算可能性理論及び証明論の観点から広く研究が行われてきた. そして近年では鳩ノ巣原 理の複雑さによる階層が発見され, その他のラムゼイ型定理や帰納法公理との関係性につ いても研究が進んでいる. 本発表では鳩ノ巣原理の階層について, 最新の研究を紹介する とともに, 発表者が関心を持っている Tree Theorem との関係についても論じる.
Title: 様相論理の強完全性証明
Venue: Complex A 801
Time: 15:00-16:30
Abstract: クリプキモデルを用いた様相論理の強完全証明が$\mathrm{ACA_0}$と同値であることを紹介します。無矛盾な集合$\Gamma$のモデルの世界として極大無矛盾な$\Gamma$ロウ集合を取るのが普通の強完全性証明と異なる点で、Low basis theorem を使います。
Title: 帰納的定義付き一階述語論理の循環証明体系におけるカット除去の反例
Venue: Online via zoom.
Time: 15:00-16:30
Abstract: 循環証明体系とは証明図にサイクル（循環）の存在を許容した証明体系である．このような体系は無限降下法の形式化とみなせる場合がある．そのため，循環証明体系は帰納法を使う証明体系の代替手段として証明探索の観点から注目されている．その一方で，循環証明体系の証明論的な性質についてはまだわかっていないことが多い．本講演では帰納的定義付き一階述語論理に対する循環証明体系のカット除去の反例を与える．反例の存在から帰納的定義付き一階述語論理に対する循環証明体系においてはカット除去性という基本的な性質が成り立たないことがわかる．
Title: 準古典的算術における冠頭標準形定理と部分トポス構造
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30
Abstract: 論理式の形に関する冠頭標準形定理は、直観主義論理上では一般には成り立たないことがよく知られている。とりわけ準古典的算術における冠頭標準形定理の成否については、藤原氏と倉橋氏により精密に調べられている[1]。彼らは証明論的議論に基づき次の否定的結果を示していた: HA + Sigma_1-DNEにおいてSigma_1に関する冠頭標準形定理は成立しない。
本講演では、この結果のトポス理論的議論に基づく別証明を与え、その一般化について考察する。
[1] Makoto Fujiwara and Taishi Kurahashi. Prenex normal form theorems in semi-classical arithmetic. Journal of Symbolic Logic, 86(3):1124--1153, 2021.
Title: On the Pi^1_2, Sigma^1_2 and Boole(Pi^1_2) sentences provable from Pi^1_1-CA_0
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30
Abstract: In [1], we introduced some characterizations of the set of Pi^1_2 sentences provable from Pi^1_1-CA_0 and a hierarchy dividing it. For a detailed study of the properties of this hierarchy, it was important to focus on the statements of the form [every coded beta-model satisfies sigma] for some specific sentences sigma.
In this talk, we summarize a part of [1]. Then we give a characterization of the set of Sigma^1_2 or
Boole(Pi^1_2) sentences provable from Pi^1_1-CA_0 by statements of the form [every coded beta-model
satisfies sigma]. Here, Boole(Pi^1_2) is the class of formulas generated by disjunction, conjunction and
negation starting from Pi^1_2.
This is joint work with J. Aguilera and K. Yokoyama.
[1] Suzuki, Y., & Yokoyama, K. (2024). On the $\Pi^ 1_2 $ consequences of $\Pi^ 1_1 $-$\mathsf {CA} _0$. arXiv preprint arXiv:2402.07136.
Title: Tree Theoremと帰納法公理の関係
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30
Abstract: ラムゼイの定理は長きにわたり逆数学研究の主要テーマのひとつであった。そのバリュエーションであるTree theoremの研究も近年進展を見せている。今回、Tree theoremの彩色のstable性に関する定理である0-S^3TT^2_2と帰納法公理の関係について、conservativityの手法により分析した。先行研究であるTT^1のconservationに関する結果を紹介するとともに研究の現状について報告する。
Title: 爆発律に関連する直観主義論理より弱い論理上での数学
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30
Abstract: 爆発律は推論規則として奇妙に見える。しかし、爆発律を除いた論理上での数学では不都合なことが起こる。このことから爆発律の数学での働きを調査すべく先ず爆発律を取り巻く環境を変えた。古典論理、直観主義論理も爆発律を持ちMinimal logicは爆発律を持たないが爆発律を加えると直観主義論理になってしまう。故に、Minimal logicより弱い論理(Subminimal Logics)で爆発律を観察した。その結果、新たな論理の構造が明らかになった。 この話では新たな論理上で数学に関する新たな事実を紹介する。
Title: Ekeland’s variational principle and reverse mathematics
Venue: Complex A 801 (and online via zoom).
Time: 14:00-15:30
Abstract: In the study of reverse mathematics for analysis, it is observed that many theorems on minimal value principles for continuous functions are provable within the system of arithmetical comprehension (ACA_0) since they are usually depended on compactness. In contrast, we will see that Ekeland’s variational principle, which is a variation of minimization theorem in non-compact situation, is equivalent to Pi^1_1-comprehenstion.
In this talk, we will overview the reverse mathematics for analysis and then see the idea for the above result.
Title: Varieties of reversals
Venue: Complex A 801 (and online via zoom).
Time: 15:00-16:30
Abstract: Reverse mathematics has become one of the most important subjects of mathematical logic. It has a rich domain of problems arising from ordinary mathematics, as well as a programmatic orientation. To put it briefly, its results seem to matter not only for logic but also for ordinary mathematics. Yet there are several different accounts of why it matters, of what a reversal tells us. I want to discuss a few of these.