Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.byu.edu
Subject: Re: formal and rigorous and paper and plastic(&metal 8-))
In-Reply-To: Your message of "Mon, 14 Mar 94 16:12:12 PST." <199403150012.AA16796@aerospace.aero.org>
Date: Tue, 15 Mar 94 16:04:08 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:150280:940315160416"@cl.cam.ac.uk>


I think that general (I almost said "informal") usage blurs together "formal"
and "rigorous". As Mark wittily pointed out, there are several shades of
meaning for both of them. Would anyone admit to doing "prim" proofs?

The view that I have subconsciously absorbed about their mathematical usage
(which may be completely mistaken) is that:

  "Rigorous" means "not susceptible to rational disputation".

  "Formal" means "adhering to a certain precisely defined framework".

So, for example you might (depending on how critical you were about what
integration is) accept a little histogram picture as a *rigorous* proof that
for any positive integer N:

     N - 1                 N
     -----                 /
      \                   |
       )   ln(n)   <=     |  ln(x) dx
      /                   |
     -----               /
     n = 1               1

but you would not call it a *formal* proof unless you had some precisely
described "formal" proof system into which it fits. (I think it would be
interesting to try and produce such a geometrically-based "formal system".)

I would also say that "rigorous" carries strong positive overtones whereas
"formal" is used in both a laudatory and pejorative sense, rather as the
term "liberal" is used in US politics. Don't forget that the term "formalism"
was first used by Brouwer as a term of abuse for Hilbert's philosophy (as
he saw it).

John.