If T is a Sigma-2-sound recursively axiomatizable extension of PA, a certain Pi-2 statement (x)(Es)F(s,x) is undecidable in T.

The significant aspect in which this result is weaker than Gödel's (for extensions of arithmetic) is that it does not prove the undecidability of a Pi-1 statement, and cannot in any obvious way be used to prove the second incompleteness theorem. However, nor does it contain anything that can clearly be called diagonalization.

The proof goes as follows. The predicate F, which is a Sigma-1 predicate given that T is recursively axiomatizable, has the form

s is a sequence (= sequence number) of length n, s₀>n, and for every i with 0<i<n, it holds that s_i>s_i-1*s_i-1, and for every i<n, s fulfills the conjunction of the first i axioms P_i of T.

We say that s is an n-sequence if the first part of this condition is satisfied, i.e. that preceding "s fulfills...". For the moment we don't need to go into the definition of "fulfills", but only note that it will be defined as a Sigma-1 predicate. It will also be seen that for every n,

(1) T proves (Es)F(s,n*)

where n* is the formal numeral with value n. So if T is Sigma-2-sound, i.e. does not prove any false Sigma-2 sentences, T does not disprove (x)(Es)F(s,x). (This follows because if T is Sigma-2-sound, (1) implies that (Es)F(s,n*) is true for every n, so (x)(Es)F(s,x) is true, so (Ex)(s)~F(s,x) is a false Sigma-2 sentence and thus not provable in T.)

To show that T does not prove (x)(Es)F(s,x), let M be a non-standard model of T. (Here we only need to assume that T is consistent.) Since (Es)F(s,n*) is true in M for every n, or in other words, M satisfies (Es)F(s,a) for every standard natural number a, there must also be a non-standard e such that M satisfies (Es)F(s,e). This is so because if (Es)F(s,x) does not hold in M for every x, there is a smallest non-standard (infinite) m such that (Es)F(s,m) does not hold in M, and then (Es)F(s,m-1) holds in M, and m-1 is also non-standard.

Now choose s so that M satisfies F(s,e)&(s')(s'<s => ~F(s',e)). Finally, let H be the substructure of M the elements of which are those a in the domain of M for which a<(s)_i for some standard natural number i. (Note that i<e holds for every such i.) This is a substructure of M because this set is closed under multiplication and addition by the definition of F. Also, M is an end extension of H, i.e. if a is in the domain of H and b<a holds in M, b is also in the domain of H.

As a consequence, H does not satisfy (Es)F(s,e). For F is a Sigma-1 predicate and is thus true in every end extension of H if it is true in H, so if H satisfies (Es)F(s,e), M will satisfy F(s',e) for an s' smaller than s.

At this point we need to invoke a further property of "fulfills" to conclude that

(2) H is a model of T.

Thus there is a model of T in which (n)(Es)F(s,n) is false, so (n)(Es)F(s,n) is not provable in T. Since ~(n)(Es)F(s,n) is not provable in T for Sigma-2-sound T, it follows that (n)(Es)F(s,n) is undecidable in T for such T.

It remains to prove (1) and (2).

To define "s fulfills A", it suffices to consider a typical case. Let A be the formula

(x1)(Ey1)(x2)(Ey2)R(x1,y1,x2,y2)

where R is a Delta-zero formula. "s fulfills A", where s is of length n, then means that

(3) for every i with 0<=i<n-2 and every x1<(s)_i there is a y1<(s)_i+1 such that for every j with i+1<j<n-2 and every x2<(s)_j there is a y2<(s)_j+1 such that R(x1,y1,x2,y2).

The general case is defined (by recursion) similarly. Informally, it is clear that "s fulfills A" is a decidable relation, and we conclude that the relation F(s,n) is Sigma-1, given that T is recursively axiomatizable.

To prove (1), we show that for every A,

PA |- A => (n)(Es)(s is an n-sequence and s fulfills A)

The proof is fully illustrated by the case of a formula (x1)(Ey1)(x2)(Ey2)R(x1,y1,x2,y2). We need to show that PA proves

(4) (x1)(Ey1)(x2)(Ey2)R(x1,y1,x2,y2) => (m)(Es1)(Es2)(Es2)(Es4)(s1>m & s2>s1*s1 & s3>s2*s2 & s4>s3*s3 & (x1<s1)(Ey1<s2)(x2<s3)(Ey2<s4)R(x1,y1,x2,y2).

Note that when the length of the sequence s is 4, only i=0,j=2 yields i and j in (3) that do not vacuously satisfy the condition.

(4) follows if we show that PA proves

(5) (a1)(Eb1)(a2)(Eb2)(x1<a1)(Ey1<b1)(x2<a2)(Ey2<b2)R(x1,y1,x2,y2).

To verify this, we note that an extension by definitions of PA proves

(6) (x1)(x2)R(x1,f1(x1),x2,f2(x1,x2))

and so b1 in (5) can be taken as any number greater than the maximum of f(x1) for x1<a1, and b2 as any number greater than the maximum of f2(x1,x2) for x1<a1 and x2<a2.

To prove (2), we need only observe that if we have an infinite s satisfying (3) in a model, we can always find, given x1, an (s)_i>x1, and thence a y1<(s)_i+1 such that for every x2 we can find j with (s)_j>x2, and hence a y2 such that R(x1,y1,x2,y2).