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