証明，　構成性，　パラドックス

本研究では，直観主義論理の基礎理論となるクライゼル-グッドマンの「構成の理論」について主として研究した．直観主義論理および直観主義形式算術の構成の理論に関する健全性，完全性を証明すること，および構成の理論の無矛盾性を証明することが目標であった．今年度は，特に当の理論の無矛盾性を証明することを主たる目標として研究を進めた．この証明にはラムダ計算のチャーチ＝ロッサーの定理を応用できることが期待されるため，この定理を証明する方法の幾つかを応用することを試みたが，現在のところ証明を得るには至っていない．このため研究の方針をある程度転換し，直観主義論理と算術の関係について述べるデ・ヨングの定理（あるいは直観主義論理の算術的完全性）と呼ばれる定理と構成の理論の関係を調べることにした．これについては，クライゼルによるsqueezing argumentと呼ばれる論法を応用することにより，構成の理論と直観主義論理の関係についてある洞察を得たため，現在論文を執筆中である．なお，この研究はワルター・ディーンとの共同研究である．また今年度は，この中心課題に関連した非古典論理に関する研究を行なった．直観主義論理の基礎と関連する「証明論理」の哲学的基礎に関する論文を準備し，パリ第一大学IHPSTの，東京大学のセミナーで発表した．また，さらに広く非古典論理に現れる論理定項を証明論の観点から特徴付けるという研究を行い，その成果を第二回MLA（JAIST主催），バーミンガム大学のWSにて発表した．現在，この研究で得られた, 技術的な成果に関する論文，またこのトピックに関する哲学的な基礎に関する論文を現在執筆中である．なお，この研究と関連して，パリ第一大学のアルベルト・ナイボ，ブラジルUFABCのマティア・ペトローロとの論理定項の証明論的特徴付けに関する証明論的研究を継続中である．

本研究では，直観主義論理の基礎理論となるクライゼル-グッドマンの「構成の理論」について主として研究した．直観主義論理および直観主義形式算術の構成の理論に関する健全性，完全性を証明すること，および構成の理論の無矛盾性を証明することが目標であった．今年度は，特に当の理論の無矛盾性を証明することを主たる目標として研究を進めた．この証明にはラムダ計算のチャーチ＝ロッサーの定理を応用できることが期待されるため，この定理を証明する方法の幾つかを応用することを試みたが，現在のところ証明を得るには至っていない．このため研究の方針をある程度転換し，直観主義論理と算術の関係について述べるデ・ヨングの定理（あるいは直観主義論理の算術的完全性）と呼ばれる定理と構成の理論の関係を調べることにした．これについては，クライゼルによるsqueezing argumentと呼ばれる論法を応用することにより，構成の理論と直観主義論理の関係についてある洞察を得たため，現在論文を執筆中である．なお，この研究はワルター・ディーンとの共同研究である．また今年度は，この中心課題に関連した非古典論理に関する研究を行なった．直観主義論理の基礎と関連する「証明論理」の哲学的基礎に関する論文を準備し，パリ第一大学IHPSTの，東京大学のセミナーで発表した．また，さらに広く非古典論理に現れる論理定項を証明論の観点から特徴付けるという研究を行い，その成果を第二回MLA（JAIST主催），バーミンガム大学のWSにて発表した．現在，この研究で得られた, 技術的な成果に関する論文，またこのトピックに関する哲学的な基礎に関する論文を現在執筆中である．なお，この研究と関連して，パリ第一大学のアルベルト・ナイボ，ブラジルUFABCのマティア・ペトローロとの論理定項の証明論的特徴付けに関する証明論的研究を継続中である．