cousin_it comments on An example of self-fulfilling spurious proofs in UDT

[cousin_it]

I see what you’re trying to do, but can you explain why A would return 1?

[gRR]

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.

[cousin_it]

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?

[gRR]

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

[cousin_it]

I think this reasoning is valid:

1. either Provable(S)=>S, or there exists T such that Provable(T) and Provable(~T)

2. either Provable(S)=>S, or Provable(Anything)

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

[gRR]

Ok, how about this:
Provable(Anything)
⇒ Provable(S is the moral argument with the shortest proof of length S
⇒ (Provable(S) ⇒ S)
?

[cousin_it]

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

[orthonormal]

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.

[gRR]

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:

def U():  
  Enumerate proofs by length up to a very large N  
    if found a proof that "A()==1 implies U()==5, and A()!=1 implies U()<=5"  
       then return (A()==1 ? 5 : 0)  
  Enumerate proofs by length up to a very large N  
    if found any other proof of the form "A()==a implies U()==u, and A()!=a implies U()<=u"  
       then return (A()==a ? u-1 : u+1)  
  return (A()==2  ?  10  :  0)  

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

[gRR]

After some more thought, I think you confused me between steps 1 and 2 :)

Provable(T and ~T) implies Anything, not just Provable(Anything). Or not? EDIT: not. sorry.

[gRR]

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

[cousin_it]

I still don’t get it… Why does Provable(Provable(S)) lead to Provable(S)?

[gRR]

Sorry, my error. Two errors, even. I’ll think more.