[laxd]

Hmm, maybe I just answered my own question. You can't define the set of integers without using elements of the set of integers. Like Peano's successor function. And if you have that power, you can state paradoxes. Like the above mentioned Yablo's paradox. ?

[mmarx]

Presburger arithmetic[0] is powerful enough to describe the natural numbers with addition, yet still consistent and complete. On the other hand, Robinson arithmetic[1] lacks induction, but axiomatizes addition and multiplication, and that is sufficient to make it incomplete. Thus, the problem is not that you can describe the set of natural numbers, or induction, but the interaction between addition and multiplication.

[0] https://en.wikipedia.org/wiki/Presburger_arithmetic [1] https://en.wikipedia.org/wiki/Robinson_arithmetic

[Animats]

There are a few ways around undecidability. One is finiteness. If you have an upper bound, or addition cycles around to zero, there are a finite number of states. Halting is decidable for deterministic machines with finite memory - eventually it must either halt or repeat a state.

(An amusing practical solution to the halting problem is to run two interpreters in parallel, with one running twice as fast as the other. If their states match after starting, the program is in a loop. This trick was sometimes used in the batch computing era to catch beginner student programs that were in a loop before they wasted much CPU time. Programs with long cycles wouldn't be caught, but that was usually not the problem with beginner programs.)

[pron]

The thing is, what does it mean to "work around"? It is true that the halting theorem in its classical formulation can be "worked around" like this, but the classical halting theorem is not the one that matters in practice. What matters in practice is what's sometimes called the bounded halting theorem (which lies at the core of the time-hierarchy theorem), which roughly states that you cannot tell whether a program will halt on input x within n steps in fewer than n steps (and a corollary is that you cannot in general extrapolate information from one input to another). Bounded halting -- which is proved using the same diagonalization proof as the "classical" halting theorem -- is pretty robust. It holds for total languages and even for finite state machines.

So what really bothers us about the halting theorem is that -- in general -- you cannot tell what a program will do with some input any faster than actually running it, and this, bounded halting, is not something we can work around.

[mmarx]

Decidability (as a property of decision problems like the halting problem) is a different notion, though: In the context of incompleteness, an undecidable statement is a statement that cannot be proven or disproved in that system. Decidability of a decision problem is concerned with an effective procedure that, for every instance of the problem, answers yes/no. Specifically for a logical theory, decidability of this theory is deciding for any formula in the same language whether it follows from the theory as a logical consequence.

Neither incompleteness nor undecidability imply the other[0].

[0] https://en.wikipedia.org/wiki/Decidability_(logic)#Relations...

[pron]

Incompleteness does not imply undecidability, but undecidability implies incompleteness, because completeness implies decidability: in a complete system (powerful enough to describe Turing machines), for every TM M and input x, there's a theorem saying that M halts or one that M doesn't halt (because the system is complete). To decide halting, we therefore just need to enumerate all theorems in the system, and we are guaranteed to stop and find the deciding theorem[1].

In fact, when Gödel saw Turing's work and was convinced that Turing indeed captured the general notion of a formal system, he said that the incompleteness theorem was finally satisfactorily proven for all formal systems.

[1]: See http://www.scottaaronson.com/blog/?p=710

[fanf2]

Tortoise/hare loop detection also works pretty well for short-cutting Mandelbrot set iteration :-)