Systems Implementing All of Mathematics

Randall Holmes <>
Message-id: <>
Date: Tue, 3 Aug 93 15:21:04 -0600
From: Randall Holmes <>
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.			|