From a newbie here, Aside from the one (and sufficient) self referential formula, have we come up with other examples of non decidable propositions that are meaningful?
Well, famously the halting problem is undecidable.
As a consequence (via Rice's theorem [1]), all nontrivial semantic properties of computer programs are undecidable. That is, there's no algorithm that can answer "does program x have property y?" for all programs, although obviously it's possible to prove propositions about many individual programs.
Because Turing completeness is a fairly low bar to clear, there are infamously a lot of systems that were not designed (or indeed designed not) to be Turing-complete but nevertheless turned out to be so [2]. As such, things like the Java type system is undecidable – in principle there exist Java programs that the compiler can neither reject nor accept.
A well known example (mentioned in the article) is the Continuum Hypothesis (CH; https://en.wikipedia.org/wiki/Continuum_hypothesis). Godel proved CH is consistent with Zermelo-Fraenkel (ZF) set theory; Paul Cohen proved that CH is independent of ZF, and hence CH cannot be decided on the basis of the ZF axioms.
By now there are numerous others; this is one of the earliest & best known examples in mathematics.
Sharlin|2 years ago
As a consequence (via Rice's theorem [1]), all nontrivial semantic properties of computer programs are undecidable. That is, there's no algorithm that can answer "does program x have property y?" for all programs, although obviously it's possible to prove propositions about many individual programs.
Because Turing completeness is a fairly low bar to clear, there are infamously a lot of systems that were not designed (or indeed designed not) to be Turing-complete but nevertheless turned out to be so [2]. As such, things like the Java type system is undecidable – in principle there exist Java programs that the compiler can neither reject nor accept.
[1] https://en.wikipedia.org/wiki/Rice%27s_theorem
[2] https://beza1e1.tuxen.de/articles/accidentally_turing_comple...
kkylin|2 years ago
By now there are numerous others; this is one of the earliest & best known examples in mathematics.