FOM: informal versus formal reasoning

[Randall Holmes]

I must hasten to add that I regard formal proof as completely
indispensible in mathematics; I would hate to be accused of being a
postmodernist.  First-order logic does capture a (nearly) universal
standard of formalized proof.

I also regard exact formal definition of what we are talking about as
being completely indispensible in mathematics; thus the need for the
expressive power of second-order logic.

Formal proofs (using generally accepted principles such as those of
first-order logic) allow us to see that the conclusions we draw follow
from our axioms.  They also allow us to identify the axioms we are
using, which themselves may require "informal" justification.  If you
do not share my conviction that a certain axiom is true, this allows
you to express your objections to my proof precisely; you can separate
objections on a formal level from objections on an informal or
"intuitive" level.  (If you are a constructivist, you can examine the
formal principles of reasoning I accept and express your possibly
stronger objections to my proof precisely as well).

As long as we confine ourselves to what can be proved within a strong
formal system such as ZFC which most of us are willing to accept as
safe, the need for informal justifications of axioms can be kept to a
minimum (even to zero) allowing some of us to be convinced (mostly
harmlessly) that the formal system in question "formalizes
mathematics".

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes