I recently wrote this answer describing Gödel's completeness and incompleteness theorems, in which I came to the conclusion that a theory is (syntactically) complete if and only if all its models are elementarily equivalent, that is no formula in the theory can distinguish between two models of the theory.

The reason is that if for two models $\mathcal M,\mathcal M'$ with $\mathcal M\models\phi$ and $\mathcal M'\not\models\phi$, then neither $\phi$ nor $\neg \phi$ is provable by (semantic) completeness.

Since proving the independence of AC comes down to constructing a model of ZF which does not satisfy AC, is it correct to conclude that the independence of AC implies incompleteness of ZF?

This seems fishy to me because the incompleteness theorem requires some sort of nontrivial Gödel encoding, whereas the construction of the ZF+$\neg$AC uses a completely different technique.

  • 2
    $\begingroup$ Instead of "no formula in the theory can distinguish", you mean "no formula in the language can distinguish", I think. $\endgroup$ Aug 6, 2020 at 20:48
  • $\begingroup$ @Magdiragdag The difference between language and theory is not at all clear to me, so possibly. $\endgroup$
    – Couchy
    Aug 6, 2020 at 20:51
  • $\begingroup$ Language is the set of all well-formed formulas; a theory is just some set of well-formed formulas (maybe required to be closed under derivations). $\endgroup$ Aug 6, 2020 at 21:13

4 Answers 4


The answer depends on what you mean by "the incompleteness theorems". If all you mean is "$ZF$ is incomplete", then yes, the independence of $AC$ is enough to prove that $ZF$ is incomplete (though it's worth remembering that the consistency of $\neg AC$ was proved much later than Gödel's incompleteness theorems).

However, Gödel actually proved statements stronger than just "$ZF$ is incomplete". For example, the first incompleteness theorem tells you that (as long as $ZF$ is consistent) not only is $ZF$ incomplete, but you can't make it complete by adding any computably enumerable list of axioms to it. The second incompleteness theorem tells you specifically that (again, assuming that $ZF$ is consistent) one of the things $ZF$ can't prove is $Con(ZF)$. This is important because there are statements of interest in set theory (such as the consistency of large cardinals) that do imply $Con(ZF)$, and hence we know that $ZF$ can't prove that these statements are true (but remember, knowing that you can't prove $\sigma$ isn't the same thing as proving $\neg\sigma$!).


With ZF and AC, it is the case that one particular set of axioms (such as ZF) is incomplete (since ZF implies neither AC nor $\lnot$ AC).

Gödel incompleteness theorem states that every [computable and consistent] set of axioms [strong enough to model arithmetic] is incomplete. So you cannot add a [computable and consistent with ZF] set of axioms to ZF to make it complete.

  • 1
    $\begingroup$ Good answer, might add that thus by Gödel's incompleteness theorems ZFC (i.e. when we add choice as an axiom) is still incomplete. $\endgroup$ Aug 6, 2020 at 21:15

As the other answers have said, the independence of $\mathsf{AC}$ over $\mathsf{ZF}$ merely suffices to establish a specific case of the incompleteness theorem: that $\mathsf{ZF}$ is not a complete theory. (All that assumes that $\mathsf{ZF}$ is consistent of course!)

However, there's also an important positive aspect here. Gödel's theorem gives a way to assign to any "appropriate" theory $T$ a sentence $\sigma_T$ which is independent of $T$. But this $\sigma_T$ isn't a very interesting sentence on its own - there's no obvious reason to care about it except because its analysis gives us the incompleteness of $T$. By contrast, Cohen and Gödel's work on $\mathsf{AC}$ shows that there is an interesting sentence which is independent of $\mathsf{ZF}$. That's the sort of thing which the incompleteness theorem can't give us on its own (unsurprisingly, since it's an informal statement): a priori there's no reason we couldn't have some "appropriate" theory $T$ that, while incomplete per Gödel, does decide every sentence that actually arises in non-logic-focused mathematics. (E.g. $\mathsf{ZFC+V=L}$ seems to come pretty close to this.)

There is a general attitude - to be fair, I don't know how general, but at least I'm an ardent believer - of "Gödelian optimism" (or "Gödelian pessimism," depending who you talk to): that in fact every "appropriate" theory will have some natural sentence independent of it. The incompleteness theorem only sets the stage for this, it doesn't actually get us all the way there. Gödel/Cohen demonstrate this convincingly for the particular case of $\mathsf{ZF}$ (and Cohen's method of forcing quickly demonstrates the same for many extensions of $\mathsf{ZF}$).

(FWIW, one weak point of evidence in favor of Gödelian optimism is that as a corollary of the incompleteness theorem the set of sentences independent of an "appropriate" theory $T$ is never computable. So there won't ever be a "single reason" that things are independent of $T$. But in my opinion this is still very weak evidence.)

  • $\begingroup$ What is a natural statement independent of V=L (or is V=L not 'appropriate', or do large cardinals and the like count)? $\endgroup$ Aug 7, 2020 at 16:36
  • 1
    $\begingroup$ @spaceisdarkgreen Well, large cardinals feel like a bit of a cheat to me since they increase the consistency strength - ideally we'd want something which is to ZFC+V=L as (say) CH is to ZFC. And I don't really know any examples of these. That said, you might find this old answer of Avshalom's interesting. $\endgroup$ Aug 7, 2020 at 16:38
  • $\begingroup$ I'd find it interesting if I understood it, I'm sure :). I did come across this answer (and also JDH's answer of same thread, which is all higher consistency strength stuff but has some interesting thoughts) $\endgroup$ Aug 7, 2020 at 19:12

As Chris Eagle said, the incompleteness theorems actually imply that ZF does not have a complete consistent extension that is recursively axiomatizable, not just that ZF is incomplete. A much more general version is that any formal system that can prove the outputs of halting program executions and has a proof verifier program cannot be both consistent and complete in its theorems about the outputs of halting program executions. This immediately implies that any recursively enumerable FOL theory that interprets (i.e. can perform the same reasoning as) TC or PA− (mentioned in the linked post) is either inconsistent or incomplete.

You also said that "the incompleteness theorem requires some sort of nontrivial Gödel encoding". That is actually incorrect, and is one of the misconceptions that I address in the linked post. Gödel coding is only needed in the case of theories extending PA− for the sole purpose of demonstrating that PA− can prove basic facts about strings (represented as finite sequences of natural numbers that are in turn encoded as natural numbers). You can observe that the incompleteness theorems for TC needs no such coding business! For similar reasons, Gödel coding is unnecessary to prove the incompleteness theorems for stronger theories that have basic ability to reason about functions on naturals, such as any FOL theory that interprets ACA (a weak theory that is essentially PA plus the ability to construct any set of naturals satisfying some arithmetical property, plus full induction).

This is because any finite string can be naturally encoded as the set $S$ such that $⟨k,x⟩∈S$ iff the k-th number (0-indexed) in the string is $x$, using the easy pair-coding methods. With this, finite strings are definable over ACA as sets encoding functions from $[0..l{−}1]→\mathbb{N}$ for some $l∈\mathbb{N}$, and the length of a string $S$, which shall be denoted as $len(S)$, is then definable as the minimum $l∈\mathbb{N}$ such that $⟨l,x⟩∉S$ for every natural $x$. Concatenation of strings $S,T$ can then be easily defined as $S ∪ \{ ⟨len(S)+k,x⟩ : ⟨k,x⟩∈T \}$, and all basic string manipulation is equally easy.

In particular, ZFC clearly interprets ACA, so you can very well prove the incompleteness theorem for every recursively axiomatizable extension of ZFC without using Gödel coding.

Hence the real reason Gödel needed coding via the β-lemma was that he proved the theorem for a weak theory of arithmetic, which did not have any set-theoretic ability, and so he had to code finite sequences of naturals as a natural itself. In general, the weaker a formal system, the harder it is to prove the incompleteness theorem for it. And Gödel chose a weak system to tackle.


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.