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 ?:

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?