By using a UTM as a metaphor for the axioms themselves, the UTM must run itself, essentially describing an infinite loop over the finite program, which is another point to consider; with any axiomatic system, is it possible to describe a UTM which you can guarantee halts in finite time? Probably not necessarily.
It seems to be a solid notion that if a paradox can be constructed, then the space is unverifiable, but in this case it feels like the paradox results only from a poorly specified question (the correct answer exists, and is an acknowledgement that the input is meaningless).
The important part to take away is that Gödel himself exists in a logical space where he is able to understand and deal with the absurdity of his paradox, which is outside the scope of the UTM. Every logical system containing a paradox, is a subset of a logical system wherein the absurdity of the paradox is understood. So, perhaps a logical system which explicitly recognises paradoxes as absurd, can be complete. Like NaN in IEEE754, or int|null in dynamic languages.
The result clearly only applies to logical spaces where the paradox is translatable, so i'd be interested to see if a version exists for only basic arithmetic.
A similarly interesting related discussion is the total, abject, and infinite unavailability of a "quadratic formula" for polynomials in x^5 or greater.
> the UTM must run itself, essentially describing an infinite loop over the finite program,
Exactly. I came up with this counterargument not so long ago. It's why neither Gödel's theorems nor the Halting problem ever really impressed me. I don't doubt their validity but the conclusion that no system can be complete is only true for very stringent definitions of "complete". I still believe the Halting problem can be solved in some sense of the word solve. But perhaps I'm being too pragmatic.
> So, perhaps a logical system which explicitly recognises paradoxes as absurd, can be complete.
Gödel explicitly counters this with his second incompleteness theorem which says that no consistent system can provide a proof of its own consistency. In other (but equivalent) words, I might be confident that my mind works correctly but there's technically no way to be completely sure. In fact if I were sure of it, my mind wouldn't be working fine.
> I still believe the Halting problem can be solved in some sense of the word solve. But perhaps I'm being too pragmatic.
While its true there are some forms of functions that can be found to either halt or not, some can't. For example, ask the user for a boolean, and do a while loop based on this value. You can't say whether this will halt or not, but it does contain unspecified variables.
Then consider the Collatz Conjecture. We can't prove any other number then 1 actually reaches 1 without simulating the process. Since we don't even know if the next step will reach the destination, we can't make any decision about when it will halt. If we can't even decide it for such a simple function, then I don't think we can 'solve' it, even for a general 'solve'.
>For example, ask the user for a boolean, and do a while loop based on this value. You can't say whether this will halt or not, but it does contain unspecified variables.
I don't think that's an issue. The Halting Problem ask the question whether a program will halt when supplied with a given input. Nothing is stopping us from providing a separate proof for every single program for every possible that it'll stop.
Either I'm misunderstanding your ideas or you've misunderstood the nature of the problem.
If you're being pragmatic, rest assured that for any machine/program we can construct in this universe, we can decide the halting problem, as it is bound to be finite state, i.e. it will have a bounded amount of states it can be in and repeat itself. Less technical, there is practically no infinite search space, even if theoretically there is - memory of a physical computer can only count up to a certain number, even if very large.
The halting problem, or undecidability in general is the application of a very basic intuition. If I give you infinite space, and ask you to find me a certain something in that space, there is no way I can be sure whether or not you will succeed. Diophantine equations for example, to solve them requires you to search infinitely through the complex plane, and is analogous to the halting problem.
Now in which sense of the word 'solve' could you possibly believe these can be solved? Yes - our problems and machines are finite, so in that sense maybe.
What I mean is that while the proof for the Halting Problem is completely valid, I find it rather "weak" as it uses self-reference. That doesn't tell you anything about how it would work for other programs. The only thing you know is that the problem is undecidable for all input. What would happen if we were to restrict the input to a program to everything that doesn't include the entire program source code?
It's quite similar to Cantor's diagonal argument. Both proofs are completely correct and use a very similar reasoning. The difference is that I'm not interested in almost denumerating the real numbers (I can do that with the rational numbers anyway), but I would be interested in almost solving the Halting Problem.
It seems to be a solid notion that if a paradox can be constructed, then the space is unverifiable, but in this case it feels like the paradox results only from a poorly specified question (the correct answer exists, and is an acknowledgement that the input is meaningless).
The important part to take away is that Gödel himself exists in a logical space where he is able to understand and deal with the absurdity of his paradox, which is outside the scope of the UTM. Every logical system containing a paradox, is a subset of a logical system wherein the absurdity of the paradox is understood. So, perhaps a logical system which explicitly recognises paradoxes as absurd, can be complete. Like NaN in IEEE754, or int|null in dynamic languages.
The result clearly only applies to logical spaces where the paradox is translatable, so i'd be interested to see if a version exists for only basic arithmetic.
A similarly interesting related discussion is the total, abject, and infinite unavailability of a "quadratic formula" for polynomials in x^5 or greater.