[FOM] Formal Proofs

[Timothy Y. Chow]

Jay Sulzberger wrote:
> Surely no serious student of logic after the publication of the 
> completeness theorem for the lower order predicate calculus ever thought 
> that formalization was impossible, in any serious sense. If one thought 
> this, then the completeness theorem must seem to lack force.

Maybe no "serious student of logic" thought so, but for a long time, I 
believe that it was the conventional wisdom that complete formalization of 
nontrivial mathematics was impossible in practice.

Just the other day, I had a conversation with a colleague who cited 
Lakatos's "Proofs and Refutations" as a devastating critique of (a certain 
version of) formalism.  Like Hersh and Steingart, my colleague likes to 
emphasize the social nature of proof.  When proponents of formal proofs 
point to Coq or Isabelle, he points to Nelson's qea and suggests that the 
machine itself does not validate the proof; the machine has to bear the 
stamp of approval of the recognized experts.  And so on.  To me, this line 
of argumentation does not clarify, but rather obscures the very real 
difference between mathematical knowledge and other kinds of knowledge. 
I'm led to assume that it is at least partially motivated by a vested 
interest in denying the claim that mathematical proof can be completely 
nailed down in a way that is immune from future falsification.  So I agree 
with Harvey that there has been, and still is, resistance to that point of 
view within the mathematical community.

Tim