[FOM] Formal Proofs
Timothy Y. Chow
tchow at alum.mit.edu
Sun Oct 26 21:19:06 EDT 2014
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.
More information about the FOM