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?
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...
By now there are numerous others; this is one of the earliest & best known examples in mathematics.