Reexamination of Brouwer's intuitionism by proof-theoretic methods

2019 Fiscal Year Final Research Report

• Project/Area Number: 16K16690
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Multi-year Fund
• Research Field: Philosophy/Ethics
• Research Institution: Waseda University
• Principal Investigator: Akiyoshi Ryota 早稲田大学, 高等研究所, その他(招聘研究員) (20587852)
• Project Period (FY): 2016-04-01 – 2020-03-31
• Keywords: 論理学の哲学 / 数学の哲学 / ブラウワー / ヒルベルト / 理論計算機科学 / ラムダ計算 / 数学基礎論 / 証明論

Outline of Final Research Achievements

By studying Brouwer's intuitionism by proof-theoretic methods, we obtained the following outputs. As to philosophical investigations, (i) a proof-theoretic interpretation of Brouwer's proof of bar induction, (ii) an elucidation of the relationship between contentual and formal elements in Gentzen's consistency proofs. As to logical investigations, (i) proof-theoretic results about the Omega-rule, (ii) an application of the Omega-rule to the context of theoretical computer science (typed lambda calculus).

All of these were published from refereed international journals and refereed international conferences. In short, our works via the Omega-rule (, which is a traditional method in proof-theory) produced fruitful results. Moreover, we began a new research about Gaisi Takeuti's philosophy of mathematics based on them.

Free Research Field

哲学，数学，理論計算機科学

Academic Significance and Societal Importance of the Research Achievements

これまでブラウワー直観主義とヒルベルトの形式主義は対立する学派であるとみなされてきたが，ヒルベルトに由来する証明論的手法でブラウワー直観主義を探求したことで，これらの学派の間にこれまで気づかれて来なかった哲学的なつながりや論理学的なつながりを見出すことができた．
さらに，日本が産んだ最大の論理学者である竹内外史の思想を研究するという新たな方向性を得た．