Restriction to Cut Rule and the Consistency of a Natural Deduction Arithmetic

摘要

In this paper, consistency of a system called S1 sub delta is proved by generalizing arguments of Schutte's paper (Math. Ann. 122: 369-389, 1957) to prove that proofs in that system need use cut only when one premise is an induction axiom. Consistency follows quickly from this fact since it means that a quantifier-free theorem has a quantifier-free proof and, hence, a false prime formula like 0 = 1 is unprov able in the system under study. However, since this system uses a set of axioms which is productive (a productive complement of a recursively enumerable set) it is not a formal system in the usually accepted sense, and its metamathematics cannot be formalized in the more usual formal systems for arithmetic. (Author)