I’m not sure that this is true. I can’t find anything that says either way, but there’s a section on Godel’s second incompleteness theorem in the book “Set theory and the continuum hypothesis” by Paul Cohen that implies that the theorem is not provable in the theory that it applies to.
I’ll rephrase it this way: For all C:
Either provable(C) or not(provable(C))
If provable(C), then provable(C)
If not provable(C), then use the above logic to prove provable C.
Therefore all C are provable.
Your reasons were that not(provable(c)) isn’t provable in PA, right? If so, then I will rebut thusly: the setup in my comment immediately above(I.e. either provable(c) or not provable(c)) gets rid of that.
I’m not claiming that there is no proposition C such that not(provable(C)), I’m saying that there is no proposition C such that provable(not(provable(C))) (again, where all of these ‘provable’s are with respect to PA, not our whole ability to prove things). I’m not seeing how you’re getting from not(provable(not(provable(C)))) to provable(C), unless you’re commuting ‘not’s and ’provable’s, which I don’t think you can do for reasons that I’ve stated in an ancestor to this comment.
I think you do misunderstand that, and that the proof of not(provable(consistency(PA))) is not in fact in PA (remember that the “provable()” function refers to provability in PA). Furthermore, regarding your comment before the one that I am responding to now, just because not(provable(C)) isn’t provable in PA, doesn’t mean that provable(C) is provable in PA: there are lots of statements P such that neither provable(P) nor provable(not(P)), since PA is incomplete (because it’s consistent).
I think step 3 is wrong. Expanding out your logic, you are saying that if not(provable(P)), then (if provable(P) then P), then provable(if provable(P) then P). The second step in this chain is wrong, because there are true facts about PA that we can prove, that PA cannot prove.
(if not(p) then (if p then q)) is provable. What I’m claiming isn’t necessarily provable is (if not(p) then provable(if provable(p) then q)), which is a different statement.
The flaw is that you are correctly noticing that provable(if(not(x) then (if x then q)), and incorrectly concluding if(not(x)) then provable(if x then q). It is true that if(not(x)) then (if x then q), but if(not(x)) is not necessarily provable, so (if x then q) is also not necessarily provable.
The whole point of this discussion is that I don’t think that your proof structure is valid. To be honest, I’m not sure where your confusion lies here. Do you think that all statements that are true in PA are provable in PA? If not, how are you deriving provable(if x then q) from (if x then q)?
In regards to your above comment, just because you have provable(x or not(x)) doesn’t mean you have provable(not(x)), which is what you need to deduce provable(if x then q).
To answer the below: I’m not saying that provable(X or notX) implies provable (not X). I’m saying...I’ll just put it in lemma form(P(x) means provable(x):
If P( if x then Q) AND P(if not x then Q)
Then P(not x or Q) and P(x or Q): by rules of if then
Then P( (X and not X) or Q): by rules of distribution
Then P(Q): Rules of or statements
So my proof structure is as follows: Prove that both Provable(P) and not Provable(P) imply provable(P). Then, by the above lemma, Provable(P). I don’t need to prove Provable(not(Provable(P))), that’s not required by the lemma. All I need to prove is that the logical operations that lead from Not(provable(P))) to Provable(P)) are truth and provability preserving
Breaking my no-comment commitment because I think I might know what you were thinking that I didn’t realise that you were thinking (won’t comment after this though): if you start with (provable(provable(P)) or provable(not(provable(P)))), then you can get your desired result, and indeed, provable(provable(P) or not(provable(P))). However, provable(Q or not(Q)) does not imply provable(Q) or provable(not(Q)), since there are undecideable questions in PA.
Ohhh, thanks. That explains it. I feel like there should exist things for which provable(not(p)), but I can’t think of any offhand, so that’ll do for now.
I agree that if you could prove that (if not(provable(P)) then provable(P)), then you could prove provable(P). That being said, I don’t think that you can actually prove (if not(provable(P)) then provable(P)). A few times in this thread, I’ve shown what I think the problem is with your attempted proof—the second half of step 3 does not follow from the first half. You are assuming X, proving Y, then concluding provable(Y), which is false, because X itself might not have been provable. I am really tired of this thread, and will no longer comment.
I’m not sure that this is true. I can’t find anything that says either way, but there’s a section on Godel’s second incompleteness theorem in the book “Set theory and the continuum hypothesis” by Paul Cohen that implies that the theorem is not provable in the theory that it applies to.
I’ll rephrase it this way:
For all C: Either provable(C) or not(provable(C)) If provable(C), then provable(C) If not provable(C), then use the above logic to prove provable C. Therefore all C are provable.
Which “above logic” are you referring to? If you mean your OP, I don’t think that the logic holds, for reasons that I’ve explained in my replies.
Your reasons were that not(provable(c)) isn’t provable in PA, right? If so, then I will rebut thusly: the setup in my comment immediately above(I.e. either provable(c) or not provable(c)) gets rid of that.
I’m not claiming that there is no proposition C such that not(provable(C)), I’m saying that there is no proposition C such that provable(not(provable(C))) (again, where all of these ‘provable’s are with respect to PA, not our whole ability to prove things). I’m not seeing how you’re getting from not(provable(not(provable(C)))) to provable(C), unless you’re commuting ‘not’s and ’provable’s, which I don’t think you can do for reasons that I’ve stated in an ancestor to this comment.
Well, there is, unless i misunderstand what meta level provable(not(provable(consistency))) is on.
I think you do misunderstand that, and that the proof of not(provable(consistency(PA))) is not in fact in PA (remember that the “provable()” function refers to provability in PA). Furthermore, regarding your comment before the one that I am responding to now, just because not(provable(C)) isn’t provable in PA, doesn’t mean that provable(C) is provable in PA: there are lots of statements P such that neither provable(P) nor provable(not(P)), since PA is incomplete (because it’s consistent).
That doesn’t actually answer my original question—I’ll try writing out the full proof.
Premises:
P or not-P is true in PA
Also, because of that, if p → q and not(p)-> q then q—use rules of distribution over and/or
So:
provable(P) or not(provable(P)) by premise 1
2: If provable(P), provable(P) by: switch if p then p to not p or p, premise 1
3: if not(provable(P)) Then provable( if provable(P) then P): since if p then q=not p or q and not(not(p))=p
4: therefore, if not(provable(P)) then provable(P): 3 and Lob’s theorem
5: Therefore Provable(P): By premise 2, line 2, and line 4.
Where’s the flaw? Is it between lines 3 and 4?
I think step 3 is wrong. Expanding out your logic, you are saying that if not(provable(P)), then (if provable(P) then P), then provable(if provable(P) then P). The second step in this chain is wrong, because there are true facts about PA that we can prove, that PA cannot prove.
So the statement (if not(p) then (if p then q)) is not provable in PA? Doesn’t it follow immediately from the definition of if-then in PA?
(if not(p) then (if p then q)) is provable. What I’m claiming isn’t necessarily provable is (if not(p) then provable(if provable(p) then q)), which is a different statement.
Oh, that’s what I’ve been failing to get across.
I’m not saying if not(p) then (if provable(p) then q). I’m saying if not provable(p) then (if provable(p) then q)
You aren’t saying that though. In the post where you numbered your arguments, you said (bolding mine)
which is different, because it has an extra ‘provable’.
So then here’s a smaller lemma: for all x and all q:
If(not(x))
Then provable(if x then q): by definition of if-then
So replace x by Provable(P) and q by p.
Where’s the flaw?
The flaw is that you are correctly noticing that provable(if(not(x) then (if x then q)), and incorrectly concluding if(not(x)) then provable(if x then q). It is true that if(not(x)) then (if x then q), but if(not(x)) is not necessarily provable, so (if x then q) is also not necessarily provable.
is x or not x provable? Then use my proof structure again.
The whole point of this discussion is that I don’t think that your proof structure is valid. To be honest, I’m not sure where your confusion lies here. Do you think that all statements that are true in PA are provable in PA? If not, how are you deriving provable(if x then q) from (if x then q)?
In regards to your above comment, just because you have provable(x or not(x)) doesn’t mean you have provable(not(x)), which is what you need to deduce provable(if x then q).
To answer the below: I’m not saying that provable(X or notX) implies provable (not X). I’m saying...I’ll just put it in lemma form(P(x) means provable(x):
If P( if x then Q) AND P(if not x then Q)
Then P(not x or Q) and P(x or Q): by rules of if then
Then P( (X and not X) or Q): by rules of distribution
Then P(Q): Rules of or statements
So my proof structure is as follows: Prove that both Provable(P) and not Provable(P) imply provable(P). Then, by the above lemma, Provable(P). I don’t need to prove Provable(not(Provable(P))), that’s not required by the lemma. All I need to prove is that the logical operations that lead from Not(provable(P))) to Provable(P)) are truth and provability preserving
Breaking my no-comment commitment because I think I might know what you were thinking that I didn’t realise that you were thinking (won’t comment after this though): if you start with (provable(provable(P)) or provable(not(provable(P)))), then you can get your desired result, and indeed, provable(provable(P) or not(provable(P))). However, provable(Q or not(Q)) does not imply provable(Q) or provable(not(Q)), since there are undecideable questions in PA.
Ohhh, thanks. That explains it. I feel like there should exist things for which provable(not(p)), but I can’t think of any offhand, so that’ll do for now.
I agree that if you could prove that (if not(provable(P)) then provable(P)), then you could prove provable(P). That being said, I don’t think that you can actually prove (if not(provable(P)) then provable(P)). A few times in this thread, I’ve shown what I think the problem is with your attempted proof—the second half of step 3 does not follow from the first half. You are assuming X, proving Y, then concluding provable(Y), which is false, because X itself might not have been provable. I am really tired of this thread, and will no longer comment.