Re: Existence of proof verifiers: A comedy

Charlie-Boo <shymathguy@xxxxxxxxx> writes:

On May 6, 4:21 am, "H. J. Sander Bruggink" <brugg...@xxxxxxxxxx>
wrote:
Charlie-Boo wrote:
On May 5, 5:09 am, "H. J. Sander Bruggink" <brugg...@xxxxxxxxxx>
wrote:
Charlie-Boo wrote:
What is a proof - how do you define proof?  And how does a list of
wffs with no natural language satisfy that definition?  (I even tell
you the 2nd question so you can change your 1st. answer to match the
2nd question.)
To quote yourself from your own infamous arXiv-paper:

   "A sequence (actually a tree) of axioms, rules and DEF, culminating
   in a sought after theorem, is a Proof."

Yes, I am reusing a standard term with a different meaning.  I should
say e.g. "For the purposes of this paper, a Formal Proof . . ."

Aah, ok, so what you're saying is that your arXiv-paper, which
you're still actively promoting, doesn't actually contain
*real* proofs? Illuminating...



And your definition of proof?

In situations where a proof is object of research,

   "a sequence of wff's such that each wff is either an instance
   of an axiom or follows from earlier wff's by the application
   of an inference rule"

No. Look up "proof" in a math dictionary.

I don't have one. What's yours say?

The point is that a proof has to show that something must be true.
That requires communication and we can only do that in natural
language. There has to be a natural language proof corresponding to
any formalism in order to have a proof. The formalism alone is not a
proof.

So e.g. if a paper contained 3,000 lines of formalisms and they say
that it proves some famous theorem, they haven't. A proof must be in
natural language, including possibly some expessions from
mathematics. It has to provide a compelling argument.

And yet all them texts in mathematical logic seem to claim that a
proof is a sequence of wffs, just as Bruggink says. Of course, an
informal argument can also count as a proof -- there is more than one
definition. But surely formal argument by themselves are called
proofs by every sensible author.

This is what Einstein said as well.

Did he? How fascinating! No greater authority on mathematical logic
than that! (Present company excepted, of course.)

--
"That's all the legacy I ever wanted, to have people remember me like
a shooting star streaking across their Life sky, illuminating, for
just one moment, unparalleled beauty unique to itself."
-- Weblogs are a particularly humble medium, unique to themselves.
.

Relevant Pages

  • Re: Existence of proof verifiers: A comedy
    ... A sequence of wffs does not do that. ... It has to be mapped into natural language. ... any formalism in order to have a proof. ...
    (sci.logic)
  • Re: Existence of proof verifiers: A comedy
    ... wffs with no natural language satisfy that definition? ...    "a sequence of wff's such that each wff is either an instance ... There has to be a natural language proof corresponding to ... any formalism in order to have a proof. ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... You have a different idea of what constitutes formalism from what ... Here A is like a natural language deductive system ... language proofs since he wants it to correspond to nature ...
    (sci.logic)
  • Re: Existence of proof verifiers: A comedy
    ... It has to be mapped into natural language. ... wffs, instead of "formal proof". ... say "Pee Vee Tilda Pee" or do you say "Pee or ... You've shown that a formal proof isn't a proof? ...
    (sci.logic)
  • Re: Formalisation
    ... as growing up from some soil and forming an ecosystem, ... it using natural language! ... faithfully those aspects of our mathematical reasoning and language we're ... DEFINED PARTS OF some formalism, IS APING a formalism (it is ...
    (sci.logic)