My mathematical logic is a bit rusty, but my impression is that the following are true:
Godel’s theorem presents a strictly stronger obstacle than Lob’s theorem. A reflectively consistent theory may still be incomplete, but any complete theory is necessarily reflectively consistent.
The undecidability of the halting problem is basically Godel’s theorem stated in computational terms. If we could identify a subset L of Turing machines for whom the halting problem can be decided, as long as it was closed under operations such as inserting a (non-self-referential) sub-routine, then we would be able to verify any (non-self-referential) property of the program that was also expressible in L. This is a sketch of a claim rather than an actual claim that I’ve proved, though.
Finally, I think it’s worth pointing out an actual example of a program analysis tool since I think they are more powerful than you have in mind. The following slides are a good example of such a tool. At a high level, it gets around the problems you are worried about by constructing an over-approximation of the halting problem that is expressible in propositional logic (and thus decidable, in fact it is even in NP). More generally we can construct a sequence of approximations, each expressible in propositional logic, whose conjunction is no longer an approximation but in fact exactly the original statement.
Godel’s theorem presents a strictly stronger obstacle than Lob’s theorem.
Why do you say that? My understanding is that Godel’s theorem says that a (sufficiently powerful) logical system has true statements it can’t prove, but these statements are excessively complicated and probably not important. Is there some way you envision an AGI being limited in its capacity to achieve its goals by Godel’s theorem, as we envision Lob’s theorem blocking an AGI from trusting its future self to make effective decisions? (Besides where the goals are tailored to be blocked by the theorem: “Prove all true statements in my formal system”)
Finally, I think it’s worth pointing out an actual example of a program analysis tool since I think they are more powerful than you have in mind. The following slides are a good example of such a tool.
As near as I can tell, this is more powerful than other static analysis tools that I have seen (though maybe not, the Google Web Toolkit optimizer is pretty impressive), but it is well within what I expect to be possible, and doesn’t get around Lob’s theorem. (I can’t be too confident in this assessment of its power because I don’t see a clear claim of what sort of statements it can prove or how it works except that it seems to detect when inputs to a statement may have invalid values and that it uses brute force techniques to analyze functions and then associates a summary of the analysis with that function (constraints on valid inputs and guarantees on outputs?) so that its analysis of call sites can use the summary.) (This sort of program analyzer is interesting in its own right, and I would like to see a more complete explanation of it, but I don’t think it’s existence says anything about the problems posed by Lob’s theorem.)
Do you agree or disagree that complete implies reflectively consistent? If you agree, then do you agree or disagree that this means avoidance of Godelian obstacles implies avoidance of Lobian obstacles? If you agree with both of those statements, I’m confused as to why:
Godel’s theorem presents a strictly stronger obstacle than Lob’s theorem.
Ah, so by “Godel’s theorem presents a strictly stronger obstacle than Lob’s theorem” you mean if you overcome Godelian obstacles you also overcome Lobian obstacles? I think I agree, but I am not sure that it is relevant, because the program analyzer examples don’t overcome Godelian obstacles, they just cope with the Godelian obstacles, which does not similarly imply coping with or overcoming Lobian obstacles.
My mathematical logic is a bit rusty, but my impression is that the following are true:
Godel’s theorem presents a strictly stronger obstacle than Lob’s theorem. A reflectively consistent theory may still be incomplete, but any complete theory is necessarily reflectively consistent.
The undecidability of the halting problem is basically Godel’s theorem stated in computational terms. If we could identify a subset L of Turing machines for whom the halting problem can be decided, as long as it was closed under operations such as inserting a (non-self-referential) sub-routine, then we would be able to verify any (non-self-referential) property of the program that was also expressible in L. This is a sketch of a claim rather than an actual claim that I’ve proved, though.
Finally, I think it’s worth pointing out an actual example of a program analysis tool since I think they are more powerful than you have in mind. The following slides are a good example of such a tool. At a high level, it gets around the problems you are worried about by constructing an over-approximation of the halting problem that is expressible in propositional logic (and thus decidable, in fact it is even in NP). More generally we can construct a sequence of approximations, each expressible in propositional logic, whose conjunction is no longer an approximation but in fact exactly the original statement.
Why do you say that? My understanding is that Godel’s theorem says that a (sufficiently powerful) logical system has true statements it can’t prove, but these statements are excessively complicated and probably not important. Is there some way you envision an AGI being limited in its capacity to achieve its goals by Godel’s theorem, as we envision Lob’s theorem blocking an AGI from trusting its future self to make effective decisions? (Besides where the goals are tailored to be blocked by the theorem: “Prove all true statements in my formal system”)
As near as I can tell, this is more powerful than other static analysis tools that I have seen (though maybe not, the Google Web Toolkit optimizer is pretty impressive), but it is well within what I expect to be possible, and doesn’t get around Lob’s theorem. (I can’t be too confident in this assessment of its power because I don’t see a clear claim of what sort of statements it can prove or how it works except that it seems to detect when inputs to a statement may have invalid values and that it uses brute force techniques to analyze functions and then associates a summary of the analysis with that function (constraints on valid inputs and guarantees on outputs?) so that its analysis of call sites can use the summary.) (This sort of program analyzer is interesting in its own right, and I would like to see a more complete explanation of it, but I don’t think it’s existence says anything about the problems posed by Lob’s theorem.)
Do you agree or disagree that complete implies reflectively consistent? If you agree, then do you agree or disagree that this means avoidance of Godelian obstacles implies avoidance of Lobian obstacles? If you agree with both of those statements, I’m confused as to why:
is a controversial statement.
Ah, so by “Godel’s theorem presents a strictly stronger obstacle than Lob’s theorem” you mean if you overcome Godelian obstacles you also overcome Lobian obstacles? I think I agree, but I am not sure that it is relevant, because the program analyzer examples don’t overcome Godelian obstacles, they just cope with the Godelian obstacles, which does not similarly imply coping with or overcoming Lobian obstacles.