RESTRICTION TO CUT RULE AND THE CONSISTENCY OF A NATURAL DEDUCTION ARITHMETIC.
Technical rept. no. 1,
CASE INST OF TECH CLEVELAND OHIO
Pagination or Media Count:
In this paper, consistency of a system called S1 sub delta is proved by generalizing arguments of Schuttes 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