FOM: Tragesser; full formalization; Lakatos; reverse mathematics

[Stephen G Simpson]

Robert Tragesser 4 Jun 1999 21:53:19

 > Simpson tries to evade the problem --

Tragesser is wrong to accuse me of evasion simply because I may not
agree with him or may not care about allegedly important issues that
seem to excite him.  Robert, please try to concentrate on scientific
issues and avoid psychological analysis.

 > implicitly raised by the apparently further seeing Friedman --

Tragesser seems to think that Friedman partially agrees with him, but
I am not so sure.  I will let Friedman speak for himself.

 > by making "involving a logical calculus" analytic of "full
 > formalization".

Tragesser seems to want to say that full formalization does not
necessarily involve a logical calculus.  I confess I have no idea what
Tragesser is talking about, because I have never considered the idea
that a piece of mathematics can be fully formalized without using a
logical calculus.  This idea seems absurd to me.

In my posting of 31 May 1999 19:36:19, I distinguished among three or
four different senses of ``formalization''.  These distinctions may be
relevant to Tragesser's complaints and demands.

Could Tragesser please try to explain his point?  In particular, could
Tragesser please indicate an example of what he considers full
formalization that doesn't involve a logical calculus?

Tragesser:

 > Here again is what must be done to make fom research fundamental
 > science --

This is obviously incorrect.  F.o.m. is already fundamental science,
without having done this.

 > to begin with a natural hbistory of mathematical proof , describing
 > carefully the operations, somewhat "dialectical" in character --
 > that legitimately lead from informal proof to its "formalization",
 > remarking at each point of what has changed, what has been left
 > behind, an full evaluzation of what has been left behind, the
 > legitimacy of those changes, the sense in which the changes do and
 > do not preserve identity of proof.

This style of analysis of mathematical proof may or may not be
interesting and worthwhile.  I think Lakatos attempted this in
``Proofs and Refutations'' for the V-E+F=2 theorem.  ``Proofs and
Refutations'' certainly created a splash among academic philosophers,
but I don't think it had much impact on f.o.m. research.

A good critique of Lakatos is in Feferman's essay ``The Logic of
Mathematical Discovery versus The Logical Structure of Mathematics''.
In particular, Feferman illustrates how the logical techniques that
are normally used in f.o.m. research can account for the same kinds of
phenomena as the Lakatosian dialectic, but in a more rigorous way.

In particular, there is reverse mathematics, as in part A of my book
``Subsystems of Second Order Arithmetic''
<http://www.math.psu.edu/simpson/sosoa/>.  It is true that reverse
mathematics primarily analyzes provability in specific formal systems,
not the structure of particular proofs.  However, reverse mathematics
does sometimes manage to distinguish between two different proofs p1
and p2 of the same theorem t, by showing that the axioms needed to
prove t are not as strong as the axioms needed to prove a particular
lemma l occuring in some known proof of t.  As an example, let

  t = ``every countable commutative ring has a prime ideal''

  l = ``every countable commutative ring has a maximal ideal''

  p1 = the usual textbook proof of t, via l

  p2 = a more complicated proof of t, formalizable in WKL0

It is known from reverse mathematics that t,l are equivalent to WKL0,
ACA0 respectively, over RCA0.  Thus the two proofs p1 and p2 of t are
certainly not equivalent to each other.  

This kind of analysis of proofs has obvious advantages over the
Lakatosian dialectic, because it is more mathematically rigorous.

-- Steve