[FOM] Dan Goodman on proof checkers

[A.P. Hazen]

  The paper Dan Goodman refers to on automated proof checkers, in Thomas
Tymoczko, ed., "New Directions in the Philosophy of Mathematics"
(Birkhäuser, 1986) is
   Richard de Millo, Richard Lipton, and Alan Perlis, "Social
   Processes and Proofs of Theorems and Programs."
  It originally appeared in "Communications of the ACM," v. 22 n. 5 (May
1979), pp. 271-280.

  Comment: It seems to me that there could be an analogy with our
"empirical" grounds for belief in the Church-Turing thesis.  Given only
Turing's original  paper and the examples discussed in it, one might well
be less than  morally certain that all algorithms are represented by Turing
machines: the process of specifying a Turing machine that "embodies" a
given, intuitively obviously effective, procedure is not transparent
enough.  (Even to show that using a two-dimensional workspace gives no more
powe in principle than can be gotten from a TM's one-dimensional tape is
not a *completely* trivial exercise!)

   Gradually, however, formal models of computation closer to our usual way
of conceiving algorithms were defined, and were proved equivalent in power
to TMs.  (I think a key step, here, was the introduction of "register
machines" by Shepherson and Sturgis (1963), and the realization that a
program for a register machine could be written in something visibly
similar to a simplified version of computer languages in actual use.)  It
seems to me that if one is presented with an intuitively described
algorithm NOW, one should be morally certain* that it can be embodied in a
TM, whereas reasonable doubt* would have been possible in, say, 1936 or
even 1954 (when Turing died).

   Analogously, were work on automated proof checking to proceed, might we
not anticipate proof checkers which could take, as input, texts coming
closer and closer to ordinary mathematical prose presentations of proofs?

---
*  These are terms from legal history.  A conscientious juror in a criminal
case, it has been written, should vote to convict only if "morally certain"
of the defendant's guilt, or only if the prosecution has established that
guilt "beyond reasonable doubt."  ...  Though I suspect that criminal
justice system muddles through with much lower standards than we FoM types
aspire to!
---

Allen Hazen
Philosophy Department
University of Melbourne