Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10.2 9/18/84; site wdl1.UUCP
Path: utzoo!linus!philabs!prls!amdimage!amdcad!decwrl!decvax!tektronix!hplabs!hpda!fortune!wdl1!jbn
From: jbn@wdl1.UUCP
Newsgroups: net.singles
Subject: Re: Re: Intelligence
Message-ID: <595@wdl1.UUCP>
Date: Mon, 5-Aug-85 10:56:06 EDT
Article-I.D.: wdl1.595
Posted: Mon Aug  5 10:56:06 1985
Date-Received: Sun, 11-Aug-85 04:07:13 EDT
Sender: notes@wdl1.UUCP
Organization: Ford Aerospace, Western Development Laboratories
Lines: 24
Nf-ID: #R:peora:-124200:wdl1:4200025:000:1379
Nf-From: wdl1!jbn    Jul 10 16:40:00 1985


      Mathematics without quantifiers is not only possible, but sounder
than quantified mathematics.  Quantifiers occupy their central place in
mathematics only for historical reasons.  With the development of
constructive mathematics, quantifiers are less necessary and in time
may be obsolete.  Read ``A Computational Logic'' by Robert Boyer and J. 
Strother Moore (ISBN 0-12-122950-5) to see how one can get along without
quantifiers.  All those annoying trouble spots, such as Russell's class of
all classes paradox, go away in constructive theory.  Constructive mathematics
tends to require more manipulation than quantified mathematics, but Boyer and
Moore have a program that mechanizes this, and it is an illuminating experience
to learn constructive mathematics with that program available.
      Later work by Boyer and Moore includes a constructive proof of the
halting problem and over a thousand theorems from various parts of
mathematics, all proved constructively with machine proofs.
      (You can get the theorem proving program over the ARPANET using FTP
and an anonynmous login by retrieving AUX:<CL.THM>-READ-.-THIS- 
at UTEXAS-20.ARPA and following the directions therein.  But read the
book first.  The prover runs on VAXen or SUNs (Franz Lisp) Multics
(MACLISP) or Symbolics systems (Zetalisp).)

				John Nagle
				League of the Militant Constructivists