Evaluation of article
Tron
Sorry, it is a Goedel again.
I just wondered if any of you cognoscenti would be so kind as to cast a
quick glance at
http://www.columbia.edu/~hg17/Diagonal-Cantor-Goedel-05.pdf
and see/say if the presentation of Goedel here is within the non-kooky
mainstream of accepted readings of G. ? I.e. not a waste of time?
TiA,
Tron
Torkel Franzen
> http://www.columbia.edu/~hg17/Diagonal-Cantor-Goedel-05.pdf
Gaifman's note is accessible and informative, and you might also want
to look at
www.andrew.cmu.edu/user/avigad/Teaching/halting.pdf
Tron
"Torkel Franzen" <tor...@sm.luth.se> skrev i melding
news:vcbek4g...@beta19.sm.ltu.se...
Thank you. I will.
Tron
Charlie-Boo
This new Gaifman paper, "The Easy Way to Godel's Proof and Related
Matters", has nothing new that I could see. That may be ok, I guess
(if that is the intent.) However, "The Easy Way" in the title
would be better served - by an easiER way - if the material were
newER.
Gaifman merely adds details to the weaker version of Godel's 1st
theorem (based on soundness), and omits the details of the
arithmetization of syntax from the stronger version (based on
w-consistency.)
The "easiest" (simplest) way to show Godel's first theorems (as
well as Rosser's, although Gaifman referred only briefly to Rosser)
that I have seen published - much simpler than Gaifman's "Easy
Way" - is in e.g. Floyd and Beigel 1994, The Language of Machines.
They prove the weaker version (Gaifman takes 2 pages including 10
expressions) by merely appealing to the existence of the following
program:
For ALL PROOFS X
If X proves this does not halt: HALT
Let G be the wff that expresses "the above program will halt".
Then G is true (the program halts) iff there is a proof X that G is
false. So G = |- ~G. Here Floyd and Beigel mistakenly cite this as
Godel's Theorem. This is actually Smullyan's Dual Form Theorem
(which appears as early as 1961 in Theory of Formal Systems) in which
the wff says (expresses) "I am refutable." Then ~G = ~ |- ~G and
letting H be ~G we have H = ~ |- H, which is Godel's construction.
Then Floyd and Beigel prove Rosser's theorem by considering the
larger program:
For ALL PROOFS X
If X proves this does not halt: HALT
If X proves this halts: LOOP
Assume our logic is complete: every sentence is provable or refutable.
Then line 2 or line 3 will be executed to their end. In line 2, this
means |-~G due to X, and G due to the HALT. But also note that since
programs and proving wffs represent the same sets, the fact that this
program halts, G, is also provable. So if it reaches the end of line 2
then |-~G and |-G, and the logic is inconsistent. Likewise if it
reaches the end of line 3, we have |-G due to X, and ~G due to the
LOOP, but more importantly |-~G (because ~G is the reaching of a point
in a program, the LOOP) and at the end of line 3 we are also
inconsistent. Thus if the logic is complete then it is inconsistent,
so if it is consistent then it is not complete, which is Rosser's
result.
The stronger version of Godel's 1st theorem (based on w-consistency)
is finessed by first proving Rosser's result, and citing this version
of Godel's 1st. theorem as somewhat of a corollary since
w-consistency implies consistency.
These published expositions are much simpler than "The Easy Way" by
Gaifman.
(If you'd like to see even easier (simpler) proofs of these theorems,
you will have to read my recent posts to this forum.)
C-B
> TiA,
>
> Tron
Torkel Franzen
> Then Floyd and Beigel prove Rosser's theorem by considering the
> larger program:
>
> 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.
Tron
Thank you. Way above and beyond. Much appreciated.
"Charlie-Boo" <ch...@aol.com> skrev i melding
news:1134639163.4...@g49g2000cwa.googlegroups.com...
> Tron wrote:
>> Hi,
>>
>> Sorry, it is a Goedel again.
>> I just wondered if any of you cognoscenti would be so kind as to cast a
>> quick glance at
>>
>> http://www.columbia.edu/~hg17/Diagonal-Cantor-Goedel-05.pdf
>>
>> and see/say if the presentation of Goedel here is within the non-kooky
>> mainstream of accepted readings of G. ? I.e. not a waste of time?
>
> This new Gaifman paper, "The Easy Way to Godel's Proof and Related
> Matters", has nothing new that I could see.
Lots of new stuff to me, though.
My main interest is that he works up to less and less formalized systems.
Thanks again.
T
Tron
"Torkel Franzen" <tor...@sm.luth.se> skrev i melding
news:vcbslsu...@beta19.sm.ltu.se...
I'll keep that caveat in mind, but at my present stage,
I'm very glad to find illustrations and expositions.
T
Charlie-Boo
At what point is the proof not valid?
Out of curiosity, do you think that Floyd and Beigel (see below)
present this program and its accompanying reasoning as being such a
proof?
C-B
Floyd and Beigel, The Language of Machines, 1994, page 571:
"Theorem 8.13 (Rosser's Version of Godel's Incompleteness
Theorem) Assume that the axioms of arithmetic are consistent. Then
there is an arithmetic statement W such that W is true, W is not a
theorem, and ~W is not a theorem.
Proof: Using the recursion theorem for 2-counter machines, we define a
2-CM program P that behaves as follows:
for i := 1 to oo do begin
if i encodes a proof that P halts, then go into an infinite loop ;
if i encodes a proof that P does not halt, then halt;
end
By construction P halts if and only if there is a proof i that P does
not halt such that i is less than any proof that P does halt. Let W be
the statement "P does not halt." Therefore,
~W <=> there is a proof of W that is less than any proof of ~W. (8.2)
Assume for the sake of contradiction that there is a proof of W or a
proof of ~W. Let the minimum such proof be i. We consider two cases.
Case 1: i a proof of W. Because i is minimal, 0, . . . , i-1 are not
proofs of ~W. By definition of proof, i cannot prove more than one
statement, so i is not a proof of ~W. We can prove ~W from (8.2) by
mechanically verifying that i is a proof of W and that 0, . . . , i are
not proofs of ~W. But then ~W is provable, contradicting consistency.
Case 2: i is a proof of ~W. Because i is minimal, 0, . . . , i-1 are
not proofs of W. We can prove W from (8.2) by mechanically verifying
that i is a proof of ~W and that 0, . . . , i-1 are not proofs of W.
But then W is provable, contradicting consistency.
In either case, we obtain a contradiction. Therefore there is no proof
of W and there is no proof of ~W. Since there is no proof of W, by
(8.2) W must be true. qed"
Charlie-Boo
Don't give up so fast on believing in Floyd and Beigel. Proving
theorems from the Theory of Computation and in Logic often uses a
program to illustrate that a particular relation is recursively
enumerable.
Along that vein, here's a little puzzle: Write a short, simple
program that proves Turing's 1937 theorem, the Unsolvability of the
Halting Problem. It can be done much simpler than the standard
(published) exposition that alters the purported solution and then
feeds the resulting program into itself. It can be shown with a
single, simple, self-contained program.
C-B
> T
Torkel Franzen
> At what point is the proof not valid?
I take it you're not actually putting forward the argument you
presented as a proof of anything? If you have in mind some simple
proof of Rosser's strengthening of the first incompleteness theorem
applied to extensions of PA or of Q, what is it? Please provide
sufficient detail to make it possible to judge the simplicity of the
proof, including, if you have the stuff quoted in your present message
in mind, a proof of the recursion theorem for 2-counter machines. Also
indicate in what respects this proof is simpler than, say, the proof
in Smullyan's book.
Charlie-Boo
> "Charlie-Boo" <ch...@aol.com> writes:
>
> > At what point is the proof not valid?
>
> I take it you're not actually putting forward the argument you
> presented as a proof of anything?
Not so. I gave proofs of three Godel and Rosser theorems. It is a
simplification of the Floyd/Beigel proofs. (I assume that any program
reaching a given point is an r.e. relation, rather than explaining in
detail how one could prove it occurs when it does in the given
program.)
Do you believe that Floyd and Beigel (see my earlier extensive quote)
are using the program that I cited to prove Rosser's result? You
wrote, "it by no means amounts to a proof of the Gödel-Rosser
theorem". In that case, either Floyd and Beigel are wrong, or they
aren't presenting this program as being part of a proof. Which is
it?
> If you have in mind some simple
> proof of Rosser's strengthening of the first incompleteness theorem
> applied to extensions of PA or of Q, what is it?
My simplification of the Floyd/Beigel proof is certainly simpler than
the Gaifman proofs.
If you are referring to my comment, "If you'd like to see even easier
(simpler) proofs of these theorems, you will have to read my recent
posts to this forum", see:
http://groups.google.com/group/sci.logic/msg/d46df7d65ea596dd?dmode=source
> Please provide
> sufficient detail to make it possible to judge the simplicity of the
> proof, including, if you have the stuff quoted in your present message
> in mind, a proof of the recursion theorem for 2-counter machines. Also
> indicate in what respects this proof is simpler than, say, the proof
> in Smullyan's book.
I'm not sure which proof you're referring to, but none of
Smullyan's treatments of Rosser's result (or any other authors I
have ever seen) is any where near as simple as mine above (copied
below.)
In Smullyan's Theory of Formal Systems, Rosser's result is proven on
pages 47-48 and requires about 10 deductive steps involving numerous
logical expressions. My proof below takes only 1 paragraph of about 5
steps and uses no complex expressions! I accomplish that by borrowing
heavily from Theory of Computation results.
In any case, it is a new proof that shows that Rosser's result is
implied by Theory of Computation results.
C-B
On 11-11-05 I wrote:
"If PA is consistent then PA-undecidable propositions do exist.
Suppose otherwise. Then PA is consistent and there are no
PA-undecidable propositions - all PA propositions are PA-decidable.
Then provable propositions are not refutable (by consistency), and
unprovable propositions are refutable (by decidability.) Then
unprovable propositions coincide with refutable ones. But the set of
refutable propositions is recursively enumerable, while the set of
unprovable propositions is not, and there is a contradiction."
Torkel Franzen
> 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.
My remark concerned your presentation, which you apparently do regard
as a proof.
> 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.
Charlie-Boo
> "Charlie-Boo" <ch...@aol.com> 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."
Torkel Franzen
> I quoted the entire Floyd/Beigel proof for you (an excerpt from their
> text, Language of Machines.)
Far from it. You didn't even formulate, let alone prove, the
recursion theorem for 2-counter machines, or even define the class
of 2-counter machines.
> Isn't the Floyd/Beigel proof "this kind of thing"?
As to that I can't say, not being acquainted with their presentation.
In referring to Smullyan, I had in mind his book "Gödel's
incompleteness theorems".
Charlie-Boo
> "Charlie-Boo" <ch...@aol.com> writes:
> > I quoted the entire Floyd/Beigel proof for you (an excerpt from their
> > text, Language of Machines.)
>
> Far from it. You didn't even formulate, let alone prove, the
> recursion theorem for 2-counter machines, or even define the class
> of 2-counter machines.
The question was: "Do you believe that Floyd and Beigel (see my
earlier extensive quote) are using the program that I cited to prove
Rosser's result?" What difference does it make how they proved the
Recursion Theorem or defined their base of computing?
In fact, 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. "
without seeing the proof of the recursion theorem (the base of
computing doesn't matter) or that 2-counter machines are Turing
complete.
Why? Because the question has nothing to do with these well-known
results. It concerns only the use of the program that you quoted -
"this kind of thing." What were you referring to by "this kind
of thing"?
I quote a proof using a program and you say "this kind of thing"
isn't a proof. I point out that Floyd and Beigel use "this kind of
thing" and you say that you can't tell. But I quoted their proof,
including the program and their use of it. Isn't the program above
(from their proof) the same program that I used?
C-B
Torkel Franzen
> What were you referring to by "this kind of thing"?
The kind of argument you presented.
> But I quoted their proof, including the program and their use of it.
It would be rash indeed to draw any conclusion about the proofs in their
book from your presentation.
Charlie-Boo
> "Charlie-Boo" <ch...@aol.com> writes:
>
> > What were you referring to by "this kind of thing"?
>
> The kind of argument you presented.
What kind is that? All you quoted was the program. Did you mean
proofs that use a program like that?
> > But I quoted their proof, including the program and their use of it.
>
> It would be rash indeed to draw any conclusion about the proofs in their
> book from your presentation.
What does my presentation have to do with commenting on their book? My
question is regarding their book only.
1. I showed a proof that used a program.
2. You quoted the program and said "this kind of thing" isn't a proof.
3. I pointed out Floyd & Beigel's use of a program and ask if they are
in fact using a program.
4. You say you can't tell because I didn't give their proof, then
because I didn't include a trivial theorem that has nothing to do with
whether or not they are using a program, and then because my making a
presentation somehow interfers with your commenting on their book.
Why can't you simply say whether or not they are using a program in
their proof? (Obviously they are.) Either they're wrong (programs
can't be used in proofs that way) or you were wrong (programs can be
used in proofs that way.) Which is it?
C-B
Torkel Franzen
> What kind is that?
The kind of argument that you put forward in your posting.
> My question is regarding their book only.
I can't comment on the book without having seen it.
Charlie-Boo
> "Charlie-Boo" <ch...@aol.com> writes:
>
> > What kind is that?
>
> The kind of argument that you put forward in your posting.
What property of the argument are you referring to?
> > My question is regarding their book only.
>
> I can't comment on the book without having seen it.
Does the passage below use a program to prove a theorem?
C-B
PASSAGE BELOW:
Torkel Franzen
> What property of the argument are you referring to?
Its woolly handwaving, lack of definitions, failure to provide, even
informally, justification at essential points.
> Does the passage below use a program to prove a theorem?
I couldn't say without studying it in context, but unlike your
rambling, it introduces a Rosser sentence and makes general sense.
Charlie-Boo
> "Charlie-Boo" writes:
> > What property of the argument are you referring to?
>
> Its woolly handwaving, lack of definitions, failure to provide, even
> informally, justification at essential points.
When I presented my proof using a program, you quoted the program and
said, "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"
How could something with "woolly handwaving, lack of definitions,
failure to provide, even informally, justification at essential
points" and "rambling, doesn't make sense" be enlightening?
Which parts are wolly handwaving?
What definitions are lacking?
What essential points are unjustified?
> > Does the passage below use a program to prove a theorem?
> I couldn't say without studying it in context,
If this passage did use a program, how could the rest of the context
cause this passage to not use a program?
They say very plainly, "We define a 2-CM program P that behaves as
follows: for i := 1 to oo do begin if i encodes a proof that P halts,
then go into an infinite loop ; if i encodes a proof that P does not
halt, then halt; end".
Don't you see the reference to "program P"?
> but unlike your rambling, it introduces a Rosser sentence and makes general sense.
What is the Rosser sentence that they introduce that I don't?
When I asked if Floyd & Beigel were using a program (as I do), you
repeatedly declined to answer, saying, "It would be rash indeed to
draw any conclusion about the proofs in their book from your
presentation." and "I can't comment on the book without having seen
it."
However, now in the midst of your criticism of my proof, you praise
them and conclude that they introduce a Rosser sentence and make sense.
Isn't that inconsistent with your earlier statement that it would be
rash to draw any conclusions concerning their proof and you are unable
to comment on it?
In other words, on the topic of similarities between Floyd/Beigel and
my proof, you say that you aren't able to make any comments or draw any
conclusions about what their proof contains. But when the topic is
differences between them and my proof, you have plenty to say: their
proof is not rambling, it uses a Rosser sentence and makes sense.
Why the big difference?
If you can see that they use a Rosser sentence, why don't you see
whether or not they use a program?
Which parts are rambling?
Which parts don't make sense?
C-B
BTW When you say that what someone wrote makes no sense, you are saying
that they are insane or severely mentally retarded. While you can
express any opinion that you wish, I don't think many people would
honestly believe that.
Torkel Franzen
> Which parts are wolly handwaving?
> What definitions are lacking?
> What essential points are unjustified?
These are good questions, and I believe you can only appreciate the
answers by working them out for yourself.
Charlie-Boo
So many criticisms and no answers or substantiation.
The most important question was: What is the Rosser sentence that they
introduce that I don't?
C-B
Torkel Franzen
Charlie-Boo
You said, "unlike your rambling, it introduces a Rosser sentence"
What is their Rosser sentence?
C-B
Torkel Franzen
> You said, "unlike your rambling, it introduces a Rosser sentence"
> What is their Rosser sentence?
A question that you may profitably answer yourself.
Charlie-Boo
Ok, here's the answer: Your statement is wrong. For you to say that
they introduced a Rosser sentence and I didn't shows you don't
understand Rosser's proof. Your answer to this question would
illustrate that. In fact, it suggests that you didn't understand most
of our conversation.
Answer the question and I'll explain in detail.
Anybody who goes on and on talking about something, then is unable to
answer simple questions - about their very own assertions - obviously
isn't up to par.
C-B
Torkel Franzen
> Ok, here's the answer: Your statement is wrong.
You must of course decide for yourself what answer to decide on.
Charlie-Boo
> "Charlie-Boo" writes:
> > Ok, here's the answer: Your statement is wrong.
> You must of course decide for yourself what answer to decide on.
And then decide on it? Ok:
RSNIM(x) : "x is a Rosser sentence in their proof and not in mine"
SUBJ : "the subject of the entire discussion between C-B and TF"
Thm. There is no Rosser sentence in their proof and not in mine.
Proof 1.
1. (eA)RSNIM(A) => |-(eA)RSNIM(A) Since RSNIM is recursive
2. ~|-(eA)RSNIM(A) TF is unable to substantiate his claim
that there is a Rosser sentence in
their proof and not in mine.
3. ~(eA)RSNIM(A) Modus Tollens
qed
Proof 2.
1. SUBJ => ~(eA)RSNIM(A) The subject of the entire discussion
between C-B and TF refutes there
being a Rosser sentence in their
proof and not mine.
2. SUBJ The subject of the entire discussion
between C-B and TF is true.
3. ~(eA)RSNIM(A) Modus Ponens
Corollary: TF doesn't understand Rosser's proof.
Corollary: TF didn't understand the subject of the entire discussion.
Corollary: TF has no idea what the Rosser sentence is in either proof.
C-B
Torkel Franzen
> Corollary: TF doesn't understand Rosser's proof.
> Corollary: TF didn't understand the subject of the entire discussion.
> Corollary: TF has no idea what the Rosser sentence is in either proof.
Everything is settled to your satisfaction, then!
Charlie-Boo
Always has been. What we have been discussing all this time is the
Rosser sentence that you now say doesn't exist.
C-B
Charlie-Boo
I think I know why you repeatedly refuse to answer this simple question
to substantiate your claim. You really don't understand Rosser's
proof. You don't give it in either of your texts on the subject:
In your "Godel's Theorem" (2005) you give (pg. 43) only an
informal description of the theorem and no proof. In your
"Inexhaustibility" (2004) you explicitly state (pg.177) that you
haven't included it: "Rosser proved a strengthening of the
incompleteness theorem. This we will set aside."
420 pages and no room for the proof that is stronger than the subject
of the books? I don't even see a proof of the stronger version of
Godel's 1st. Incompleteness Theorem (based on w-consistency) given by
Godel himself.
Nor do you even mention the computability based version that has been
in print since at least 1994 ("The Language of Machines", Floyd &
Breigel) that I have been trying to explain to you - despite your
chapters on Turing Machines.
If all of this is too complex for you to fathom, I'll do you a little
favor. You can use the ultra-simple proof that I recently devised (in
brief, if a system is consistent and complete, the disprovable wffs are
the unprovable wffs, but the former is recursively enumerable while the
latter is not.) Just spell my name right.
C-B
Torkel Franzen
> I think I know why you repeatedly refuse to answer this simple question
> to substantiate your claim. You really don't understand Rosser's
> proof.
Ah, you've found me out.
Charlie-Boo
Otherwise you obviously would have included it in your 2 books on the
subject. Your only response is sarcasm. (I had nothing to do with
your writing of these books, so you can't blame me!)
You're starting to sound like Gregory Chaitin. He's been writing about
"improving" Godel's Theorem for 40 years without ever mentioning
w-consistency or Rosser's improvement.
C-B