Yes, I’m referring to 5a/5b in conjunction with self-reflection as a deduction rule, since the agent is described as being able to use these to derive new propositions.
There is also a serious problem with 5a itself: the agent needs to try to prove that some new proposition P is “consistent with its model of the world”. That is, for its existing axioms and derivation rules T, prove that T+P does not derive a contradiction.
If T is consistent, then this is impossible by Gödel’s second incompleteness theorem. Hence for any P, Step 5a will always exhaust all possible proofs of up to whatever bound and return without finding such a proof. Otherwise T is inconsistent and it may be able to find such a proof, but it is also obvious that its proofs can’t be trusted and not at all surprising that it will take the wrong route.
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.
Yes, I’m referring to 5a/5b in conjunction with self-reflection as a deduction rule, since the agent is described as being able to use these to derive new propositions.
There is also a serious problem with 5a itself: the agent needs to try to prove that some new proposition P is “consistent with its model of the world”. That is, for its existing axioms and derivation rules T, prove that T+P does not derive a contradiction.
If T is consistent, then this is impossible by Gödel’s second incompleteness theorem. Hence for any P, Step 5a will always exhaust all possible proofs of up to whatever bound and return without finding such a proof. Otherwise T is inconsistent and it may be able to find such a proof, but it is also obvious that its proofs can’t be trusted and not at all surprising that it will take the wrong route.
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.