FOM: Reply to Taatikainen on Chaitin and Incompleteness

[Joe Shipman]

Rattikainen:
> I strongly disagree. The easiest way is to use the notion of truth
> and show by diagonal argument that provable does not exhaust
> true. (see e.g. Smullyan's book on incompleteness).

Shipman:
> THIS IS NOT SO EASY, EXCEPT FOR SPECIALLY CHOSEN FORMAL SYSTEMS LIKE
> SMULLYAN'S WHICH ARE DESIGNED FOR SELF-REFERENCE

Raatikainen:
>RE: I am not sure if I understand this comment. I don't think that
>PA etc. are in any way specially chosen or designed for self-reference.

I was referring to "Smullyan's Easy Language For Self-reference"
("SELF") and his language of Arithmetic SAr which he used to develop
incompleteness very smoothly in J. Symb. Logic 22, no.1 (1957), 55-67.
Smullyan's development is repeated in Manin's remarkable text "A Course
in Mathematical Logic" (Springer GTM#53).  Those languages are carefully
contrived to make the proofs of Incompleteness easy, and they are not
the standard way of formalizing arithmetic (though they are reasonable
considered as formal systems, it's not difficult to use them).


Raatikainen:
> Indeed, a
> rigorous proof of Chaitin's theorem requires one to arithmetize both
> Turing machines and the syntax of the theory in question (Gödel's
> proof requires only the latter) and move back and forth between
> these two codings (no wonder so many people have got lost).

Shipman:
> WRONG.  FIRST OF ALL, ONCE YOU HAVE ARITHMETIZED TURING MACHINES YOU
DON'T
> NEED TO ARITHMETIZE SYNTAX, YOU CAN SIMPLY *PROGRAM* THE SYNTAX.

Raatikainen:
>RE: I am sorry to disagree: I submit that it makes no sense to talk
>about programming the syntax - in the context of Turing machines
>reading and writing only zeros and ones, which is the case in the
>algorithmic information theory - independently of a binary coding
>of the syntax.

I think we differ about the meaning of "arithmetize".  I am not
requiring the Turing machines to have a binary alphabet, and I am
certainly not requiring that they be formalized in a theory of
arithmetic with only + and * as operations.  ZF, or ZF-Infinity, can
*formalize* Turing machines perfectly straightforwardly, and the
Turing-machine-coding needed to make a Universal Turing Machine and get
results about the Halting Problem is MUCH easier than "arithmetizing
TM's" in the sense of representing them in Peano Arithmetic.

Shipman:
> SECONDLY,
> YOU DON'T EVEN NEED TO ARITHMETIZE TURING MACHINES TO GET
INCOMPLETENESS
> RESULTS, JUST TO GET INCOMPLETENESS FOR PEANO ARITHMETIC WHICH IS MUCH

> STRONGER.

Raatikainen:
RE: in a sense, yes (if I got your idea right - at least, if one has a
theory that is about Turing machines directly). But in order to have
interesting and generalized incompleteness results, there is no
choice.

If you admit exponentiation into your arithmetic it is very easy to
translate finite set theory into arithmetic using the enumeration of the
hereditarily finite sets "f(t)=the sum over s in t of 2^f(s)".  So you
can get generalized incompleteness results about Peano Arithmetic
augmented with exponentiation without difficulty.  It is a separate fact
that exponentiation can be represented in terms of + and *, and there
was no a priori reason to suppose that the theory of + and * was general
enough to get incompleteness (the theory of + and the theory of * are
each decidable but the proofs are hard).

Shipman:
> CHAITIN'S APPROACH VIA THE HALTING PROBLEM MAKES IT VERY EASY TO SHOW
THAT
> ANY SOUND THEORY WHICH CAN FORMALIZE THE STATEMENTS K(m)>n IS
INCOMPLETE.

Raatikainen:
RE: to repeat myself a little: in order to formalize the statements
K(m) > n" in an ordinary mathematical theory one has to
arithmetize Turing machines first.

No, you just have to *formalize* Turing machines which is easier than
arithmetizing them.  ZF certainly suffices, as do much weaker theories.
The theorems of ZF are obviously enumerable, and someone who has learned
enough about the theory of computation to understand that general
programs can be executed by a Turing machine can therefore get the
incompleteness of ZF quickly, and generalize it to PA+Exponentiation
with only a little work.

Raatikainen:
But similarly, if one just assumes that a theory can formalize
Prov(x) and Diagonalization and is sound, it is extremely easy to
prove Gödel's first theorem fo such a theorem (see e.g. pages 827-
8 of Smorynski's Handbook survey; the proof takes just 6 lines).

Yes, the hard part is formalizing Prov(x) and Diagonalization.  I claim
that for someone with any computer programming education, it is far
easier to get Prov(x) and Diagonalization by going through Turing
machines than by trying to work in PA directly.  The only thing you
sacrifice is the separate result that exponentiation is representable in
terms of + and *.

-- Joe Shipman