= 27d567bc2d48d9f40e9ccc20ea370b15)
gRR comments on An example of self-fulfilling spurious proofs in UDT - Less Wrong
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 (39)
The intuition is that the proof of "A()==1 implies U()==5, and A()!=1 implies U()<=5", if it exists, would not depend on N, whereas any proof of "A()==2 implies U()==10..." would have to be longer than N, so by making N large enough...
The setup should make "if S has a proof of length < N, then S" apparent by inspection, answering your earlier objection: if S is (<N)-provable, then U() will find the proof (because finding any other proof first would imply U() is unsound), and then return (A()==1 ? 5 : 0), which requires A() to return 1, otherwise U() is unsound again.
I don't think A can assume soundness of the proof system, because soundness implies consistency. Or is there some way for A to reach the proof for A()==1 without using consistency?
But A can use consistency arguments when proving "Provable(S) => S", can't it?
Let S be "A()==1 implies U()==5, and A()!=1 implies U()<=5".
Then the following is provable by inspection: "if T is a moral argument with the shortest proof of length <N, then either T=S or ~T". From this it follows that "either Provable(S) => S, or there exists T, such that Provable(T) and Provable(~T)". From the second part everything provably follows, including "Provable(S) => S". Putting everything together, we get Provable(Provable(S) => S).
I think this reasoning is valid:
either Provable(S)=>S, or there exists T such that Provable(T) and Provable(~T)
either Provable(S)=>S, or Provable(Anything)
either Provable(S)=>S, or Provable(Provable(S)=>S)
But the last step doesn't seem to imply Provable(S)=>S. Or am I missing something again?
Ok, how about this:
Provable(Anything)
=> Provable(S is the moral argument with the shortest proof of length <N)
=> S
=> (Provable(S) => S)
?
Let X be the statement "S is the moral argument with the shortest proof of length <N". Then it's true that X=>S and Provable(X)=>Provable(S), but I don't see why Provable(X)=>S.
In general I think your proof is missing a compelling internal idea, so you probably can't patch it by manipulating symbols. You'll just be inviting more and more subtle mistakes. When I find myself in a situation like this, I usually try to rethink the whole thing until it becomes obvious, and then the proof becomes inevitable even if I compose it sloppily. It's kinda hard to explain...
Good way of putting it.
Yes, I think I know what you mean... it just feels as if there must be an easy technical proof, but, I can't find it...
So I tried to change the solution again, to make the proof easier:
With this, Provable(S) implies S directly, so S is provable, so A must find it, because there are no other short-proof moral arguments if A an U are consistent.
But the provability of S does not depend on A, so U() will never get past the first loop, no matter against which agent it is played. So this is a wrong solution to the original problem. And the previous one would be wrong for the same reason, even if I did find the proof...
[EDIT: this is wrong] You're saying, I don't get "Provable(Provable(S) => S)", but only "Provable(Provable(Provable(S) => S))"?
But then,
Provable(Provable(Provable(S) => S)) =>
Provable(Provable(Provable(S)) => Provable(S)) => /Loeb's theorem/
Provable(Provable(S)) =>
[EDIT: this is also wrong] Provable(S)
I still don't get it... Why does Provable(Provable(S)) lead to Provable(S)?
Sorry, my error. Two errors, even. I'll think more.