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