impossible to prove something

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.

Q.E.D.

Is this correct reasoning?

• Your definition of $P$ is circular, i.e. it refers to itself in the definition. – xyzzyz Apr 20 '13 at 21:22
• 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. – Carl Mummert Apr 20 '13 at 21:43
• 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. – Larry D'Anna Apr 20 '13 at 21:52
• 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$. – Carl Mummert Apr 20 '13 at 21:58
• 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. – Larry D'Anna Apr 20 '13 at 21:58