論理の階層的構造と超限的型理論

点击翻译按钮获取中文摘要

当研究の主目的は、当申請者が提案した構成的解析学の体系(TRDB)と、その計算性を実現する超限的型理論(TRM)の諸関係の解明である。平成6年度の課題として、TRMの超限的型の集合論的意味付け、TRMのTRDBへの翻訳、TRDBからTRMへの写像と、その反対の写像の合成が恒等写像ではないことの証明、およびその意味の解明、などを提案し、予定通りの結果を得た。詳しくは、下記のとおりである。集合論の内包公理や帰納的集合の定義を使って、型の自然なモデルをつくる:型を論理式へ(とくに超限的型を超限帰納法で述語記号へ)写し、汎関数を証明図へ(とくにbar関数をbar帰納法へ)写す:TRDBとTRMの間の写像がたがいに逆写像になっていなくても、ある種の性質が保存されことを示す、など。さらにこのような体系と実際の数学との関連の考察のために、幾何学、整数論、解析学、などの専門家の協力をえた。とくに、構成的体系において微分積分法を展開することにより、区間解析の理論的基礎づけを与える端緒を得た。構成的世界では、有限の情報で数学を組み立てるので、関数の諸性質などは、区間上で決定される。見かけ上ふつうの微分積分法を展開しているような設定にして、そこからの情報は区間上でのみ得られるようにする。これらの成果は、証明論研究会(数理解析研究所短期共同研究集会)、Workshop on Constructivity,Computability,and Language(京都産業大学計算機科学研究所主催)などでも、発表した。