Speaker: 横山 駆（名古屋大）
Title: On computable real numbers uniformly distributed modulo 1 with respect to Koksma sequences
Abstract: (1+x)^nの小数部分が[0,1]上に一様に分布するような実数xとして、ML-random real等がこれに該当することは示されている。しかし、計算可能な実数でこの性質を持つものが存在するかは(恐らく)未解決であった。本講演では、一様分布論とランダムネスの関係性について簡単に紹介し、先の問題についての肯定的な解答を提示する。
Speaker: 中田 哲（名古屋大）
Title: 一般化された神託を可能世界にもつクリプキ意味論
Abstract: 通常、一階述語論理に対するクリプキ意味論は、可能世界として集合論に基づくモデルが用いられている。そのため直観主義一階算術のクリプキ意味論を計算する場合、算術の超準モデル論など技巧的な議論を要することが知られている。
そこで本講演では、算術への応用を念頭に、可能世界として計算論に基づくモデルを用いたクリプキ意味論を考察する。ここでは一般化された神託(実効トポスのLawvere-Tierney位相)による定義を採用し、そのクリプキ意味論が直観主義一階算術に対して健全となることを示す。また時間の許す限りその計算例を紹介する。
Speaker: 齋藤 彰悟（東北大）
Title: ∃ℝの有界算術について
Abstract: BussのS_2^iなどをはじめとして， 弱い算術の体系と計算複雑性クラスは互いに密接に関連していることが知られている．ここでは∃ℝ(existential theory of the reals)と呼ばれる計算複雑性クラスについて，それと関連した有界算術の体系を定義しその基礎的な性質を調べた．
Speaker: 高瀬 理人（神戸大）
Title: 様相論理PFの一般化の位相意味論
Abstract: Hamkins-Lõweは様相論理を用いて強制拡大の性質をとらえた．また，Solovayは様相論理を用いて証明可能性述語の性質を調べた．
これらの研究の手法は類似のものであるが，異なる文脈で研究されていた．Kurahashi-T.はこれら二つを同時に扱い，様相論理PFの定義と完全性を示した．
本発表では様相論理PFを少し一般化した論理について掘り下げ，位相意味論や強完全性について示せたことを紹介する．
Speaker: Leonardo Pacheco （東京科学大）
Title: IGL without sharps
Abstract: Das, van der Giessen and Marin recently defined an intuitionistic version of the provability logic GL. They define birelational and predicate semantics and two non-wellfounded proof systems lIGL and mlIGL. They prove the completeness and soundness of the two proof systems with respect to both semantics. In the proof of the completeness of mlIGL with respect to the predicate semantics, they use $\Sigma^1_1$-determinacy; a statement not provable in ZFC. We define a cyclic proof system clIGL for IGL and prove its completeness with respect to predicate semantics using open determinacy. In particular, this implies that the completeness of mlIGL does not need $\Sigma^1_1$-determinacy.
Speaker: 竹田 侑人（東北大）
Title: Completeness theorem of modal logic in second-order arithmetic
Abstract: In this survay, we investigate the logical strength of completeness theorems for modal propositional logic in second-order logic. There have been various attempts to formalize and analyze mathematical logic in second-order arithmetic in recent years [1, 2]. In this survay, we show that ACA_0 is equivalent over RCA_0 to the strong completeness theorem for modal propositional logic. Moreover, we introduce the weak form strong completeness theorem and show that it is equivalent with WKL_0 over RCA_0.
[1] Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in Logic. Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, second edition, 2009.
[2] Takeshi Yamazaki. Reverse mathematics and completeness theorems for intuitionistic logic. Notre Dame J. Formal Logic, 42(3):143–148, 2001.
Speaker: 鈴木 悠大（小山高専）
Title: 弱いbeta_nモデル反映原理と強従属選択公理
Abstract: 逆数学ビッグ5最強の公理系Pi^1_1-CA_0は，beta_1-model反映原理というある種の反映原理によって特徴づけられることが知られている．
またこの結果として，Pi^1_1-CA_0はPi^1_2文で公理化することができず，したがってPi^1_1-CA_0のPi^1_2帰結全体Thm_{Pi^1_2}(Pi^1_1-CA_0)はPi^1_1-CA_0の真の部分理論となることがわかる．[SuY]ではThm_{Pi^1_2}(Pi^1_1-CA_0)と対応するbeta_1-model反映原理の弱化が導入された．
また，beta_1-model反映原理の自然な一般化としてbeta_n-model反映原理を考えることもでき，これはΣ^1_n強従属選択公理とACA_0上同値になることが知られている．Σ^1_n強従属選択公理はPi^1_n-CA_0はPi^1_n-CA_0のPi^1_4保存拡大となっていて，両者は極めて近い公理系であるといえる．[ASY]では[SuY]と類似の方法でbeta_n-model反映原理の弱化を考えることにより，e < n + 1に対して，ACA_0 + Σ^1_n強従属選択公理のPi^1_{e}帰結，Sigma^1_{e}帰結，Bool(Pi^1_{e})帰結などの特徴づけを与えた．またこの結果として，保存性の成り立つ範囲でPi^1_n-CA_0のPi^1_{e}帰結，Sigma^1_{e}帰結，Bool(Pi^1_{e})帰結などの特徴づけを与えた．
本講演では上記の結果について紹介する．
[SuY] Suzuki, Yudai, and Keita Yokoyama. “On the $\Pi^ 1_2 $ consequences of $\Pi^ 1_1 $-$\mathsf {CA} _0$.” arXiv preprint arXiv:2402.07136 (2024).
[ASY] Aguilera, Juan P., Yudai Suzuki, and Keita Yokoyama. “On some subtheories of strong dependent choice.” arXiv preprint arXiv:2411.17415 (2024).
Speaker: 市川航士郎（東京理科大）
Title: Modular Ordinal Analysis via Iterated ω-Model Reflection and Dilators
Abstract: Modular ordinal analysis, presented by Dieter Probst in his habilitationsschrift [1], aims to compute proof-theoretic invariants of a theory by decomposing the theory into some modules. It enables us to compute the invariants of a theory from that of a weaker one.
Recently, Fedor Pakhomov and James Walsh [2, 3] proposed a new approach to compute invariants by iterated reflection principles. We combine these two results by iteration of reflection principles along Girard's dilators and give simple calculation methods to compute the invariants of theories in the hierarchies of \(\Pi^1_n\) \(\omega\)-model reflection over some base theory. Particularly when the base theory is \(\mathsf{ACA}_0\), this hierarchy encompasses intriguing theories such as \(\mathsf{ATR}_0\), \(\Pi^1_n\text{-}\mathsf{BI}_0\), Towsner's \(Σ^0_n\text{-}\mathsf{LPP}_0\) and so on, offering the potential for various applications.
In this talk, we introduce these results with several examples of theories.
[1] Dieter Probst, A modular ordinal analysis of metapredicative subsystems of second order arithmetic. Habilitationsschrift, Institut für Informatik Universität Bern, 2017
[2] Fedor Pakhomov and James Walsh. Reflection ranks and ordinal analysis. The Journal of Symbolic Logic, 86(4):1350–1384, 2021.
[3] Fedor Pakhomov and J. Walsh. Reducing \(\omega\)-model reflection to iterated syntactic reflection. Journal of Mathematical Logic 23.02, 2023.
Speaker: 関隆宏（新潟大）
Title: 公理KとSを持つ部分構造論理における構造規則の導出可能性
Abstract: 古典論理や直観主義論理のHilbert流の形式化における公理としてKとSが採用され，基本的な構造に関する規則はすべて導出される。本講演では，結合則も交換則も持たない部分構造論理に公理KとSを加えた論理においても，基本的な構造に関する規則がすべて導出されるかについて論じる。
Speaker: 安部達也（千葉工大）
Title: タイムスタンプ意味論と Owicki--Gries 論理
Abstract: Floyd--Hoare論理に非干渉性条件を追加して並行プログラムの検査を可能にしたOwicki--Gries論理は弱メモリモデルに対して健全でない。本発表では、Owicki--Gries論理の非干渉性条件を修正することによって、ストア命令の遅延が起こり得る弱メモリモデルを表すタイムスタンプ意味論に健全なプログラム論理を与える。一見非干渉性条件を修正するだけでは不十分で代入文の公理の変更も必要であるように思えたり、また、なにか修正を加えたとしても非干渉性条件を課すとタイムスタンプ意味論に対して十分な証明力を有する論理を与えることは本質的にできないように思えたりもするのだが、これらを克服するにあたって今回おこなった工夫を報告する。本発表で扱う内容は原始的なものばかりで、Floyd--Hoare論理の健全性の扱いに慣れていること以外に前提知識を仮定しない。
Speaker: 西村祐輝（東京科学大）
Title: Tableau Calculus for Strict Partial Order
Abstract: Hybrid logic にはモデルの非反射性に対応する公理が存在する。そのため、非反射的かつ推移的な二項関係、すなわち狭義半順序を表現することが可能である。本発表では、到達関係が狭義半順序をなすモデルについてこれと対応するような hybrid logic のタブロー計算を提案し、その完全性を示す。また、タブローの生成が有限時間内で終わる、という性質（停止性）も示す。非反射性と推移性に対応する公理を加えた hybrid logic は有限フレーム性をもたないことが知られているが、本発表にて紹介するタブロー計算を用いることで、論理式の決定手続きを与えることができる。