Lately I’ve been thinking about proof-based agents: agents that search for proofs in Peano Arithmetic of the consequences of their actions, and decide based on that.
I think when you formulate them right (which would be very different from the last attempt), they have a kind of “free will” that comes from this kind of underspecification.
Specifically: the proof system used to derive stuff like “if I take action A, then the environment will be in state S” cannot derive stuff like “I take action A”.
The model of the agent where I think this works out is it is doing a random proof search. Or a pseudorandom proof search, and “I take action A” means “I take action A regardless of the seed for the random number generator”. That is, the proofs are actually about an ensemble of agents with different RNG seeds.
Since the proof system can’t prove its consistency, it can’t prove that all proof searches will come up with the same result.
This incompleteness about the antecedents of our counterfactuals looks a bit like free will, but it requires considering this ensemble of agents, where we specify they’re doing a proof search but leave out the “microscopic” detail of the RNG seed.
This is in contast to functional decision theory, where we work with a complete specification of the agent, and thus need counterpossible implications, where the antecedent is provably false.
I’m hoping to work out the details and post more about it soon. For now you can believe me or not that this is a coherent theory.
But yeah, I think underspecifying “microscopic” details in a “macroscopic” description is where you get something like free will.
People always say randomness doesn’t help with free will, but it seems to me there’s this weird middle path, where your actions are not determined (in PA), but still not arbitrary (becaue they’re determined in PA+consistency of PA).
An action is later in logical time than the prior considerations that determine it. And the prior considerations shouldn’t always be consequentialist with respect to the resulting action (they could be unrelated background facts, or consequentialist with respect to some other decision, perhaps made by a different agent, which is important for acausal coordination). I think this is conceptually cleaner than only considering consequentialist arguments.
In general, you can’t insist on waiting for a prior consideration to settle before making a decision, since it can take too long (or it can even directly wait for your own action before giving its answer, making it impossible to out-wait it). So there needs to be a timeout. Proof length bounded provability ia one way of doing it, where you wrap all prior considerations in provability-within-length-k boxes. But the issue here is that you might want to care about the proof being used, rather than be OK with any old sufficiently short proof. This is similar to how you might want to care which prior considerations to use, rather than go with all possible consequentialist considerations with respect to your action.
Lately I’ve been thinking about proof-based agents: agents that search for proofs in Peano Arithmetic of the consequences of their actions, and decide based on that.
I think when you formulate them right (which would be very different from the last attempt), they have a kind of “free will” that comes from this kind of underspecification.
Specifically: the proof system used to derive stuff like “if I take action A, then the environment will be in state S” cannot derive stuff like “I take action A”.
The model of the agent where I think this works out is it is doing a random proof search. Or a pseudorandom proof search, and “I take action A” means “I take action A regardless of the seed for the random number generator”. That is, the proofs are actually about an ensemble of agents with different RNG seeds.
Since the proof system can’t prove its consistency, it can’t prove that all proof searches will come up with the same result.
This incompleteness about the antecedents of our counterfactuals looks a bit like free will, but it requires considering this ensemble of agents, where we specify they’re doing a proof search but leave out the “microscopic” detail of the RNG seed.
This is in contast to functional decision theory, where we work with a complete specification of the agent, and thus need counterpossible implications, where the antecedent is provably false.
I’m hoping to work out the details and post more about it soon. For now you can believe me or not that this is a coherent theory.
But yeah, I think underspecifying “microscopic” details in a “macroscopic” description is where you get something like free will.
People always say randomness doesn’t help with free will, but it seems to me there’s this weird middle path, where your actions are not determined (in PA), but still not arbitrary (becaue they’re determined in PA+consistency of PA).
An action is later in logical time than the prior considerations that determine it. And the prior considerations shouldn’t always be consequentialist with respect to the resulting action (they could be unrelated background facts, or consequentialist with respect to some other decision, perhaps made by a different agent, which is important for acausal coordination). I think this is conceptually cleaner than only considering consequentialist arguments.
In general, you can’t insist on waiting for a prior consideration to settle before making a decision, since it can take too long (or it can even directly wait for your own action before giving its answer, making it impossible to out-wait it). So there needs to be a timeout. Proof length bounded provability ia one way of doing it, where you wrap all prior considerations in provability-within-length-k boxes. But the issue here is that you might want to care about the proof being used, rather than be OK with any old sufficiently short proof. This is similar to how you might want to care which prior considerations to use, rather than go with all possible consequentialist considerations with respect to your action.