Puzzeling with PA
translogi
an i am wondering
In Pa
Prov is true iff the formula x is provable
Ax [Prov(x) -> Prov(Prov(x))]
and
~Ax[Prov(x) <-> Prov(Prov(x))]
Therefore
Ex[ Prov(Prov(x)) & ~Prov(x)]
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)?
Rupert
> 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.
Frederick Williams
Are you sure that Prov(x) means that formula x is provable? Surely it
means that the formula with Godel number x is provable. What (if
anything) are you reading?
--
He is not here; but far away
The noise of life begins again
And ghastly thro' the drizzling rain
On the bald street breaks the blank day.
translogi
>
> - Show quoted text -
Thanks both
I am studying Paul Smiths and Boolos "the logic of provability" in
tandem.
More and more puzzeling if GL really is equivalent to PA
(Is it not GLS that is equivalent to PA)
Boolos says that there is a formula's that is "obviosly false" is
provable in GL.
(while untrue in GLS )
should still be provable in pA (will give formula and refgerence
later)
translogi
there is a sentence [formula] S such that it is consistent with PA
that both S is undecidable and it is provable that S is decidable.
it folows from the (arithmetical) completeness of GL and because PA is
an interpretation of GL.
george
> 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.
This is not even the way you want to phrase this.
The right-arrow IS a theorem of PA.
Therefore you just want to concentrate on the left arrow.
>
> > 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?
Rupert is not answering the question.
It is one thing to give axioms.
It is another to give the requested example.