FOM: True = provable? Was: Goedel: truth and misinterpretations

[V. Sazonov]

Here are two simple (metamathematical) results related with my 
attempts to give (one of) formalization to ``true, but not provable''. 
They look as something opposite to this phrase. For definiteness, 
consider that all the considerations below such as consistency of 
theories or first order models or the concept of truth (probably 
assumed implicitly) are given in the framework of ZFC. 

As such a subject is not my current everyday mathematical work, 
I would be especially grateful for any comments by specialists. 
The results are rather simple, but are they known, etc.? 


Let T be arbitrary sufficiently strong r.e. theory (say, PA 
or PRA) and A, B, C, etc. are any sentences (having no free 
variables) in the language of T. Consider the following axiom 
schema

(*)    (A => Pr[T](`A')

where Pr[T](x) is arithmetically definable predicate of 
provability in T of a formula with Goedel number x and 
`A' is numeral (term SSS...S0) representing Goedel number 
of A. 

Theorem 2. If T is consistent then it is consistent 
T* = T + the above axiom schema (*). 

Proof. Assume that T* has a contradiction. Then 

T |- 
(A & ~Pr[T](`A')) V (B & ~Pr[T](`B')) V ... V (C & ~Pr[T](`C'))

and by distributivity and de Morgan law we have 

T |- ~(Pr[T](`A')) & Pr[T](`B')) & ... &  Pr[T](`C')) & ...

It follows that T |- con[T], and, therefore, due to Goedel, 
T |- 0=1. QED. 


Comment 1. Roughly speaking, Theorem 1 means that we can 
reasonably assume that 

	every true sentence is provable. 




Now consider a stronger schema 

(**)     (A <=> Pr[T](`A')

Let us call a theory T *strongly consistent* (PA is an example of 
such theory) if it does not proves ``pathologies'' as 

	~A <=> Pr[T](`A')

or any their finite disjunctions. 

Arithmetical statement expressing strong consistency 
could be denoted CON[T] in contrast with the ordinary 
consistency con[T]. Evidently, CON[T] => con[T] 
(and this is provable in PA). 


Theorem 2. If T is strongly consistent then it is consistent 
T** = T + the above axiom schema (**).

Proof. Assume that T** has a contradiction. Then 

T |- ~[(A <=> Pr[T](`A')) & ... & (C <=> Pr[T](`C'))], 

i.e. 

T |- (~A <=> Pr[T](`A')) V ... V (~A <=> Pr[T](`A')) 

what means that T is not strongly consistent (``pathological''). 
QED. 


Comment 2. Roughly speaking, Theorem 2 means that we can 
reasonably assume that 

	  true = provable.


Of course, here is no contradiction with the well known 
(and non-deniable!) results on non-recursive enumerability 
of arithmetical truth. (All of this except comments being 
in precise (meta)mathematical sense. No philosophy!). 

It is desirable to get analogous results for the case 
of Feasible proofs (by using FPr, Fcon, FCON, etc.). But 
it requires using some appropriate formalization of feasibility 
concept. Thus, we could probably get that 

	  true = feasible provable, 

in the above sense. Otherwise, what does it mean provable in 
practice? The previous results gives no guarantee for feasible 
provability, only imaginary finite provability. Nevertheless, 
they ``demonstrate'' the relation between ``true'' and ``provable'' 
in one of the ways discussed in FOM

Comments on the well-known reflection principle 

	Pr[T](`A') => A. 

are probably also expectable. 


Vladimir Sazonov