Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP) id <11064-0@swan.cl.cam.ac.uk>; Thu, 15 Aug 1991 17:13:44 +0100 Received: from linus.mitre.org by ted.cs.uidaho.edu (15.11/1.34) id AA06637; Thu, 15 Aug 91 09:01:33 pdt Received: from malabar.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA09058; Thu, 15 Aug 91 12:01:51 -0400 Full-Name: Joshua D. Guttman Posted-Date: Thu, 15 Aug 91 12:01:51 -0400 Received: by malabar.mitre.org (5.61/RCF-4C) id AA02335; Thu, 15 Aug 91 12:01:51 -0400 Date: Thu, 15 Aug 91 12:01:51 -0400 From: guttman@org.mitre.linus Message-Id: <9108151601.AA02335@malabar.mitre.org> To: info-hol@edu.uidaho.cs.ted Cc: Rob Arthan In-Reply-To: Rob Arthan's message of Tue, 13 Aug 1991 21:05:07 GMT Subject: Choice Postal-Address: MITRE, Mail Stop A156 \\ Burlington Rd. \\ Bedford, MA 01730 Rob, I suppose that the point I made in response to Ian too probably makes it clearer what was on my mind. It was that @ should probably be thought of as a *non-logical constant* that happens to be present in every language of interest to the HOL user. Similarly, the axiom of infinity is a *non-logical axiom* that happens to be present in every theory of interest to the HOL user. That pre-empts my complaints about its semantics when construed as a logical operator. Josh Rob-- I sent a message to you on 2 Aug, which I suspect never reached you. There must be something wrong with our local mailer (or was previously). If you would like to see a copy, please send me an alternative address, such as a path through uunet.uu.net. Sorry about the apparent non-response.