FOM: role of formalization in f.o.m.

[Stephen G Simpson]

Robert Tragesser's posting of 29 May 1999 07:52:33 can be read and
reacted to at various levels.

On a very bland level, there is Tragesser's suggestion to be careful
with the term ``formal'', i.e. to distinguish among various senses of
the term ``formalization''.  This suggestion strikes me as obvious and
uncontroversial, even if until now we have not paid enough attention
to these distinctions here on the FOM list.

As a preliminary scheme that seems appropriate for discussing the
current scene in f.o.m., I would propose to distinguish among:

 1. rigorous mathematics, referring to normal 20th century standards
    of mathematical rigor.  

    Examples: (a) journals such as Annals of Mathematics; (b)
    graduate-level textbooks such as Rudin's ``Real and Complex
    Analysis'' or Hartshorne's ``Algebraic Geometry''.

 2. metamathematics, i.e. rigorous arguments showing showing how
    various pieces of rigorous mathematics can be codified in the
    predicate calculus.

    Examples: (a) textbooks of axiomatic set theory, which state the
    axioms of ZFC and then sketch (in adequate but not excruciating
    detail) how to introduce various mathematical concepts such as the
    real number system in (definitional extensions of) ZFC and prove
    standard theorems about such concepts, all on the basis of the
    axioms; (b) the parts of my book ``Subsystems of Second Order
    Arithmetic'' <http://www.math.psu.edu/simpson/sosoa/> exploring
    how much of standard core mathematics is captured in various
    subsystems of Z_2, which are also based on the predicate calculus.

    Note: This is the kind of formalization that, according to my
    posting of 27 May 1999 20:27:12, constitutes ``much of the fabric
    of contemporary f.o.m. research''.
    
 3. detailed formalization, i.e. nearly complete line-by-line
    translations of mathematical arguments into a specified formal
    system.  

    Example: Principia Mathematica.
 
 4. complete formalization, i.e. totally formalized statements and
    proofs in the predicate calculus.  These will usually be generated
    with the aid of a computer.

    Example: the Mizar project.

It might be interesting to discuss the Elements of Euclid in terms of
this 4-fold scheme.

In the 20th century, pure mathematicians usually present the results
of their research in form 1 (i.e. rigorous mathematical exposition),
while 2,3,4 (i.e. various kinds of formalization within the predicate
calculus) are mostly the province of f.o.m. researchers.

My impression is that, when mathematicians and f.o.m. researchers
speak of ``formalization'', they are usually referring to 2,3,4 and
not to 1.  On the other hand, the usage among philosophers such as
Tragesser may be quite different.  Perhaps Tragesser would like to
clarify this.

It would be interesting to explore the history of the contemporary
20th century standard of mathematical rigor.  I have the impression
that this marvelous standard was shaped and molded by the same 19th
and early 20th century foundational activity that also ultimately gave
rise to formalization a la 2,3,4.  This close genetic relationship is
perhaps not adequately appreciated by the majority of contemporary
mathematicians, who tend to scorn formalization.

Isn't it wonderful that we have an electronic forum such as the FOM
list, where scientists from various communities (mathematicians,
f.o.m. researchers, computer scientists, philosophers of mathematics)
can come together, in the spirit of tolerance and patience, to compare
notes and illuminate questions of mutual interest.

Moving on, another aspect of Tragesser's posting is that he wants to
discuss particular chapters in the history of mathematics, from the
perspective of formalization.  I find this admirable.

Tragesser:

 > Although of course inadequately formal,  PM was important in ...

Why does Tragesser think Principia Mathematica was ``inadequately
formal''?  Inadequate for what?  

 > Hilbert's formalization of elementary geometry in FoG (where there
 > is no logical calculus in evidence)

Perhaps one could make a case that Hilbert's Grundlagen der Geometrie
is on the borderline between 1 (rigorous mathematics) and 2
(metamathematics).  Hilbert's exposition contains enough detail to
view it as metamathematical, once we write down the axioms and rules
of second-order logic.

 > and its subsequent (as by Tarski) presentation

I assume Tragesser is referring to Tarski's elementary geometry,
referenced in my posting of 17 Feb 1999 17:27:08.  Surely Tarski's
elementary geometry falls under heading 2.

 > This would also give us a way of distinguishing the use of
 > axiomatic method to do mathematics in the spirit of Emily Noether

I am not sure exactly what work of Noether Tragesser is referring to,
but I take it to be some rigorous mathematics a la heading 1 above,
e.g. a chapter on Noetherian rings in a modern algebra textbook.
(Confusion may arise because such textbooks tend to refer to the
Noetherian property and other structural properties as ``axioms'', but
from the logical point of view they are really definitions.)

Yet another aspect of Tragesser's posting is the polemical.

Attempting to speak for Conway and other mathematicians, Tragesser
says:

 > This doesn't require that the deny the
 > importance/value/significance of fom in anything like an absolute
 > way

My suggestion for Tragesser would be to send his comments to Conway
(CC to FOM please) and try to find out Conway's actual opinion on
these matters.  I am genuinely curious to know what Conway meant by
his anti-formalization remarks.

Don't forget that, according to Conway, formalization is irrelevant
``even for foundational studies''.  That is a direct quote from
Conway.  I find it almost incredible that a respected mathematician
would say such a thing, but there it is.  I wish Conway or his
followers would explain how this can be.

Tragesser muses:

 > 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.

To answer Tragesser's question, I would point out that
f.o.m. researchers may simply not be interested in the allegedly
important issue which Tragesser raises.  For one thing, Tragesser's
statement of the issue does not seem very realistic to me, because I
don't know of any instance where formalization a la 2,3,4 above has
been ``set up in place of'' rigorous mathematics.

Perhaps Tragesser's real concern is with some psychological or social
aspect of mathematical understanding.  I urge Tragesser to try to
state his concerns more clearly.

In any case, putting Tragesser's ``mysterious dimension'' aside, the
question of the exact relationship between (a) rigorous mathematical
exposition a la 1, and (b) formalization a la 2,3,4, is certainly of
general intellectual interest.  If Tragesser can come up with any
serious ideas that would tend to elucidate this relationship, I am
sure that f.o.m. researchers and many other people would love to hear
them.

Tragesser:

 > I've not seen such a discussion anywhere.  This seems to indicate a
 > tremendolus discrepancy in our understanding or
 > intellectual/philosophical short-fall, if not dishonesty, in the
 > thinking of fomers.

I would point out that, if the issues that excite Tragesser do not
excite f.o.m. researchers, that does not necessarily imply that the
f.o.m. researchers are intellectually or philosophically deficient or
dishonest.  Perhaps Tragesser merely needs to develop a little more
appreciation for the other fellow's perspective.

-- Steve