On Jul 25, 4:36 am, translogi <wilem
...@googlemail.com> wrote:
> Started to puzzle with PA again.
> an i am wondering
> In Pa
> Prov is true iff the formula x is provable
In PA, I will assume you mean.
> Ax [Prov(x) -> Prov(Prov(x))]
This is a theorem of PA.
> and
> ~Ax[Prov(x) <-> Prov(Prov(x))]
This is not a theorem of PA, but it is consistent with PA.
> Therefore
> Ex[ Prov(Prov(x)) & ~Prov(x)]
That is consistent with PA, yes. It can be proved in PA+Con(PA)+~Con(PA
+Con(PA)), for example, which is a consistent extension of PA.
> what is an example of formula x?
> I just don't understand Prov(Prov(x))
> what is the difference between Prov(Prov(x)) and Prov(x)?
We will work in the theory PA+Con(PA)+~Con(PA+Con(PA)), which is
consistent but not 1-consistent. All models of this theory are
nonstandard. This theory asserts that there exists a natural number x
which is the Gödel code for a proof in PA of the assertion "There
exists a natural number y which is the Gödel code for a proof in PA of
a contradiction", which we will denote by S. In a model M for the
theory we are discussing, there does indeed exist such a natural
number x. It is a nonstandard natural number. In the model M, this
nonstandard natural number x is a Gödel code for a proof in PA of the
assertion S. However, in the model M, PA is not 1-consistent. PA is 1-
consistent in "real life", in the standard model, but not in this
nonstandard model. So even though there exists an element of the model
M which is a Gödel code for a proof in PA of the assertion S, there
does not exist an element y of the model M of the kind claimed to
exist by S. There does not exist an element y of the model M which, in
the model, is a proof in PA of a contradiction. PA says (in the model
M) that there exists such a y, but PA is lying. In this model M, you
can't believe everything PA tells you. In the standard model, you can.
In the standard model, Prov(Prov(x)) and Prov(x) are indeed always
equivalent. But there exist consistent extensions of PA in which this
is not the case.
