Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! qed-owner@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 3 Aug 1993 22:26:12 +0100 Received: by antares.mcs.anl.gov id AA03624 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 3 Aug 1993 16:20:48 -0500 Received: from diamond.idbsu.edu by antares.mcs.anl.gov with SMTP id AA03615 (5.65c/IDA-1.4.4 for ); Tue, 3 Aug 1993 16:20:44 -0500 Message-Id: <199308032120.AA03615@antares.mcs.anl.gov> Received: by diamond.idbsu.edu (16.8/16.2) id AA17797; Tue, 3 Aug 93 15:21:04 -0600 Date: Tue, 3 Aug 93 15:21:04 -0600 From: Randall Holmes To: qed@mcs.anl.gov Subject: Systems Implementing All of Mathematics Sender: qed-owner@mcs.anl.gov Software capable of implementing mathematics already exists: for example, the HOL dialect of Edinburgh LCF (implementing classical type theory, basically the system of Russell's Principia Mathematica). The Nuprl project of Constable and others at Cornell has the same capabilities, although the foundational system they are using is of an unfamiliar type (constructive type theory). All of classical mathematics could be implemented in either of these systems (either has the capability of storing libraries of theorems built in). The opinions expressed | --Sincerely, above are not the "official" | M. Randall Holmes opinions of any person | Math. Dept., Boise State Univ. or institution. | holmes@math.idbsu.edu