Re: Comparing Proofs of Rosser's 1936 Theorem

Charlie-Boo says...

Daryl McCullough wrote:
Charlie-Boo says...

Should proofs that use existing results copy their proofs?

If you are only interested in the *truth* of the result, then no.
If you are trying to measure the "simplicity" of a proof, then yes.

Who has ever copied the proof of an existing result into an article
(not an introductory exposition)?

Who has every claimed that a trivial consequence of an existing
result is a "proof"?

You know, people are allowed to use existing results without having
to reprove it.

Yes, if you are only interested in establishing the *truth* of
a result, then by all means use any existing results you like.
But we already knew that Rosser's theorem was true.

Are you saying that its doesn't matter if what is needed has already
been established or not?

Not for measuring "simplicity".

There is no value to reusing existing results?

Not for measuring "simplicity".

If you are making a comparison of the *simplicity* of one proof
over another, then the comparison makes no sense if you don't
take into account the complexity of proving any lemmas used.

If they have already been proven?

*Rosser's* theorem has already been proven. What is the point
of reproving it, unless (1) it's to understand for yourself
how the proof works, or (2) your proof introduces something
new---a new concept, a new proof strategy.

Do you agree with Occam?

He didn't say anything about judging the simplicity of
mathematical proofs, as far as I know.

I have a result that is a corrolary of Godel's. Now,
someone gives a 3 page proof without using Godel's
results, and points out that Godel took 10 pages, while
he took only 3 pages. Which proof is simpler?

The 3 page proof is certainly *shorter*. I would have
to look at the proofs to know which one was simpler.

--
Daryl McCullough
Ithaca, NY

.

Relevant Pages

  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... If you are only interested in the *truth* of the result, ... If you are trying to measure the "simplicity" of a proof, ... Not for measuring "simplicity". ... What constitutes a well-designed formalization? ...
    (sci.logic)
  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... Daryl McCullough wrote: ... If you are only interested in the *truth* of the result, ... If you are trying to measure the "simplicity" of a proof, ... take into account the complexity of proving any lemmas used. ...
    (sci.logic)
  • Re: Comparing Proofs of Rossers 1936 Theorem
    ... Charlie-Boo says... ... If you are only interested in the *truth* of the result, ... If you are trying to measure the "simplicity" of a proof, ... Daryl McCullough ...
    (sci.logic)
  • Re: help with Godels
    ... Daryl McCullough wrote: ... You can let absolutely any mathematical object be your zero, ... but the truth of GC certainly doesn't depend on what object ... Given *any* model M of PA whatsoever, the standard model is isomorphic ...
    (sci.logic)
  • Re: Deep Thoughts # 17: Liar Paradox is a Formal Metamathematical Theorem
    ... Daryl McCullough wrote: ... >>How else can you arrange for provability to coincide with truth in ... How else could you define system N so that provability and truth ...
    (sci.logic)