講演一覧
Leonardo Pacheco (東北大学理学研究科)
タイトル：The mu-calculus collapses to modal logic over frames of IS5 [slides]
アブストラクト：Abstract: The mu-calculus is obtained by adding fixed-point operators to modal logic. Alberucci and Facchini showed that every mu-formula is equivalent to some modal formula over frames of S5. The modal logic IS5 is an intuitionistic variation of S5, first defined by Prior in 1957. We show that, with slight changes, Alberucci and Facchini's proof also works in frames of IS5. That is, every mu-formula is equivalent to some modal formula over frames of IS5.倉橋太志 (神戸大学システム情報学研究科)
タイトル：R と無矛盾な理論の不完全性と決定不可能性 [slides]
アブストラクト：Tarski, Mostowski and Robinson (1953) の算術 R は本質的決定不可能性である．特にR の拡大有限理論である Robinson の算術 Q の本質的決定不可能性から，Q と無矛盾な理論の決定不可能性が導ける．他方，Rと無矛盾な理論の決定不可能性は R が有限公理化可能ではないことから非自明である．このことはCobham によって証明されたらしいが，Cobham による証明は残されていない．Vaught(1962) は Cobham の定理を直ちに導く次の主張を述べているが，証明を残していない：Rと無矛盾な c.e. 理論は，ある R を含む有限理論と無矛盾となる．今回はこの Vaughtの定理の証明を再発見し，更に拡張することを試みる．鈴木悠大 (東北大学理学研究科)
タイトル：Pseudo-hierarchy method in Weihrauch degrees [slides]間庭彬仁 (東京工業大学)
タイトル：脱出のメカニズムのための証明体系
アブストラクト：Curry–Howard 対応において，大域脱出のメカニズムを備える計算体系と古典論理が対応関係にあることはよく知られている．一方で，適切な制約を課すことで直観主義論理と対応のを考えることも可能であり，いくつかの体系が知られている．本発表ではこのような直観主義的な脱出のメカニズムの実現のために nested sequent のアイディアを用いることを考える．西村祐輝 (東京工業大学情報理工学院)
タイトル：Kripke frameの性質とTableauの停止性 [slides]
アブストラクト：Tableau calculusの性質として、停止性(termination)というものがある。これは任意のtableau（証明木）は有限長のbranchしか持たない、すなわち計算が有限で停止する、というものである。本発表では、hybrid logicのtableau calculusを紹介し、その停止性を示す。さらに、frameの反射性や推移性に対応するtableau calculusで、停止性をもつものを紹介する。対称性に対応するtableau calculusの停止性は未解決であるため、解決に向かうだろう展望を述べる。木村大輔 (東邦大学)
タイトル：含意と余含意をもつ双側面的自然演繹に対応するラムダ計算
アブストラクト：双側面的論理は，主張に対する是認と否認の協調によりその意味を得る双側面的主義に基づく論理である．本発表では，含意と余含意をもつ双側面的論理の自然演繹体系にカリー・ハワード対応するラムダ計算 λconf およびその値呼び計算体系を提案する．これは古典シーケント計算に対応する計算体系として知られた双対計算の部分体系と同型であり，従って合理的な計算的意味をもつ．また，λconf を拡張することにより限定継続演算子の挙動が模倣できる．本研究は千葉工大の安部達也氏との共同研究である．
鹿島亮 (東京工業大学)
タイトル：証明可能性論理GLSの意味論とカット除去 [slides]
アブストラクト：The quasi-normal modal logic GLS is a provability logic formalizing the arithmetical truth. Kushida (2020) gave a sequent calculus for GLS and proved the cut-elimination theorem. We introduce semantical characterizations of GLS and give a semantical proof of the cut-elimination theorem. These characterizations can be generalized to other quasi-normal modal logics. （これは加藤裕との共同研究である。）木原貴行 (名古屋大学)
タイトル：計算可能数学のトポスとLawvere-Tierney位相織田幸弘 (総合研究大学院大学複合科学研究科情報学専攻)
タイトル：循環証明体系とプレスバーガー算術 [slides]
アブストラクト：循環証明体系は証明図の形がサイクル付きの有限木になっている証
明体系である．いくつかの循環証明体系は無限降下法の形式化と見ることができる．そのため，帰納法を含む証明の代替手段とみなすこともできる．一般に，帰納法を含む通常の証明体系で証明できるシークエントは対応する循環証明体系で証明ができる．しかし，その逆は一般に明らかではない．たとえば，帰納的定義付き一階述語論理の循環証明体系では証明できるが、通常の証明体系では証明できないシークエントの存在が知られている．述語論理において，帰納法を含む通常の証明体系と循環証明体系の同等性が知られている例はペアノ算術を含む例であった．プレスバーガー算術はペアノ算術から乗算を取り除いた体系である．プレスバーガー算術は完全な理論としても知られている．本講演では，プレスバーガー算術の循環証明体系を定義し，その証明能力がプレスバーガー算術と同等であることを示す．同等性の証明にはプレスバーガー算術の完全性が主要な役割を果たす．
森田泰聖 (東邦大学大学院) [slides]
タイトル：時相論理CTLの証明論的分析のためのカット除去定理と拡張した部分論理式性にむけてThibaut Kouptchinsky
タイトル：Determinacy in and out second order arithmetic : An introduction to the proof theoretic strength of the determinacy scale五十里大将 (東北大学理学研究科) [slides]
タイトル：Basis theorems and conservation results around RT^2_2黒田 覚(群馬県立女子大学)
タイトル：Linear algebra in bounded arithmetic II只木孝太郎 (中部大学工学部情報工学科)
タイトル：An effectivization of the law of large numbers for algorithmically random sequences and its absolute speed limit of convergence
アブストラクト：The law of large numbers is one of the fundamental properties which algorithmically random infinite sequences ought to satisfy. In this talk, we show that the law of large numbers can be effectivized for an arbitrary Schnorr random infinite sequence, with respect to an arbitrary computable Bernoulli measure. Moreover, we show that an absolute speed limit of convergence in this effectivization exists and it equals 2 in a certain sense. In the talk, we also provide the corresponding effectivization of the strong law of large numbers in the context of the conventional probability theory, with respect to an arbitrary probability measure, not necessarily computable.関隆宏 (新潟大学経営戦略本部評価センター)
タイトル：公理Sの族に対応する推論規則
アブストラクト：部分構造論理で含意公理Sを考える場合，いくつかの変種が考えられるが，これらに対応するGentzen流の推論規則について論じる。