Non-constructive Proofs of a Metamathematical Theorem Concerning the Consistency of Analysis and its Extension

スポンサーリンク

概要

• 論文の詳細を見る

• In this paper we shall treat the following theorem, and to which we shall give three proofs : THEOREM. Let A be a formula in the predicate calculus of 1st order. If A is provable in the type-logic, that is, in the predicate calculus of ωth order, then it it also provable in the predicate calculus of 1st order. First, S. Seki obtained a proof of the theorem by applying Godel's completeness theorem. In the next, S. Maehara obtained the second proof by using the so-called Lindenbaum algebra. And, T. Nishimura obtained the third proof and an extension of the theorem by utilizing Schutte's idea. This theorem means : If a system of axioms is consistent in the predicate calculus of 1st order, then it is also consistent in the type logic. On the other hand, it is well-known that, in the predicate calculus of 1st order, the natural number theory of some kind is consistent. Therefore, our theorem implies that a considerably large part of analysis is also consistent. But it should be remarked that none of our proofs is finitary. Prof. G. Takeuti extended Gentzen's LK to a type-logic, and called his system GLC. He calls the next statement the fundamental conjecture of GLC : G. Gentzen's cut-elimination theorem holds in GLC. That is, if a sequent in GLC is provable, then it is also provable without cut. It should be interesting and important to know whether or not the conjecture is affirmative. But it is remained open up to now. Our theorem implies that a special case of the conjecture is yes. That is, if a sequent in LK is provable in GLC, then by our theorem it should be also provable in LK. Therefore it should be provable without cut by Gentzen's cut-elimination theorem. This paper is divided into three chapters, each of which contains one of our proofs of the theorem. They are written by S. Seki, S. Maehara and T. Nishimura respectively.

• 科学基礎論学会の論文
• 1960-03-31

著者

• Maehara Shoji

  Waseda University

• NISHIMURA TOSHIO

  Hosei University

• SEKI SETSUYA

  St. Paul's University

• Seki Setsuya

  St. Paul's University

関連論文

• Non-constructive Proofs of a Metamathematical Theorem Concerning the Consistency of Analysis and its Extension
• Cut-Elimination Theorem Concerning a Formal System for Ramified Theory of Types Which Admits Quantifications on Types
• General Recursive Functions in the Number-Theoretic Formal System
• The Consistency and the Impredicative Statement

スポンサーリンク