On Thu, Apr 17, 2008 at 1:36 PM, Sean O'Halpin <sean.ohalpin / gmail.com> wrote:
> On Thu, Apr 17, 2008 at 10:29 AM, Eivind Eklund <eeklund / gmail.com> wrote:
>  >  In the absence of hardware failure (something we of course can't prove
>  >  and is a problem in the real world), we can trivially prove halting
>  >  for a lot of
>
>  (trivlal :)

A surprisingly non-trivial number of cases are trivial.

>  > cases.  E.g, the simple program "halt" halts.
>
>  If 'halt' is defined as implying that the program halts, then you're
>  not really proving anything here. Like saying that true implies true.
>  You have to take that as an axiom.

I am proving that a specific program will halt.  This is a very
trivial proof; that was the intent.  You could of course use an "X:
goto X" for the halt example; it does the same thing.

>
>  > halt if
>  >  true halts.  halt if 1 == 1 would generally halt, assuming no
>  >  redefinition of ==.  An so on.
>
>  Once you invoke conditions, you are invoking some formal system of
>  axioms (like your assumption above) which you have to define. I grant
>  that there are very simple formal systems which are 'complete' but
>  they are generally not 'interesting'. If you want even simple integer
>  arithmetic[1], you're subject to Goedel's incompleteness theorem.

My claim wasn't that reasoning about the system is not subject to
Goedel's incompleteness theorem - it is.  It was that the properties
that was described as being a result of Goedel's incompleteness
theorem was in fact not related to that theorem.  That state proving
is impossible in the case of an infinite memory computer and often
infeasible the case of finite memory computers is, to the best of my
knowledge, a fully separate result.

Eivind.