(Independence) \(\mathbf{PA} + \varphi\) が無矛盾なら \(\rho(\ulcorner \varphi \urcorner)\) は \(\mathbf{PA} + \varphi\) から証明も反証もできない．
(Extensionality) \(\mathbf{PA} \vdash \varphi \leftrightarrow \psi\) ならば，\(\mathbf{PA} \vdash \rho(\ulcorner \varphi \urcorner) \leftrightarrow \rho(\ulcorner \psi \urcorner)\) .

この問題は，文全体を \(\mathbf{PA}\) 上の同値性で割ったときに，各同値類 \([\varphi]\) に対して独立な同値類 \(\rho([\varphi]) : = [\rho(\ulcorner \varphi \urcorner)]\) を well-defined に与える \(\rho(x)\) の存在を問うており，不完全性定理現象として面白い．

しかし，Visser [2] はそもそもこの2条件を満たす \(\rho(x)\) が存在しないことを証明した．一方，(Extensionality) を次の (Conditional Extensionality) に弱めると，存在することを証明した．

(Conditional Extensionality) \(\mathbf{PA} \vdash \varphi \leftrightarrow \psi\) ならば，\(\mathbf{PA} + \varphi \vdash \rho(\ulcorner \varphi \urcorner) \leftrightarrow \rho(\ulcorner \psi \urcorner)\) .

その上で，Hamkins の問題に答えるには (Extensionality) と (Conditional Extensionality) の中間にある (Consistent Extensionality) を満たすものの存在が示せるか，という問いに答える必要があることを述べた．

(Consistent Extensionality) \(\mathbf{PA} + \varphi\) が無矛盾かつ \(\mathbf{PA} \vdash \varphi \leftrightarrow \psi\) ならば，\(\mathbf{PA} \vdash \rho(\ulcorner \varphi \urcorner) \leftrightarrow \rho(\ulcorner \psi \urcorner)\) .

今回はその問題を解いた．その証明を紹介する．

参考文献：
[1] Joel David Hamkins. Nonlinearity and illfoundedness in the hierarchy of large cardinal consistency strength. Monatshefte für Mathematik, published online 2025.
[2] Albert Visser, On a Question of Hamkins', 2025. arXiv:2502.09109.

参考文献:
[1] H. Kogure and T. Kurahashi, A variety of partially conservative sentences, arXiv:2412.08208.
[2] H. Kogure and T. Kurahashi, Doubly partially conservative sentences, arXiv:2503.12373.

参考文献:
・Richard E. Ladner. The Computational Complexity of Provability in Systems of Modal Propositional Logic. SIAM Journal on Computing, 6(3):467–480, September 1977.
・Edith Spaan. Complexity of Modal Logics. Doctoral, University of Amsterdam, February 2016.

参考文献:
[1] Litak and Visser. Lewis meets Brouwer: constructive strict implication. Indagationes Mathematicae, 29(1):36–90, 2018.
[2] Iemhoff. Preservativity logic: An analogue of interpretability logic for constructive theories. Mathematical Logic Quarterly, 49(3):230–249, 2003.

- Hybrid Logic の Kripke 意味論
- Hilbert 流公理系とその健全性・完全性
- Pure Completeness

Hybrid Logic には，どのようなオペレーターを採用するかによってさまざまな変種がある．今回はもっとも簡単な，充足演算子 @ のみを採用したものを扱う．

論文 [1] において \(\mathbf{S4}\) の無矛盾正規拡大論理のうち，高さが有限のあるクリプキモデルのクラスによって特徴づけられる論理に対する LIP の分析を行った． CIP をもつそのような論理はちょうど18個であり（Maksimova 1979），更にそのうちの4個が LIP を持ち，4個が LIP を持たないことが既に知られていた（Maksimova 1982 [3], Fitting 1983, Maksimova 2014 [4]）． 今回の分析の結果として，残りの10個の論理について LIP の成立・不成立を明らかにできた（7個が成立，3個が不成立）． 特に \(\mathbf{LV}\) の modal companion である \(\mathbf{GV}\) が LIP を持つことを証明できたため，系として \(\mathbf{LV}\) が LIP を持つことが得られる． したがって，中間命題論理に対する LIP の分析が完了した． 本発表では上記の結果の概要を紹介する．適宜，様々な論理の補間性の状況を参照されたい．

参考文献:
[1] Kurahashi, T. (2024). Lyndon interpolation property for extensions of \(\mathbf{S4}\) and intermediate propositional logics. arXiv:2407.00505.
[2] Kuznets, R. and Lellmann, B. (2018). Interpolation for intermediate logics via hyper- and linear nested sequents. In Advances in modal logic. Vol. 12, 473–492.
[3] Maksimova, L. L. (1982). The Lyndon interpolation theorem in modal logics. Trudy Instituta Matematiki Sibirskogo Otdeleniya AN SSSR, 2, 45–55.
[4] Maksimova, L. L. (2014). The Lyndon property and uniform interpolation over the Grzegorczyk logic. Siberian Mathematical Journal, 55(1), 118–124.

参考文献：
[1] Fitting et al. The pure logic of necessitation. Journal of Logic and Computation, 2(3):349-373, 1992.
[2] Kurahashi. The provability logic of all provability predicates. Journal of Logic and Computation, 34(6):1108-1135, 2024.
[3] Kurahashi & Sato. The finite frame property of some extensions of the pure logic of necessitation. Studia Logica, to appear.

予定では三部構成で進める．
1. そもそも定理証明支援系とはどういうものなのか．
2. 簡単な例を用いて実際に Lean のコードなどを見てみる．
3. 現状の論理学の形式化の進捗と展望（様相論理と算術/不完全性定理周りについて）．

本発表では， \(\mathbf{N}\) に \(\Box^n p \to \Box^m p\) という形の公理と，\(\mathrm{Ros}^\Box\) として知られる規則を追加した論理 \(\mathbf{N^+A}_{m,n}\) に対して，Craig 補間性をはじめとする各種補間定理の証明を行う．特に，\(\mathbf{K4} = \mathbf{K} + \Box p \to \Box \Box p\) が一様補間性 (UIP) を持たないのに対して， \(\mathbf{N4} = \mathbf{N} + \Box p \to \Box \Box p\) が UIP を持っていることを示す．

今回はこのスマリヤンの枠組みにおける各定理と, 記号ルール, モデルとの関係性を紐解き, より深く繊細な立場から定理を理解することを目指し, 性質間の同値性を検証し, 加えて各記号ルールが定理の各々にどのように寄与しているのかについて, 記号ルールの一部を除外して構成した反例モデルの考察から検討した.
参考文献:
・Smullyan, R.M.Truth and Provability, The Mathematical Intelligencer, vol.35, no.1, pp.21--24, 2013.

参考文献：
L. Beklemishev, On the Craig interpolation and the fixed point property for \(\mathbf{GLP}\), 2007.
L. Beklemishev, Kripke semantics for provability logic \(\mathbf{GLP}\), 2010.

参考文献:
L. Beklemishev and D. Shamkanov, Some abstract versions of Gödel's second incompleteness theorem based on non-classical logics, 2016.

参考文献:
Borga, On some proof theoretical properties of the modal logic GL. Studia Logica 42, 453--459, 1983.

・GLP における「正規形」を定義し，GLP において，任意の閉論理式は正規形に同値変形できる．
・新たに，論理 GLP_0 を導入し，閉論理式に関して GLP が GLP_0 の保存拡大となる．

参考文献:
Konstantin N Ignatiev. The closed fragment of Dzhaparidze’s polymodal logic and the logic of \(\Sigma_1\)-conservativity. ITLI Prepublication Series for Mathematical logic and Foundation, X-92-02, University of Amsterdam, 1992.

参考文献:
・Pakhomov, Fedor N., Solovay's completeness without fixed points, WoLLIC 2017: Logic, Language, Information, and Computation, 2017.

参考文献:
・S. V. Goryachev, Arithmetic with a local reflection principle for Rosser provability formulas, Matematicheskie Zametki, 1989.
・T. Kurahashi, Henkin sentences and local reflection principles for Rosser provability, APAL, 2016.

Visser は解釈可能性論理 \(\mathbf{IL}\) に対する SVF に関する完全性を示している．\(\mathbf{IL^-(J2_+, J5)}\) に対する SVF に関する完全性は，Visser の手法とほぼ同様の方法で証明できることを紹介する．

定理 (Abashide-Blass)
順序数 \(\alpha \geq \omega^\omega\) 上の順序位相 \(\tau\) について \((\alpha, \tau)\) の論理がちょうど \(\mathbf{GL}\) である．

参考文献：Blass - Infinitary combinatorics and modal logic (1990)