On 17 Apr 2008, at 07:25, Robert Dober wrote: > On Thu, Apr 17, 2008 at 1:31 AM, Eleanor McHugh > <eleanor / games-with-brains.com> wrote: >> Of course this is a terrible abuse of Church-Turing, but it seems >> to fit >> the real world pretty well. > > Oh I was not clear enough I am afraid. I challenge that you can prove > that one cannot prove if your Aircraft control system can halt or not. > I even believe that in theory it can be proven. And if you are not > talking about theory than I agree with you > it is not a fair statement. > This is not nitpicking because I think that serious work is still done > in automatic proving of theorems and the day might come where even > complex systems can be proven to be correct. > Göäel and Turing only show that *complete* systems cannot be correct, > they say nothing about *complex*. It's an interesting semantic point, in that complex is not necessarily he same as complete. But likewise a Turing machine is an ideal device hich cannot exist in the real world: it requires both infinite storage and infinite time so perforce there are computations which it ould make that cannot be made using the means available within our physical environment. However for sake of argument let's suppose that ur complex system is being implemented on such an ideal device and that our interest is in determining whether or not Godel incompleteness is significant. What matters is not specifically how complex the system is, in that a ighly complex system from our perspective may still be composed of provable states, but how many of its states are unprovable within the ontext of the complete system of which it forms a subset. We can therefore see that the application of Godel to a complex but incomplete system operating in ideal conditions would result in a probabilistic incompleteness in that system that at least theoretically could be measured. However this then leads to the question of whether or not the complex ystem is in fact only a subset of a larger complete system, or a complete system in its own right. Considering that it is itself based n a set of axioms (the requirements for the system) and therefore in hat regard complete, I would argue that it was not a subset at all. This appears to create a probabilistic, relativistic incompleteness (which is analogous to the viewpoint that physics has reached regarding our physical universe). But even if we allow the subset to be an incomplete system we can see hat increasing complexity increases the number of states in the system, thus increasing the likelihood of included states being drawn rom the full set of states possible in the complete system. Yet again, we can see that there is a probability of included states being nprovable which beyond a certain level of complexity specific to the ystem would be significant in preventing a formal proof of all the included states. Given that Godel's incompleteness applies to systems as simple as arithmetic, and that even simple desktop applications often contain many more orders of axioms than this, the concept of formal proof should always be seen in light of this probabilistic incompleteness. That is not to say that attempting to prove a system is futile, but merely a recognition that beyond a certain level of complexity specific to a given system there will always be an element of unpredictability even when environmental adjustment of the system does ot apply. Ellie Eleanor McHugh Games With Brains http://slides.games-with-brains.net ---- raise ArgumentError unless @reality.responds_to? :reason