Re: Kress's Probability Trilogy Q's

George W Harris <gharrus@xxxxxxxxxxxxxx> wrote:
However, that's the process of creating the proof.
A rigorous proof is completely formal.

Which, AFAIK, means that it can be verified by a machine.

This then leads us to a very simple machine algorithm for *generating* the
proofs: generate a random string, then verify it. If it fails, start over.
If it succeeds, add it to your list of true things and go again.

It's extremely slow, to the point where it will take many times the age of
the universe to create any non-trivial result, but that's just
engineering. It's a quantitative difference, not a qualitative one.

Goedel says that this system will not generate all truths, but then again
Goedel says that humans won't be able to prove all truths either, so
there's no loss here.

Of course there's still the question of where the axioms come from. We
seem to be divided into two camps here, with all of us on one side saying
that axioms are simple things which are borne out of experience and which
have no real verification behind them, and then James on the other side
saying that axioms are universal truths and humans have some special
mechanism to pull them out of the ether.

Given that his favorite examples seem to involve Euclidian geometry, which
does not appear to actually exist anywhere within the real universe, I am
somewhat skeptical.

--
Michael Ash
Rogue Amoeba Software
.

Relevant Pages

  • Re: Deep Thoughts # 7: A New Kind of Mathematics
    ... Consider Boyer and Moore's paper, ... the idea of writing software to prove HP and generate axioms. ... They never do present a verification of what they call a formal ... Journal of the ACM foolish to publish what amounts to something less ...
    (sci.math)
  • Re: Deep Thoughts # 7: A New Kind of Mathematics
    ... Consider Boyer and Moore's paper, ... the idea of writing software to prove HP and generate axioms. ... They never do present a verification of what they call a formal ... Journal of the ACM foolish to publish what amounts to something less ...
    (sci.logic)
  • Re: Hans startling new set theory.
    ... > But then the verification process is not a verification of some ... it is a verification that the physical device indeed ... > does obey the axioms we originally posited. ...
    (sci.math)