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

证明、组合性、悖论

基本信息

批准号：
15J05414
负责人：
黒川英徳
金额：
$ 1.58万
依托单位：
Kanazawa University (2017)Kobe University (2015-2016)
依托单位国家：
日本
项目类别：
Grant-in-Aid for JSPS Fellows
财政年份：
2015
资助国家：
日本
起止时间：
2015-04-24 至 2018-03-31
项目状态：
已结题

项目摘要

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

在这项研究中，我们主要研究了克莱塞尔-古德曼的“合成理论”，它是直觉逻辑的基本理论。目的是证明直觉逻辑和直觉形式算术构造理论的健全性和完整性，并证明构造理论的一致性。今年，我们开展研究的主要目的是证明相关理论的一致性。预计lambda演算的Church-Rosser定理可以应用于这个证明，因此我们尝试应用其中的一些方法来证明这个定理，但到目前为止我们还没有能够获得证明。为此，我决定在某种程度上改变我的研究方向，研究描述直觉逻辑与算术关系的德容定理（或直觉逻辑的算术完备性）与理论之间的关系。的组成。关于这一点，我目前正在写一篇论文，因为我通过应用克赖塞尔的一种称为“挤压论证”的论证，对合成理论与直觉逻辑之间的关系有了一些了解。这项研究是与 Walter Dean 的联合研究。今年我们也针对这个中心问题进行了非经典逻辑的研究。我准备了一篇关于与直觉逻辑基础相关的“证明逻辑”的哲学基础的论文，并在 IHPST、巴黎第一大学和东京大学的研讨会上发表了它。此外，我还从证明论的角度进行了更广泛地表征非经典逻辑中出现的逻辑常数的研究，并在伯明翰大学的第二届 MLA（由 JAIST 主办）和 WS 上发表了结果。我目前正在写一篇关于这项研究的技术成果的论文，以及一篇关于该主题的哲学基础的论文。结合这项研究，我正在与巴黎第一大学的 Alberto Naibo 和巴西 UFABC 的 Mattia Petrolo 一起继续对逻辑常数的证明理论表征进行证明理论研究。