Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 14 Jul 1994 21:07:33 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14119; Thu, 14 Jul 1994 13:57:42 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA14113; Thu, 14 Jul 1994 13:57:35 -0600 Received: from air52.larc.nasa.gov by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA07260; Thu, 14 Jul 1994 12:54:05 -0700 Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA14524; Thu, 14 Jul 94 15:54:42 -0400 Message-Id: <9407141954.AA14524@air52.larc.nasa.gov> Date: Thu, 14 Jul 94 15:54:42 -0400 From: Victor "A." Carreno To: info-hol@cs.uidaho.edu Subject: FM etiquette and accuracy Cc: vac@air16.larc.nasa.gov I would like to point out the misuse(or abuse) of a word which I keep comming across in numerous discussions and documents. I am referring to `formalization`. If I have an expression that says: All cats have four legs, this is a cat, therefore it has four legs. That *is* a formal expression. I can replace cat and four legs and preserve the truth of the statement: All x have P, this is x, therefore it has P. If I am going to represent this in HOL, the tendency is to say: "I am going to formalize the expression." Well, I am just going to represent it in a different notation. "(!x:*. P x) ==> P (y:*)" Some people get rather annoyed, and with good reason, when you tell them you are going to formalize their proof. Maybe mechanically check it is more accurate. Victor.