FOM: Replies to Friedman and Martin on induction

[Colin McLarty]

Harvey Friedman <friedman at math.ohio-state.edu> wrote:

>THEOREM. ZFC proves the consistency of each of its finitely axiomatized
>fragments.
>
>Furthermore, this Theorem is provable in Peano Arithmetic, and even in weak
>fragments thereof such as EFA = exponential function arithmetic.

The facts are well known. By standard use of Goedel numbering you can state
in the language of ZFC

        "Every finitely axiomatized fragment of ZFC is consistent."

You cannot prove it in ZFC (let alone EFA).

Yet for any finitely axiomatized fragment T of ZFC, you can prove in ZFC

        "T is consistent".


The step from individual fragments to the single assertion about "every
finitely axiomatized fragment" requires induction that cannot be done within
ZFC. Nearly everyone on this list accepts that further induction. I
certainly to. Only some radical finitists may question it in some way.
Analoguous facts apply to any standard formal foundation for mathematics

This proves what I earlier said: 

>>        No consistent formal, first order, axiomatic theory includes every
>>case of induction that you yourself will want to accept.



Martin Davis differed with my remarks on Poincare, saying:

>Poincare's position needs to be understood in historical context. There was
>no first order logic. There was logicism: Frege's that had turned out to be
>inconsistent, and Poincare was especially interesteed in Russell's. Russell
>proposed to develop arithmetic from "logic", and Poincare was attacking this
>program. 
>There's a lot more than could be said about this, but Poincare's objections
>had nothing to do with formalized arithmetic as we understand it today, and
>certainly was not directly relevant to the more sophisticated remarks of
>McLarty.

Of course thie issues are clearer today, but I think there is direct
relevance. Poincare felt the heart of logicism was to codify logic by
"purely mechanical rules", and giving a machine recognizable set of axioms
for geometry, so that the machine can generate "all of geometry". (See below
for the citation.) Today we know such enumerability of the theorems is the
key to Goedel's incompleteness theorems. It is not important whether you use
first or higher order types in the language.

Poincare approved of formulating geometry this clearly, yet he insisted that
no formalization could be basic to our knowledge of math. Specifically, he
insisted that the logistic program presupposes the principle of mathematical
induction. He gave two arguments for this:

1)Even to describe the logicist formulas you need the notion of a "finite
string of symbols" and this notion of "finite" relies on induction.    

2)You must use induction to prove the consistency of any logistic system.

That second point is directly relevant to the more sophisticated, later
results I cite. Today we only strengthen his claim: Not only must we use
induction to prove consistency of any formal theory (aside from trivial
exceptions such as an empty theory). We must use CASES OF induction that the
theory itself does not include. And we must use this not only to prove
consistency but even for many weaker interesting results.

Colin McLarty 


        The quoted passages of Poincare are from his essay recommending
Hilbert for the Lobachevski Prize. This was reprinted many times in slightly
different forms. The most accessible printing today may be the translation
in Philip Ehrlich editor, _Real Numbers, Generalizations of the Reals, &
Theories of Continua_, Synthese Library Vol. 235. Dordrecht: Kluwer Academic
Publishers (1994). See page 150.  Or see Poincaré, H. 1902: "Les fondements
de la géométrie", reprinted in his Oeuvres vol.11, 92-113; especially p.95.