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

V. Sazonov V.Sazonov at doc.mmu.ac.uk
Tue Nov 7 15:37:56 EST 2000

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