FOM: defining ``mathematics''

[Matt Insall]

This is my second reply to Professor Sazonov's response to comments about
his advocacy of formalism.

Matt Insall

>
>
>
> Harvey Friedman <friedman at math.ohio-state.edu>
>     Date: Tue, 28 Dec 1999 13:05:02 -0500
> wrote replying to Buss:
>
>
> >   4. One of the distinguishing features of mathematics is the use of
> >       proof and of mathematically rigorous reasoning.  Especially
> noteworthy
> >       is the fact that mathematicians will nearly always agree on
> whether a
> >       given asserted theorem has been correctly proved.  When there
> are
> >       agreements on whether a proof is correct, mathematicians try to
> >       resolve their disagreement by breaking their argument into
> smaller
> >       steps, down to the level of first-order logic if necessary (but
> >       not down to the level of set theory.)
>
> I would not characterize the way mathematicians try to resolve their
> disagreements over correctness of proofs in the way that you are. The
> process mathematicians most commonly use has nothing whatsoever to do
> with
> first order logic, or no more than any other mathematics has to do with
> first order logic. It is the following professional and mathematical
> process:
>
> 1) first demand that there be a manuscript available;
> 2) try to reconstruct the proof,
>asking questions if necessary;
>
> Assuming this fails,
>
> 3) try to give another proof;
>
> Assuming this fails and one is suspicious,
>
> 4) give counterexamples to lemmas and/or other assertions in the
> manuscript; and/or
> 5) prove that certain definitions are ill defined for various reasons.
>
> In other words, the usual way to show that a proof Pi is incorrect is to
>
> engage in normal mathematical activity without regard to first order
> logic
> or ZFC. There is nothing formal about this process, and so it makes no
> sense to me to compare the roles of set theory and first-order logic in
> this process.
>
> MY COMMENT:
>
> Here I ignore comparison of FOL with set theory. Only on rigor.
> The point of Buss here is formal character of mathematical
> proofs. I agree with this completely and do not see the
> real reason for the above objections.

I must agree with you here.  The format of the proofs attempted by
mathematicians is generally well-described by FOL or set theory.  Thus the
above objections do not seem to apply.

>
> I think here is some mixture of various aspects of mathematical
> activity. Who likes to read the formal (or semi-formal) proof
> written by somebody else, whose way of writing is probably not
> the best one, say for the given reader? It is essentially the
> same as reading a program written by other programmer. As a
> creating person any mathematician prefers  to guess himself
> how the prove was (or may be) discovered. This is much more
> useful and interesting than just to read and check even
> absolutely formal proof. But eventually, the ideal result
> should be anyway a formal(izable) proof, i.e. a construction made
> according to some (sufficiently) formal rules. Moreover, this
> process may be not very conscious. Mathematicians "know" their
> formal rules of reasoning just by training (like swimming or
> driving bicycle or car).

I would aggre, except that I believe some of the tools of reason are innate.
In fact, they probably all are innate, but undeveloped, in most people.

>We do many things mechanically
> (formally) without thinking very much how this is happening.
> The goal of formalisms in mathematics consists not in forcing
> mathematicians to write everything absolutely formally but,
> rather to organize, mechanize, accelerate thought and to make
> it precise.
>
> Say, one of the goal of formalization consists in the possibility
> to write proofs in the manner like:
>
> "... then apply modus ponens five times more ..."
>
> instead of real applying it five times. If mathematics would not
> be based on formal rules it would be impossible to make such
> "accelerations of thought". We essentially explain one to another
> how it is possible in principle to write a formal proof. Of course
> it does not always look like the above artificial example. But
> I believe that any mathematical proof (whichever informal it looks
> like) can be most reasonably treated in analogous way. Of course
> we may and should use additionally various images, appealing to
> the intuition, to the real life, etc. The final (ideal) result is
> essentially the same - formal(izable) proof. Eventually, such a
> proof may be checked only in accordance with the formal rules of
> a given formalism.

I would comment, but I doubt if I can improve on this. :-)

>And this is actually confirmed by
>
>
> FRIEDMAN:
>
> Buss continues:
>
> >Lasting disagreements
> >       on whether a proof is correct are rare; on the contrary, they
> can
> >       usually be resolved to *everyone's* satisfaction.
> >          I believe that this fact is due directly to the fact that
> >       mathematicians are reasoning with methods that are *formalizable
>
> >       in principle* in a first-order system.  This makes the notion
> >       of mathematical rigor a robust and objective concept.
>
> I don't think this explains why things are so often fully resolved. For
> instance, it is likely that one can decide *in principle* whether a
> comet
> will destroy human life on this planet within 200 million years. Just
> wait
> 200 million years and see. However, that is too impractical a method,
> and
> it doesn't prevent people from having sharply different views about
> this.
>
> On the other hand, I have no doubt that ZFC and first order logic would
> play a role in any sufficiently long dispute about the correctness of an
>
> argument if the process I outlined above were to continue to fail over
> and
> over again, even after the "proof" was cut up into manageable pieces and
>
> examined independently. But it would come into play only as a last
> resort
> and only when it can be applied to tiny subproofs.
>
>
> MY COMMENT:
>
> Of course as "as a last resort"! And it is the main point
> that mathematics is based on existence of this "last resort".
>
> As to formalizability *in principle*, there may be two main versions:
>
> (1) A mathematician argues that the proof (with such and such
> abbreviations, if he pays attention to this important subtlety)
> may be really written, say, in a book of a reasonable size.
>
> (2) He/she even do not try to be sufficiently precise in this sense.
> Only relies on the ordinary mathematical practice of writing/checking
> proofs. So that the length of the resulting formal proof even cannot be
> reasonably estimated.
>
> (By the way, we could doubt that we have really a rigorous proof
> in the last case. However, usually these doubts may be resolved.)
>
>
>
> This only shows that "absolute" mathematical rigor (if any) in
> real mathematical practice is yet not achieved even nowadays.

It may never be achieved, but does that mean that it cannot ever be
achieved?  I think not.  Many possible things never happen.  This
``absolute'' mathematical rigour is an ideal to be strived for, as is a
utopian society.  It may not physically exist, but that does not mean that
it does not exist, for, as I think you would agree, even physical existence
is ``fluid'' enough to be not well-defined, and hence cannot be the ultimate
criterion for a test of existence of a mathematical formal system, or
concept, such as ``rigour''.  There may be some time in the future when all
mathematicians will agree on a standard of rigour.  (I doubt it, but even
this should not be the criterion for ``existence''.)


Matt Insall
http://www.rollanet.org/~montez
montez at rollanet.org