Cut-Elimination Theorem Concerning a Formal System for Ramified Theory of Types Which Admits Quantifications on Types

概要

論文の詳細を見る
In 1938, Prof. K. Ono introduced a ramified theory of types, and he proved the consistency of a formal number theory with restricted induction schema by reducing the consistency of the latter theory to that of the former. In fact, he did not formulate the theory of types oneself as a formal system, but he stated methods which were named 'Erweiterungsprinzipien' and by which, when an axiom system formalized in the first-order predicate calculus is given, we can develope, in the scope of the first-order predicate calculus, various theories of types based on the given axiom system. The purpose of this paper is to formulate a ramified theory of types as a formal system, and to prove the cut-elimination theorem on that system. If an axiom system consisting of only formulae in the first-order predicate calculus is treated in that formal system, the formal theory which was named 'M^nP-Er-weiterung' of the axiom system in Ono, and which is a ramified theory of types based on the axiom system, will be essentially contained in that treatment, for every natural number n. And, as an application, we shall give a modification of Ono's consistency proof for formal number theory with restricted induction schema. In author's opinion, by this modification the essence of Prof. Ono's idea for the consistency proof will be made more clear.
科学基礎論学会の論文
1962-03-05