FOM: g"odel's proof: software engr's version

[vznuri@earthlink.net]

hi all. since I wrote my last post, n.shankar, 
the author of "metamathematics, machines and g"odel's proof"
tipped me off via email to this really great paper
that actually nails down the viewpoint
that g"odel's proof is a version
of the halting problem, and not vice versa.

"beautifying g"odel, by eric c.r.hehner,
U of toronto" (1990)

http://www.cs.toronto.edu/~hehner/God.pdf

imho, this is the best & most intuitive presentation
of g"odels thm I have ever seen, in terms
of computer language interpreters.

imho, this paper raises the distinct possibility
that the g"odel proof may actually be asserting
a trivial unprovable statement.

I just asked hehner via email what implications his perspective
have on the matijasevich proof of unprovable statements
in diophantine equations.. no reply yet.

I have a similar agenda as dr.simpson in attempting
to resucitate the hilbertian goal of a robust
automated thm proving system for mathematics,
and as part of this, even though it is mathematical sacrilege
(re: a recent thread on theory-edge with TF taking the
establishment/status quo position), imho 
questioning/reexamining the true implications
of the g"odelian thm are in order.

in fact, dr.simpson, I suspect I may have stumbled
on some of your writings when I started theory-edge
over 3 yrs ago, looking for whether anyone had already
covered the area, & I formulated the charter based
on their influence. the theory-edge faq has similar sentiments.
thanks!!