Ebthgidr comments on Stupid Questions December 2014 - Less Wrong

16 Post author: Gondolinian 08 December 2014 03:39PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (341)

You are viewing a single comment's thread. Show more comments above.

Comment author: Ebthgidr 17 December 2014 05:44:27PM 0 points [-]

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.

Comment author: DanielFilan 18 December 2014 12:47:12AM 0 points [-]

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.

Comment author: Ebthgidr 18 December 2014 03:30:07AM 0 points [-]

Well, there is, unless i misunderstand what meta level provable(not(provable(consistency))) is on.

Comment author: DanielFilan 18 December 2014 10:54:58AM 0 points [-]

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

Comment author: Ebthgidr 18 December 2014 07:59:31PM *  0 points [-]

That doesn't actually answer my original question--I'll try writing out the full proof.

Premises:

  1. P or not-P is true in PA

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

Comment author: DanielFilan 18 December 2014 09:17:27PM 0 points [-]

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.

Comment author: Ebthgidr 19 December 2014 12:40:39AM 0 points [-]

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?

Comment author: DanielFilan 19 December 2014 07:41:26AM 0 points [-]

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

Comment author: Ebthgidr 19 December 2014 06:12:12PM *  0 points [-]

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)

Comment author: DanielFilan 20 December 2014 06:10:52AM *  0 points [-]

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)

if not(provable(P)) then provable(if provable(P) then P)

which is different, because it has an extra 'provable'.