FOM: RE: Re: Re: Godel, f.o.m.

[Matt Insall]

Steve Stevenson writes:


> I have the same experiences as you do with program verification. While
> there are some well known views and "foundations," we seem not to make
> much headway in this area. One of Dijkstra's famous "examples" is a
> proof with predicate transformers on gcd. The problem with is "proof",
> as far as I can see, is that he reaches into a magic hat to pull out a
> number theory result that is true in the countable integers but
> probably not true of finite integers in machines.
>



I think this is a singularly important point.  Proofs in computer science
that use ideal objects, such as all the positive integers, generally make
sense only for some sort of approximation theory or for finding a ``negative
result''.  An example of such a ``negative result'' is, of course, the
following corollary of the Halting Problem solution of Gödel/Turing, etc.:
``No physical computer with only finite resources, can be designed and
programmed so that it checks the validity of all existent or possible
programs on such computers.''  Whether this corollary has ever been
``proved'' or not, I am unsure, but it seems to me that it underlies much of
the theory of the limitations on computing in the twentieth century, before
the questions of feasibility (polynomial time vs. exponential time, etc.)
were developed.  To me, such a use of the Gödel/Turing theorem makes sense,
but, as you say, using the completed set of integers to provide a ``positive
result'', such as a program verification, would be, in most cases, tenuous
at best.  One should view it skeptically, therefore, until the method has
been studied in detail.  But in fact, it seems to me that this very problem
of finiteness in physical machines should provide an impetus for more study
of what arithemtic theorems DO hold for finite sets of integers on a
machine.  The study of such things would, I presume be a part of finite
model theory, which has been addressed abstractly in Flum, et. al.
(Ebbinghaus?) in their book ``Finite Model Theory'', which summarizes some
of the literature on the subject in course-form.  The specific study of
``integer arithmetic restricted to the integers between -n and n'' I have
not seen, though I have not looked very hard.  I have at times given it some
thought, but I have not found anything remarkable yet, and something more
interesting to me, and more do-able, always seems to pop up.  :-)





 Name: Matt Insall
 Position: Associate Professor of Mathematics
 Institution: University of Missouri - Rolla
 Research interest: Foundations of Mathematics
 More information: http://www.umr.edu/~insall