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

证明、组合性、悖论

• 批准号: 15J05414
• 负责人: 黒川 英徳
• 金额: $ 1.58万
• 依托单位: Kanazawa University (2017)Kobe University (2015-2016)
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for JSPS Fellows
• 财政年份: 2015
• 资助国家: 日本
• 起止时间: 2015-04-24 至 2018-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-15J05414/
• 关键词: 直観主義論理; 構成の理論; 算術的完全性; 非古典論理; 論理定項; シークエント計算; 無矛盾性証明; カット除去証明; 無際限拡張可能性; 証明論的意味論; 直観主義; 証明論; 下部構造論理; 様相論理; 証明論理

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

这项研究主要研究了克雷塞尔·古德曼（Kreisel-Goodman）的“构建理论”，这是直觉主义逻辑的基本理论。目的是证明直观逻辑和直觉形式算术的构建结构的健全性，完整性和理论，并证明结构的共识。今年，我们以证明该理论达成共识的主要目标进行了研究。由于预计可以将Lambda计算的教堂 - 劳动定理应用于此证明，因此我们试图应用一些证明该定理的方法，但尚未获得证明。因此，我们决定在某种程度上改变研究政策，并研究定理与构建理论之间的关系，称为de jong的定理（或直觉主义逻辑的算术完美），它描述了直觉主义逻辑与算术之间的关系。我目前正在撰写本文，因为我通过应用Kreisel的论点来了解构建理论与直观逻辑之间的关系，我目前正在写这篇论文。这项研究是沃尔特·迪恩（Walter Dean）的联合研究项目。今年，我们还对与这个中心问题有关的非经典逻辑进行了研究。关于直觉主义逻辑的基本原理以及与证明逻辑基础有关的“证明逻辑”的基础的论文，并在巴黎IHPST的Tokyo University的一次研讨会上介绍。此外，他对从证明理论的角度进行了广泛出现在非古典逻辑中的逻辑成分进行了研究，并在第二个MLA（由Jaist主持）和伯明翰大学的WS中介绍了结果。目前，我目前正在撰写有关从这项研究中获得的技术结果的论文，以及有关此主题的哲学基础的论文。在这项研究中，我们将继续对巴黎大学的阿尔贝托·尼伯（Alberto Nibo）和巴西UFABC的马蒂亚·佩特罗洛（Mattia Petrolo）进行逻辑成分的特征验证验证研究。

项目成果

On the Interpretation of HPC in the Kreisel-Goodman Theory of Constructions

论Kreisel-Goodman构造理论中HPC的解释

• 发表时间: 2015
• 作者: Hidenori Kurokawa;Hirohiko Kushida;Hidenori Kurokawa;Hidenori Kurokawa;Hidenori Kurokawa
• 通讯作者: Hidenori Kurokawa

Generic common knowledge and other fixed point logics

通用常识和其他定点逻辑

• 发表时间: 2015
• 作者: Hidenori Kurokawa;Hirohiko Kushida;Hidenori Kurokawa
• 通讯作者: Hidenori Kurokawa

Incompleteness and the indefinite extensibility

不完整性和无限扩展性

• 发表时间: 2016
• 作者: Hidenori Kurokawa;Hidenori Kurokawa;Hidenori Kurokawa;Hidenori Kurokawa;Hidenori Kurokawa;Hidenori Kurokawa and Takeshi Yamada
• 通讯作者: Hidenori Kurokawa and Takeshi Yamada

Labelled sequent calculi for substructural logics I: relevant logics

子结构逻辑的标记顺序演算 I：相关逻辑

• 发表时间: 2015
• 作者: Hidenori Kurokawa;Hirohiko Kushida;Hidenori Kurokawa;Hidenori Kurokawa
• 通讯作者: Hidenori Kurokawa

Advances in proof-theoretic semantics (Trends in Logic, Vol. 43), (eds.) Th. Pietscha, P. Schroder-Heister, Ch 3. Kreisel’s theory of constructions, the Kreisel-Goodman paradox, and the second clause

证明理论语义学的进展（逻辑学趋势，第 43 卷），（编辑）Th. Pietscha，P. Schroder-Heister，第 3 章。克莱塞尔的构造理论、克莱塞尔-古德曼悖论和第二个子句

• 发表时间: 2015
• 作者: Hidenori Kurokawa;Sara Negri;菊池誠，黒川英徳;佐野勝彦, 倉橋大志, 薄葉季路, 黒川英徳, 菊池誠 （共著）;W. Dean & H. Kurokawa
• 通讯作者: W. Dean & H. Kurokawa