Excellent! I wonder how far the malicious behavior can be extended.
Here the problem is that A directly uses a valid but malicious inference module Q. If A were built to enumerate proofs by length and act on the first one of the form “A()==a implies U()==u, and A()!=a implies U()<=u”, can U be rewritten to guarantee that a particular spurious proof comes up first?
Or if A uses a halting oracle to check through statements of that form, can U be written (incorporating that oracle) so that the halting oracle fails to return for the genuine counterfactual and only returns “True” for a particular spurious one?
My next attempt :) Below, “PA” means Peano Arithmetic.
def A():
Enumerate proofs (in PA) by length
if found a proof that "A()==a implies U()==u, and A()!=a implies U()<=u"
then return a
def U():
Enumerate proofs in PA+Consistent(PA) by length up to a very large N
if found a proof that "A()==1"
then return (A()==1 ? 5 : 0)
if(A()==2) return 10
return 0
Proposition: A() returns 1 (if PA is consistent). Proof: Let X = “there exist a!=1 and u, such that: A()==a ⇒ U()==u and A()!=a ⇒ U()<=u”. Let S = “there exists u, such that: A()==1 ⇒ U()==u and A()!=1 ⇒ U()<u”. Let T = “A()==1”. Let ProvableU(P) = the provability formula of U (PA+Consistent(PA), with proofs of length < N). Let ProvableA(P) = the provability formula of A (PA). Let “U⊦ P” mean P is a theorem of U’s proof system. Then:
1. U⊦ ProvableU(T) => S // by inspection of U
2. U⊦ S => ~X // by definitions of X and S
3. U⊦ ProvableU(T) => ~X // from the previous two
4. U⊦ ~X => ~ProvableA(X) // by the axiom Consistent(PA)
5. U⊦ ProvableA(ProvableU(T) => S) // by A's inspection of U
6. U⊦ ProvableA(ProvableU(T)) => ProvableA(S) // from the previous
7. U⊦ ProvableU(T) => ProvableA(ProvableU(T))
// because PA is sufficient to model provability in any formal system
8. U⊦ ProvableU(T) => ProvableA(S) and ~ProvableA(X) // from 3, 4, 6, and 7
9. U⊦ ProvableA(S) and ~ProvableA(X) => T // by inspection of A
10. U⊦ ProvableU(T) => T // from the previous two
11. U⊦ T // by Loeb's theorem
Sorry for not noticing your comment earlier. It would be nice to have a way to subscribe to comment threads.
I don’t understand why the definitions of X and S imply that S ⇒ ~X. Does that rely on specific features of your A and U? For example, if we take a different A and U so that A()==2 and U()==0, then X is true for a=2 and u=0, and S is true for u=1.
Here’s another interesting followup question. My implementation of Q relies on enumerating all proofs in order, so running Q requires exponential time. Is there a “Henkin-style” implementation of Q that constructs the self-referential proof quickly and directly, maybe using the steps of Löb’s theorem or something? That’s how I first tried to construct Q after reading your comments, and failed, but it might still be possible.
where IsValidProof(Statement, Proof) is Goedel’s Bew function, Proof1 is a formalization of the argument that “if Q() returns a valid proof of X, then A() will return 1, and X will be true”, and Proof2 is a formalization of the argument that “a valid proof of A=>B, followed by a valid proof of A, followed by B, is a valid proof”.
def A():
Enumerate proofs by length and act on the first one of the form
"A()==a implies U()==u, and A()!=a implies U()<=u"
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 if(A()==1) return 5
if(A()==2) return 10
return 0
The proof of the statement S: “A()==1 implies U()==5, and A()!=1 implies U()<=5” exists, so it will be found by both A() and U(). Any proof of another statement of the same form would imply “there was no proof of length <N of statement S”, which would be false given high enough N, so it couldn’t be found.
Why is S provable? As far as I can see, you can’t easily prove it by Löb’s theorem, because “if S is provable then S” is not apparent by inspection of A and U, because A could find a different proof earlier.
In Lobian cooperation, the agents search for proofs of only one statement, never stopping early because they found a proof of something else. Your implementation of A doesn’t seem to work like that. Or did I misunderstand and your version of A only looks for proofs where A()==1?
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)
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)
if(A()==2) return 10
return 0
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 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).
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...
[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 thought it couldn’t find any other proofs of length < N, because it would imply there was no proof of S. But this is not a problem if S is false… Ok, modification:
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 if(A()==1) return 5
if found any other proof of the same form
then whatever A() return 0
if(A()==2) return 10
return 0
EDIT: Wait, this is not good, now if(A()==2) is unreachable... EDIT2: No, not actually unreachable, but any proof for a statement of the form “A()==2 ⇒ U()==10...” must be of length > N, which is what was needed, I suppose. Still feels like cheating, but I’m not sure why...
Excellent! I wonder how far the malicious behavior can be extended.
Here the problem is that A directly uses a valid but malicious inference module Q. If A were built to enumerate proofs by length and act on the first one of the form “A()==a implies U()==u, and A()!=a implies U()<=u”, can U be rewritten to guarantee that a particular spurious proof comes up first?
Or if A uses a halting oracle to check through statements of that form, can U be written (incorporating that oracle) so that the halting oracle fails to return for the genuine counterfactual and only returns “True” for a particular spurious one?
These are reasonable questions. I don’t know the answers. Would be cool if someone else figured them out ;-)
My next attempt :) Below, “PA” means Peano Arithmetic.
Proposition: A() returns 1 (if PA is consistent).
Proof:
Let X = “there exist a!=1 and u, such that: A()==a ⇒ U()==u and A()!=a ⇒ U()<=u”.
Let S = “there exists u, such that: A()==1 ⇒ U()==u and A()!=1 ⇒ U()<u”.
Let T = “A()==1”.
Let ProvableU(P) = the provability formula of U (PA+Consistent(PA), with proofs of length < N).
Let ProvableA(P) = the provability formula of A (PA).
Let “U⊦ P” mean P is a theorem of U’s proof system.
Then:
QED
Sorry for not noticing your comment earlier. It would be nice to have a way to subscribe to comment threads.
I don’t understand why the definitions of X and S imply that S ⇒ ~X. Does that rely on specific features of your A and U? For example, if we take a different A and U so that A()==2 and U()==0, then X is true for a=2 and u=0, and S is true for u=1.
Use “Subscribe to RSS Feed” on the right.
Here’s another interesting followup question. My implementation of Q relies on enumerating all proofs in order, so running Q requires exponential time. Is there a “Henkin-style” implementation of Q that constructs the self-referential proof quickly and directly, maybe using the steps of Löb’s theorem or something? That’s how I first tried to construct Q after reading your comments, and failed, but it might still be possible.
Maybe something like this:
where IsValidProof(Statement, Proof) is Goedel’s Bew function, Proof1 is a formalization of the argument that “if Q() returns a valid proof of X, then A() will return 1, and X will be true”, and Proof2 is a formalization of the argument that “a valid proof of A=>B, followed by a valid proof of A, followed by B, is a valid proof”.
The proof of the statement S: “A()==1 implies U()==5, and A()!=1 implies U()<=5” exists, so it will be found by both A() and U(). Any proof of another statement of the same form would imply “there was no proof of length <N of statement S”, which would be false given high enough N, so it couldn’t be found.
I can’t parse your source code for U, does it return a value in every case?
To write code in comments, prefix lines with four spaces, like this:
Thanks, edited.
Why is S provable? As far as I can see, you can’t easily prove it by Löb’s theorem, because “if S is provable then S” is not apparent by inspection of A and U, because A could find a different proof earlier.
I thought it is similar to your proof here.
In Lobian cooperation, the agents search for proofs of only one statement, never stopping early because they found a proof of something else. Your implementation of A doesn’t seem to work like that. Or did I misunderstand and your version of A only looks for proofs where A()==1?
I see what you’re trying to do, but can you explain why A would return 1?
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 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 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...
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.
[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.
I thought it couldn’t find any other proofs of length < N, because it would imply there was no proof of S. But this is not a problem if S is false… Ok, modification:
EDIT: Wait, this is not good, now if(A()==2) is unreachable...
EDIT2: No, not actually unreachable, but any proof for a statement of the form “A()==2 ⇒ U()==10...” must be of length > N, which is what was needed, I suppose. Still feels like cheating, but I’m not sure why...
What’s the intended consequence of A()==2 in your implementation of U? Is it U()==0 or U()==10? And which of those would actually happen?