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).

This comment has been removed by the author.

ReplyDeleteNice post .Keep updating

ReplyDeleteArtificial Intelligence Online Training