著者

秋吉 亮太

出版者

科学基礎論学会

雑誌

科学基礎論研究 (ISSN:00227668)

巻号頁・発行日

vol.39, no.2, pp.93-107, 2012-03-25 (Released:2017-08-01)

参考文献数

57

---

Proof theory was initiated by Hilbert for the foundation of mathematics, especially for carrying out "Hilbert's program". After Godel's incompleteness theorems, proof theory (ordinal analysis) has been developed as pure mathematics. It has been widely held that it is quite difficult to explain what has been gained in proof theory (ordinal analysis). In this paper we review the development of proof theory and its recent results for impredicative subsystems of analysis from the viewpoint of "analysis of impredicativity". We point out the main difficulties to explain conceptual significance of proof theory. Our conclusion is that such difficulties should be addressed by developing (not only proof theory as pure mathematics) philosophy of mathematics in future.

著者

秋吉 亮太 高橋 優太

出版者

科学基礎論学会

雑誌

科学基礎論研究 (ISSN:00227668)

巻号頁・発行日

vol.41, no.1, pp.1-22, 2013-11-30 (Released:2017-08-31)

参考文献数

50

被引用文献数

1 2

---

Gentzen proved the consistency of elementary arithmetic (i.e. first-order Peano arithmetic) in 1936 before his most famous and influential proof in 1938. The consistency proof in 1936 contains some ambiguous parts and seems to be quite different from his consistency proof in 1938. The aim of the consistency proof in 1936 is "to give finitist sense" to provable formula. In this paper, we give an exact reconstruction of the consistency proof in 1936 and claim that "to give finitist sense" is a uniform idea behind Gentzen's three consistency proofs including the proof in 1938. First we explain Gentzen's basic ideas of the proof in 1936 in detail. In particular, the idea of finitist interpretation and the main structure of the proof are explained. Secondly, we define a reduction step via the modern method of proof theory called "finite notation for infinitary derivations" due to Mints-Buchholz. It is shown that the reduction essentially coincides with Gentzen's reduction in 1936. Especially we give a definition of "normalization tree" describing Gentzen's reduction step. Moreover, the well-foundedness of this tree is proved. The well-foundedness of the normalization tree implies the consistency of elementary arithmetic. Together with Buchholz's analysis of Gentzen's 1938 consistency proof, this shows that the proof in 1938 is just a special case of the proof in 1936. Thirdly, we clarify what the normalization tree is. According to Gentzen, the normalization tree makes us possible to see the "correctness" of a provable formula in elementary arithmetic. Then we propose a uniform reading of three consistency proofs as based on the same spirit. Finally we discuss some relationship between Gentzen's idea, the method of "finite notation for infinitary derivations", and Gödel's idea of his famous Dialectica interpretation. According to our analysis, Gentzen's idea and the method of "finite notation for infinitary derivations" can be explained in the same way as "carrying out finite proof as program". Moreover, we suggest that Gödel's interpretation (no-counterexample interpretation) should be obtained by describing the normalization tree as functionals.

著者

佐藤 雅彦 秋吉 亮太

出版者

京都大学

雑誌

挑戦的萌芽研究

巻号頁・発行日

2016-04-01

---

述語論理を史上初めて整備し、分析哲学の源流となったフレーゲがその著書『Grundgesetze der Arithmetik』で構築した論理体系は、ヒルベルトの形式主義への道を切り拓いた極めて重要なものであったがラッセルのパラドックスを含んでいた。本研究は矛盾の根本原因を証明論的および意味論的手法により解明することを目指す。本年度はフレーゲ論理学に関して、(i)フレーゲの無矛盾性証明の分析 (ii)フレーゲの『概念記法』における記号法の分析、という二つの課題に取り組んだ。(i)については引続き、伝統的証明論の手法を適用することでフレーゲの無矛盾性証明の矛盾の原因を明らかにすべく取り組んだ。分担者である秋吉はパリ第一大学科学史・科学哲学研究所(IHPST)で、ドイツにおける伝統的証明論の手法であるΩ規則に関するレクチャーを昨年に引続き行い、パリ第一大学アルベルト・ナイーボ准教授と討論を行った。今後は、より抽象的な仕方で証明を捉えるフランス証明論の概念(具体的にはフランスのジラールによるlinear logicやludics)を用いることで,まずはΩ規則の理解を深めることを目標とすることで合意を得た。また,本研究の成果として, 2018年出版予定の著書『よくわかる哲学・思想』 (納富信留,檜垣立哉,柏端達也編, ミネルヴァ書房 ) に「論理学」の項目を執筆した。(ii)については、普遍限量子の論理的振舞いを分析するために、λ項の代数的構造を分析した。この結果、変数の概念を経由せずに、普遍限量子の導入および除去の規則を記述できることを解明した。