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; Wed, 24 Nov 1993 17:43:06 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03653; Wed, 24 Nov 1993 10:31:25 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.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 AA03648; Wed, 24 Nov 1993 10:31:22 -0700 Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA06931; Wed, 24 Nov 93 09:29:01 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Wed, 24 Nov 1993 17:28:42 GMT From: David Shepherd Message-Id: <2763.9311241727@frogland.inmos.co.uk> Subject: Re: Need "an undefined value", but not what you think. To: guttman@linus.mitre.org Date: Wed, 24 Nov 1993 17:27:45 +0000 (GMT) Cc: info-hol@cs.uidaho.edu (info-hol mailing list) In-Reply-To: <9311241549.AA01777@nausicaa.mitre.org> from "guttman@linus.mitre.org" at Nov 24, 93 10:49:59 am X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 714 guttman@linus.mitre.org has said: > You might alternatively consider using a different proof system such as Imps, > in which partial are handled directly. That is, 23/0 is simply undefined. An > *atomic* formula with an undefined immediate subterm is *false*, so that 23/0 = > 22/0 is false. (No "maybe" about it, though.) The logic above the level of > atomic formulas is perfectly classical. what about 23/0 = 23/0 ? -------------------------------------------------------------------------- david shepherd: des@inmos.co.uk tel: 0454-616616 x 625 inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq "you might think that --- I couldn't possibly comment"