形式算術における数学命題のサブリカ-ジョン理論による解析

本研究の目的に揚げた,「算術の形式理論とそこで定義可能な関数の計算複雑度の関係を,数学基礎論の方法で明らかにすること」の研究報告を,研究計画に沿って以下のように行う.1.証明論と計算理論の中間領域における結果をまとめること.このことについては,証明論や計算理論(帰納的関数論)の研究者と研究連絡を行いさらに資料収集を行って,証明論における組み合わせ的独立命題の研究結果,また計算理論におけるコルモゴロフ計算量の理論の研究結果などをまとめることができた.2.カテゴリー論の概念をサブリカ-ジョン理論に導入して,証明の複雑度をファンクター等の概念で計ること.このことについては,Girard等によるPi-1-2 Logicの研究成果をふまえて,急増加関数のサブリカ-ジョン階層をカテゴリーを用いて拡張することにより,上記の組み合わせ的独立命題の研究に有効であることが解った.3.2.の理論を実際の算術の形式理論にあてはめて,そこでの定義可能な関数の計算複雑度を決めること.このことについては,上記2.で述べたカテゴリーを用いた計算複雑度の計り方を使って,証明論での具体的な算術体系(ペアノ算術,Pi-1-1内包公理など)で定義可能関数の複雑度を計ることができ,さらに組み合わせ論的独立命題の証明可能性,不可能性を議論できることが解った.4.数学的な命題の算術の形式理論での強さを,その命題が内包する関数の計算複雑度を見ることで決定すること.このことについては,一般の数学的命題についての結果は得られてはいないが,上記のような組み合わせ的命題や計算理論における命題等で決定されることが解った.今後の課題として,ここで得られた結果を情報理論の命題に対してより広く応用して,証明論的な形式理論体系が持つ情報量に関する知見を得てゆくことを計画中である.

本研究の目的に揚げた,「算術の形式理論とそこで定義可能な関数の計算複雑度の関係を,数学基礎論の方法で明らかにすること」の研究報告を,研究計画に沿って以下のように行う.1.証明論と計算理論の中間領域における結果をまとめること.このことについては,証明論や計算理論(帰納的関数論)の研究者と研究連絡を行いさらに資料収集を行って,証明論における組み合わせ的独立命題の研究結果,また計算理論におけるコルモゴロフ計算量の理論の研究結果などをまとめることができた.2.カテゴリー論の概念をサブリカ-ジョン理論に導入して,証明の複雑度をファンクター等の概念で計ること.このことについては,Girard等によるPi-1-2 Logicの研究成果をふまえて,急増加関数のサブリカ-ジョン階層をカテゴリーを用いて拡張することにより,上記の組み合わせ的独立命題の研究に有効であることが解った.3.2.の理論を実際の算術の形式理論にあてはめて,そこでの定義可能な関数の計算複雑度を決めること.このことについては,上記2.で述べたカテゴリーを用いた計算複雑度の計り方を使って,証明論での具体的な算術体系(ペアノ算術,Pi-1-1内包公理など)で定義可能関数の複雑度を計ることができ,さらに組み合わせ論的独立命題の証明可能性,不可能性を議論できることが解った.4.数学的な命題の算術の形式理論での強さを,その命題が内包する関数の計算複雑度を見ることで決定すること.このことについては,一般の数学的命題についての結果は得られてはいないが,上記のような組み合わせ的命題や計算理論における命題等で決定されることが解った.今後の課題として,ここで得られた結果を情報理論の命題に対してより広く応用して,証明論的な形式理論体系が持つ情報量に関する知見を得てゆくことを計画中である.