Re: Epistemology 201: The Science of Science

From: Jason (jasonstevensNOSPAM_at_free.net.nz)
Date: 01/25/05 

Date: Wed, 26 Jan 2005 11:19:28 +1300

> >> >> A proof is a proof (in mathematics) solely through the logical
> >> >> mechanisms that enables one step of the proof to be infered from an
> >> >> earlier step or steps. A rigorous proof is strictly formal, even if non
> >> >> formal means were used to discover it. Distinguish between discovery and
> >> >> justification. Discovery can be very empirical and heuristic, but
> >> >> justification (actual proof) is formal.
> >> >
> >> >Maths as a formal system is incomplete, so some statements cannot be
proven
> >as
> >> >derivations from the axioms. Some of these statements are true or false
> >under
> >> >the standard interpretation of the language of mathematics. In these
cases,
> >> >discovery IS justification. Proof is empirical:
> >> >
> >> >The four colour map problem was finally 'proved' by computer. That is,
every
> >> >possible combination of neighbouring map shapes were tried and tested.
This
> >is
> >> >empirical. There is (or at least was at the time) no know formal method
to
> >> >prove it.
> >> >
> >> Oh, you miss the key thing here. A priori, the number of possible
> >> combinations is infinite. It was only *after* you had a proof that
> >> any of these combinations is equivalent to one from a smaller, finite
> >> set, that you could go and check the combinations in this finite set,
> >> one by one. Absent the proof, and yes, it was a formal proof, you
> >> could run all the computers in the world for eternity, getting
> >> nowhere.
> >>
> >> So, yes, there most certainly *was* a formal method to prove it,
> >> consisting of reducing the problem to a finite number of cases.
> >
> >They key to the proof being empirical is that a computer is used.
>
> Nope. The key to the proof above is the step where you reduce the
> apriori infinite set of possibilities to a finite one, at which point
> the individual cases can be enumerated and checked one by one. This is a
> standard technique used in math for centuries. Now, would the finite
> set consist of just few or, at most, few dozen cases, you could've
> checked them by hand. Since the number, though finite, is still
> rather large, you use a computer. The computer here is not a "key",
> just a time saving device. That's all.

How to you prove that an algoritm is correct and that it has been implemented
and carried out correctly?

Because it has been used for centuries, it should be used today is an empirical
reason.

> >
> >My contention is not that the four colour problem is not formally provable.
It
> >may well be by someone with a lot of time on their hands. But unless the
> >referees are prepared to spend the same amount of time, then they can only
> >appeal to a computer proof.
> >
> And if you take a proof aof a problem which reduces to few hundred
> cases, with somebody checking them manually one by one, then you can
> either believe that he made no error in checking or spend the same
> amount of time repeating the verification. And even if, after
> spending all the time needed, you got the same result, there is still
> a non-zero (though very small) probability that the original checker
> made an error in some place and you just happened to repeat same
> error. This doesn't make it "empirical".

It does, or at least did, to some mathematicians. We hold on to this
mathematical ideal as if it actually happens. The history of maths is full of
bogus proofs.

Relevant Pages

  • Re: Epistemology 201: The Science of Science
    ... Absent the proof, and yes, it was a formal proof, you ... amount of time repeating the verification. ... a non-zero probability that the original checker ...
    (sci.math)
  • Re: Epistemology 201: The Science of Science
    ... Absent the proof, and yes, it was a formal proof, you ... amount of time repeating the verification. ... a non-zero probability that the original checker ...
    (sci.cognitive)
  • Re: Epistemology 201: The Science of Science
    ... Absent the proof, and yes, it was a formal proof, you ... amount of time repeating the verification. ... a non-zero probability that the original checker ...
    (sci.physics)
  • Re: Epistemology 201: The Science of Science
    ... >>My contention is not that the four colour problem is not formally provable. ... > amount of time repeating the verification. ... > a non-zero probability that the original checker ...
    (sci.physics)
  • Re: Epistemology 201: The Science of Science
    ... >>My contention is not that the four colour problem is not formally provable. ... > amount of time repeating the verification. ... > a non-zero probability that the original checker ...
    (sci.cognitive)