FOM: true but not provable

[William Tait]

Whether or not

(1) A is true but not provable

i.e.

(1) A and {A is not provable)

is meaningful or not for a mathematical proposition A, it is 
certainly a useless proposition. To be warranted in asserting (1), we 
must be warranted in particular in asserting A (which, unlike `A is 
provable', is a mathematical proposition), i.e. we must have a proof 
of A, thereby refuting (1).

Torkel Franzen wrote (Oct 27)


>   As for your claim that it is "wrong and basically meaningless" to
>say that there are true but unprovable sentences, I don't think I
>understand it. You agree that it is a mathematical theorem that there
>are true arithmetical sentences not provable in T, for any consistent
>extension T of PA, but you seem to be saying that we must not take
>this theorem at face value, but regard it from some purely formal
>standpoint. Why is that?


But clearly when whoever wrote that it is wrong and basically 
meaningless to say that there are true but unprovable sentences, he 
did not intend the proof predicate to refer to some particular formal 
system. For the extension T of PA in question, assuming it partially 
formalizes our mathematics, we can say that the Goedel sentence G for 
it is true, i.e. assert G, because we can prove it in the 
second-order extension of T. (Here I am assuming, only for 
simplicity, that T is first-order.) So in the intended sense of 
provability, G is provable.

The question is: what does `A is unprovable' mean? I suggested 
recently that, in the case of A = CH or any other presently 
undecidable sentence, it is best understood as a sociological 
prediction about what axioms we might in the future adopt.

Bill Tait