As a mathematician interested in novel applications I am trying to gain a deeper understanding of (the non-constructiveness of) Gödel's Completeness Theorem and have recently studying two texts: Mathematical Logic for Mathematicians (by Y.Manin) and the book on Reverse Mathematics by Simpson [2009]. Having read Mendelsohn and Crossley (and other works) I am actually surprised by the non-constructivism in this proof, due to the fact that many classic logic texts do not emphasis it.

However Manin emphasises that the proofs (and he presents 4 proofs for completeness/compactness) are all via the Axiom of Choice.

Meanwhile in the Reverse Mathematics work we learn that the non-constructiveness is identified as the "Weak Konig's Lemma" (WKL) assumption. I see from reviewing the online summaries of Gödel's original proof that Gödel used Konig's Lemma itself. Konig's Lemma lies in a higher "non-constructivity class" ACA in Reverse Mathematics, than does WKL.

Now the problem I have with this non-constructiveness is that both Axiom of Choice and WKL are not necessary truths: we can (I think) have a mathematical universe in which they are negated. However I see that WKL is provable in ZF. Hence Gödel's Completeness theorem is not a necessary truth either - but to be a logic theorem it needs to be a necessary truth, not conditional on another assumption surely?

In this paper Gödel ends his dissertation with :

"essential use is made of the principle of the excluded middle for infinite collections... It might perhaps appear that this would invalidate the entire completeness proof."

In summary has this invalidation has not been suggested in recent years by the recognition of the following facts not known to Gödel or in 1930 ?:

  1. Konig's Lemma is a consequence of the Axiom of Choice
  2. The proof can be reduced to Weak Konig's Lemma, but no further
  3. Axiom of Choice is not a necessary logical truth (merely a mathematical convenience)
  4. The theorems of Turing Computability theory (which play a role in understanding the Lindenbaum Lemma non-constructivity from another perspective)
  • or does it all depend on whether WKL (as opposed to AC) actually is classically refutable?

EDIT: I have a linked question which contains discussion on a related topic.

I shall add a summary of some of the comments from below, to make the question more self-contained. Also I hope that it will make answering it easier if I add some more background.

In this question I am viewing Logic and Mathematics as separate, but overlapping topics: there are aspects of Logic not relevant to Mathematics and vice versa. This question is primarily about its title: the Constructiveness (or otherwise) of Gödel's Completeness Theorem (GC) and the consequences of that. Mathematical topics and mathematical philosophy are relevant only if they are directly connected, as I see this as a question about Logic.

Historically there is a particular timeline, which contains some unexpected twists:

Gödel (1929) Dissertation (Unpublished) --- Contains qualms about non-constructiveness in GC

Gödel (1930) GC paper Published --- All qualms removed, giving initial appearance of constructiveness. Reinvents Konig's Lemma.

Kleene (1952) Intro. to MetaMathematics --- Proves GC non-constructively using Gödel-Henkin proof. This uses "Lindenbaum Lemma". Claims that AC is not required in his proof.

Later texts (e.g. Boolos-Jeffrey) --- No reference to non-constructiveness in GC

Manin "Logic for Mathematicians" --- "we shall have to use Zorn's Lemma"

Reverse Mathematics --- Weak Konig Lemma for GC

So which of all these is correct? If an Answer were to claim that GC was constructive, then the Answerer will have to justify that answer. If an Answer were to claim that GC was non-constructive then we have at least two distinct possibilities: WKL or Zorn. Furthermore the latter case re-opens Gödel's original non-Constructiveness qualms. Do these qualms have any validity - for example is there a sense in which it is not "universally valid"?

Note also that GC is exceptional amongst Gödel's work in that he generally worked within constructive frameworks as with his Incompleteness Theorem, etc.

I have now studied another proof of GC by Hilbert-Bernays(1939). This theorem only applies in the Arithmetic domain (not Sets) and is again non-constructive. The "price" that has been paid for the non-constructivity is that the system will be $\omega-$inconsistent (rather than incomplete- since it is a completeness theorem). Summarising: a "true" statement (for all numbers) can be falsified by a proof of its negation.

Now $\omega$-inconsistency does not exist for general domains, so is the non-constructive proof still considered entirely valid? Put simply: is there a new type of Gödel Incompleteness?

  • 1
    $\begingroup$ What do you mean "truth"? $\endgroup$ – Asaf Karagila Feb 2 '14 at 23:17
  • $\begingroup$ "Logical truth" here is shorthand for the fact that Cohen independence makes AC not a necessary consequence of ZF. For a statement which is a consequence of ZF (like WKL) the question is whether ZF is logically necessary (at least WKL). In each case can one construct a counterexample? IE False = a counter-example exists. $\endgroup$ – Roy Simpson Feb 2 '14 at 23:25
  • $\begingroup$ So "truth" means a consequence of $\sf ZF$? Are you trying to find out consistent counterexamples for the completeness theorem in $\sf ZF$ or...? $\endgroup$ – Asaf Karagila Feb 2 '14 at 23:26
  • $\begingroup$ 1. Can a consistent counterexample to completeness exist in ZF? No if it really only depends on WKL and not AC. Yes if there is a tacit dependence on AC somewhere in the proof. 2. Otherwise could a consistent counterexample exist in a simpler structure than full ZF, one that does not imply WKL? After all Godel completeness is about Logic not Set theory per se. $\endgroup$ – Roy Simpson Feb 2 '14 at 23:32
  • $\begingroup$ Okay. I can write a partial answer now. And I will. $\endgroup$ – Asaf Karagila Feb 2 '14 at 23:34

Here is a partial answer.

Godel's theorem connects logic and set theory. Syntax is the part of the logic, it's where the formulas and proofs live; set theory is the part of the semantics, where the interpretations and models live. Of course one can have them relocated to other contexts, but classically I think that it's a theorem about logic and set theory.

It is provable without the axiom of choice that if we have an infinite tree whose nodes are the natural numbers, and every level of the tree is finite, then there is a branch in that tree. If we omit the requirement that the nodes of the tree are the natural numbers, it won't be true anymore and counterexamples do exist (by which I mean, consistent with $\sf ZF$, of course).

Similarly, given a countable language we write the proof of the completeness theorem for that language, and all our uses of the axiom of choice will be mitigated by the fact that we have a uniform enumeration of all the objects of interest. Therefore some fragment of the completeness theorem is in fact provable without any appeal to the axiom of choice.

On the other hand, the completeness theorem is not about countable languages. It is about any language of first-order logic. So we can have a lot of function symbols, or constants, or so on. So what about the above proof? Well, it can be shown that if the language is well-orderable, then indeed we can repeat the same arguments and everything is well-orderable uniformly and everything is fine.

But alas, without the axiom of choice, not every set can be well-ordered. And that where the non-constructive nature of the proof sneaks in. Let me give a particular counterexample.


We say that a set $A$ is amorphous if it is infinite, and cannot be written as a disjoint union of two infinite sets. One can show that if $A$ is an amorphous set, then there is no way to linearly order $A$. That is, there is no $R\subseteq A\times A$ such that $(A,R)$ is a linearly ordered set.

Suppose that $A$ is an amorphous set (and it is consistent that such set exists), and let $\mathcal L$ be the language in which $<$ is a binary relation symbol, and for every $a\in A$ there is a constant symbol $c_a$.

We write the axioms, $\varphi$ is the conjuction of the statements $<$ is a linear order, and for every distinct $a,b\in A$ we write $\varphi_{a,b}:=c_a\neq c_b$. This theory is consistent, because if it were to prove a contradiction there would be a finite number of $a\in A$ whose constants appear in the proof, but then we can construct a finite linear order which will be an interpretation of these axioms. This is impossible of course.

However, the theory as a whole, despite being consistent, does not have a model. Because in any model of the theory, reducing just to the constants will have defined a linear order of $A$, and $A$ itself is an amorphous set, so it cannot be linearly ordered.

So where is the axiom of choice coming into the play? When we construct models we need to make some arbitrary choices along the way. When the language is well-ordered then we can delegate these choices to the well-ordered and uniformly make them all; but when the language is an arbitrary set which may not be well-orderable to begin with, then the axiom of choice is needed.

In fact, one can prove that the completeness theorem (and its equivalent, the compactness theorem) is equivalent to the ultrafilter lemma, stating that every filter can be extended to an ultrafilter. These all are also equivalent to many other weak choice principles such as Tychonoff theorem for Hausdorff spaces, or the Boolean Prime Ideal theorem.

So what is missing from this answer? Well, I don't know about contexts where the WKL is not provable, so I cannot help in that aspect. But hopefully this answer shed some light on where the theorem is using fragments of choice and non-constructiveness.

  • $\begingroup$ Thanks for this answer. I had not encountered Amorphous Sets before - which WP claims are Dedekind-finite. There is a related question, though on "Countable Languages" which I might ask. My only question on this Answer is whether it is consistent to have the negation of AC in one place and use AC somewhere else in such an overall modeling building construction? I appreciate that the corresponding WKL question remains open - that is the one which would give a full counter-example to Godel Completeness if it can exist. $\endgroup$ – Roy Simpson Feb 3 '14 at 12:52
  • $\begingroup$ Roy, one doesn't usually encounter amorphous sets. As for your question, it's unclear to me. It is consistent that some fragments of the axiom of choice fails, but other fragments hold. If that's what you're asking. (Strongly amorphous sets, however, are generally strongly counterexamples for many choice principles...) $\endgroup$ – Asaf Karagila Feb 3 '14 at 16:18
  • $\begingroup$ As far as AC fragments are concerned do amorphous sets live in the space "WKL + not AC" ... or "not WKL + not AC". If it is the former then do we have sets (or other constructs) in "not WKL"? I have asked my related question, which gives another angle on this entire issue. $\endgroup$ – Roy Simpson Feb 3 '14 at 16:24
  • $\begingroup$ Well, since WKL is provable from ZF, and the whole context here is ZF, then amorphous sets live certain models of WKL+not AC. If you want something which cannot prove WKL you are going to need to weaken your system by far more. $\endgroup$ – Asaf Karagila Feb 3 '14 at 16:26
  • $\begingroup$ ZF-I ZF minus the Infinity axiom might do the trick. $\endgroup$ – Roy Simpson Feb 4 '14 at 14:45

If the axiom of choice is not a "necessary logical truth", but only a "mathematical convenience", the same can be said for every axiom of ZFC. None of them is a logical truth, after all. Even the axiom of induction for natural numbers (in Peano arithmetic) is not a logical truth.

In short, almost no interesting theorem of mathematics or logic is a logical truth, unless it is stated in the form $H \to C$, where $H$ is the conjunction of all the axioms needed to prove some theorem $C$. Usually, we just state "$C$" as a theorem, rather than stating "If these axioms hold, so does $C$".

Avigad explains in his paper (linked in the question) what Gödel means by "invalidate". Avigad writes,

I wish to highlight Gödel’s remarkable sensitivity to the question as to what metamathematical methods are necessary to obtain the requisite results, and the impact these methods have on the epistemological consequences

The key word there is "epistemological consequences". The use of the axiom of choice to prove the completeness theorem in ZFC, or the use of weak König's lemma to prove it in second-order arithmetic, in no way diminishes the mathematical correctness of the theorem. But the study of what axioms are needed to prove a particular theorem does influence how we interpret the theorem.

Finally, let me emphasize that the axiom of choice is not very tightly related to constructivism in mathematics. There are fully constructive systems that include the axiom of choice, and fully nonconstructive systems (such as ZF set theory) that do not. So it is often a red herring to focus on whether a proof uses the axiom of choice, because many classical proofs are already nonconstructive long before they try to use that axiom.

  • $\begingroup$ What would be an example of a fully constructive system that includes AC? $\endgroup$ – Michael Greinecker Feb 3 '14 at 0:32
  • 2
    $\begingroup$ @Michael Greinecker: Here are two. Some forms of Martin-Löf intuitionistic type theory actually prove the relevant form of the axiom of choice as a theorem - and these systems have inscrutable "constructive" bona fides. Some theories of second-order or higher-order intuitionistic arithmetic include the relevant form of the axiom of choice as an axiom scheme. (In contrast, Diaconescu's theorem shows that the axiom of choice implies classical logic in many constructive set theories.) $\endgroup$ – Carl Mummert Feb 3 '14 at 0:43
  • $\begingroup$ Thank you, that are pointers I should be able to work with. $\endgroup$ – Michael Greinecker Feb 3 '14 at 0:47
  • 1
    $\begingroup$ @Michael Greinecker: The following article by Per Martin-Löf has a nice discussion of how this phenomenon occurs: "100 years of Zermelo’s axiom of choice: what was the problem with it?" at math.kth.se/~kurlberg/colloquium/2005/MartinLooef.pdf $\endgroup$ – Carl Mummert Feb 3 '14 at 0:47
  • $\begingroup$ @CarlMummert: I find Asaf's answer closer to what I require. I shall review your answer by paragraph to clarify any misconceptions. Para1: I agree. Para2: For general mathematics yes, but this question is not about mathematics - it is about the special (and to me surprising) nature of the proof of Godel Completeness/Compactness -in contrast to (a) other theorems in (two valued) fundamental logic; and (b) the fact that older logic textbooks are not emphasising this. The proofs of soundness are a matter of just checking that the rules work, likewise many proofs of completeness in limited logics. $\endgroup$ – Roy Simpson Feb 3 '14 at 11:13

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.