FOM: true but not provable

[Torkel Franzen]

William Tait says:

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

  That would have been clear enough, were it not for the fact that V.
Kanovei had attributed the idea that there are "true but unprovable
statements" to Jeffrey Ketland on the basis of the latter's interpretation
of Godel's theorem - quite mistakenly.

  When we say that Con(T) is true but not provable in T, provided T is
consistent, we are not saying or assuming anything about whether or
not Con(T) is in any sense provable. It is only in this sense that
provability is separated from truth. If somebody then asks us "but may
Con(T) then be unprovable in an absolute sense?" the natural reply
is "What's that supposed to mean?".

  Similarly, when we note that there are infinitely many true
arithmetical sentences not provable in ZFC, we're not saying anything
about whether these sentences are in any sense provable. Provability
simply doesn't enter into it.

  Again, when we speak, from a realistic viewpoint, of sets of natural
numbers, we are not assuming that those sets are in any sense definable.
This does not mean that we are assuming that sets may be absolutely
undefinable, or that it makes any sense whatever to speak of sets as
absolutely undefinable.

  In short, if we are to criticize a realistic view of arithmetical truth
or of sets, we must first set aside the mistaken idea that such a view
entails any notion of "true but (absolutely) unprovable statement" or
"existing but (absolutely) undefinable sets". It is perfectly compatible
with the realistic view to hold that it makes no sense whatever to speak
of true but absolutely unprovable arithmetical statements, or existing
but absolutely undefinable sets.

 ---

  Torkel Franzen, Luleå university