FOM: Re: Visual Proofs: Reply to Silver and Hayes

[Joe Shipman]

Charles Silver wrote:

>         I would bet that very few people in FOM have ever *seen* a
> "rigorous sentential proof" in this sense.  Simple truths in set theory,
> become monstrously long when reduced to sentences of first-order logic.
> ... So, I think a "rigorous proof" must stop short of
> being a first-order derivation.

That's OK, I was only talking about the *possibility* of converting the proof
to sentential form -- the point is to convince yourself of the possibility.
In my analogy with Church's thesis, this would correspond to writing down
every quadruple of an actual Turing machine, a stage which also never needs to
be reached when convincing oneself that a function is recursive.  My
distinction between the two situations is that going all the way down to the
Turing machine specification, while cumbersome, is quite a bit more feasible
than going all the way down to a ZFC-FOL proof (even allowing abbreviations).
Furthermore, we even have tools (compilers and interpreters to reduce
high-level computer languages like LISP to register machine code, which is
easily translatable to Turing machine code) that mechanize this process very
nicely, while the technology of machine-aided proofs is much more primitive.