Constructiveness of Proof of Gödel's Completeness Theorem

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?

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.

Example:

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.

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.