[FOM] Are proofs in mathematics based on sufficient evidence?

[Robert Lindauer]

On Thu, Jul 8, 2010 at 5:17 PM, Martin Davis <eipye at pacbell.net> wrote:

> Gottlob Frege discovered the simple logical rules of inference that
> underlie mathematical proofs.

In Frege's system, obviously the Frege's foundations of Arithmetic is
primarily a philosophical exploration in which he contrasts -not
completely fairly- opposing views of the concept of number, and
proposes his own concept of number (again philosophical) which is in
turn contradictory.  The resulting hierarchical formalizations (PM,
ZF) while no longer obviously contradictory, can not be fixed to be
known to be non-contradictory, and are without the intuitive force of
Frege's system.  Hence Hilbert's finitism and consistency goals,
Godel's proof that these were unavailable and a resulting rift in
FOM-like activities between formalists who reject the notion of any
need for "underlying logical notions" and realists who think that this
work can't be done in the straightforward way that frege wanted to,
but that, as you seem to imply, has already been "effectively done".

The differences between them appears to be mainly a question of
epistemological optimism, but optimism is not admissible in court.
Realists optimistically assert that the question of the consistency of
ZFC is unimportant and "effectively solved anyway" whereas these
effective solutions (e.g. the ability to perform any proof available
in ZFC using finitary methods) tend to offer ever-more complex and
unintuitive axioms, definitions and methods which makes the formalist
have the tendency to think that this problem is insoluble.

Thus, I think the search for an epistemology adequate foundation for
mathematical practice is at a standstill, probably because it is a
wholly philosophical exercise, since the questions are analogous to
questions that make physics epistemologically and metaphysical
unsatisfying (what is observation? what is "physical"? are parallel to
"what is proof?  what is number?"), and only tend to invite
speculation and not straightforward solution.

Were there a Jury convened to decide the matter of whether or not a
given sufficiently complex mathematical proof is "epistemologically
acceptable" it would very much depend on who was on the jury, in much
the same way that a conviction of murder depends.  But just as we know
there are innocent people on death row, so also we know that there are
false theorems that are commonly believed to be true (and of course we
don't know which!).  It seems even that we could never have any
reasons to believe that we had all and only death-deserving theorems
in our mathematical practice.

That is, for all our attempts at formalization, all we do
epistemologically is push our question further back to method and the
justification of the choice of axioms and logic(s) themselves.

With that a quote from the late Torkel Franzen regarding formal
proof's differences with "other kinds of proof":

"What follows or does not follow from a religious or philosophical
text, a scientific theory, or a system of laws is not determined by
any formal rules of inference, such as might be imple- mented on a
computer, but is very much a matter of interpretation, argument, and
opinion, where the relevant reasoning is limited only by the vast
bound- aries of human thought in scientific, religious, political, or
philosophical contexts."

But it seems that these several differences: intuitionism, formalism,
realism, finitism and "the standard view" make up exactly religious,
political and philosophical differences between factions in an ongoing
development of mathematical art, and the resolution of these questions
clearly are not formal ones within the scope of mathematical practice.

Best,

Robbie Lindauer