Re: The incompleteness theorems, Sigma-1-completeness, induction, all that


Aatu Koskensilta wrote:
In the thread "Provable in T" the incompleteness theorem and their exact
requirements - Sigma-1-completeness in particular - have been the
subject of much discussion.

Obviously I have to begin by thanking AK for being willing to
undertake a technical discussion on points I have been struggling with.
It's not like I've actually earned all this free tuition. This is a
charitable
gesture.


Tbe first incompleteness theorem is usually expressed something like the
following

For any extension T of Robinson arithmetic we can effectively find a
sentence G_T, s.t. G_T is true and undecidable in T iff T is
(1-)consistent.

Not *any* extension.
Obviously, if you extend all the way to something negation complete
(is there a canonical complete NON-standard model, the way N is
the canonical complete standard one?) then it won't be diagonalizable.

There is no such thing as G_T(N)
since N already decides everything.

One therefore should say something like "any formal extension".

In fact one really *means* "any r.e. extension".

But that, despite the fact that it is exactly what one means,
is the LAST thing one could say! It is the LEAST permissible
way of phrasing it -- BECAUSE the
Whole REASON why the theorem is
significant in the first place is that formal extensions
MUST be r.e.-but-not-recursive;
that is the conclusion the theorem is demonstrating.

But the fact that it seemed natural to phrase this without "formal"
(thereby allowing this nit to be picked) implies that more people
than just me know that the kinds of "theories" and "extensions" that
DESERVE the name ARE FORMAL theories. ARBITRARY collections
of statements that are NOT characterizable as theorems-generated-
from-axioms REALLY OUGHT to be called something else. Most of
the time, those are going to wind up being generated from models
or some other semantic structure, as opposed to being generated
syntactically (even though the output of the generation is a set
of strings).

.