[joelshep]

I may be misremembering Godel's proof or misunderstanding your last paragraph, but I thought Godel's proof actually presented a specific undecidable statement. The hope then was that somehow undecidable statements could be cordoned off from decidable statements, and Turing's result showed that that wasn't possible. Perhaps that's what you mean by "the nonexistence of a single algorithm that correctly answers every instance in that family"?

[justinpombrio]

There's no such thing as an undecidable statement. A single statement can't be undecidable. Undecidability is a property of a class of statements.

For example, you can ask whether a Java program, run with infinite memory, will eventually halt. For any particular Java program, there's obviously an algorithm that says whether it halts or not. The algorithm is a single statement, which says either "yes" or "no". Might be hard to figure out which is the correct algorithm, but the Java program is fixed so the algorithm is definitely one of the two.

However, there is no algorithm which can take an arbitrary Java program as input and determine whether it will halt. It's about the class of all possible programs.

[scapp]

That's a different meaning of the word "undecidable". You're talking about undecidable problems [1]. The meaning in Gödel's incompleteness theorem is different and is a synonym with independent [2].

[1] https://en.wikipedia.org/wiki/Undecidable_problem

[2] https://en.wikipedia.org/wiki/Independence_(mathematical_log...

[masfuerte]

> For any particular Java program, there's obviously an algorithm that says whether it halts or not. The algorithm is a single statement, which says either "yes" or "no".

This isn't true.

In general, if a program hasn't halted yet you don't know if it will.

In particular, consider the Collatz conjecture. You can't even tell if your Java implementation of it will halt for a particular input, until it does.

https://en.wikipedia.org/wiki/Collatz_conjecture

[Twey]

And yet there is a correct algorithm — it's either the const yes algorithm or the const no algorithm.

We don't _know_ which algorithm it is, but that's not relevant to the definition of undecidability, which only requires that the algorithm exist.

[masfuerte]

Cheers, I had missed the nuance.

[Twey]

In constructive mathematics I think you'd be right: to call a problem decidable would require you to produce the algorithm that decides it, so you couldn't call the Collatz conjecture decidable (nor could you call it undecidable!). But the usual definition of decidability is classical.

This is slightly bizarre now I think about it: the definition of decidability allows the algorithm selection to be undecidable!

[GoblinSlayer]

It's a gap between physics and mathematics. Undecidable statements exist mathematically, but don't exist physically: mathematics and physics have different concepts of existence. Ironically, even mathematical universe hypothesis deliberately limits mathematics-as-physics to specifically resemble physics of a spontaneous material world, and this limitation is just an axiom.