#### 4000OA非可述性の分析としての証明論(<特集>あたらしい数理論理学の揺籃:証明論的な順序数と集合論的な順序数)

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.

#### 2000OAゲンツェンを読む : 三つの無矛盾性証明の統一的解釈

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

50

1

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