Gödel has proved the existence of undecidable propositions for any system of recursive axioms capable of formalizing arithmetic. But do we know the logical causes of this state of undecidability? In other words, what are the common or recurrent characteristics of this type of propositions, if any?

  • 2
    Welcome to Philosophy.SE. The list of undecidable problems is very varied. To prove that problem P is undecidable, you can use reduction: show that if you could solve P with a solver S, then you can solve a known-undecidable problem U with S(f(U)), where f is some transformation. That is, you can reduce U to P - and since U is undecidable, P has to be. I doubt that we can give any characteristics other than the definition.
    – user2953
    Jan 9 '17 at 22:27
  • 3
    The "cause" of undecidability in the Gödel sentence specifically is the ability of sufficiently expressive systems to model self-reference, this is discussed in detail in Hofstadter's Gödel, Escher, Bach. Whether undecidable statements in general rely on some hidden self-reference is not entirely clear but highly unlikely, e.g. the continuum hypothesis is undecidable apparently for other reasons, something like inherent vagueness of the continuum notion, see Feferman.
    – Conifold
    Jan 9 '17 at 23:03
  • 1
    You might also like Hofstadter's short article, "Analogies and Metaphors to Explain Gödel's Theorem" as his book, "Gödel, Escher, Bach: An Eternal Golden Braid" is fairly long.
    – MmmHmm
    Jan 10 '17 at 8:23
  • 1
    Gödel created in a very clever way a statement S so that the statement S was equivalent to saying "there is no proof for statement S". If the statement S was true then S would be a true statement with no proof because S says "there is no proof for statement S". If S was false then S would be a false statement for which we have a proof, because "S is false" means "there is a proof for statement S". How to create that statement S you'll need to read up, doesn't fit into 500 or so characters.
    – gnasher729
    Jan 10 '17 at 14:16
  • 1
    A statement S is undecidable if there is neither a proof that it is true, nor a proof that it is false. Gödel created such a statement by basically creating a statement that said it was itself undecidable. There will be other statements where there just isn't a proof. There are plenty of famous mathematical statements for which we don't know a proof, and it wouldn't be unsurprising if many of them don't have a proof.
    – gnasher729
    Jan 10 '17 at 14:20

This answer is a bit technical, but I think the OP will find it interesting.

Let me first recall a bit about the history of the incompleteness theorem (IT). How IT is usually stated is:

If PA (or any recursively axiomatizable theory extending PA) is consistent, then "PA is consistent" is undecidable in PA.

However, this is not what Goedel originally proved! Goedel's proof required an additional assumption: that PA is reasonably correct (specifically, that PA is $\omega$-consistent). This is of course an unfortunate hypothesis; besides making the theorem weaker, it also brings in a hopefully-unnecessary bit of Platonism. (OK, let's say you're fine with Platonism; why should you care about theories which are consistent but false? See below for an answer to this.)

Specifically, Goedel could easily show that "PA doesn't prove Con(PA)," but showing "PA doesn't disprove Con(PA)" required the additional assumption. So strictly speaking, Goedel's original argument certainly contained an unprovability theorem, but arguably fell short of a full undecidability (i.e. unprovability and undisprovability) theorem.

Goedel left it as an open question whether this assumption could be done away with. This was resolved, leading to the usual statement of IT, by Rosser, who showed how a technical trick could improve Goedel's argument. So that lifted Goedel's proof to a genuine undecidability theorem.

Rosser's improvement didn't just lead to a "more formalist" version of IT; it also had real consequences, relevant to your question. Specifically, it shows:

Unprovability is incomputable: there is no algorithm which can determine if a given sentence in the language of arithmetic is unprovable from PA.

Why not? Well, suppose A were such an algorithm. Then we could construct a consistent complete recursively axiomatizable extension of PA (contradicting Rosser's version of IT!) as follows:

  • Enumerate the sentences of arithmetic in a reasonable way as P_1, P_2, P_3, ...

  • Define Q_i inductively as follows:

    • Q_1="Not P_1" if P_1 is unprovable in PA, and Q_1="P_1" otherwise.

    • Having defined Q_i, we let Q_{i+1}="Not P_{i+1}" if the sentence "(Q_1 and Q_2 and ... and Q_i) implies P_{i+1}" is unprovable in PA, and Q_{i+1}="P_{i+1}" otherwise.

Assuming the existence of A, the sequence Q_i is computable. Now consider the theory T=PA+{Q_1, Q_2, Q_3, ...}; this theory is recursively axiomatized, extends PA, and (by an easy induction argument) is consistent; whoops!

Now note that T is probably wrong about many things! At no point in the construction of T did we refer to the truth of sentences of arithmetic, merely their (un)provability. So this argument really needed the full strength of Rosser's version of IT; yet the conclusion, that PA-provability is incomputable, is of interest even if we adopt a fully Platonistic viewpoint and have no a priori interest in incorrect theories of arithmetic.

Now on to the meat of the question: some reasons for undecidability.

The point above - that unprovability is incomputable - can be modified to "undecidability is incomputable" without too much effort. Intuitively, this says that there are many reasons for undecidability (or unprovability), and that we will never have a full understanding of what drives the phenomenon. Interestingly, this clashes with the general fact - mentioned by jobermark above - that almost all currently known examples of undecidability come from self-reference issues.

There are instances of unprovability which do not come from paradoxes, however, and for which there is reasonable philosophical evidence for undisprovability; let me give an example of one of these, which I learned from Asaf Karagila. This is an instance of undecidability, not from PA, but rather from ZFC ( = standard set theory; this is a first-order theory, despite being about sets, and Goedel's theorems apply to it). In particular, the relevant language is different - rather than working in the language ${+, \times, <, 0, 1}$ (or similar) of arithmetic, we're working in the language ${\in}$ of set theory.

An inaccessible cardinal is a particularly large infinite cardinal. Specifically, it is a cardinal which is bigger than the powerset of any cardinal below it, and also satisfies a more technical "regularity" condition. Intuitively, inaccessible cardinals cannot be "built out of smaller cardinals".

Let P be the sentence "There is an inaccessible cardinal" (it is not hard, but somewhat tedious, to express this in the language of set theory), and let's think about P in the set theory ZFC. There are a number of philosophical arguments for the consistency of ZFC together with P; see e.g. Penelope Maddy's article "Believing the axioms". So let's for the moment take Con(ZFC+P) for granted, that is, that ZFC doesn't disprove P. How can we show that ZFC doesn't prove P either?

The usual proof of this is via Goedel's theorem: show that ZFC+P proves Con(ZFC). However, there is a proof avoiding this! Suppose ZFC did prove P. Then let V be a model of ZFC. Since V is a model of ZFC, and ZFC proves P, there is some k in V that V thinks is (i) an inaccessible cardinal, and (ii) the least inaccessible cardinal (since V satisfies Regularity, for any definable property there is a least cardinal with that property if any cardinal with that property exists in the first place).

But now consider V_k, the kth level of the cumulative hierarchy of V. It's not hard to check that V_k satisfies the ZFC axioms. But V_k can't have an inaccessible cardinal! This is because any inaccessible cardinal m in V_k would also be an inaccessible cardinal in V (this isn't obvious, and takes a short argument; in particular, this fails if we replace "inaccessible" with a more complicated large cardinal notion!), and would be less than k (since every cardinal in V_k is less than k); but k was by definition the least inaccessible cardinal in V. So this is a contradiction.

Note that at no point did we invoke IT! This is an example of an unprovability phenomenon which arises for "purely mathematical" (that is, non-metamathematical) reasons. Of course, the distinction is a very subjective one, and reasonable people much smarter than me may very well disagree with the claim I made in the previous sentence; but I still think it's interesting.

Incidentally, it's also worth pointing out that the incompleteness theorem itself has a proof which doesn't really hinge on the paradoxes: namely, Kripke gave a proof which in certain respects is similar to the argument about inaccessibles I outlined above. See this question of mine at mathoverflow for some more proofs of incompleteness.

  • Out of curiosity, why the downvote? Jan 12 '17 at 15:39
  • (Not about the downvote.) Your definition of inaccessible is really just the definition of a limit cardinal, so the continuum would be an example. You need the idea that it cannot be gotten to or jumped over by taking the power set of anything smaller. Otherwise ZFC accesses your cardinal by the axiom of the power set.
    – user9166
    Jan 13 '17 at 17:16
  • Also, independence is not undecidability unless you can state the question. I don't think you can state the question of the existence of the inaccessible cardinal in first order logic. So to my mind, this is a different topic from Goedel's.
    – user9166
    Jan 13 '17 at 17:22
  • @jobermark Re: your first comment, whoops, that was a typo - supposed to read "bigger than the powerset of any cardinal below it." Fixed. (Also my link was wrong - I linked to the axiom of regularity instead of regular cardinals! Fixed that too.) Re: your second comment, this is in the language of set theory - remember, ZFC is a first-order theory in that language. The language is no longer the same, but the existence of inaccessibles is absolutely first-order expressible in the relevant language. Goedel's theorem isn't only limited to the language of arithmetic (cont'd): Jan 13 '17 at 17:26
  • any recursively axiomatizable theory which "interprets" a strong enough theory of arithmetic, in a precise sense, is also subject to it. ZFC is one such theory. See e.g. this question at MSE. Jan 13 '17 at 17:28

We know some, but not all of the potential causes of undecidability, and the ones we do know about are, at root, the same reasons we have paradoxes in ordinary thought. The proofs we have of undecidability generally rely upon a specific known paradox and just formalize it.

For instance Goedel's proof is an elaborate inescapable version of the Cretan paradox. It produces a proposition that says: Proposition #[big number] is not on the list of things we can ever prove, and by the way this is proposition #[big number]. In other words: Cretan-numbered propositions are never provably true, says the Cretan-numbered proposition. But unlike the original Cretan, it only says it is not provable, not that it is lying. So we can avoid absolute paradox by accepting the fact there are things that are true but the system can't prove them.

A simpler version relies upon the 'Berry paradox' -- 'The smallest positive integer not definable in fewer than twelve words' contains less than twelve words and therefore does not define any positive integer. If we count off the numbers of provable propositions systematically, we can, using the system of enumeration always find the equivalent of the magic number twelve in the original paradox. We can prove that any statement provable about a given number is 'at least so complex to state', but state that fact in a statement less complex than that stated minimum.

But we can only see the paradoxes that we see. If we can force a single paradox into so complex a system, we cannot know that there are not other paradoxes lurking around the corner. We in fact know that we cannot know that. The proof itself is not a single deduction, but an algorithm one can apply to any such system. So elaborating the system to resolve a known paradox always still leaves it subject to the same proof of incompleteness.

We can find new undecidable aspects of any formal system by formalizing the principles that the paradoxes that we know derive from:

  1. Self-reference and negation have limited compatibility (Russel's paradox and all its relatives)
  2. Infinity and ordering have limited meaningful application with respect to one another (the unexpected independence of the Axiom of Choice and the Continuum Hypothesis)
  3. Continuity and identifiability have limited compatibility (sorites issues, the quirky limitations of infinitesimals, and the Banach-Tarski paradox)
  4. The ability to know which generalizations constitute definitions and which do not, is implicitly limited (important Goedel-Bernays-VonNeumann collections that cannot be sets -- e.g. the 'group' of all groups under products, which cannot be a group because its base set would contain sets of every size but simply is a group from any normal perspective.)

Kant had already pointed at a single case of each of these limitations with his 'antinomies' -- four problems he felt he had demonstrated were meaningful issues beyond the ability for humans to resolve:

  • 1 is the essence of his answer to the problem of free will,
  • 2 is the essence of his answer to the problem of the end of time,
  • 3 is the essence of his answer to the problem of atoms,
  • 4 is the essence of his answer to the problem of the necessary being.

Now that we understand that formal systems don't really help remove these limitations, we have produced formal systems that evade or resolve them, or we have come to accept them. But that does not mean they are the only sources of potential conflict. We know that they are not.


Given that your main question has been adequately tackled in the comments and answers, I thought perhaps another perspective might be illuminating.

Definition:A statement is undecidable if there is neither a proof that it is true, nor a proof that it is false.

Proposition: Yesterday, I had a cup of coffee in the morning

Now, is there a proof of this fairly innocuous proposition? There is nothing complicated or metaphysical about it; its easy to understand and requires no complicated or even simple mathematics, and is within the everyday experience of just about everybody; as for it's truth...I can vouch for its truth.

Ergo: true, undecidable propositions are easy to find; you too can do this at home, without any danger to one's health or those of your guests or friends; though they may not be impressed.

I would suggest that most propositions are like this, true or false but undecidably so. Why then should we suppose that formal systems are any different?

The question can be turned on its head, can we find a formal system such that all propositions about it can be shown to be decidable? Yes, there are; but they're so simple that they're not worth bothering about.

What is important about the exercise that Godel went through is the invention of a formal system, and its attendent apparatus; for example, theres a proof of Hilberts Nullstellensatz using tools developed from Godels ideas.

Undecidability then is a pervasive phenomena about the real world, which we should not be at all surprised to find reflected in formal systems that look to explain or reflect it - like the natural numbers or geometry; the surprise, I suppose, is that it can be shown in such a simple system as arithmetic; but then, as questions like Fermats theorem have shown, or the still outstanding Riemanns hypothesis they can be very difficult; so, not really that surprising.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.