| 研究課題/領域番号 |
19J01239
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 審査区分 |
小区分12030:数学基礎関連
|
|---|
| 研究機関 | 明治大学 |
|---|
研究代表者 |
藤原 誠 明治大学, 理工学部, 特別研究員(PD)
|
|---|
| 研究期間 (年度) |
2019-04-25 – 2022-03-31
|
| 研究課題ステータス |
完了 (2021年度)
|
| 配分額 *注記 |
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2021年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2020年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2019年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
|
|---|
| キーワード | 構成的数学 / 直観主義算術 / 保存性定理 / 構成的推論 / 実現可能性解釈 / 最小論理 / ベス意味論 / BHK解釈 |
|---|
| 研究開始時の研究の概要 |
数学や論理学の分野においてコンセンサスが乏しい構成的推論という概念に対して，現代的視座に立って数学的に妥当な定式化を与える．
ブラウアーの直観主義数学における構成的推論の形式化を目指し，1920-30年代に直観主義論理が考案された．直観主義論理はその後発展した計算機科学の理論的基盤である一方，当初の目的であった構成的推論の形式化としては弱すぎる．
本研究では，構成的推論の自然な表現である抽象実現可能性解釈という意味論に着目し，抽象実現可能性解釈が健全かつ強完全となる矛盾記号を言語に含まない形式論理で，かつ算術の公理を加えれば半直観主義有限型算術となるものを構築することを目指す．
|
| 研究実績の概要 |
本研究の目標は，BHK解釈に基づいた意味論に対して健全かつ完全となる形式論理を構築し，構成的推論を数理論理学の現代的立場から特徴付けることである. 本年度は，統語論と意味論の両側面からのアプローチを試みた．
統語論的側面からは，古典論理の証明を構成的推論と関連が深い最小論理の証明に変換する一般化されたゲンツェンの否定翻訳を詳しく解析し，それを用いて，古典算術と直観主義算術の間の保存性定理を拡張する古典算術と中間算術の間の保存性定理を得た．また，典型的な論理式のクラスに対する拡張された保存性定理と直観主義算術上の論理原理の階層構造の関係を詳しく解析し，その構造をおおよそ明らかにした．この結果は，通常の数学の証明における推論と構成的推論の差を詳しく解析するために有用であると思われる．これらは倉橋太志氏(神戸大学)との共同研究の成果である．さらに，BHK解釈に基づく意味論に対して健全かつ完全となる形式論理の構築のための足がかりとなる選言記号及び矛盾記号を含まない有限型算術及びその自然な拡張の詳しい解析を進め，問題の適当な定式化のための着想を得た．
意味論的側面からは，中間命題論理を分離するクリプキモデルを用いて中間算術の階層を分離する一般的な手法を精査して改良した．また，最小論理に対して健全かつ完全であることが構成的に示される意味論であるSchwichtenberg氏の木意味論について，直観主義論理で証明可能であることの特徴付けに関する新たなる知見を得た．さらに，木意味論とクリプキ意味論の関係について調査と分析を行い，その関連性を数学的に記述するための端緒を得た．
|
| 現在までの達成度 (段落) |
令和3年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
令和3年度が最終年度であるため、記入しない。
|
