Reconsideration of the relationship between formalism and intuitionism via proof-theoretical method

从证明理论的角度重新思考形式主义与直觉主义的关系

• 批准号: 22820054
• 负责人: AKIYOSHI Ryota
• 金额: $ 1.5万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Research Activity Start-up
• 财政年份: 2010
• 资助国家: 日本
• 起止时间: 2010 至 2011
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-22820054/
• 关键词: 哲学; 倫理学; 数学基礎論

We investigated the relationship between formalism and intuitionism from the view points of mathematical logic and philosophy. In the joint mathematical work with G. Mints(Stanford University), the complete cut-elimination theorem for Omega-rule, which had been an open problem, is proved. In the philosophical work, we analysed the history of proof theory from the viewpoint of "analysis of impredicativity" and presented some issues to be addressed.

我们从数理逻辑和哲学的角度考察了形式主义与直觉主义的关系。在与斯坦福大学G. Mints合著的数学著作中，证明了欧米伽规则的完全切消定理，该定理一直是一个开放问题。在哲学工作中，我们从“不可预测性分析”的角度分析了证明论的历史，并提出了一些有待解决的问题。

项目成果

Introduction to Proof Theory for Impredicative Systems

命令式系统证明论简介

• 发表时间: 2010
• 作者: Suzuki;M;竹村亮;秋吉亮太
• 通讯作者: 秋吉亮太

Gentzen's First Consistency Proof Revisited

重新审视 Gentzen 的第一个一致性证明

• 发表时间: 2010
• 期刊: CARLS Series of Advanced Study of Logic and Sensibility
• 作者: Nakanishi;H;Yokokawa;H;Ryota Akiyoshi
• 通讯作者: Ryota Akiyoshi

Finite Notations for Omega_mu+1-rule

Omega_mu 1 规则的有限表示法

• 发表时间: 2010
• 作者: Yuri Sato;Koji Mineshima;Ryo Takemura;Ryota Akiyoshi
• 通讯作者: Ryota Akiyoshi

ゲンツェンの無矛盾性証明再訪

重新审视 Gentzen 的一致性证明

• 发表时间: 2010
• 作者: Suzuki;M.;竹村亮;秋吉亮太
• 通讯作者: 秋吉亮太

非可述性の分析としての証明論

证明理论作为未陈述的分析

• 发表时间: 2012
• 期刊: 科学基礎論研究
• 作者: Nakanishi;H.;秋吉亮太
• 通讯作者: 秋吉亮太