I thought about a different axiomatization, which would not have the same consistency problems. Not sure whether this is the right place, but:
Let X be a variable ranging over all possible agents.
(World Axioms) forall X [Decides(X)=1 ⇒ Receives(X)=1000000] forall X [Decides(X)=2 ⇒ Receives(X)=1000]
(Agent Axioms—utility maximization) BestX = argmax{X} Receives(X) Decision = Decides(BestX)
Then Decision=1 is easily provable, regardless of whether any specific BestX is known.Does not seem to lead to contradictions.
I thought about a different axiomatization, which would not have the same consistency problems. Not sure whether this is the right place, but:
Let X be a variable ranging over all possible agents.
(World Axioms)
forall X [Decides(X)=1 ⇒ Receives(X)=1000000]
forall X [Decides(X)=2 ⇒ Receives(X)=1000]
(Agent Axioms—utility maximization)
BestX = argmax{X} Receives(X)
Decision = Decides(BestX)
Then Decision=1 is easily provable, regardless of whether any specific BestX is known.
Does not seem to lead to contradictions.