I think that I should modify 5a from “Search for a proof that this sentence is consistent with your model of the world, up to a maximum proof length of one million characters” to “Search to a proof of this sentence, using your model of the world as a set of starting assumptions”. This is indeed a significant change to the algorithm and I thank you for pointing it out. I think that would resolve your second concern, about the problem with 5a itself, yes?
I think it might also resolve your first concern, about the unsoundness of the logical system, because the agent does not have a deduction rule that says that if P can be proved then P is true, but rather reasons from the fact that P can be proved, and the fact that this particular agent chooses its actions based on proof search and will behave in such-and-such a way if it finds a proof of this particular P, to conclude P. This only work for certain particular sentences P, such as the one that is constructed in this story, since this particular sentence P is one that, if the agent finds a proof of it, will cause it to take actions that lead to P itself being true.
Yes, I think this change is much better. I’m still a bit unclear about how exactly the agent reasons about itself. That doesn’t seem to be well-defined.
Is it capable of distinctions between its models of the world? The reasoning in the article leads me to think not. The wording used is of the form “a proof exists of P” rather than “in hypothetical situation H in which I have world model M, my deductive rules could find a proof of P”.
This may lead it to equivocation errors, where the same symbols are used to refer to different things.
I think that I should modify 5a from “Search for a proof that this sentence is consistent with your model of the world, up to a maximum proof length of one million characters” to “Search to a proof of this sentence, using your model of the world as a set of starting assumptions”. This is indeed a significant change to the algorithm and I thank you for pointing it out. I think that would resolve your second concern, about the problem with 5a itself, yes?
I think it might also resolve your first concern, about the unsoundness of the logical system, because the agent does not have a deduction rule that says that if P can be proved then P is true, but rather reasons from the fact that P can be proved, and the fact that this particular agent chooses its actions based on proof search and will behave in such-and-such a way if it finds a proof of this particular P, to conclude P. This only work for certain particular sentences P, such as the one that is constructed in this story, since this particular sentence P is one that, if the agent finds a proof of it, will cause it to take actions that lead to P itself being true.
Yes, I think this change is much better. I’m still a bit unclear about how exactly the agent reasons about itself. That doesn’t seem to be well-defined.
Is it capable of distinctions between its models of the world? The reasoning in the article leads me to think not. The wording used is of the form “a proof exists of P” rather than “in hypothetical situation H in which I have world model M, my deductive rules could find a proof of P”.
This may lead it to equivocation errors, where the same symbols are used to refer to different things.