Prev: 3SAT - CNF to CNF Conversion
Next: Program automatically Solves Sudoku
From: cplxphil on 3 Apr 2010 21:04

Consider the following sentence :

S = "S cannot be proven true in PA, and the sentence '(The axioms of
PA are consistent) --> S' cannot be proven true."

Assume that PA is consistent. Then, is S true or false? Assume, for
the sake of contradiction, that it is false. Then we have, "S can be
proven true in PA, OR '(The axioms of PA are consistent) --> S can be
proven true' can be proven true." The first part of the OR clause is
false, because S cannot be proven true in PA if S is false and PA is
consistent. The second part is also false, because if S were true,
then by our assumption that PA is consistent, we would have that PA is
consistent, and thus that S can be proven true.

Thus, we have that if PA is consistent, S is true. However, because
of the fact that S is true, we know that not only can S not be proven
true, but the sentence "PA is consistent --> S" cannot be proven
true...however, that is exactly what we've just proven.

My question is: What is going on here? I don't believe that PA is
inconsistent, but I think that the above sentence can be constructed.
I suppose it's possible that perhaps the sentence '(The axioms of PA
are consistent) --> S' can't be constructed (because we can only refer
to the provability of S, not to the truth of S directly). However, I
was able to construct the following similar sentence with Turing
machines:

(Assume that B is a brute-force Peano-arithmetic proof-finding
algorithm. If it successfully finds a proof of a sentence, it will
accept and halt; otherwise, it will continue searching for a proof
forever and will never halt.)

bool W (algorithm X)
{
if ( B("X(X) accepts")
|| B("PA is consistent --> X(X) accepts"))
//if there's a proof of either sentence
{
while (1)
; //loop forever
}
else //otherwise,
{
return true; //accept
}
}

The sentence is: "W(W) accepts."

Assume that PA is consistent, for the sake of contradiction.

Now assume that W(W) accepts. Because W is a completely defined
algorithm, we know that if the algorithm accepts an input, there is a
proof in PA that it accepts; we merely simulate the input. Thus, if
W(W) accepts, there is a proof that W(W) accepts, and the first half
of the OR clause is satisfied...meaning that the algorithm loops
forever--contradiction. Thus W(W) does not accept.

From our assumption and the above, we can conclude that "PA is
consistent and W(W) does not accept." This can be formalized in Peano
arithmetic as a formal proof; note also that this is the negation of
the second part of the OR clause in the if statement in W.

By inspection, W(W) cannot reject; thus it must loop forever. This in
turn means (also by inspection) that either there is a proof that W(W)
accepts, or a proof that "PA is consistent --> W(W) accepts". We've
already established that both of these sentences are false; thus we
have a contradiction, and that our original assumption is false.
Therefore Peano arithmetic is inconsistent.

As usual, I've probably made a mistake; but I don't know what it is.
If someone could point it out that would be greatly appreciated.

Thank you.

-Phil
From: cplxphil on 3 Apr 2010 21:14
On Apr 3, 9:04 pm, cplxphil <cplxp...(a)gmail.com> wrote:
> Consider the following sentence :
>
> S = "S cannot be proven true in PA, and the sentence '(The axioms of
> PA are consistent) --> S' cannot be proven true."
>
> Assume that PA is consistent.  Then, is S true or false?  Assume, for
> the sake of contradiction, that it is false.  Then we have, "S can be
> proven true in PA, OR '(The axioms of PA are consistent) --> S can be
> proven true' can be proven true."  The first part of the OR clause is
> false, because S cannot be proven true in PA if S is false and PA is
> consistent.  The second part is also false, because if S were true,
> then by our assumption that PA is consistent, we would have that PA is
> consistent, and thus that S can be proven true.
>
> Thus, we have that if PA is consistent, S is true.  However, because
> of the fact that S is true, we know that not only can S not be proven
> true, but the sentence "PA is consistent --> S" cannot be proven
> true...however, that is exactly what we've just proven.
>
> My question is:  What is going on here?  I don't believe that PA is
> inconsistent, but I think that the above sentence can be constructed.
> I suppose it's possible that perhaps the sentence '(The axioms of PA
> are consistent) --> S' can't be constructed (because we can only refer
> to the provability of S, not to the truth of S directly).  However, I
> was able to construct the following similar sentence with Turing
> machines:
>
> (Assume that B is a brute-force Peano-arithmetic proof-finding
> algorithm.  If it successfully finds a proof of a sentence, it will
> accept and halt; otherwise, it will continue searching for a proof
> forever and will never halt.)
>
> bool W (algorithm X)
> {
> if ( B("X(X) accepts")
> || B("PA is consistent --> X(X) accepts"))
> //if there's a proof of either sentence
> {
> while (1)
> ; //loop forever}
>
> else //otherwise,
> {
> return true; //accept
>
> }
> }
>
> The sentence is:  "W(W) accepts."
>
> Assume that PA is consistent, for the sake of contradiction.
>
> Now assume that W(W) accepts.  Because W is a completely defined
> algorithm, we know that if the algorithm accepts an input, there is a
> proof in PA that it accepts; we merely simulate the input.  Thus, if
> W(W) accepts, there is a proof that W(W) accepts, and the first half
> of the OR clause is satisfied...meaning that the algorithm loops
> forever--contradiction.  Thus W(W) does not accept.
>
> From our assumption and the above, we can conclude that "PA is
> consistent and W(W) does not accept."  This can be formalized in Peano
> arithmetic as a formal proof; note also that this is the negation of
> the second part of the OR clause in the if statement in W.
>
> By inspection, W(W) cannot reject; thus it must loop forever.  This in
> turn means (also by inspection) that either there is a proof that W(W)
> accepts, or a proof that "PA is consistent --> W(W) accepts".  We've
> already established that both of these sentences are false; thus we
> have a contradiction, and that our original assumption is false.
> Therefore Peano arithmetic is inconsistent.
>
> As usual, I've probably made a mistake; but I don't know what it is.
> If someone could point it out that would be greatly appreciated.
>
> Thank you.
>
> -Phil


Oops, I caught my own error in the Turing-machine part. The issue is
that there's another way for the algorithm to never halt: If the
proof-finding algorithm never finds a proof of either sentence.

On the bright side, I guess Peano arithmetic is probably consistent
after all. :)

-Phil
From: Tim Little on 4 Apr 2010 04:54
On 2010-04-04, cplxphil <cplxphil(a)gmail.com> wrote:
>
> Consider the following sentence :
>
> S = "S cannot be proven true in PA, and the sentence '(The axioms of
> PA are consistent) --> S' cannot be proven true."

OK, so S = '~Provable(S) and ~Provable(Con(PA) -> S)'


> Assume that PA is consistent. Then, is S true or false? Assume, for
> the sake of contradiction, that it is false. Then we have, "S can be
> proven true in PA, OR '(The axioms of PA are consistent) --> S can be
> proven true' can be proven true." The first part of the OR clause is
> false, because S cannot be proven true in PA if S is false and PA is
> consistent.

Careful: PA has to be more than just consistent to avoid proving
falsehoods. A theory with "1+1=3" as the only nonlogical axiom is
perfectly consistent, but under the most usual interpretation does
prove a falsehood. In this case it's even more distanced, since not
just the theory itself but also the notions of provability need some
sound interpretation into the theory.


> The second part is also false, because if S were true

You are already within an assumption that S is false. If you make the
additional assumption that S is true, you don't need any conditions on
the consistency of PA to derive a contradiction.


- Tim
From: Daryl McCullough on 4 Apr 2010 08:31
cplxphil says...
>
>
>Consider the following sentence :
>
>S = "S cannot be proven true in PA, and the sentence '(The axioms of
>PA are consistent) --> S' cannot be proven true."

If Pr(A) means A is provable, and Con(PA) means PA is consistent,
and ~X means the negation of X, then you are saying that

S <-> ~Pr(S) & ~Pr(Con(PA) -> S)

>Assume that PA is consistent. Then, is S true or false? Assume, for
>the sake of contradiction, that it is false. Then we have, "S can be
>proven true in PA, OR '(The axioms of PA are consistent) --> S can be
>proven true' can be proven true."
>The first part of the OR clause is false, because S cannot be
>proven true in PA if S is false and PA is consistent.
>The second part is also false, because if S were true,
>then by our assumption that PA is consistent, we would have that PA is
>consistent, and thus that S can be proven true.

Okay, we have:

~S <-> Pr(S) or Pr(Con(PA) -> S)

So if S is false, we have:

Pr(S) or Pr(Con(PA) -> S)

Now, you say that if PA is consistent and S is false,
then it is not possible for S to be provable. But that doesn't
follow. A consistent theory can prove false statements.

You need something stronger than Con(PA) to be able
to conclude

~S -> ~Pr(S)

You need soundness: PA is sound if it doesn't prove any false statements.
It follows from your argument that:

If PA is sound, then S is true.

But it doesn't follow that

If PA is consistent, then S is true.

You could try redoing your argument with soundness instead of consistency,
but unfortunately, there is no single statement in PA saying "PA is sound".

--
Daryl McCullough
Ithaca, NY

From: cplxphil on 4 Apr 2010 13:25
On Apr 4, 8:31 am, stevendaryl3...(a)yahoo.com (Daryl McCullough) wrote:
> cplxphil says...
>
>
>
> >Consider the following sentence :
>
> >S = "S cannot be proven true in PA, and the sentence '(The axioms of
> >PA are consistent) --> S' cannot be proven true."
>
> If Pr(A) means A is provable, and Con(PA) means PA is consistent,
> and ~X means the negation of X, then you are saying that
>
> S <-> ~Pr(S) & ~Pr(Con(PA) -> S)
>
> >Assume that PA is consistent.  Then, is S true or false?  Assume, for
> >the sake of contradiction, that it is false.  Then we have, "S can be
> >proven true in PA, OR '(The axioms of PA are consistent) --> S can be
> >proven true' can be proven true."
> >The first part of the OR clause is false, because S cannot be
> >proven true in PA if S is false and PA is consistent.
> >The second part is also false, because if S were true,
> >then by our assumption that PA is consistent, we would have that PA is
> >consistent, and thus that S can be proven true.
>
> Okay, we have:
>
> ~S <-> Pr(S) or Pr(Con(PA) -> S)
>
> So if S is false, we have:
>
> Pr(S) or Pr(Con(PA) -> S)
>
> Now, you say that if PA is consistent and S is false,
> then it is not possible for S to be provable. But that doesn't
> follow. A consistent theory can prove false statements.
>
> You need something stronger than Con(PA) to be able
> to conclude
>
> ~S -> ~Pr(S)
>
> You need soundness: PA is sound if it doesn't prove any false statements.
> It follows from your argument that:
>
> If PA is sound, then S is true.
>
> But it doesn't follow that
>
> If PA is consistent, then S is true.
>
> You could try redoing your argument with soundness instead of consistency,
> but unfortunately, there is no single statement in PA saying "PA is sound".
>
> --
> Daryl McCullough
> Ithaca, NY


Ah...OK, that makes sense. Thanks to both of you (Tim Little and
Daryl McCullough) for pointing this out. I've been confused by this
point before, I think; I've always (inaccurately) equated consistency
with soundness.

I was, actually, wondering why the universe didn't promptly end after
I came up with my "proof" that the axioms of PA are inconsistent. :)

Are there any axiom systems that are powerful enough to express the
notion of their own soundness? If so, would it not follow that all
such axiom systems are inherently inconsistent?

Thanks again.

-Phil
 |  Next  |  Last
Pages: 1 2 3 4 5
Prev: 3SAT - CNF to CNF Conversion
Next: Program automatically Solves Sudoku