= 27d567bc2d48d9f40e9ccc20ea370b15)
Ebthgidr comments on Stupid Questions December 2014 - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (341)
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: 1. 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.