FOM: Re: Reply to Detlefsen on consistency-completeness

[Karlis Podnieks]

-----Original Message-----
From: Shipman, Joe
Date:  4 Feb 18:27
Subject: FOM: Reply to Detlefsen on consistency-completeness
...
If it is ZF, then you are saying "ZF proves ((PA proves G)
implies (PA
inconsistent))."  But in ZF we know PA is consistent so this is
the
same as saying (PA does not prove G).  This seems not to be what
you
meant.
If it is PA, then you are saying "PA proves (PA proves G
implies PA inconsistent)". This is precisely stated!
-- Joe Shipman

KP> This sounds like a balsam for my fanatic formalist soul! By
the way, formalism is a quite natural religion for computer
scientists. Mathematicians can live safely cheating themselves,
but we - programmers cannot live cheating our computers.

One funny theorem seems to be relevant to this discussion. I
published it in 1975 (when I was still a mathematician) and
called "the double incompleteness theorem":

Let T and M be two formal theories containing the first order
arithmetic, M is used as a metatheory of T. Then there is a
formula H of first order arithmetic such that: if T and M both
are consistent, then H is undecidable in T, but this cannot be
proved in M (more precisely, you cannot prove in M neither that
H is T-unprovable, nor that H is T-unrefutable).

The proof is, of course, a slight variation of the Rosser's
classical proof.

It should be noted also that since the negative solution of the
Hilbert's 10th problem we can have all these Gs and Hs
in the following form:
    not ExEyEz.... D(x, y, z, ...)=0,
where D=0 is some Diophantine equation. Hence, there is a
Diophantine equation D=0 such that if ZF is consistent, then one
cannot prove in ZFC neither that D=0 has solutions, nor that it
has no solutions, but neither of these two unprovabilities can
be established in ZFC.

Best wishes,
K.Podnieks
podnieks at cclu.lv
http://sisenis.com.latnet.lv/~podnieks/
http://www.latnet.lv/LU/MII/Grade/
University of Latvia
Institute of Mathematics and Computer Science