reply to Friedman FOM: new inductions unimportant

[William Tait]

dear Colin,

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.

I have in mind e.g. the first-order theory of real closed fields.

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

Best,  Bill