Shutte's Consistency of Arithmetic

[Daniel Schwartz]

Dear FOM group,

In 1951 Kurt Schutte published a proof of the consistency of Arithmetic.
This proof hass ben reiterated in the appendix to the first edition of
Elliott Mendelson's "Introduction to Mathematical Logic".  The proof goes as
follows.

Starting with a first-order theory S of Arithmetic, he constructs a system
S_infinity whose axiomatization employs the Cut Rule.  He shows that
anything provable in S is also provable in S_infinity.  Then, using a system
of ordinal notations for proofs, he shows by transfinite induction that
anything provable in S_infinity is provable without using Cut.  He then
notes that, by inspecting the inference rules other than Cut, the formula
0!=0 could not be derivable unless it were already an axiom, which it isn't.
Thus, since it is not derivable in S_infinity without Cut, it is not in any
way derivable in S_infinity, so it is not derivable in S, and S is
consistent.

I'm wondering is Shutte or anyone else has published any similar proofs.

Specifically, I'm interested in other proofs that use this same approach for
establishing the underivability of other, more complex, formulas in S or
S_infinity.  I would like to know if there is a general strategy for showing
that a formula cannot be derived in S_infinity without Cut.

Thanks and best regards,

Dan Schwartz

************************************************************************
Dr. Daniel G. Schwartz                            Office    850-644-5875
Dept. of Computer Science, MC 4530                CS Dept   850-644-4029
Florida State University                          Fax       850-644-0058
Tallahassee, FL 32306-4530                        schwartz at cs.fsu.edu
U.S.A.                                   http://www.cs.fsu.edu/~schwartz
************************************************************************