FOM: provability and truth

[Walter Felscher]

All mathematicians present their insights as theorems and support them
with chains of arguments they call proofs. Of course, these are not
formal proofs with explicitly stated logical rules, but mathematicians
believe that they proceed by the "laws of logic" (and the logician
will know how to rewrite a mathematician's proof as a formal one, from
the mathematician's hypotheses and in a suitable frame such as PA or ZF).

In particular, mathematicians do _not_ verify the truth of a universally
quantified statement U(x) a(x)  [where x , say, ranges over natural or
real numbers]  by verifying that a(x) is true for every single assignment
of a number n to x ; rather they argue with a "general n ", i.e. they
prove a(y) with an eigenvariable y .

Note 1 . When Frege in 1879 formulated the logical rules for the
         universal quantifier (Ux), he did so by analyzing the
         mathematicians' usage in their informal proofs. In particular,
         he formulated the first of the two _critical_ rules, namely
         that, in order to logically conclude from assumptions M upon
         a statement (Ux) a(x) , it is a sufficient hypothesis to
         conclude from M upon a(y) where y is a variable (a letter,
         Frege says) not occurring free in the expressions of the
         conclusion. In Gentzen's convenient notation, these rules
         take the form

         M  ==>  a(y)                 M , a(y)       ==>  b
         M  ==>  (Ux) a(x)            M , (Ex) a(x)  ==>  b     .

         where y then is called an eigenvariable.

         Talking about numbers n , angels and demons may be able to
         evaluate a(x) for every single n assigned to x ; man in his
         finite life never will achieve that task. Instead, he is
         required to secure a(y) with an eigenvariable, i.e. to
         present a schematical argument working with such y . So the
         mathematician, indeed, will justify his conclusion from a
         much _stronger_ hypothesis, namely a proof of M ==> a(y)
         which is _uniform_ in y . In case our language admits, for
         every number n , a name ^n , the verification of the truth of
         M ==> (Ux) a(x) amounts to an omega-rule requiring the
         infinitely many premisses M ==> a(^n) , while man's single
         premiss M ==> a(y) entails M ==> a(^n) _uniformly_ for every n .

         Thus the conclusions  M ==> (Ux) a(x) which the mathematician
         proves are justified in a much _stronger_ way than those which
         angels and demons might obtain from their omega-rules and
         their alleged verifications of truth.

Note 2 . Clearly, the situation is completely analogous in the case of
         mathematical induction where in the induction premiss
         M , a(y) ==> a(y+1) the letter y must be an eigenvariable. This
         becomes particularly plain in the induction proofs taught to
         beginners in which a(y+1) is secured from a(y) by a
         computation with letters at the level of school algebra.

         Again, the mathematician secures the induction hypothesis in
         a _uniform_ way. And again his conclusions then are justified
         in a much stronger manner than would be those which angels and
         demons might obtain by verifying for every n separately that
         a(^n) entails a(^n+1) .

So the mathematician does _not_ secure his insights by verification -
in whichever real or mental world one might conceive. Still, he
usually calls what he has proven to be true - and only what he has
proven he does call so. [The background for this terminology is, we
may suppose, the soundness of the logical rules: if the mathematician's
hypotheses are assumed to be true, then so are the results of his
proofs.] In so far, the mathematician identifies truth, sometimes
specified as "in the usual mathematical sense", and (informal)
provability.

Note 3 . Assuming soundness, it is unproblematical to call true what
         has been proven. Conversely, it may be unproblematical as
         well to call provable what is conceived to have been
         recognized as true, as long as it is kept in mind that,
         verification in infinite domains being inaccessible, the only
         means of such recognition is a proof.

Note 4 . The mathematician's identification of truth and provability
         is closely connected with the fact that his notion of
         provability is that of classical logic with classical
         negation. Its laws can be motivated only by properties
         conceived to hold for truth. Examples abound, such as the
         uses of classical contraposition, of tertium non datur, or of
         -(Ux)a(x) -> (Ex)-a(x) .


Distinguishing between truth and provability becomes, obviously,
necessary in certain discussions of Goedel's incompleteness theorem.
The setting there is the following.

   There is the set N of natural numbers for which we have developed
   the theory of recursive functions. [ N and its functions must not
   necessarily be present in their infinity, but at least as far as our
   considerations need it.] Let R abbreviate 'recursive' and RE
   abbreviate 'recursively enumerable'.

   There is a formal language L containing a constant ^n for every n
   in N . There is an axiom system G formulated in L (e.g. Robinson's
   arithmetic).

   An 2-ary relation R is _G-defined_ by a formula v(x,y) if R(n,m) iff
   G proves v(^n,^m). R is _G-represented_ by a formula v(x,y) iff
   (R(n,m) implies that G proves v(^n,^m) and not R(n,m) implies that G
   proves -v(^n,^m)). A function f(x)=y is _G-represented_ by a term
   t(x) if f(n)=m implies that G proves t(^n)=^m . These notions
   extend to n-ary relations and functions in the obvious way.

   There is a coding of terms and formulas from L and derivations from
   G , assigning to every such object a a code |a| in N . The function
   sub(|v|,|x|,|t|)=|sub(x,t;v)| is R . If G is RE the so is the 2-ary
   relation ded holding between |v| and |s| if s is a deduction from G
   of the formula v . The function from n to |^n| is R .

   The assumption, when made, that there be a model A of G on the set
   N will be stated explicitly.

Let the sets prov and provs consist of the codes of provable formulas and
sentences. There now is a first

Thm 1  Let G be RE a assume that every recursive relation is
       G-definable. Then [G is incomplete and] prov and provs are RE
       but are not R .

The proof is indirect. [This seems to be the theorem to which Mr. Kanovei
alluded in his note on Oct 25, 19:28 +2.] - If there is a model A of G
then provs is a subset of the set trues of codes of sentences true in A .
If G is incomplete then provs must be a proper subset of trues. Hence

Cor 1  Let G be RE and assume that every recursive relation is
       G-definable. If A is a model of G then there is a true, but not
       provable sentence.

Observe that this true sentence is not exhibited. -  There now is a
second

Thm 2  Let G be R and assume that every recusive relation and every
       recursive function is G-representable. Assume that A is a model
       of G . Then a true, but not provable sentence s can be explicitly
       exhibited.

The sentence s may, for instance, be obtained by starting from a formula
DED(z,y) which represents the relation ded (mentioned above), setting
BEW(z)=(Ey)DED(z,y) and taking s as the fixpoint to -BEW(z), i.e. such
that s is G-provably equivalent to -BEW(^|s|). 

Without assuming the model A , we see only that G is omega-incomplete:
(Uy)-DED(^|w|,y) is not provable, while -DED(^|w|,^|m|) is provable for
every m . Mr. Davis, in his note on Nov.8, 10:23 -8, observed already that
in order to conclude upon the truth of s the full properties of a model A
are not quite needed

   ["the soundness of T <G> (even with respect to sentences of a very
    simple logical form) ..."] ,

and indeed, it suffices to have 

   (1) the notion of truth in A for sentences DED(^|n|,^|m|), -DED(^|n|,^|m|),
       BEW(^|n|), -BEW(¬|n|) such that for any sentence s of this type
       either s or -s is true, and if BEW(^|n|) is true then there exists
       b in A such that n,b satisfy DED(z,y) ,

       if s and s -> s' are true then s' is true

   (2) if w is semantically equivalent in A to -BEW(^|n|) then provability
       of w implies that w is true

where (2) indeed connects provability from G with truth in A .  
           
In view of the differences both in the hypotheses and in the results of
Cor 1 and Thm 2 , it should be clear that semantical hypotheses for such
theorems not only are required, but that they should carefully be spelled
out. Hypotheses about soundness cannot be waved away in a cavalier
manner by referring to "truth in the usual mathematical sense".


W.F.