There are at least two meanings of "undecidable". The one, from computer science, is discussed in the blog post. The other, from formal logic, is a synonym to "independent". A proposition (not property) is independent of some axiomatic theory with respect to a proof system, if and only if the proposition can neither be proved nor disproved in that theory. For example, the continuum hypothesis is independent of ZFC. A…
Independent and undecidable aren't quite the same, even in formal logic. Or rather, sometimes they are but it’s worth being specific. A proposition P being independent of a theory T means that both (T and P) and (T and not P) are consistent. T has nothing to say about P. This may very well be what Gödel was indicating in his paper. On the other hand, undecidable has a sharper meaning in computation contexts as well a…
> On the other hand, undecidable has a sharper meaning in computation contexts as well as constructive logics without excluded middle. In these cases we can comprehend the “reachability” of propositions. A proposition is not true or false, but may instead be “constructively true”, “constructively false”, or “undecidable”.
Yes, but that just means that independence/undecidability depend on the proof system, as I said before. So when using a constructive proof system, more statements will turn out to be undecidable/independent of a theory than with a classical one, since the constructive proof system doesn't allow non-constructive proofs, but the classical one does.