FOM: formalization

[Harvey Friedman]

Reply to Tragesser 7:52AM 5/29/99.

It is not easy to talk about formalization in a clear way. Unless one is
almost unprecedently careful, one is surely going to be misunderstood. I
will attempt to be that careful.

The previous paragraph is so very important, that I repeat it verbatim:

It is not easy to talk about formalization in a clear way. Unless one is
almost unprecedently careful, one is surely going to be misunderstood. I
will attempt to be that careful.

The quest for formalization - in the relevant sense here - arises whenever
there is an intellectual development in which the underlying assumptions
have not been clearly identified. Often there is unclarity about what the
underlying undefined concepts are.

As one gets away from mathematics, it normally gets quite difficult to make
such clarifications. But because of the computer revolution, there is a
great deal of practical interest - and success - in making such
clarifications in order to create new hardware and software systems.

In mathematics itself, there has been a great deal of success in making
such clarifications and providing formalizations based on such
clarifications. In order to carry this out one must provide for what is
normally called "purely logical" inference. This crucial part of
formalization is normally presented and studied in isolation, and is
generally called "first order predicate calculus with equality."

It should be recognized that the actual formalization of mathematics in any
of the usual formalizations is extremely awkward and generally
unmanageable. It is physically impossible without apparatus for
abbreviations. In any case, no one is actually doing this except with the
aid of a computer and more flexible formalizations created for this
purpose. E.g., see the Mizar project.

But the fact that one has a formalization of mathematics that is obviously
appropriately faithful and complete is certainly one of the great
achievments of mathematical thought. This is noramlly done through set
theory with ZFC. To this date, alternatives turn out to be essentially
equivalent (and usually far more cumbersome) in various precise senses.

Given the grossly cumbersome nature of actual formalization, many people
think that logicians who investigate formalization and formalizations must
be doing actual formalization. This is definitely not the case. One
develops techniques and intuitions that allow one to see what can be
formalized in what without carrying that formalization out explicitly.
Without this, much of f.o.m. would be impossible to develop.

One might ask for a formalization that satisfies some additional criteria.
E.g., that it be convenient to read and write in that formalization. I have
gotten interested in this question from time to time, and my latest modest
foray into this is with Randy Dougherty.

One might also ask what benefits accrue to having found such a
formalization? First and foremost, it is of obvious intrinsic intellectual
interest, not only for mathematics, but for all of systematic intellectual
thought. Secondly, one can prove impossibility theorems. I.e., that some
question or other cannot be answered using the usual axioms and rules of
inference of mathematics. Thirdly, by building on such formalizations, one
can make some clear distinctions between different kinds of proofs, and
show that it is impossible to prove such and such using proofs that are of
such and such kind. Fourthly, one may investigate systematically the
question of consistency, relative consistency, and interpretability. There
are other benefits, too.

>        I urge that clarity or rigor demands that one be careful with
>the term "formal".  ... There is no commitment here to
>codifying the principles in a (privileged) logical calculus.
>        One should preserve this distinction.  Instead of "is
>formalized" as it is currently used,  one should say,  for the sake fo
>precision,  "formalized and coded in a logical calculus" (or something
>like this).  Without this distinction readiuly at hand,  it is very
>difficult to distinguish between,  say,  Hilbert's formalization of
>elementary geometry in FoG (where there is no logical calculus in
>evidence)  and its subsequent (as by Tarski) presentation "formalized
>and coded in a logical calculus".  The same might be said for PM,  which
>is formal,  but inadequately coded in a logical calculus.

A full formalization of mathematics or an area of mathematics seems to
necessary involve a logical calculus - or equivalent. So your distinction
appears to be based on a confusion.

>        This would also give us a way of distinguishing the use of
>axiomatic method to do mathematics in the spirit of Emily Noether,  as
>emphasized by Herman Weyl,  where one wants to think out and write out
>the mathematical principles germane to a subject and of immediately
>value to proving strong theorems in a few pages (instead of several
>hundred pages as in PM).

You are confusing informal proofs with formal proofs. The latter is what is
relevant when discussing formalization. An important project is to redesign
the axioms and rules of logic so as to be closer to the way informal
reasoning is conducted.

>        It would be not unreasonable for the mathematician -- for their
>immediate purposes -- to foresee no advantage in worrying about or even
>mentioning the problem of whether the formal-principles set out could be
>translated into some logical calculus.  It would be quite understandable
>why they'd have no interest in that.

It is already well known to virtually all mathematicians that what they are
doing is formalizable in ZFC. So many are not worried about this, and do
not mention this, as is the case with other well known facts that they do
not use. But having no interest in it - well, that is akin to saying that
one has no interest in, say, music, physics, statistics, algorithms,
etcetera. Nothing to be terribly proud of.

>        It would also be reasonable for a fomer to point out that
>something interesting and even worthwhile could be learned through
>metamathematical investigations,  but,  given the extreme difficulties
>of the latter -- >especially in the past two or so decades --

What does that mean? I do not have "extreme difficulties" with it in the
"past two or so decades".

>it would
>not be unreasonable for the mathematician to take a "show me" attitude,
>given their (the mathematician's) objectives/goals/interests.

"Show me" what?

>After
>all,  it is quite possible to do some interesting mathematics,  even
>enduring mathematics,  without any concern for fom
>issues/investigations,  even when the mathematician's' concepts swerve
>toward those fom has most to say about.

It is also quite possible to do some enduring mathematics, without any
concern for real analysis; or enduring mathematics without any concern for
number theory; or enduring mathematics without any concern for geometry;
etcetera.

>It is not unreasonable for a
>mathematician to say in such a case,  given their immediate objectives
>and interests,  that they don't see any percentage just then in
>formalized-and-represented-in-a-logical-calculus not looking promising
>enough to make the perhaps titantic effort required.

Titantic effort is quite unusual.

>This doesn't
>require that the deny the importance/value/significance of fom in
>anything like an absolute way;  nor does it require Steve Simpson's nose
>to fall out of joint.

Even your nose should fall out of joint under certain interpretations of
what some mathematicians may sometimes seem to say about some aspects of
f.o.m.

>        As a sort of philosopher of mathematics,  I have only been
>curious about why fomers have not been more philosophically rigorous,
>yes even logically rigorous,  about articulating clearly and honestly
>and elaborately what is left behind when a formal-logical-calculus
>translation of a piece of mathematics is set up in place of the  piece
>of mathematics.

I have never seen a "formal-logical-calculus translation of a piece of
mathematics .. set up in place of the piece of mathematics." Perhaps I
don't know what "set up in place of" means. Also, by the way, I don't know
what "left behind" means. Does "left behind" mean the left side of part of
your anaotomy?

>It doesn't seem right to dismiss the distinction
>without an elaborate and careful discussion of the difference(s);  I've
>not seen such a discussion anywhere.

I think you should be much clearer about what you are after.

>This seems to indicate a
>tremendolus discrepancy in our understanding or
>intellectual/philosophical short-fall,  if not dishonesty,  in the
>thinking of fomers.
>
Before tending to attribute "dishonesty" to people working in f.o.m., I
think you should clarify exactly what you are after. Your "honesty" will no
doubt compel you to do so.