Re: Comparing Proofs of Rosser's 1936 Theorem

David C. Ullrich wrote:
On 19 Feb 2006 15:15:30 -0800, "Charlie-Boo" <chvol@xxxxxxx> wrote:

What is the relationship between the following two proofs of Rosser's
1936 theorem?

1. [Turing 1937] We can list the provable sentences, and by negating
each list the refutable sentences. If the system is both complete and
consistent then any given sentence will be provable or refutable but
not both, and thus will be seen in either but not both lists, and we
can tell if the given sentence is provable, which amounts to solving
the halting problem where halt yes means provable and halt no means
refutable, so halt means decidable.

2. [C-B 2005] If the system is both complete and consistent, then the
refutable sentences coincide with the unprovable sentences, but the
former is an r.e. set whereas the latter is not.

The first is written out in much more detail, perhaps
because the concepts mentioned in the second were less
well-known in 1937

These concepts (facts concerning recursivity), far from being unknown,
were formally introduced by Godel in 1931. In any case, why would the
popularity of a theorem or concept influence how much detail an author
provides for his proof? That doesn't make any sense.

If your point is that Turing simply lacked the sophistication to
develop proof # 2, then I might agree with that. However, in all
fairness, Turing lacked the benefit of computers to rigorously
formalize and fine-tune his analysis. And of course formalizing is the
whole problem. (All of these new proofs were formally generated. That
is why they are so concise.)

C-B

************************

David C. Ullrich

.

Relevant Pages

  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... [Turing 1937] We can list the provable sentences, ... not both, and thus will be seen in either but not both lists, and we ... the halting problem where halt yes means provable and halt no means ... refutable sentences coincide with the unprovable sentences, ...
    (sci.logic)
  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... David C. Ullrich wrote: ... not both, and thus will be seen in either but not both lists, and we ... refutable sentences coincide with the unprovable sentences, ... Well, you really beat me on that one, David. ...
    (sci.logic)
  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... David C. Ullrich wrote: ... not both, and thus will be seen in either but not both lists, and we ... refutable sentences coincide with the unprovable sentences, ... Well, you really beat me on that one, David. ...
    (sci.logic)
  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... It seems that Rossers achivement is, ... not both, and thus will be seen in either but not both lists, and we ... the halting problem where halt yes means provable and halt no means ... refutable sentences coincide with the unprovable sentences, ...
    (sci.logic)
  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... not both, and thus will be seen in either but not both lists, and we ... the halting problem where halt yes means provable and halt no means ... If the system is both complete and consistent, ... refutable sentences coincide with the unprovable sentences, ...
    (sci.logic)