= 27d567bc2d48d9f40e9ccc20ea370b15)
DanielFilan 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)
A question about Lob's theorem: assume not provable(X). Then, by rules of If-then statements, if provable(X) then X is provable But then, by Lob's theorem, provable(X), which is a contradiction. What am I missing here?
I'm not sure how you're getting from not provable(X) to provable(provable(X) -> X), and I think you might be mixing meta levels. If you could prove not provable(X), then I think you could prove (provable(X) ->X), which then gives you provable(X). Perhaps the solution is that you can never prove not provable(X)? I'm not sure about this though.
I forget the formal name for the theorem, but isn't (if X then Y) iff (not-x or Y) provable in PA? Because I was pretty sure that's a fundamental theorem in first order logic. Your solution is the one that looked best, but it still feels wrong. Here's why: Say P is provable. Then not-P is provably false. Then not(provable(not-P)) is provable. Not being able to prove not(provable(x)) means nothing is provable.
You're right that (if X then Y) is just fancy notation for (not(X) or Y). However, I think you're mixing up levels of where things are being proved. For the purposes of the rest of this comment, I'll use provable(X) to mean that PA or whatever proves X, and not that we can prove X. Now, suppose provable(P). Then provable(not(not(P))) is derivable in PA. You then claim that not(provable(not(P))) follows in PA, that is to say, that provable(not(Q)) -> not(provable(Q)). However, this is precisely the statement that PA is consistent, which is not provable in PA. Therefore, even though we can go on to prove not(provable(not(P))), PA can't, so that last step doesn't work.
Wait. Not(provable(consistency)) is provable in PA? Then run that through the above.
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.
Ok, thanks for clearing that up.