Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Posted-Date: Mon, 14 Mar 94 16:12:12 PST
Message-Id: <199403150012.AA16796@aerospace.aero.org>
Date: Mon, 14 Mar 94 16:12:12 PST
From: cal@aero.org
To: info-hol@leopard.cs.byu.edu
Subject: formal and rigorous and paper and plastic(&metal 8-))


notes on formal and rigorous -

matthew morley gets it right (at least as mathematicians use it) - formal
means "out of context" - i.e., that nothing except the explicitly allowed
rules can be used (anything that is not explicitly allowed is forbidden) - the
other description of formal, too mean without enumeration, is just wrong

i used to annoy my boss (who developed a proof system for an interesting and
useful version of temporal logic) by saying that "producing proofs by computer
automatically makes them less reliable" - what i meant by that is that there
are some fairly well-understood conventions about what is and is not rigorous
proof in mathematics, so any purported proof can be fairly readily checked -

however, when we start looking at proofs built by computer, there are very
different capabilities for symbol manipulation - so, for example, computer
generated proofs are MUCH harder to read and understand (and i am not talking
at _all_ about the proof of the Four-Color Theorem, which is a whole 'nother
can of worms), because they use different conventions for what they report and
for what level of abstraction they can use - so the correctness of the proof
comes down to the correctness of the program, which is problematical at best
(yes, i know, programs with a sufficiently long track record become trusted -
well, so do mathematicians *smile* and i haven't yet found a prover that i
trust without lots of careful checking of the individual proofs produced)

flames to /dev/null, please

more later,
cal