2019 Fiscal Year Annual Research Report
A logical foundation for constructivism
| Project/Area Number |
19J01239
|
|---|
| Research Institution | Meiji University |
|---|
Principal Investigator |
藤原 誠 明治大学, 明治大学, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2019-04-25 – 2022-03-31
|
| Keywords | 構成的数学 / BHK解釈 / 直観主義算術 / 最小論理 |
|---|
| Outline of Annual Research Achievements |
本研究全体の目的は，数学や論理学の分野においてコンセンサスが乏しい構成的推論という概念に対して，現代的視座に立って数学的に妥当な定式化を与えることである．伝統的に，構成的推論はBHK(ブラウアー/ハイティング/コルモゴロフ)解釈と呼ばれる論理結合子の直観主義的解釈を用いて説明される．構成的推論の形式的取り扱いのため，1920-30年代に直観主義論理が考案された．直観主義論理はその後発展した計算機科学の理論的基盤として幅広く研究されている一方で，当初の目的であった構成的推論を特徴付ける形式論理としては十分に満足がいくものではない．本研究では，BHK 解釈に基づく意味論が健全かつ強完全となるような矛盾記号を言語に含まない形式論理で，かつ算術の公理を加えれば半直観主義有限型算術となるものを構築することを目指している．
本年度の研究において，私は矛盾記号，選言記号，存在量化子を持たない弱い直観主義有限型算術を導入し，その算術が型付き実現可能性解釈や二重否定翻訳と密接に関係していることを明らかにした．また，有限型選択公理の二重否定翻訳はその算術の言語で表現されるが，それが有限型算術における二重否定シフト公理に対応するものであることを示した．
また，直観主義数学や構成的数学における構成的推論の数学的側面をより深く理解するため．BHK解釈の基点となったL.E.J Brouwerのバー定理を構成的逆数学の立場から詳しく分析し，バー定理と論理原理の関係，バー定理とバー再帰の関係，バー定理と連続性公理の関係を明らかにした．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
矛盾記号を含まない言語において二重否定シフト公理に対応する公理はどのようなものであるかを明らかにすることが本年度の具体的な目標であったが，おおよそそれを達成できたという面において，本研究はおおむね順調に進展していると言える．
また，バー定理の構成的逆数学に関しては，当初の期待以上に新しい結果が次々と得られている．
|
| Strategy for Future Research Activity |
型付き実現可能性解釈がBHK解釈を自然に形式化したものであることを鑑みれば，本年度の研究成果は，今回新しく導入した矛盾記号，選言記号，存在量化子を持たない弱い直観主義有限型算術に二重否定シフト公理の対応物を加えて得られる算術(以下，算術Bと書く)の論理部分が所望の論理に近いものであることを示唆する．算術Bは矛盾記号だけでなく選言記号や存在量化子をも言語に持たないため，「算術Bの論理部分」は構成的推論に関連する良く知られた既存の論理である最小論理よりも弱いものであるように思われる一方で，最小論理よりも真に強い直観主義論理でさえ証明できない二重否定シフト公理の対応物を含んでいる．
今後は，この「算術Bの論理部分」がどのようなものであるかについて，証明論と意味論の両側面から解析する．最小論理はベス意味論と呼ばれる意味論によって健全かつ完全となることが知られており，ベス意味論と型付き実現可能性解釈の関係が解明されれば本研究課題の達成に大きく近づく．そのため本年度は，最小論理のベス意味論に詳しいHelmut Schwichtenberg教授が指揮するルートヴィヒ・マクシミリアン大学ミュンヘンの数理論理学研究グループを長期訪問し，最小論理のベス意味論を詳しく学ぶと共に，ベス意味論と型付き実現可能性解釈の関係を調べる．さらに，ベス意味論における二重否定シフト公理の振る舞いを詳しく調べ，算術の言語を含まない論理の文脈における二重否定シフト公理の対応物を探る．一方，並行して，選言記号と存在量化子を含まない最小論理の証明論的性質を調べる．
また，直観主義数学や構成的数学における構成的推論の数学的側面をより深く理解するため，Brouwerのバー定理やそれに関連する連続性公理の構成的逆数学をさらに推し進める．
|
