Tait on reply to Friedman FOM: new inductions unimportant

[Colin McLarty]

William Tait <wtait at ix.netcom.com> wrote

>I've been busy and came in late to this discussion. So forgive me if I'm
>going over old ground. But can you literally mean this?
>
>>   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.

        You are right, I meant formal theories that could possibly claim to
be foundations for mathematics.

>I expect you are thinking only of theories S to which G\"odel's
>incompleteness theorems apply. But even in this case, though, your
>statement isn't literally true: I will `accept' Consis(S) only if I *know*
>S is consistent. (Indeed, knowing this, I will also know there is an
>arithmetical model of S and then can prove inductively on the length of
>proofs, in second order arithmetic, that every theorem of S is true in that
>model.)

        This only shows that Consis(S) is not an example. My example was:

         "If T is a finitely axiomatized fragment of ZFC, then ZFC 
        proves Consis(T)".

Like nearly all logicians, I believe that quoted assertion, which can
obviously be expressed in ZFC. I cannot make the infinitely many separate
ZFC verifications for each finitely axiomatized fragment T, but I've seen
the  familiar inductive proof which cannot be formalized in ZFC. Similar
proofs will be available in for any formal theory that could plausibly serve
as a foundation for mathematics. 

        Possibly a side issue: I am not sure what difference you mean
between 'accept' and *know*. It seems to me that I will believe Consis(S) if
I believe S is consistent. For example, I believe ZF is consistent, and I
believe the ZF formula Consis(ZF). Do you have something else in mind?

Colin