impossible to prove something

Question

(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.

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
@xyzzyz diagonalization method can be used here. For example, P(X)≡if ( ZFC ⊢ Q ) then ( ZFC ⊢ X(X) ) and Q≡P(P) is not provable. Fixed point theorem also can be used here. such P exist... — martian03, Apr 20 '13 at 21:27
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. — Lawrence D'Anna, Apr 20 '13 at 21:52
I think you are using Löb's theorem in the wrong direction. — Carl Mummert, Apr 20 '13 at 21:53
Sorry. I just thought that { ( A ≡ if B then C ) and (B is provable) }results (A implies C). Maybe error reasoning. — martian03, Apr 20 '13 at 21:55
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. — Lawrence D'Anna, Apr 20 '13 at 21:58
@HoCheolSHIN what did you do to the definiton of P? I think it was a lot more clear what you meant before. — Lawrence D'Anna, Apr 20 '13 at 22:16
I actually think your original impredicative definitions of P and Q were clearest, and justified by the usual fixed point shenanigans. — Lawrence D'Anna, Apr 20 '13 at 22:18
@LarryD'Anna it was just P instead of P(P). Pvbl( P ) → { if Pvbl(Q) then P }. — martian03, Apr 20 '13 at 22:19
@LarryD'Anna I changed the direction also. Original was P≡{ if Pvbl(Q) then pvbl(P) } — martian03, Apr 20 '13 at 22:23
OK, but now how do you justify that ZFC proves "Prv(P(P)) -> P(P)" in the first place? — Lawrence D'Anna, Apr 20 '13 at 22:30

Lawrence D'Anna · Accepted Answer · 2013-04-20T22:58:16.797

3

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"

edited Apr 20 '13 at 22:58

answered Apr 20 '13 at 21:32

Lawrence D'Anna

727

in the beginning, I said "under the assumption of consistency of ZFC"...... – martian03 Apr 20 '13 at 21:38
how does consistency of ZFC give you ZFC proving P(P)? – Lawrence D'Anna Apr 20 '13 at 21:39
By definition of P(P) ≡ if ( ZFC ⊢ Q ) then ( ZFC ⊢ P(P) ) – martian03 Apr 20 '13 at 21:40
2

@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. – Carl Mummert Apr 20 '13 at 21:41
HoCheol, perhaps you could spell out as precisely as you can why you think that it ZFC will prove P(P). – Lawrence D'Anna Apr 20 '13 at 21:44
I edited question by comments from @CarlMummert... – martian03 Apr 20 '13 at 21:48

impossible to prove something

1 Answers1