FOM: Re: Reply to Detlefsen on consistency-completeness

Karlis Podnieks podnieks at
Thu Feb 5 04:05:12 EST 1998

-----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
same as saying (PA does not prove G).  This seems not to be what
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,
podnieks at
University of Latvia
Institute of Mathematics and Computer Science

More information about the FOM mailing list