• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2021 年度 実施状況報告書

中間2階命題論理の研究

研究課題

研究課題/領域番号 20K03712
研究機関東京工業大学

研究代表者

鹿島 亮  東京工業大学, 情報理工学院, 准教授 (10240756)

研究期間 (年度) 2020-04-01 – 2025-03-31
キーワード様相論理
研究実績の概要

本研究課題である中間2階命題論理はクリプキモデルに様々な条件を加えることで得られる論理であるが、クリプキモデルを用いる論理の研究の一般論が様相論理の研究である。すなわち中間2階命題論理の研究は様相論理の研究の特殊例とみなすこともできる。現在、中間2階命題論理の当初計画していた研究はやや行き詰まっているので、2021年度はより広い視点で様相論理の研究に重点を置いた。具体的には、算術の証明可能性述語に対応する様相記号を持つ論理についての結果を得た。この分野の出発点であるSolovayの先駆的な研究(1976年)で与えられた基本的な二つの論理 GL と GLS については、前者はその後非常に多くの変種も導入されて広く研究されているが、後者についての研究はあまり進んでいない。その理由はGLSについては扱いやすいクリプキ型意味論が見つかっていなかったからと思われる。本研究では、新しい発想によるとても性質のよい意味論を発見した。この結果は近々発表予定である。
なお学生の教育用および本研究成果を一般に発信するための準備として、様相論理の教科書を執筆・出版した。この教科書には従来の成書(洋書も含む)にはほとんど載っていない重要事項(様相ミュー計算のゲーム意味論の妥当性定理など)も載せており、これを大学院生に学んでもらうことで2022年度以降に本研究の一部分を担ってもらう準備をしている。
これらの研究の他に、数理論理学の基本定理のひとつである Lindstrom の定理を変数の個数を制限した1階述語論理に対して示す、という研究も行った。

現在までの達成度 (区分)
現在までの達成度 (区分)

3: やや遅れている

理由

ひとつは既に2年間続く新型コロナウイルス感染症による社会活動の制限である。大学では出張、特に海外出張が制限されており、共同研究が当初の予定のように進んでいない。
もうひとつは計画策定時の見込み違いである。中間2階命題論理の性質が当初想定したものとやや異なることがわかり、当初やろうと思っていたことがあまり綺麗にできないことがわかってきた。これをどう回避するかは検討中である。

今後の研究の推進方策

ひとつは様相論理研究を幅広く進める。特に、研究実績概要に記載したGLSの新しい意味論については、多くの研究会や学外セミナーに参加して他研究者との議論を通じてさらに研究を発展させていく。
もうひとつは中間2階命題論理について、当初の計画を柔軟にアレンジしながら研究を進める。学外の研究協力者との対面での研究打ち合わせも徐々に再開できる状況になっているので、これを進める。
なお博士課程学生にRAとして研究補助をしてもらう計画である。

次年度使用額が生じた理由

所属大学における新型コロナウイルス感染症対策により対面での研究打ち合わせや研究集会への対面参加に制限があったため旅費があまり使用できなかった。2022年度は制限緩和が期待できるので、海外出張を含めて計画通りに使用していく計画である。

  • 研究成果

    (2件)

すべて 2022 2021

すべて 学会発表 (1件) 図書 (1件)

  • [学会発表] 変数の個数を制限した一階述語論理に対する Lindstrom 定理2021

    • 著者名/発表者名
      鹿島亮,木内詠美
    • 学会等名
      RIMS 共同研究(公開型)「証明と計算の理論と応用」
  • [図書] コンピュータサイエンスにおける様相論理2022

    • 著者名/発表者名
      鹿島 亮
    • 総ページ数
      176
    • 出版者
      森北出版
    • ISBN
      978-4-627-85641-7

URL: 

公開日: 2022-12-28  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi