FOM: true but not provable

[V. Sazonov]

William Tait wrote:
> 
> Whether or not
> 
> (1) A is true but not provable
> 
> i.e.
> 
> (1) A and {A is not provable)

Yes, this is a possible reading (or variation of?) (1) 
(with using \not\exists x Proof(x,`A')) 
which I did not take into account in my postings on this subject. 
However, strictly speaking, I would not write here "i.e.". 
I am not sure that for everybody "A is true" is just A. 
For me "A is true" in some philosophical contexts is just 
nonsense. In mathematical context it really seems the same 
as A. 

Anyway, we should appropriately transform a statement 
of a natural language to make it mathematical. Moreover, 
there may be various ways of such transformation. 
What therefore means using natural language in mathematics 
if we are often not very careful? 

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


Strange! "Unlike", even if "provable" will be interpreted with 
the help of Goedel's predicate Proof(x,y)? Of course this is also 
called Metamathematics, what does not mean that it is not a 
kind of Mathematics. 


i.e. we must have a proof
> of A, thereby refuting (1).

That is a formal theory having 

A and {A is not provable)

as an axiom or theorem is inconsistent. It seems to me that 
Torkel Franzen had in mind not that mathematical reading of 
(1) described above. Otherwise he would see immediately the 
contradiction. I guess he considered some mysterious for me 
Philosophical meaning of "A is true", and such a "meaning" 
is the stumbling block of many discussions in FOM. 


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

No, e.g. I meant (if not Goedel's formalized Prove_{PA}(x,y) predicate) 
just "unprovability in PA" or in any other formal system like PA. 
Even in this case the English word "unprovable" (in philosophical 
context) seems to me too ambiguous until it will not be explained 
by the author of such a phrase on unprovability, as I wrote in my 
last postings. 


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. 

But it is disprovable in also consistent T' = T + not G. 
Why do you decide that G is true? It is true IN a theory, 
but not just true. By the way, I do not understand this 
"just true". On the other hand, we could discuss plausibility 
of T, T' and other formalisms and decide that some of them are 
more interesting for us (from some point of view) and then, 
probably, so to speak, to "conclude" plausibility of G. 
But this is not just saying that G is true. 

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

One more meaning of a sentence written in a natural language! 
Philosophers of mathematics should be extremely careful. 
What is better than mathematics where seemingly no SUCH problems 
arise? However, we also need a philosophy which would say us 
something very important about the nature of mathematics. 


Vladimir Sazonov