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

[Robin Adams]

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
correctly?

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,
too?

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
first?

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