[FOM] Has Principia Mathematica been formally verified?

[Vaughan Pratt]

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