1998 Fiscal Year Annual Research Report

算術と計算の論理構造に関する研究

Research Project

Project/Area Number	09440072
Research Institution	Tohoku University
Principal Investigator	田中一之東北大学, 大学院・理学研究科, 教授 (70188291)
Co-Investigator(Kenkyū-buntansha)	長谷川立東京大学, 大学院・数理科学研究科, 助教授 (20243107) 龍田真京都大学, 大学院・理学研究科, 助教授 (80216994) 廣川佐千男九州大学, 大型計算機センター, 教授 (40126785) 安本雅洋名古屋大学, 大学院・多元数理科学研究科, 助教授 (10144114) 寛来正子 (高橋雅子) 東京工業大学, 大学院・情報処理工学研究科, 教授 (00015588)
Keywords	論理構造 / 計算論 / 型理論 / 形式算術 / 2階算術 / 逆数学 / 限定算術 / ラムダ計算
Research Abstract	本研究の目的および実施計画に沿って、研究代表者と研究分担者は相互に緊密な連絡を取り合い、また研究集会での発表や討論を通して、算術と計算の論理構造に関する研究を行った。主な研究内容を研究者毎にまとめると、以下の通りである。田中一之は、数学の定理を証明するのにどれくらい複雑な集合が必要かという問題(逆数学)を研究した。とくに無限2分木に対するケーニヒの補題に基づく2階算術の体系WKL_0に対し超準的手法を開発し、Haar測度の存在などを導くのにこの体系が必要十分であることを示した。宝来(高橋)正子は、論理体系、計算体系、型理論の三者の関係について研究した。とくに、新しい(自然な)高階論理体系を導入することにより、高階論理体系と高階型理論の関係を明瞭にした。また、型理論の中で最も基本的かつ重要な体系である「単純型理論」について、その表現力を考察した。安本雅洋は、限定算術の超準モデルMのプール値拡大MAB、およびgeneric拡大M[G]の構造に関する研究を行った. P=NPを仮定すると、M[G]はS_2のモデルとなること、またP=NPを仮定しない場合は、M[G]はS_2∧1のΣ_1∧-partのモデルになることなどを証明した. 廣川左千夫は、ラムダ項を用いて、推論や証明の構造を解析する研究を進めた。具体的には、contractionのない部分構造論理である適切さの論理P-Wについて、ラムダ項の型としての特徴付けを得た。龍田真は、フェファーマンの関数およびクラスの構成的論理T0に対して、集合完備化プログラムを用いて変数を二重化せずに、q-実現可能性解釈を与え、その健全性を証明した。さらに、単調余帰納的定義のプログラム合成への応用や、グラフモデルおよび部分関数モデルの性質を調べた。長谷川立は、ラムダ計算に対する解析関手を用いたモデルを調べることにより、ラムダ計算にあらわれる不動点演算子と、解析学にあらわれるLagrange-Goodの逆関数公式との間に密接な関係があることを示した。鹿島亮は、適切含意論理の代表的な公理系Eが線形Uモデル(「半束」と「Kripke流の可能世界集合」を組み合わせたモデル)に対して完全であることを証明した。

Research Products
(8 results)

All Other

All Publications (8 results)

[Publications] K.Tanaka,T.Yamazaki: "A non-standard construction of Haar measure and WKLo" Journal of Symbolic Logic. (印刷中). (1999)
[Publications] M.Takahashi: "Lambda-representable functions over free structures revisited" Proc.of 3rd Fuji Int.Symp.on Func.and Logic Programming. 1-19 (1998)
[Publications] G.Takeuti,M.Yasumoto: "Forcing on Bounded Avithmetic II" Journal of Symbolic Logic. 63. 860-868 (1998)
[Publications] S.Hirokawa: "Infiniteness of proof(alpha)is polynomial-space complete" Theoretical Computer Science. 206・1-2. 331-339 (1998)
[Publications] M.Tatsuta: "Realizability for Constractive Theory of Functions and Classes and Its Application to progranc Synthesis" Proc.of 13th Ann.IEEE Symp.Logic in CS. 358-367 (1998)
[Publications] R.Kashima,N.Kamide: "Substructural implicational logic includiog the relevant logic E" Studia Loyica. (印刷中). (1999)
[Publications] M.Takahashi,M.Dezani,M.Okada: "Theories of Types and Proofs" 日本数学会(MSJ-Memoirs Vol.2), 295 (1998)
[Publications] 田中一之: "数学の基礎をめぐる論争" シュプリンガーフェアラーク東京, 224 (1999)

1998 Fiscal Year Annual Research Report

算術と計算の論理構造に関する研究

Principal Investigator

田中 一之 東北大学, 大学院・理学研究科, 教授 (70188291)

Research Products

[Publications] K.Tanaka,T.Yamazaki: "A non-standard construction of Haar measure and WKLo" Journal of Symbolic Logic. (印刷中). (1999)

[Publications] M.Takahashi: "Lambda-representable functions over free structures revisited" Proc.of 3rd Fuji Int.Symp.on Func.and Logic Programming. 1-19 (1998)

[Publications] G.Takeuti,M.Yasumoto: "Forcing on Bounded Avithmetic II" Journal of Symbolic Logic. 63. 860-868 (1998)

[Publications] S.Hirokawa: "Infiniteness of proof(alpha)is polynomial-space complete" Theoretical Computer Science. 206・1-2. 331-339 (1998)

[Publications] M.Tatsuta: "Realizability for Constractive Theory of Functions and Classes and Its Application to progranc Synthesis" Proc.of 13th Ann.IEEE Symp.Logic in CS. 358-367 (1998)

[Publications] R.Kashima,N.Kamide: "Substructural implicational logic includiog the relevant logic E" Studia Loyica. (印刷中). (1999)

[Publications] M.Takahashi,M.Dezani,M.Okada: "Theories of Types and Proofs" 日本数学会(MSJ-Memoirs Vol.2), 295 (1998)

[Publications] 田中 一之: "数学の基礎をめぐる論争" シュプリンガー フェアラーク東京, 224 (1999)

田中一之東北大学, 大学院・理学研究科, 教授 (70188291)

[Publications] 田中一之: "数学の基礎をめぐる論争" シュプリンガーフェアラーク東京, 224 (1999)