Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9403151921.AA03909@switha.dcs.gla.ac.uk>
To: John Harrison <John.Harrison@cl.cam.ac.uk>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: formal and rigorous and paper and plastic(&metal 8-))
In-Reply-To: Your message of "Tue, 15 Mar 94 16:04:08 GMT." <"swan.cl.cam.:150280:940315160416"@cl.cam.ac.uk>
Date: Tue, 15 Mar 94 19:21:07 +0000


One of my favorite definitions of "formal" is Carnap's (who
really ought to know):

  "A theory, a rule, a definition, or the like is to be called
  _formal_ when no reference is made in it either to the meaning
  of the symbols (for example, the words) or to the sense of the
  expressions (e.g. the sentences), but simply and solely to the
  kinds and order of the symbols from which the expressions are
  constructed".  [Carnap, The Logical Syntax of Language]

Another useful bit of reading is the section on "Formalism" in
Quine's "Quiddities".  In keeping with the above (and some of
the previous remarks in this thread) Quine defines formalism as
disinterpretation - i.e. formulating purely in terms of
syntactic manipulation.  Quine goes on to say:

  "Ironically, though formalism is the ultimate in disinterpretation,
  it spares us the need of disinterpreting.  Once the allowable moves
  in a deduction are stipulated in aseptically typographic terms, we
  are free to luxuriate in the full meaning of the logical and 
  mathematical expressions we are manipulating; there is no longer
  the danger that the meanings will affect the deduction."

Following this usage, by the way, I don't believe things admit
to "degrees" of formality - something is either formal or not.
On the other hand, one may choose to treat only *parts* of a
problem formally.

As for "rigour", this is a more slippery concept.  Some interesting
reading is Lakatos's "Proofs and Refutations" -- see secton 5 of
Chapter 1, for example. Rigour is related to the idea of there being
no "gaps" in a proof or impreciseness in the uderlying definitions.

Tom