reply to Friedman FOM: new inductions unimportant

[Colin McLarty]

        I am happy with Mic Detlefsen's  1 Mar 1999 12:03:54  post
clarifying the confusion over "each/every finitely axiomatized fragment of ZFC".

        The point is that nearly everyone on FOM accepts inductive proofs,
of statements that can be made in ZFC, but where the induction cannot be
done in ZFC. 

        In reply to me, Harvey Friedman <friedman at math.ohio-state.edu> made
a perfectly correct point about how set theory advanced formal logic:

>But no one accepts this further induction until after they first introduce
>set theories with unrestricted quantification over sets.

and I agree when you speak of 

>the overwhelming power of the existing standard
>formal systems such as ZFC.

        But that does not bear on the question. My conclusion remains
simply, and literally, true:

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

        I can even strengthen it:

In the language of any consistent formal theory there are statements, which
the theory cannot prove, but which you actually accept because of inductive
arguments not available in that theory. 

Colin