第39回 記号論理と情報科学 研究集会

開催要領

日時：2022年9月20日(火)〜9月21日(水)

開催形式：対面開催＋オンライン

会場：東邦大学習志野キャンパス (対面) ，Zoom (オンライン)

参加費：無料

プログラム

(オンラインと注釈がついていないものは現地発表です)

9月20日(火)

• 13:00〜13:10 オープニング・諸連絡

• 13:10〜15:10 セッション1 (座長：木村大輔)

• 13:10〜13:50 西村祐輝「Index frame と 2次元 Fusion の完全性」

• 13:50〜14:30 織田幸弘「プレスバーガー算術の循環証明体系」(オンライン)

• 14:30〜15:10 中澤巧爾「不動点演算子を持つ命題論理の循環証明体系」

• 15:10〜15:30 休憩

• 15:30〜17:30 セッション2 (座長：津久浦健太)

  • 15:30〜16:10 鈴木悠大「カントール空間の単調作用素の不動点定理と Weihrauch 次数」

  • 16:10〜16:50 只木孝太郎「An effectivization of the law of large numbers for an arbitrary Schnorr random sequence and its absolute speed limit of convergence」(オンライン)

  • 16:50〜17:30 津久浦健太「強制法の代数的側面」(座長代理：木村)

9月21日(水)

• 10:00〜10:10 諸連絡

• 10:10〜12:10 セッション3 (座長：中澤巧爾)

• 10:10〜10:50 石原豪人「新世界教育学革命」(オンライン)

• 10:50〜11:30 佐々木克巳「非直接推論の分類について」(オンライン)

• 11:30〜12:10 福田陽介「Modal linear decoration の計算的解釈について」(オンライン)

• 12:10〜14:00 昼休憩

• 14:00〜15:20 セッション4 (座長：松田直祐)

  • 14:00〜14:40 山形頼之「On proving consistency of equational theories in Bounded Arithmetic」(オンライン)

  • 14:40〜15:20 松田直祐「直観主義論理とBool 関数の完全性」

講演タイトル・概要一覧 (順不同)

• 佐々木克巳 (南山大学) 「非直接推論の分類について」
  概要：自然演繹の体系 NK における，(∨除去規則) や (→導入規則) のような一時的な仮定をもつ推論は，(∧導入規則) や (→除去規則) のような一時的な仮定をもたない推論と比べ，難しいと捉えられることがある．ここでは，前者を非直接推論，後者を直接推論と呼ぶことにする．これらを区別するシークエント体系は，構造に関する規則だけを推論規則とする形で構成できることが知られている．本講演では，そのシークエント体系を用いて，非直接推論を分類した結果を示す．

• 福田陽介 (京都橘大学) 「Modal linear decoration の計算的解釈について」

概要：直観主義論理や古典論理から線形論理への埋め込みには Girard 変換が有名であるが，その他の変換として，変換後の線形論理の証明図から変換前の証明図を一意に復元できる Linear Decoration (cf. [1, 2]) と呼ばれる手法が知られている．本発表では， Schellinx [3] により提案された Linear Decoration の古典様相論理 S4 に対する拡張について，その計算的解釈を Curien & Herbelin [4] の結果を基に議論する．

[1] V. Danos, J.-B. Joinet, and H. Schellinx. LKQ and LKT: Sequent calculi for second order logic based upon dual linear decompositions of classical implication. Advances in Linear Logic, pp. 211-224, Cambridge University Press, 1995.

[2] V. Danos, J.-B. Joinet, and H. Schellinx. A New Deconstructive Logic: Linear Logic. Journal of Symbolic Logic, Volume 62, Number 3, 1997.

[3] H. Schellinx. A Linear Approach to Modal Proof Theory. Proof Theory of Modal Logic, pp. 33-43, Springer, 1996.

[4] P.-L. Curien and H. Herbelin. The Duality of Computation. In Proceedings of International Conference on Functional Programming (ICFP) 2000, pp. 233-243, 2000.

• 石原豪人 「新世界教育学革命」
  概要：2010 年代より京都大学で松下・西岡・石原を中心に平和的科学特に数学を用いた教育学が起こりその一般論は教育学の古典論として 2022 年に概ね完成した (事実)．今回は古典論に加えて個別対応を考慮した新世界教育学を議論する．新世界教育学の最重要問題の 1 つは組み合わせ論的に増える良質データの記録の問題である (事実)．今回それを foundation of mathematics (2022 年完成) によって事実上完璧に乗り越える方法を議論する．また京都大学総合人間学部にも認められた「言語の発音臨界期問題」の解を今回数学系の方々に初めて紹介する．

• 松田直祐 (新潟工科大学)「直観主義論理とBool 関数の完全性」

概要：Bool 関数の集合Fが完全であるとは，任意の Bool 関数に対しそれと (古典的意味論の下で) 同値な論理式を F の関数を組み合わせて作ることができる時をいう．例えば，{NOT,AND} や {NAND} といった Bool 関数の集合はいずれも完全である．F が 完全であるための必要十分条件は Post [1] によって与えられている．本講演では，Roussezu [2] によって与えられた論理式の Kripke 流意味論を用いて 同様の問題を考える．

[1] Post, E. L., The Two-Valued Iterative Systems of Mathematical Logic. (AM-5), Volume 5, Princeton University Press, 1942.

[2] Rousseau, G., “Sequents in many valued logic II,” Fundamenta Mathematicae, vol. 67 (1970), pp. 125–131.

• 織田幸弘 (総合研究大学院大学) 「プレスバーガー算術の循環証明体系」

概要：循環証明体系 (cyclic proof system) とは，帰納法を含んだ証明体系において，帰納法の導出則を別の導出則に置き換えた上で，証明図の形をサイクル付きの木に拡張することで得られる証明体系である．循環証明体系はその基になる帰納法規則を含む通常の証明体系に比べて，証明能力が一般に高くなる [1]．しかし，その逆の包含関係が成り立つかどうかは自明ではない．本講演では，「プレスバーガー算術の循環証明体系」と「その基になる通常の証明体系」の証明能力が一致することを示す．

[1] Stefano Berardi and Makoto Tatsuta. Classical system of martin-löf’s inductive definitions is not equivalent to cyclic proofs. Logical Methods in Computer Science, 15(3), 2019

• 津久浦健太 (筑波大学) 「強制法の代数的側面」

概要：強制法は Cohen によって導入された，集合論の主張の無矛盾性証明に用いられる手法である．多くの書籍では強制法は集合論の宇宙を拡大した新たなモデルを与える技術として説明される．実際，直接そのモデル内で議論をする事も多いが，強制法定理を通じて，それらは全て完備 Boole 代数の計算として見る事が出来る．本講演ではそういった代数的側面から強制法の紹介をする．特に完備 Boole 代数間の射影の代数的性質と商強制法の強制法的性質の関連について紹介したい．

• 西村祐輝 (東京工業大学) 「Index frame と 2次元 Fusion の完全性」

概要：Index frame は、様相記号を2種類以上持つ (multi-modal) 様相論理におけるフレームの一種である．通常の Kripke frame における可能世界を，いくつかの index の組として（座標のように）表すのが特徴である．これに対応する論理は Fusion と呼ばれる．本研究では， Fusion の tableau 体系を構築し， index frame との健全性・完全性を示す．さらに，任意の tableau が有限の長さで停止するという性質，termination も示す．

※ こちらの研究は佐野勝彦，Elise Perrotin との共同研究である．

• 山形頼之 (産総研)「On proving consistency of equational theories in Bounded Arithmetic」

概要：We consider pure equational theories that allow substitution but disallow induction, which we denote as PETS, based on recursive definition of their function symbols. We show that the Bounded Arithmetic theory S12 proves the consistency of PETS. Our approach employs models for PETS based on approximate values resembling notions from domain theory in Bounded Arithmetic, which may be of independent interest. (講演は日本語です)

• 鈴木悠大 (東北大学)「カントール空間の単調作用素の不動点定理と Weihrauch 次数」

概要：Weihrauch 次数は，数学の定理の複雑さを測るための指標の一つである．定理の複雑さを測る研究としては，証明論的な視点から複雑さを測る逆数学がよく知られているが，これに対して近年は，計算論的な視点から定理の複雑さを測るWeihrauch 次数の研究，及び逆数学と Weihrauch 次数の比較が盛んに研究されている．本講演ではカントール空間上の単調作用素の不動点定理および周辺の話題について，Weihrauch 次数の観点から分析した結果を，逆数学の結果と比較しつつ紹介する．

なお，本講演での発表内容は，横山啓太との共同研究によるものである．

• 只木孝太郎 (中部大学)「An effectivization of the law of large numbers for an arbitrary Schnorr random sequence and its absolute speed limit of convergence」
  概要：In this talk, we study an effectivization of the law of large numbers for algorithmically random infinite sequences. 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 present an absolute speed limit of convergence in this effectivization of the law of large numbers 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.

• 中澤巧爾 (名古屋大学) 「不動点演算子を持つ命題論理の循環証明体系」

概要：不動点演算子を持つ命題論理，および，その様相演算子による拡張に対して，無限証明体系と循環証明体系が証明能力において等価であることを示す．また，これらの循環証明体系がカットなしで完全であることを示す．

本研究は堀弘昌 (名古屋大学)，龍田真 (NII) との共同研究である．