Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Sun, 7 Mar 1993 15:19:29 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA11760; Sun, 7 Mar 93 07:08:35 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA11755; Sun, 7 Mar 93 07:08:30 -0800 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Sun, 7 Mar 1993 15:08:12 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Re: Constructive logic, Nuprl and Hardware Verification In-Reply-To: Your message of Sat, 06 Mar 93 23:01:47 -0800. <9303070701.AA05638@maui.cs.ucla.edu> Date: Sun, 07 Mar 93 15:08:06 +0000 From: John Harrison Message-Id: <"swan.cl.ca.357:07.03.93.15.08.15"@cl.cam.ac.uk> Ching Tsun says: > Personally I suspect few hardware engineers (or mathematicians, for > that matter) doubt the soundness of classical reasoning. Didn't Brouwer actually think mathematics might be consistent when based on intuitionistic logic but not when based on classical logic, before his "hopes" were dashed by Glivenko(?)'s double negation interpretation? Is it easy to use something like double negation to show that, say, HOL or NuPRL with the law of the excluded middle is consistent provided the version without it is? (This is not to deny that there's more to constructivism than consistency, or that Nuprl's constructivism may be worthwhile and interesting in other respects.) John.