Systems Implementing All of Mathematics

• Mail folder: QED
• Next message: Zdzislaw Meglicki: "Re: from idea to project"
• Previous message: jt@linus.mitre.org: "Re: from idea to project "

Message-id: <199308032120.AA03615@antares.mcs.anl.gov>
Date: Tue, 3 Aug 93 15:21:04 -0600
From: Randall Holmes <holmes@diamond.idbsu.edu>
To: qed@mcs.anl.gov
Subject: Systems Implementing All of Mathematics
Sender: qed-owner

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