FOM: true => provable [Ignore previous posting with true = provable]

[V. Sazonov]

Let me try again. 

I ask everybody to ignore my previous posting with the subject: 
FOM: True = provable? Was: Goedel: truth and misinterpretations
Here follows a corrected version. 

------------
Here is one simple (metamathematical) result and corresponding 
considerations related with my attempts to give (one of) 
formalizations to ``(ontologically) true, but not provable''. 
The result looks 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, if not explicitly stated otherwise. 

As such a subject is not my current everyday mathematical work, 
I would be especially grateful for any comments by specialists. 
The result is rather simple, but is it 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 1. If T is consistent then it is consistent its 
extension 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 laws we have 

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

It follows that  ~(`T proves a contradiction')
because otherwise the proved contradiction would yield A, B,...,C 
of which it is proved in T that them altogether are unprovable. 

That is T |- Con[T].  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 (true => provable). 

I omit motivation for such kind of result. Read the current 
discussion in FOM where even 

	true = provable 

was suggested as a definition of mathematical truth. 
Is it possible to have any analogous result asserting 
(roughly) this equality by extending T with the stronger 
schema 

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

No, this is hopeless because the negation of (**) may 
equivalently be presented as equivalence 

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

where A asserts its own non-provability. Goedel explicitly 
presented (by a `diagonal' construction) some such sentence 
G = G[T] for the case of any sufficiently strong T (including the 
case of T = PA). 

As Jeffrey Ketland correctly noted, (*) and (***) holding for 
Goedel's diagonal sentence G give T* |- ~G & Pr[T](`G'). 
Moreover, as T |- Con[T] <=> G we also have T* |- ~Con[T]. 
That is T* proves existence of a proof of a contradiction! 
It is well-known that in the case of T = PA, G and Con[T] are 
true in the standard model N of PA. Therefore T* does not hold 
in N. However, all this enterprise with T* was undertaken not 
for the sake of standard model. 


Informal notes. 

As I often mentioned in FOM, I have no idea what is standard 
model from a general point of view, when I think on mathematics 
outside of some its set-theoretic formalisms (specifically, 
outside of ZFC). The only (mathematical) way to approach to 
natural numbers is via formal systems of arithmetics or formal 
systems where arithmetical notions are interpretable. Thus, 
we could probably say that T* (or, say, PA*) is not so bad theory 
describing some natural imaginary world satisfying initial 
(presumably) natural axioms T plus some, also natural axioms 
(*) of metamathematical flavor. There may be some doubts on 
the naturality of the "imaginary world" of T* because it is 
somewhat unlike to what we have usually. Let us discuss this below. 

Thus, we have `truth => provability', but not vice versa (due to 
Goedel), as noted above. It looks strange, at first, that the 
converse implication does (or can) not hold. We know very well 
that what is provable is automatically considered as true in 
mathematics. If we imagine the (illusory) world of objects 
described by any given formal systems, then how it is possible 
that we cannot additionally assume that provable should be true 
(in this, even illusory world)? Mathematical theories and 
thinking are always based on this consideration! Provability is 
the only rational way to approaching to this illusory world. 
The answer which comes to my mind consists in the following. 
Any formalism intended to describe some reality or our fantasies, 
idealizations, illusions about this reality (in the case of PA 
we can think about reality of finite sets of pebbles or the like, 
embodying physically natural numbers) usually results in 
something different from initial plans. (Who predicted or wanted 
that the epsilon-delta definition of continuity would include 
also continuous, but nowhere differentiable functions; such 
"defects" of any formalization are absolutely normal and 
inevitable phenomenon.) Thus, any *traditional* formalism on 
natural numbers leads to "existence" in the imaginary world of 
these numbers some "numbers" which have no relation to the real 
sets of pebbles. We know about non-feasible numbers such as 
2^1000 or 10^{10^{10^{10^{10}}}} or much much bigger "numbers". 
Where from should it follow that any imaginary proof of 
imaginary finite length (assumed in the predicate 

Pr[T](y) \bydef \exists x Proof[T](x,y) 

under the name of the variable x under existential quantifier) 
will give a true (even in the imaginary sense of the imaginary 
world) theorem? (In our case we even have T* |- ~Con[T].) 
Therefore it seems quite reasonable that we have only one way 
implication in (*). (Recall that, newertheless, T* consistently 
extends T.) 

Imaginary provability does not guarantee truth (even illusory one)
Imaginary provability could even give an (imaginary) contradiction. 

On the other hand, it is desirable to have a "feasible" 
version of Theorem 1 with feasible proofs by using 

FPr(y) \bydef \exists feasible x Proof[T](x,y), 
FCon[T] \bydef \not\exists feasible x Proof[T](x,`0=1'), 

etc. But this requires using some appropriate formalization 
of feasibility concept (what is a separate problem). Thus, 
we could probably get a better result that 

	  true => feasible provable 

in the above sense. (Otherwise, what does it mean to be provable 
in practice?) This would be a stronger version of Theorem 1. 
Its previous version gives no guarantee for feasible (real) 
provability, only imaginary finite provability. Nevertheless, 
it demonstrates approximately the relation between ``true'' 
and ``provable'' in one of the ways discussed in FOM these days. 

Moreover, there is probably a hope that Theorem 1 could be 
further strengthened for feasible version of (**), giving 

	true = feasible provable  

which is still desirable, natural and seemingly possible. 
For feasible proofs the Goedel's diagonal trick will hardly 
work! According to one approach to feasible numbers they are 
closed only under addition operation. Multiplication is 
only a partial function there. Bur recall that Goedel's 
trick is based on syntactic substitution operation which 
corresponds to multiplication on natural numbers. 


Of course, here is no contradiction with the well known 
(and non-denial!) results on non-recursive enumerability 
of arithmetical truth in the standard model (understood in 
the framework of ZFC). Th.1 and hopefully its discussed 
above feasible versions (except informal comments) have 
precise (meta)mathematical sense.  


Anyway, this was an exercise around "true = provable". 
I myself should think more on its proper value. 


Any comments, please. 


Vladimir Sazonov