Re: Epistemology 201: The Science of Science

mmeron_at_cars3.uchicago.edu
Date: 01/25/05 

Date: Tue, 25 Jan 2005 23:03:51 GMT

In article <QAzJd.11563$mo2.891705@news.xtra.co.nz>, "Jason" <jasonstevensNOSPAM@free.net.nz> writes:
>> >> >> 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?
>
How would you prove that a manual verification process is correct and
has been implemented correctly?

If you're asking for absolute certainty, regarding anything, you're
bound to be disappointed and, beyond some point, the quest for
certainty may become counterproductive. Engineers have a saying to
the effect that "'Perfect' is the enemy of 'good'" and it applies
here.

But, again, the computer issue is a red herring, here. There is no
qualitative difference between computer checked proofs and human
checked proofs. In both cases a non-zero probability of error exists.

>Because it has been used for centuries, it should be used today is an empirical
>reason.
>
If you want to use "empirical" as a synonym for "not absolutely
certain" then, first, this is a highly unorthodox use of the term and,
second, it is totally useless. Since, as I said, nothing is
absolutely certain, the word "empirical" as you use it applies to
everything and any term that applies to everything serves no useful
purpose.
>
>> >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.
>
Indeed. And Santa Claus doesn't really exist. So?

Mati Meron | "When you argue with a fool,
meron@cars.uchicago.edu | chances are he is doing just the same"

Relevant Pages

  • Re: Epistemology 201: The Science of Science
    ... >> apriori infinite set of possibilities to a finite one, ... If you're asking for absolute certainty, regarding anything, you're ... qualitative difference between computer checked proofs and human ... >> amount of time repeating the verification. ...
    (sci.cognitive)
  • Re: Epistemology 201: The Science of Science
    ... >> apriori infinite set of possibilities to a finite one, ... If you're asking for absolute certainty, regarding anything, you're ... qualitative difference between computer checked proofs and human ... >> amount of time repeating the verification. ...
    (sci.physics)
Quantcast