日程：２０２３年９月９日（土）～１０日（日）

※翌日９月１１日から、東京にて数学基礎論サマースクールが開催されます。

場所：国立オリンピック記念青少年総合センター（東京都渋谷区）センター棟 405号室

※宿泊希望の方は、オリンピックセンター内宿泊施設にて宿泊できます（4000円程度の実費徴収）。

参加費：無料（懇親会に参加される方のみ懇親会費を別途徴収）

旅費支援：遠方からの参加者には予算の範囲内で旅費支援が可能です

宿泊費支援：学部生については予算の範囲内で経済支援が可能です 

幹事

• 渡部耀介（名古屋大学）

• 高木翼（JAIST）

• 西村祐輝（東京工業大学）

※本研究集会は、JST次世代研究者挑戦的研究プログラム JPMJSP2106 の支援を受けています。

参加申し込みの締め切りについて

• 参加希望者（現地参加またはオンライン参加）：９月７日まで

• 宿泊希望者：８月９日まで

• 発表希望者（現地発表またはオンライン発表）：８月２４日まで

• 懇親会参加希望者：８月２４日まで

会場名：国立オリンピック記念青少年総合センター（センター棟 405号室）

住所：東京都渋谷区代々木神園町3-1 

最寄り駅は小田急線の参宮橋駅です。

pdf 版はこちら（最終更新：2023-09-06 20:30）

9/9

9:00 開場

10:00-10:10 開会式

座長：高木翼（JAIST）

10:10-10:50 福田 陽介（京都橘大学工学部情報工学科）

10:50-11:30 谷口 雅弥（理化学研究所）

昼休憩

座長：渡部耀介（名古屋大学）

13:00-13:15 長 連成（京都大学人間・環境学研究科）[スライド]

13:15-13:30 荒武 永史（京都大学数理解析研究所）[スライド]

13:30-13:45 後藤 達哉（神戸大学）[スライド]

13:45-14:00 五十里 大将（東北大学理学研究科）

座長：渡部耀介（名古屋大学）

14:15-14:55 橋本 航気（名古屋大学情報学研究科）

14:55-15:35 鈴木 悠大（東北大学理学研究科）

15:35-16:15 Leonard Pacheco (Technische Universität Wien)

16:30-17:30 招待講演：東条 敏（亜細亜大学）[スライド]

タイトル：なぜ嘘はバレるか？ 

概要：様相論理はAlethic/Epistemic-Doxastic/Deontic/Temporal Logicなど，多様の解釈ができるフィージビリティの高い枠組みである．またSTIT(see to it that)など新しいオペレータの話題も豊富である．特にクリプケ意味論を用いては，人間の知識・信念のモデル化に応用でき，動的認識論理(Dynamic Epistemic Logic)は信念修正に関わるメカニズムを形式化できる．特にエージェント間通信を含む体系では，エージェント間通信による信念修正，エージェント群によるグループ知識(共通知識や集合知識)など多彩な話題が含まれる．このうち特に相互知識(mutual knowledge)では，信念修正 よって相手の知識状態が変わったにも関わらず古い信念を持ち続けたり，相手が知らないことを誤って認識する問題が生ずる．本講演では，こうした相互知識の問題・アウェアネスの問題・忘却の例などを紹介しながら，動的認識論理の有用性と限界について紹介する．また，講演後半には可能世界間の距離の概念を紹介し，近傍論理・インテリア意味論が近年の確率を伴う機械学習とも相性がよいことを示唆する．

19:00 懇親会（懇親会会場：都夏）

・9/10

9:00 開場

座長：西村祐輝（東京工業大学）

9:30-10:10 森岡 蒼（東京工業大学情報理工学院）

10:10-10:50 劉 偲卓 （北海道大学大学院文学院）

昼休憩

座長：高木翼（JAIST）

12:20-12:35 宇田津 孝介 （JAIST）

12:35-12:50 佐藤 遼一（静岡大学）

12:50-13:05 奥田 壮一郎（名古屋大学情報学研究科）

座長：後藤 達哉（神戸大学）

13:25-14:05 山添 隆志（神戸大学）[スライド]

14:05-14:45 市川 航士郎（東京理科大学）

15:00-16:00 招待講演：鹿島 亮（東京工業大学）

タイトル：様相論理の入れ子シークエント計算について

概要：入れ子シークエント計算(nested sequent calculus)とは入れ子になったシークエントを扱う証明体系の総称である．これは入れ子構造がクリプキモデルの世界の構造を反映しており，クリプキモデルで特徴付けられる論理に対する完全性を自然に示すことができる．本講演では入れ子シークエント計算を様相命題論理KとS4を例にして説明する．特に以下に列挙した比較を論じる．

・普通のシークエント計算の完全性証明と入れ子シークエント計算の完全性証明．

・意味論的カット除去と構文論的カット除去．

・入れ子シークエント計算の構文論的カット除去と古典１階述語論理の構文論的カット除去．

・シークエントを論理式の集合で定めるか多重集合で定めるか．

・入れ子シークエント計算とラベル付きシークエント計算．

資料配布：９月８日（金）正午までにこちらをご覧ください．

16:00-16:10 閉会式

9/9

福田 陽介（京都橘大学工学部情報工学科）

タイトル：証明論的な〈意味〉から観る型システムのメタ性質について

概要：構成的証明のための型理論や関数型プログラミング言語の型システムを，理論の構築者の観点から考えると，その理論の〈正しさ〉は正規化定理(Normalization Theorem)や主部簡約定理(Subject Reduction Theorem)，型健全性(Type Soundness)などによって保証されることがある．しかし，体系定義の実践においては「帰納法が回るように定義・体系を考える」といった職人技が（少なくとも発表者の経験上は）しばしば必要となる．本発表では，型システムの〈正しさ〉について理論的に考察するため，証明の理論（General Proof Theory, Structural Proof Theory, Proof-Theoretic Semanticsなど）や論理の哲学の観点から型システムのメタ性質について議論する．なお，本発表で議論の対象とするのは，基本的には直観主義命題論理（＋いくつかの様相）程度の限られた体系に関係する型システムであることを予めお断りしておく．

谷口 雅弥（理化学研究所）

タイトル：組合せ範疇文法の計算論

概要：我々の話すことば(自然言語)は主語・述語のように構造を内包している。

この構造の複雑さは計算可能性理論によって分類できる。

とくに自然言語は線形拘束オートマトン(LBA)で受理判定できると目されている。

LBAは決定可能な手続きが存在することが知られている。

自然言語の文法とその構文解析器も決定可能であることが期待される。

本発表では自然言語の構文解析に用いられている組合せ範疇文法を対象にする。

これは組み合せ論理に基づいた文法である。

この文法の構文解析について決定可能な手続きは知られていなかった。

我々は証明論の観点からことばの構造を分析し決定可能な手続きを部分的に明かにした[Taniguchi 2022]。

本発表では決定可能な手続きの詳細とその後の成果について紹介する。

[Taniguchi 2022]: Masaya Taniguchi, "Decidable Algorithm for CG with Type-raising", 4th The Proof Society Autumn School and Workshop, 2022 

長 連成（京都大学人間・環境学研究科）

タイトル：部分和問題の形式証明のサイズ

概要：本研究ではNP完全問題として有名な部分和問題の形式証明のサイズの下限を調べる。

シーケント計算と環論をもとに形式証明を定め、証明に含まれる文字列の長さでサイズを定義する。

入力サイズに対して超多項式的な証明を持つことが分かった。 

荒武 永史（京都大学数理解析研究所）

タイトル：層表現を持つモデル全体のクラスについて

概要：モデル理論や普遍代数学においては、構造のクラスについて「部分構造や直積などの構成で閉じるかどうか」と「良いaxiomatizationを持つかどうか」という2つの性質の関係性が調べられている（e.g. Birkhoff's variety theorem）。本発表では、「T-モデルの層の大域切断全体として表されるモデル」のクラスについて、これらの問題を考察することのモチベーションと現段階で得られている部分的結果を紹介する。 

後藤 達哉（神戸大学）

タイトル：基数不変量のゲーム理論的変種

概要：基数不変量は実数の集合論で重要な研究対象であり、無限ゲームも集合論において大変重要な役割を果たす。我々はよく知られた基数不変量のゲーム理論的変種を考えることにより、この二つの分野を接続する。今回は特にsplitting gameと呼ばれるゲームに焦点を当てて発表する。

これはJorge Antonio Cruz Chapitalおよび林佑亮との共同研究である。 

五十里 大将（東北大学理学研究科）

タイトル：$\Pi^1_1$-conservation between $RT^2$ and $B\Sigma^0_3$

概要：種々のラムゼイ定理は，逆数学の文脈でその強さがよく研究されている．本公演では Slaman, Yokoyama [1] の結果($RT^2$ が $B\Sigma^0_3$ の $\Pi^1_1$-保存拡大となること)の新証明を与える．また，基底定理に基づいた議論を行うことで各種保存拡大性に新たな観点を与える．

なお，本公演の内容は横山啓太氏(東北大学教授)との共同研究である．

[1] T. A Slaman and K. Yokoyama, The strength of Ramsey’s theorem for pairs and arbitrarily many colors, The Journal of Symbolic Logic 83 (2018), no. 4, 1610–1617 

橋本 航気（名古屋大学情報学研究科）

タイトル：擬超算術的解析

概要：二階算術といえばBig fiveと総称される$\mathsf{RCA}_0,\mathsf{WKL}_0,\mathsf{ACA}_0,\mathsf{ATR}_0,\Pi^1_1{\mathchar`-}\mathsf{CA}_0$の理論群が古典的逆数学の文脈で有名だが，それとは別に，独自の閉性を持った超算術的解析（hyperarithmetic analysis，以下$\mathcal{HA}$と書く）という理論群が存在する．発表者はこの$\mathcal{HA}$の概形を把握するために，$\mathcal{HA}$を近似する理論群を導入しその性質を調べた．本発表ではこの取り組みの経過と合わせて，これまでに考えついた問題を紹介する． 

鈴木 悠大（東北大学理学研究科）

タイトル：$\omega$モデル反映のヴァリエーションについて

概要：$T$を二階算術の理論とする．このとき，``任意の集合$X$に対して，$X$を含む$T$の$\omega$モデルが存在する"という主張を$T$の$\omega$モデル反映と呼ぶ．

$\mathsf{ACA}_0^+,\Sigma^1_1\mathchar`-\mathsf{DC}_0,\Pi^1_1\mathchar`-\mathsf{CA}_0$など，$\omega$モデル反映やその変種と密接に関わる理論が存在していることからもわかる通り，$\omega$モデル反映は二階算術の諸理論を分析する上で有用な道具である．

本講演では，$\omega$モデル反映の変種をいくつか導入し，それぞれの性質を見る．特に，これらを用いて，$\mathsf{ATR}_0$より複雑な$\Pi^1_2$理論の分析を行う．

なお，本講演は東北大学の横山啓太氏との共同研究に基づく． 

Leonard Pacheco (Technische Universität Wien)

タイトル：ωオートマタの逆数学

概要：I’ll review some recent results on the reverse mathematics of automata on infinite words. This is still a new subarea of reverse mathematics, but it already touches very weak and very strong subsystems of second order arithmetic. I also comment on some of my recent research on the reverse mathematics of the Wagner hierarchy. 

9/10

森岡 蒼（東京工業大学情報理工学院）

タイトル：証明可能性論理Dのモデルの拡張

概要：証明可能性論理Dは完全性やカット除去など、基本的な性質が成り立つことがわかっている。その手法を応用してDのモデルを拡張した体系においても完全性が成り立つことを示す。

劉 偲卓 （リュウ サイタク）（北海道大学大学院文学院）

タイトル：Non-labelled Sequent Calculi of Public Announcement Expansions of K45 and S5

概要：This paper proposes non-labelled sequent calculi, G(K45PAL) and G(S5PAL), for the public announcement expansions of modal logics K45 and S5. We transform each of the recursion axioms of PAL into left and right rules for the sequent calculi. For G(K45PAL), the cut elimination theorem is shown using the complexity measure introduced by van Ditmarsch et al. (2007). This measure was originally employed to establish semantic completeness via recursion axioms. While the cut elimination theorem fails in G(S5PAL), we adopt Takano's strategy (1992) to establish that the cut formula in G(S5PAL) can be restricted to the set of suitably extended subformulas (i.e., closure) of the conclusion of the cut rule. 

宇田津 孝介（JAIST）

タイトル：Awareness Logic

概要：Awareness Logicとは何か、Awarenessの条件・定義にはどういった物があるのかを主に話して、最後にそれに関するどんな研究をしているかについて触れます。 

佐藤 遼一（静岡大学）

タイトル：量子論理での集合論

概要：竹内外史の導入した量子集合論では、ブール代数ではなくオーソモジュラー束に値をとるモデルが構成される。そこではどのような公理が成立するかを見る。 

奥田 壮一郎（名古屋大学情報学研究科）

タイトル：ロジックで圏論しよう！

概要：内部論理わちゃわちゃしてたら元の圏のことがわかった！な話って意外と聞かないよね～。 

山添 隆志（神戸大学）

タイトル：Cichoń's maximumとevasion number

概要：「実数全体を覆うために必要なLebesgue測度0の集合の個数」のように、連続体濃度以下の定義可能な非可算濃度を(実数上の)基数不変量と呼び、複数の基数不変量が異なる値を取ることの無矛盾性を証明することを基数不変量の分離と呼ぶ。基数不変量を分離する際には、連続体仮説の否定の無矛盾性を示すためにCohenが開発した強制法の手法が主に用いられ、複数の基数不変量が異なる値を取るような集合論のモデルを構成することでその無矛盾性を示すという原理になっている。代表的な基数不変量をまとめた図にCichoń's diagramがあり、図にあるすべての基数不変量を可能な限り分離したモデルであるCichoń's maximumが2022年に構成された。発表者の研究目的はCichoń's maximumに別の基数不変量を追加することであり、そのために古典的な基数不変量の一つであるevasion numberに注目した。そして発表者はevasion numberとそのヴァリアントである基数不変量がCichoń's maximumに追加できることを示した。本講演ではその概要について解説する。 

市川 航士郎（東京理科大学）

タイトル：（未定）

概要：（未定）