Extending the Cut-Free Version of the Second Incompleteness Theorem Almost to Robinson’s Arithmetic Q

Dan E. Willard

Let us recall that Robinson’s Arithmetic system Q differs from Peano Arithmetic by containing no Induction axioms [3]. In 1985, Pudlák strengthened a theorem by Bezboruah and Shepherdson [2] to show that the cut-permissive version of the Second Incompleteness (that discussed the capacities of the Hilbert-style deduction calculus) generalized from Peano Arithmetic to all possible extensions of Q.

The main gap left by the prior literature was it had not resolved to what extent the Second Incompleteness Theorem was valid for weak systems with respect to cut-free deductive methods. In particular, Adamowicz [1]) had shown that IΣ_{0} + Ω_{2} satisfied the Second Incompleteness property for semantic tableaux deduction, but it was not known how much closer to Robinson’s Arithmetic Q this result would extend.

We have obtained a partial (albeit not complete) answer to this question. Let d denote any cut-free method of deduction, such as for instance the Herbrand methodology, Semantic Tableaux, Resolution or the Cut-Free Sequent Calculus. For each such d , we have proven there exists a corresponding Π_{1} sentence, called V_{d} , such that if α is any consistent extension of Q + V_{d} then α cannot prove that the deduction-method d applied to the axiom set α is assured not to produce a proof of 0=1.

Our prior research [5, 6, 7] had documented the existence of some exceptions to the cut-free version of the Second Incompleteness Theorem when an axiom system had a capacity to prove only Addition is a total function (and it viewed Multiplication instead as a 3-way relation). The combination of this prior negative result and the new positive results, reported in the preceding paragraph, tightly complement each other.

[1] Z. Adamowicz, On The Tableaux consistency in weak theories , circulating manuscript from the Mathematics Institute of the Polish Academy of Sciences (1999).

[2] A. Bezboruah & J. Shepherdson, Gödel’s Second Incompleteness Theorem for Q , JSL 41 (1976), pp. 503–512.

[3] E. Mendelson, Introduction to Math Logic, Wadsworth-Brooks-Cole Math Series, 1987. See page 157 for Q’s definition.

[4] P. Pudlák, Cuts Consistency Statements and Interpretations, JSL 50 (1985), pp. 423–442.

[5] D. Willard, Self-Verifying Axiom Systems, Third Kurt Gödel Symp (1993), Springer-Verlag LNCS#713, pp. 325–336.

[6] D. Willard, The Tangibility Reflection Principle, Fifth Kurt Gödel Symp (1997) SpringerVerlag LNCS#1289, pp. 319-334.

[7] D. Willard, Self-Verifying Systems, the Incompleteness Theorem & Tangibility Reflection Principle, to appear in the JSL.

Address: SUNY at Albany, Computer Science Department, Albany, NY 12222, USA

E-mail: dew@cs.albany.edu