[FOM] Has Principia Mathematica been formally verified?
Vaughan Pratt
pratt at cs.stanford.edu
Tue Jul 26 21:09:55 EDT 2011
On 07/26/2011 07:41 AM, Timothy Y. Chow wrote:
> I'm aware that Newell, Simon, and Shaw wrote a program in the 1950's
> called Logic Theorist that was designed to *find* proofs of PM theorems.
> Though this isn't exactly what I'm asking about, it's close.
> Unfortunately I haven't been able to find too many details of how Logic
> Theorist chose to formalize things, since their paper was apparently
> rejected for publication.
A couple of early papers on the Logic Theorist:
[1] A. Newell, H. Simon, "The logic theory machine--A complex
information processing system", Information Theory, IRE Transactions on
In Information Theory, IRE Transactions on, Vol. 2, No. 3. (1956), pp.
61-79.
Andrzej Ehrenfeucht reviewed this paper in JSL 22:3 331-332 (Sept.
1957), see
http://www.jstor.org/stable/2963663?seq=1
Andrzej was rather critical of the paper's clarity and lack of precise
definitions, complaining that it "becomes thus a kind of 'hieroglyphic
writing'." With that caveat, I think nevertheless that this is the
paper you should find most useful for insight into LT.
[2] Allen Newell, J.C. Shaw and Herbert A. Simon (May 1958). "Elements
of a theory of human problem solving". Psychological Review 65 (3): pp.
151-166
This paper presented the underlying ideas to a psychology audience, and
will therefore probably be of less interest to you.
The rejected paper you refer to was submitted to JSL and exhibited a
computer-generated proof of Theorem 2.85 of Russell and Whitehead's
Principia Mathematica, that if pvq implies pvr, then either p holds or q
implies r. R&W took six arguably obscure steps to prove it, including
appeals to three earlier theorems, but the theorem itself is easily seen
to be true by case analysis on p (when p is true it simplifies to true
implies true, and when p is false it simplifies to (q implies r) implies
(q implies r)), so it's quite plausible that LT could have found a
simpler argument than R&W's while playing by the same rules as R&W (the
ground rules N&S laid down for LT), the point being to show that a
computer could play R&W's game better than R&W themselves. Obviously
truth tables would trivialize the problem, but that wasn't the point
with LT, which was not to solve the problem but to model how humans
(might) do so when obliged to reason from prescribed axioms rather than
semantically.
Anyone know the actual argument LT found for Theorem 2.58, or the exact
reason given by the editor for rejection? The page
http://www.manhattanrarebooks-science.com/newell.htm
quotes the Babbage Institute as saying the JSL "would not publish the
description of a proof coauthored by a computer program" and Džeroski
and Todorovski say the same in their book on "Computational discovery of
scientific knowledge." The Wikipedia article on Logic Theorist however
says "it was rejected on the grounds that a new proof of an elementary
mathematical theorem was not notable, apparently overlooking the fact
that one of the authors was a computer program" and cites Daniel
Grevier's "Tumultuous History" book as the source, but I couldn't find
any confirmation of this reason in Grevier's book. (A lot of Wikipedia
sources are like this; I suspect many Wikipedia editors supply sources
at random merely to avoid the dreaded citation-needed tag for some claim
they're sure must be true but haven't bothered to verify. Related
misinformation on the web is the attribution to Logic Theorist of the
elegant proof by Herbert Gelernter's geometry program of Pons Asinorum,
appeal to the invariance of an isosceles triangle under reflection about
its axis of symmetry, which in any event was noticed well before
computers by Pappus in the third century.)
In hindsight a case could have been made for acceptance on the ground of
historical importance, that it was the first improvement on a published
proof to be found by a computer program. However the public has a
tendency to attach too much significance to rejections by important
journals of visibly problematic submissions whose rationale for
acceptance is unclear at the time. Resubmission elsewhere, preferably
after some rewriting to incorporate the referees' feedback, is always an
option. Moreover while some proportion of the JSL audience presumably
cared in 1957 about how humans solve logic problems, they may not have
been terribly interested in how they solve PM's Theorem 2.58, which is
at the sort of trivial level that would appeal more to a psychology
audience than professional logicians.
On 07/26/2011 04:48 PM, Martin Davis wrote:
> This was quite different from Newell, Shaw, and Simon's program which
> did provide proofs in Principia style from the axioms. Wang was quite
> critical of their approach.
I understood Wang and NSS to be pursuing different objectives. Wang was
interested in how one (human or machine) might go about algorithmically
finding proofs of the theorems in question, which included flexibility
in choice of suitable axiom system. Newell and Simon were interested in
the psychological question of how humans might go about solving the sort
of problems Russell and Whitehead set themselves, which obliged them to
stick to R&W's axioms. Any criticism of Newell and Simon's approach
would have to be firstly with their assumption that humans reason
heuristically, the approach adopted for LT, and secondly (assuming
humans do reason heuristically) whether the heuristics LT used had much
to do with those employed by humans such as R&W.
Vaughan Pratt
More information about the FOM
mailing list