Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9403142027.AA16868@sics.se>
To: info-hol@leopard.cs.byu.edu
Cc: markaa@box.ee.cornell.edu
Subject: Re: [markaa@box.EE.CORNELL.EDU (Mark D. Aagaard): terminology: "rigor" 
         vs "formality" ?]
Date: Mon, 14 Mar 1994 21:27:11 +0100
From: Matthew Morley <mjm@sics.se>


No doubt this'll promote some lively debate on the list!

mark>So, I'm leaning towards using `rigorous' for mechanized proofs and
mark>`formal' (or `prim') for paper proofs.

Oh! Dear me, no! The distinction between formal and `rigorous' can be
recognised in the attempts of Russell and Whitehead (and their ilk) to
`formalise' mathematics -- in a *formal system*. I don't know if the
dictionaries you have checked (you looked at more than Webster's,
right?)  will tell you what a formal system is, but you mentioned one
or two already -- higher-order logic, constructive type theory,
first-order propositional logic... "a given collection of primitive
symbols (the alphabet) and axioms (basic sentences) and a collection
of inference rules by which new sentences can be inferred from the
basic ones."

I'm sure someone will pop up with a better definition. But check out
`Godel Escher Bach' (say) if you are in doubt about what formal means
in mathematical proof! (I mean Hofstader's explanations are accessible
at least.)

Formal proofs are very tedious to write down precisely because you
can't step outside the rules of the formal system -- so mathematicians
always use `informal' arguments when presenting their theorems -- that
is, they practice `rigourous' logical argument, but never formal
logical argument. (The alternative spelling for rigorous comes from
Chamber's, by the way.)

Proof tools save us from doing formal proofs by hand. These formal
symbolic -- syntactic -- manipulations are what computers excel
at. You never see the formal proof that the HOL system constructs --
you only ever see the ML program that will construct it; the same is
true of most other proof tools (exception: Imperial College's ICLE,
for example).

So please lean the other way: formal if you did it all by hand without
skipping any steps, or if you helped a proof tool to do it all without
cheating (mktheorem, etc.) but rigorous otherwise. The proof script
isn't a proof, by anyone's imagination (is it?) 

Now, when is a rigourous proof of a subtle theorem more valuable than
a formal one...? And reach for the asbestos overcoat...

Matthew

- ---------------------------------------------------------------------- -
- Matthew Morley, GMD I5-SKS, P.O. Box 1316, 53731 St. Augustin, Germany -
- Tel: (+49) 2241 14-2267 ______________________ Fax: (+49) 2241 14-2035 -
- on loan to SICS ------------------------------------------------------ -