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.
Best Answer
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$!).