Relationship between first and second incompleteness theorems

Question

By my understanding, Gödel's first incompleteness theorem says that any theory with sufficient¹ interpretability strength is essentially incomplete, that is, any consistent recursively enumerable extension of the theory must be incomplete.

Meanwhile, the second theorem says that any theory with sufficient² interpretability strength can formulate, but not prove, a statement of its own consistency (and this is also true for any consistent, recursively enumerable extension of the theory).

Obviously, any theory satisfying the second theorem must also satisfy the first. But what about the converse: are there (consistent, recursively enumerable) essentially incomplete theories which can prove a statement equivalent to their own consistency, or which cannot formulate such a statement?

Answer 1

It is possible to construct first-order theories which prove their own consistency (and which are incomplete). Here is one example.

Consider a first-order theory with equality with a constant symbol 0 (zero), a unary predicate symbol N (the natural numbers), and a binary predicate symbol σ (the sequential relationship). Make the usual Peano Axiom assumptions, with the exception that one does not assume that σ is a total function, i.e. one does not assume that, for every natural number, there exists a natural number which is its successor. That is, it assumes every axiom in the following list except PA3:

(PA1) Ν0

(PA2) ∀n∀m ( Νn & σn,m ⇒ Νm )

(PA3) ∀n ( Νn ⇒ ∃m σn,m )

(PA4) ∀n∀m∀m' ( Νn & σn,m & σn,m' ⇒ m = m' )

(PA5) ∀n∀m∀n' ( Νn & Νn' & σn,m & σn',m ⇒ n = n' )

(PA6) ∀n ( Νn ⇒ ¬ σn,0 )

(PA7) Induction schema. Let φ be a well-formed formula where m does not occur and n is not a bound variable. Suppose φ[0\n] and ∀n∀m ( Νn & σn,m & φ ⇒ φ[m\n] ). Then ∀n ( Νn ⇒ φ ).

Now add a 3-ary symbol ∂. ∂f,x,n can be thought of as meaning that f is a sequence whose nth term is x. Make four assumptions about ∂:

(SEQ1) ∀x ( Nx ⇒ ∃f ∀i∀y (∂f,i,y ⇔ i = 0 & y = x) )

(SEQ2) ∀f ∀n∀m∀x ( ∂f,m,x & Nn & σn,m ⇒ ∃y ∂f,n,y )

(SEQ3) ∀f ∀n∀m∀x∀y ( ∂f,n,x & Ny & Nm & σn,m ⇒ ∃g ( ∂g,m,y & ∀i(¬ i = m ⇒ ∀z(∂f,i,z⇔∂g,i,z)) ) )

(SEQ4) ∀f∀i∀x∀y ( ∂f,i,x & ∂f,i,y ⇒ x = y )

Call this theory fpa. The most important thing to take away from fpa is that its ontological assumptions about the naturals are downward. That is, if a natural number n exists, then one can prove that all natural numbers less than n exist and have all the normal properties, but not that any number greater than n exists. As to sequences, if a natural number n exists, one can prove that there is a sequence from 0 to n but not any longer, and all properties of sequences and subsequences up to length n hold.

It is easy to define addition and multiplication formulas which have all the usual properties, with the exception of totality. E.g. one can prove commutativity of addition

+(x,y,z) ⇒ +(y,x,z)

even though one can't prove, given x and y, that there exists such a z.

Continue in this way. Define a predicate one(x) to abbreviate Nx & σ0,x. Again, one can prove all the usual properties of 1 except that it exists. Define two(x) and so forth.

Prove simple facts about sequences, in particular what it means for h to be the concatenation of f and g. Again, remark that given f and g, one cannot prove that h exists.

Now provide some Godel numbering for your system. Say use one(x) to represent left-parenthesis and two(x) to represent right-parenthesis and so forth. variable(x) can be defined by ∃y (ten(y) & x > y). (I haven't said how to define > but it's defined in the obvious way.)

A string, a formula, and a proof are just sequences of symbols. You can define what it means to be a term, an atomic wff (it's a particular kind of sequence), and then a wff (another particular kind of sequence). Eventually you can define the particular sequences which are proofs. That is, Proof(s) will state that sequence s represents a proof (as usual one will not be able to prove that there exists a sequence which is a proof). Finally, define the consistency of fpa as the wff Cons asserting the non-existence of a proof of the wff ¬ 0 = 0.

One proves Cons as follows. Suppose there exists a sequence-proof of the contradiction ¬ 0 = 0. But fpa can be modeled by a model of a single element, 0. For atomic wffs Nt, ∂f,t,u, and t = u assign the value of true. For atomic wffs St,u assign the value false. Continue in the obvious way. For instance a wff equivalent to ∀x(W) gets assigned the value that W has. Then one can prove that every wff gets assigned one and only one value (true or false), all the axioms will be assigned true, and that Modus Ponens and Generalization preserve truth. Hence, one can prove that every step in any proof in fpa must be true. But ¬ 0 = 0 is assigned the value false. This is a contradiction. Hence there does not exist a sequence-proof of a contradiction, i.e. fpa is consistent. But one has proved this in fpa, i.e. fpa has proved its own consistency.