[FOM] Disproving Godel's explanation of incompleteness

[Roger Bishop Jones]

Godel believed that:

(A).  The truth predicate of a language cannot be defined in that 
language.

and

(B).  That (A) explains the incompleteness of arithmetic.

Before I learned these facts I already had an explanation of 
incompleteness which seems to me a better one, so when I came 
across Godel's explanation (not so very long ago) I was 
skeptical about whether it was the "right" or even a "true" 
explanation.
Only today has it occurred to me that Godel's explanation can be 
disproved.

I propose to sketch here such a disproof, which consists in 
describing a language for which (A) is false, whose 
incompleteness cannot therefore be explained by (A).

The counterexample is:

	ZFC under the "provability semantics"

The "provability semantics" is as follows.
A sentence of ZFC is true iff it is provable in ZFC, false iff 
its negation is provable in ZFC (and otherwise has no truth 
value).

[Note: that this definition is a definition only of the notion of 
truth (simpliciter) of a sentence of ZFC, and no change is made 
to any other aspect of the semantics of ZFC (particularly not to 
the notion of "true under an interpretation"), or to its 
deductive system.
It can be presented alternatively as:
	True (simpliciter) <=> true in every model of ZFC

Note: also that for the purposes of this proof this semantics 
does not need to be "correct" (whatever that might mean), it 
need only be well-defined.  Perhaps it needs to be correct for a 
certain portion of the arithmetic statements in ZFC, which it 
is.
]

Conjecture:
The truth predicate for ZFC under the provability semantics
is definable in ZFC under that semantics.
Hence (A) is false for ZFC under the provability semantics.

Observation:
The incompleteness of ZFC, in the sense relevant to Godel's 
theorem on the incompleteness of arithmetic, is a purely 
syntactic property, hence even ZFC under the provability 
semantics is incomplete in this sense (though under the 
provability semantics ZFC is complete in the different sense 
that it proves all true sentences).

Conclusion: (B) is false (as well as (A))

[ a shorter disproof might be: (B) is false, because (A) is 
false, presumably you can't explain anything with a falsehood.
My use of ZFC is a bit of a distraction here, I think the whole 
thing works if you substitute PA for ZFC, though in that case 
the provability semantics is more obviously "wrong", but still 
not (IMO) wrong enough to invalidate the disproof.
I could offer a semantics for ZFC which is arguably right on the 
money (not "wrong" at all) which may also be a counterexample]

Though Godel was notoriously precise and painstaking in his work, 
I have not seen any attempt by him to make (A) precise.
Does anyone know whether he ever tried to make this claim precise 
(or showed any awareness that it might be vague or false)?

For anyone interested, here is my explanation of incompleteness:

It is part of our requirements of a formal deductive system that 
proofs in that system provide checkable tokens of truth, and 
hence that proofhood be decidable and theoremhood 
semi-decidable.
Arithmetic truth is not decidable (as shown by Turing) but a 
complete (in G's sense) deductive system for a language which 
included arithmetic would yield a decision procedure (as noted 
by Turing), hence there can be none.

Or, more briefly, formalisations of arithmetic must be incomplete 
because the truths of arthmetic are not recursively enumerable.

Proving that this is a good explanation is not so easy.

Roger Jones