Re: Evaluation of article

Torkel Franzen wrote:
> "Charlie-Boo" <chvol@xxxxxxx> writes:
>
> > Do you believe that Floyd and Beigel (see my earlier extensive quote)
> > are using the program that I cited to prove Rosser's result?
>
> I can't comment on the paper you cite without having looked at it.

I quoted the entire Floyd/Beigel proof for you (an excerpt from their
text, Language of Machines.)

http://groups.google.com/group/sci.logic/msg/564970551af877f3

> My remark concerned your presentation, which you apparently do regard
> as a proof.

You wrote:

"> For ALL PROOFS X
> If X proves this does not halt: HALT
> If X proves this halts: LOOP

While this kind of thing can be quite entertaining and even
enlightening, it by no means amounts to a proof of the Gödel-Rosser
theorem. "

Isn't the Floyd/Beigel proof "this kind of thing"? Have you seen this
particular proof before?

> > In any case, it is a new proof that shows that Rosser's result is
> > implied by Theory of Computation results.
>
> A non-constructive proof that every consistent r.e. extension of Q i
> incomplete can indeed "easily" be given by way of recursion
> theory. Odifreddi presents it in an article "Gödel for children"
> (available on the net). Shoenfield also takes this route.

My theorem formally produces an incompleteness result for each Theory
of Computation theorem of the form "Relation R is/isn't r.e.",
including the exact results of Godel, Rosser, Smullyan and others. Do
you still think your reference does that? If so, please give the
formal derivation of 1 or more incompleteness theorems.

The problem with Smullyan's treatment (see below) is something that I
have been observing for years: many logicians need to be better
Computer Scientists. Smullyan never writes about Turing or Theory of
Computation results, instead couching everything in terms of proof
systems. Programs (Turing Machines) are equivalent to formal systems
in general, but only programs are a priori consistent: no program can
both halt yes and halt no by its very design, yet all r.e. sets are
represented.

(Actually, Rosser used the same principle in his 1936 result. A
program must be "consistent" because it stops as soon as it halts
yes or no, so there is no chance for it to both halt yes and halt no.
Rosser characterized wffs the same way: by whether its first (smallest
code number) proof proves it true or proves it false, which also cannot
be both.)

Programming languages also make is very easy to show relations to be
recursively enumerable, in a way unmatched by Logic. This has been
occurring in the literature since about the 1990's (see e.g. Automata
and Computability, Kozen 1997, pg. 233-247, or Introduction to the
Theory of Computation, Sipser 1997, pg. 192-194, or The Language of
Machines, Floyd & Beigel 1994, pg. 571-572.)

In my proof of Rosser's 1936 result, the argument begins with Theory
of Computation results:

The set of programs that halt no (refutable wffs) is r.e. while the set
of programs that don't halt yes (unprovable wffs) is not r.e. Thus
the set of refutable wffs is not the set of unprovable wffs. However,
if a system is consistent and complete, then every refutable wff is
unprovable (by consistency) and every unprovable wff is refutable (by
completeness) and the two sets must be equal. Therefore the system is
not consistent and complete - if it is consistent it is not complete,
which is Rosser's result.

I don't think even some of the readers of this forum will deny that
my proof is about an order of magnitude simpler than that published
e.g. by Smullyan or even the more modern version presented by Floyd and
Beigel.

And don't forget Occam's Razor: "It is vain to do with more what
can be done with less." and "An explanation for unknown phenomena
should first be attempted in terms of what is already known." This
is exactly what I did. (I once pointed this out and a professor
responded with, "Well, I once wrote an article advocating that
Occam's Razor is wrong." LOL I'm not surprised.)

C-B

Smullyan's proof of Rosser's 1936 theorem in Theory of Formal
Systems, page 47-48 (e = is an element of, c = is a subset of, n =
intersect, A* = the numbers N such that the Godel number of wff N with
N substituted for its one free variable is in set A, h = the Godel
number of wff H, Hx = wff H with x substituted for its free variable):

"5. Separability within Z ; Rosser's Theorems. Godel's
incompleteness theorems (in the abstract form of Theorem 2) was based
on the first diagonalization lemma. We now consider a more powerful
lemma which will yield stronger incompleteness theorems (and subsequent
undecidability theorems) due to Rosser.

Suppose W is a set of expressions of Q which is disjoint from T. By
the first diagonalization lemma we know that a sufficient condition for
the existence of a sentence which is outside both W and T is that W* be
represent able in Q. We now prove the stronger fact:

LEMMA II. (Second Diagonalization Lemma), If H represents some
superset A of W* which is disjoint from T*, then its diagonalization Hh
is outside both W and T. PROOF. Let H represent A; W* c A ; A n T* be
empty. Since H represents A, then for any number n e A <=> Hn e T.
Setting n=h, we have h e A <=> Hh e T <=> h e T*. So h e A <=> h e T*.
But A is disjoint from T*, therefore h ~e A and h ~e T*. Since h ~e A
and W* c A, then h ~e W*. Thus h ~e W* and h ~e T* - i.e., Hh ~e W and
Hh ~e T. Thus Hh is outside both W and T.

Weak separability within Z. Let A and B be disjoint sets of numbers.
We will say that A is weakly separable from B within Q iff there exists
a predicate H which represents some superset of A which is disjoint
from B such a predicate H will be said to weakly separate A from B in
the system Q. Lemma II says that if H weakly separates W* from T* in Q
then Hh is outside both W and T. Taking W to be the set R, we
immediately have:

THEOREM 4 (A rudimentary form of Rosser's theorem). A sufficient
condition for Z to be incomplete is that R* be weakly separable from T*
in Z. And if h [sic, should be H] effects this separation, then Hh is
an undecidable sentence of Z."

.

Relevant Pages