FOM: Re: reply to Kanovei

[Colin McLarty]

Kanovei objects to my argument that no formal theory can express the actual
extent of our knowledge of mathematical induction.

He writes

>Indeed, take PA as a consistent formal theory. 
>There are statements of PA which PA really 
>cannot prove or reject: say Con PA, the 
>Paris--Harrington theorem, and many more. 
>Some of them are accepted as true theorems 
>just because ZFC (or say 2nd order PA) proves them 
>(although PA cannot prove). 
>In those ZFC proofs there may happen some 
>induction arguments, of course, which cannot 
>be justified in PA (say because they appeal 
>to real numbers). 
>
>So what ? 

        The point is: It cannot be true that you accept these theorems "just
because ZFC (or say 2nd order PA) proves them". 

        If provability in ZFC was really your standard of truth, then you
could not also believe Con ZFC. (I assume that by second order PA you mean
some axiomatic theory, and so something weaker than ZFC, which we can
neglect for our purposes.) 

        Will you say you do not believe Con ZFC? I doubt you will. 

        Will you say you believe Con ZFC because it is derivable from the
axioms ZFC+(Con ZFC)? That is absurd. You can just as well derive not-Con
ZFC from the axioms ZFC+(not-Con ZFC). How do you choose which to believe?

        I'll tell you how I choose. I believe Con ZFC because I understand
the axioms (and various extensions of them) fairly well and find them
persuasive, and people far more expert than I understand them better and
find them persuasive, and ZFC has worked well under considerable
investigation over the past 70 years or so. None of these facts are proved
by appeal to any formal theory.

        Poincare was quite right. No one actually bases their mathematical
knowledge on provability in any formal system.