Hal Ruhl wrote:
My originating post appeals only to the result of Turing to the effect that there is in general no decision procedure.
There's no single decision procedure for a Turing machine, but if you consider more general kinds of "machines", like a "hypercomputer" that can check an infinite number of cases in a finite time, then there may be a single decision procedure for such a machine to decide if any possible statement about arithmetic is true or false. If your "everything" includes only computable universes, then such hypercomputers wouldn't exist in any universe, but if you believe in an "everything" more like Tegmark's collection of all conceivable mathematical structures, then there should be universes where it would be possible to construct such a hypercomputer, even if they can't be constructed in ours.
By the way, do you understand that Godel's proof is based on the idea that, if we have an axiomatic system A, we can always find a statement G that we can understand to mean "axiomatic system A will not prove statement G to be true"? Surely it is not simply a matter of random choice whether G is true or false--we can see that as long as axiomatic system A is consistent, it cannot prove G to be false (because that would mean axiomatic system A [i]will[/i] prove G to be true), nor can it prove it is true (because that would mean it was proving true the statement that it would never prove it true). But this means that A will never prove G true, which means we know G *is* true, provided A is consistent. I would say that we can *know* that the Peano axioms are consistent by consulting our "model" of arithmetic, in the same way we can *know* the axiomatic system discussed in my post at http://www.escribe.com/science/theory/m4584.html is consistent, by realizing those axioms describe the edges and vertices of a triangle. Do you disagree that these model-based proofs of consistency are valid?