A logical foundation for constructivism

本研究の目標は，BHK解釈に基づいた意味論に対して健全かつ完全となる形式論理を構築し，構成的推論を数理論理学の現代的立場から特徴付けることである. 本年度は，統語論と意味論の両側面からのアプローチを試みた．統語論的側面からは，古典論理の証明を構成的推論と関連が深い最小論理の証明に変換する一般化されたゲンツェンの否定翻訳を詳しく解析し，それを用いて，古典算術と直観主義算術の間の保存性定理を拡張する古典算術と中間算術の間の保存性定理を得た．また，典型的な論理式のクラスに対する拡張された保存性定理と直観主義算術上の論理原理の階層構造の関係を詳しく解析し，その構造をおおよそ明らかにした．この結果は，通常の数学の証明における推論と構成的推論の差を詳しく解析するために有用であると思われる．これらは倉橋太志氏(神戸大学)との共同研究の成果である．さらに，BHK解釈に基づく意味論に対して健全かつ完全となる形式論理の構築のための足がかりとなる選言記号及び矛盾記号を含まない有限型算術及びその自然な拡張の詳しい解析を進め，問題の適当な定式化のための着想を得た．意味論的側面からは，中間命題論理を分離するクリプキモデルを用いて中間算術の階層を分離する一般的な手法を精査して改良した．また，最小論理に対して健全かつ完全であることが構成的に示される意味論であるSchwichtenberg氏の木意味論について，直観主義論理で証明可能であることの特徴付けに関する新たなる知見を得た．さらに，木意味論とクリプキ意味論の関係について調査と分析を行い，その関連性を数学的に記述するための端緒を得た．

本研究の目標は，BHK解釈に基づいた意味論に対して健全かつ完全となる形式論理を構築し，構成的推論を数理論理学の現代的立場から特徴付けることである. 本年度は，統語論と意味論の両側面からのアプローチを試みた．統語論的側面からは，古典論理の証明を構成的推論と関連が深い最小論理の証明に変換する一般化されたゲンツェンの否定翻訳を詳しく解析し，それを用いて，古典算術と直観主義算術の間の保存性定理を拡張する古典算術と中間算術の間の保存性定理を得た．また，典型的な論理式のクラスに対する拡張された保存性定理と直観主義算術上の論理原理の階層構造の関係を詳しく解析し，その構造をおおよそ明らかにした．この結果は，通常の数学の証明における推論と構成的推論の差を詳しく解析するために有用であると思われる．これらは倉橋太志氏(神戸大学)との共同研究の成果である．さらに，BHK解釈に基づく意味論に対して健全かつ完全となる形式論理の構築のための足がかりとなる選言記号及び矛盾記号を含まない有限型算術及びその自然な拡張の詳しい解析を進め，問題の適当な定式化のための着想を得た．意味論的側面からは，中間命題論理を分離するクリプキモデルを用いて中間算術の階層を分離する一般的な手法を精査して改良した．また，最小論理に対して健全かつ完全であることが構成的に示される意味論であるSchwichtenberg氏の木意味論について，直観主義論理で証明可能であることの特徴付けに関する新たなる知見を得た．さらに，木意味論とクリプキ意味論の関係について調査と分析を行い，その関連性を数学的に記述するための端緒を得た．