FOM: truth and provability

[Kanovei]

> Date: Tue, 07 Nov 2000 14:38:27 -0800
> From: Martin Davis <martin at eipye.com>
 
> Can I be the only fom-er getting tired of this discussion going round and=
> round in circles

That you go in circles is simply because you do not like 
to accept that there is no any mathematical statement that 
can me qualified as TRUE by reasons different from its being 
PROVED mathematically, or, saying the same differently, 
that the existence of such a sentence can be demonstrated 
only assuming "ontological" existence of some kind of 
"standard model" of PA.  

> following variant form of Goedel's theorem:
> 
> For any consistent axiomatic extension T of Robinson's Q (hence certainly
> PA and ZFC are included) there is a formula with one free variable G(x),
> where numerals representing natural numbers may be substituted for x, such
> that:
> 1. for each numeral n, G(n) is provable in T.
> 2. (Ax)G(x) is not provable in T.
 
This is just another form of the same. 
What you suggest amounts to the following. 

THEOREM (ZFC or PA). 
There is a formula G(x) such that, if Con ZFC, then  
(1) ZFC-Prov G(n) for any n in N 
(2) not-ZFC-Prov (An)G(n). 
PROOF 
See Goedel.
END OF PROOF

REMARK 
G(x) can be taken to say: "x does NOT code a proof of 0=1 in ZFC". 
In this case, ZFC-Prov G(n) implies G(n) (assuming Con ZFC). 
Therefore, (1) can be replaced by
(1') G(n) for any n, hence, (Ax)G(x) "is true".
END OF REMARK,

Which leads us exactly to the same true-non-provable myth as in 
the earlier course of discussion. 

V.Kanovei