Let's start with a definition. The language of an AFT of arithmetic is

**sufficiently expressive**if and only if:

- It can express quantification over numbers, and
- It can express every effectively decidable two-place numerical relation.

Proof sketch:Theorem 1:The set of true sentences of a sufficiently expressive language of arithmetic is not effectively enumerable.

- According to the previous post, the set K is effectively enumerable. Therefore, there is an effectively computable function f from ℕ to K that enumerates K.
- Now, consider the binary relation
*R(x,y)*that is true if and only if f(x)=y. Then, n ∈ K if and only if there exists a number x such that*R(x,n)*holds. *Since f is effectively computable, R*is effectively decidable; so, by definition, a sufficiently expressive (interpreted) language L can express*R*and the existential quantifier. Let ∃x R(x,n)*"there exists a number x such that**R(x,n)*holds."- In short: n ∈ K if and only if ∃x R(x,n) is true in L's interpretation.
- That is: n ∉ K if and only if ¬ ∃x R(x,n) is true in L's interpretation.
- If the set of true sentences of L were effectively enumerable, then we could go through and, for each formula of the form ¬ ∃x R(x,n), we could output the value of n (while skipping all of the other sentences). But this algorithm would constitute an effective enumeration of K. Since we proved that K is not effectively enumerable, the set of true sentences of L is not effectively enumerable.

The main result of this post follows easily from Theorem 1.

Let's call S1 the set of theorems of an AFT built on top of a sufficiently expressive language L. We know that S1 is effectively enumerable. But, according to theorem 1, the set S2 of the true sentences of L is not effectively enumerable. From this simple counting argument, we can infer that S1 ≠ S2. So, either some theorems are not true or some true sentences are not theorems.

If we assume that the AFT is sound, then it must be the case that S1 ⊂ S2. Therefore, there must exist at least one true sentence φ in L that is not a theorem. In addition, since φ is true, ¬ φ is false and thus cannot be a theorem either. In conclusion, neither φ nor ¬ φ is a theorem. This is a proof of:

Theorem 2:Sound AFTs of arithmetic whose language is sufficiently expressive are negation-incomplete.

Since the proof of theorem 1 does not rely on the definition of K, it seems to me that a general statement of the main idea underlying this proof by contradiction is the following:

ReplyDeleteIf the set of true sentences were effectively enumerable, then the complement of every effectively enumerable set would have to be effectively enumerable (which we know is not true).