(Edited by comments)

Let sentence P and Q are under this situation:

, in logic of ZFC theory

Pvbl( P(X) ) → { if Pvbl(Q) then X(X) }

Q≡ ¬pvlb( P(P) )

using fixed point theorem, let's make it more clearly.

Pvbl( P ) → { if Pvbl(Q) then P }

Q≡ ¬pvlb( P )

claim: under the assumption of consistency of ZFC, Q is not provable

proof of claim:

Assume Pvbl(Q), Then, ZFC proves "Prv(Q)".

so ZFC proves " Prv(P) → P " by modus ponons

by Lob theorem, P is provable.

But Q implies ¬(Pvbl(P), so P is disprovable.

P is provable and disprovable. It means ZFC is inconsistent.

But we assumed that ZFC is consistent.

Therefore, Q is not provable.


Is this correct reasoning?

  • 1
    $\begingroup$ Your definition of $P$ is circular, i.e. it refers to itself in the definition. $\endgroup$ – xyzzyz Apr 20 '13 at 21:22
  • 1
    $\begingroup$ The question seems to indicate that you have not yet completely understood the difference between saying "ZFC proves Z" and "ZFC proves Pvbl(Z)". In particular, both of the $\vdash$ near the top of the question should be Pvbl. ZFC cannot refer to the actual $\vdash$ relation. $\endgroup$ – Carl Mummert Apr 20 '13 at 21:43
  • 2
    $\begingroup$ are you saying "P(P) implies automatically ( Pvbl(P(P)) )" inside ZFC? It's very unclear when you are switching between the object and the meta language. $\endgroup$ – Larry D'Anna Apr 20 '13 at 21:52
  • 2
    $\begingroup$ Yes, that is not correct reasoning. For example, ZFC proves the statement A = "$0 = 1 \to 1 = 2$", but "Pvbl(0=1)" does not imply $A \to 1 = 2$. You are mixing real provability with formalized provability. It is true that if $ZFC \vdash B \to C$ and $ZFC \vdash B$ then $ZFC \vdash C$. $\endgroup$ – Carl Mummert Apr 20 '13 at 21:58
  • 2
    $\begingroup$ ok, actually you are right about that part, but the way you phrased it very confusing.. what you have is this: assume ZFC proves "Q". then ZFC proves "Prv(Q)". so ZFC proves "P(P) -> Prv(P(P))" by modus ponons but then when you go to use Lob, you're using it backwards. $\endgroup$ – Larry D'Anna Apr 20 '13 at 21:58

The conclusion is correct, but the argument is not. ZFC will not prove Q because Q implies Con(ZFC), which we can't have by Gödel. however you are using Lob's Thorem backwards. Lob says if you can prove "Prbl(X) -> X" then you can prove "X", not the other way around.

(edit): I think we've resolved the confusion. The argument is this: Let P and Q be sentences such that ZFC proves "Prv(P) -> Prv(Q) -> P" and "Q <-> ~Prv(P)" then (assuming it's consistent) ZFC doesn't prove Q.

proof: if it does, then it proves "Prv(Q)", so it proves "Prv(P) -> P", so it proves P by Lob, so it proves "Prv(P)", so it proves "~Q"

  • $\begingroup$ in the beginning, I said "under the assumption of consistency of ZFC"...... $\endgroup$ – HoCheol SHIN Apr 20 '13 at 21:38
  • $\begingroup$ how does consistency of ZFC give you ZFC proving P(P)? $\endgroup$ – Larry D'Anna Apr 20 '13 at 21:39
  • $\begingroup$ By definition of P(P) ≡ if ( ZFC ⊢ Q ) then ( ZFC ⊢ P(P) ) $\endgroup$ – HoCheol SHIN Apr 20 '13 at 21:40
  • 2
    $\begingroup$ @HoCheol SHIN: even if we assume ZFC is consistent, ZFC does not prove Con(ZFC). In fact, when we assume ZFC is consistent, the incompleteness theorem tells us that one thing ZFC will not prove is Con(ZFC). But then ZFC cannot prove Q either, as Larry D'Anna has explained. $\endgroup$ – Carl Mummert Apr 20 '13 at 21:41
  • $\begingroup$ HoCheol, perhaps you could spell out as precisely as you can why you think that it ZFC will prove P(P). $\endgroup$ – Larry D'Anna Apr 20 '13 at 21:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.