[FOM] Query for Martin Davis. was:truth and consistency

Robin Adams Robin.Adams at stud.man.ac.uk
Thu Jun 12 07:32:58 EDT 2003

On Wed, 11 Jun 2003, Vladimir Sazonov wrote:

> You posting looks like taking my "rules of the game" to demonstrate
> that this leads to some absurd conclusions. But you wrongly
> understood my rules. I think that I already answered to you
> posting in general in my reply to Bill Taylor. I do not know,
> whether this is enough for you. Give me know, if it is not the case.

I wasn't attempting to derive a contradiction.  I was trying to show that,
if one is allowed to reason *about* formal systems, not just within them,
then one can do number theory; one can read number theory as statements
about a formal system N, not merely the derivation of strings within the
formal system PA.  Your answer seems to be that it is illegitimate to
reason about formal systems; what seems to be reasoning about formal
systems should be read just as the derivation of strings within another
formal system, such as ZF (the metatheory).  Have I understood you

If so, why am I not allowed to reason about formal systems the way I
reason about any other activity?  When playing chess, if I am left with a
king and two knights, I am able to deduce that, no matter what moves I
make, I will never be able to produce a position in which my opponent is
checkmated.  Likewise, when deriving strings in N, I am able to deduce
that, whatever string I produce, I will be able to produce a longer string
that is prime, in the sense I defined above.  Why not?  Or is it your
position that I can only reason about chess within some formal system,

Turning the question round, suppose one does maintain the discipline of
only ever doing the metatheory of one system within another; say, one
considers the metatheory of PA as formalised within ZF.  How does the
derivation of strings within ZF tell us anything about PA?

For example, I have read and understood the proof of Godel's theorem, and,
since I believe PA is consistent, I now believe that PA is incomplete.
Let us even say I perform the Herculean labour of writing down the Godel
sentence G as a string of PA.  Now, I think that I have proved that it is
impossible to prove G in PA --- `prove' in the same sense that I can prove
a checkmate impossible from a given chess position, or a Rubik cube
impossible to solve from a given position.

However, according to you, what I have really been doing is deriving
strings in ZF.  Well, why should the fact that

The string ~(PA |- G) is derivable in ZF

cause me to believe that

The string G is underivable in PA

?  These are not the same statement.  How do I infer the second from the

To summarise: if I am allowed to reason about formal systems, then I
maintain my position that number theory is better read as reasoning
*about* N, rather than reasoning *within* PA.  If I am not allowed to
reason about formal systems, then how can metatheory ever be useful?

Robin Adams

More information about the FOM mailing list