Godel's Completeness Theorem is a straightforward consequence of Skolem 1922 and yet this conclusion was not drawn by Skolem himself. In a letter to Wang (Dec. 7, 1967 in Godel 2003) Godel gives an explanation for this oversight:



> 
> At that time, nobody (including Skolem himself) drew this conclusion ... I think the explanation is not hard to find. It lies in a widespread lack, at that time, of the required epistemological attitude toward metamathematics and toward nonfinitary reasoning.
> 
> 
> 


I know some form of Konig's Infinity Lemma or the "law of infinite conjunction" (Quine) is necessary to prove semantic completeness, but (a) is this what Godel must be referring to as "nonfinitary reasoning", and (b) where/how does this law figure in Godel's original proof? 



Infinitary reasoning in Godel's Completeness Proof
The best write-up I know of Godel's proof of the completeness theorem is by Avigad, in his paper [Godel and the metamathematical tradition](http://www.andrew.cmu.edu/user/avigad/Papers/goedel.pdf) (section $4$). Avigad divides the proof into $5$(ish) steps, and step $2$ crucially uses Konig's lemma:



> 
> Step $2$: If a set $\Gamma$ of propositional formulas is not refutable, it has a satisfying truth assignment. Write $\Gamma=\{\varphi\_0,\varphi\_1,\varphi\_2,...\}$. **Build a finitely branching tree** where the nodes at level one are all the truth assignments to variables of $\varphi\_0$
>  that make $\varphi\_0$ true; the nodes at level two are all the truth assignments to
>  variables of $\varphi\_0\wedge\varphi\_1$ that make that formula true; and so on. (The descendants of a node are all the truth assignments that extend it.) If, at some level $k$,
>  there is no satisfying assignment to $\varphi\_0\wedge\varphi\_1\wedge ...\wedge\varphi\_{k-1}$, then, by step $1$, $\Gamma$
>  is refutable. **Otherwise, by Konig’s lemma, there is a path through the tree,
>  which corresponds to a satisfying truth assignment for $\Gamma$.**
> 
> 
> 


*(Emphasis mine.)* This is the only way Konig gets used here.


Specifically, here's what's going on in the rest of the proof:


* Step $1$ is just the completeness theorem for propositional logic for individual sentences (which Step $2$ lifts to *sets of sentences* via Konig).
* Step $3$ shows completeness for individual $\forall^\*\exists^\*$-sentences without function symbols or equality, and is entirely straightforward.
* Step $4$ extends Step $3$ to individual sentences without function symbols or equality to arbitrary-complexity sentences, a la Skolem.
* Step $???$ extends the result of Steps $3$ and $4$ to *arbitrary sets of* such sentences. Avigad doesn't mention this step by name, instead relegating it to the end of Steps $3$ and $4$, but I think it's worth stating separately. However, this extension doesn't involve an application of Konig's lemma, just annoying bookkeeping.
* Step $5$ wraps everything up by observing that function symbols can be replaced by relation symbols and additional axioms saying they behave as graphs of functions, and that equality can be replaced with a binary relation together with new axioms for its handling (we just take an appropriate quotient structure at the end of the day). This is again entirely straightforward.




---


As to whether that's what Godel meant by "nonfinitary reasoning," I'm not sure. Personally Skolem 1922 already feels pretty nonfinitary (in a good way) to me. My personal guess is that it's a bit more subtle than that: the missing philosophical ingredient was perhaps the realization that nonfinitary methods are relevant to finitary conclusions, even in foundational topics. As opposed to an elementary submodel, a proof is a fully finite object, and it was definitely surprising to me at least that infinitary reasoning could be used to demonstrate the existence of a proof *(in fact, the completeness theorem itself deeply shocked me when I first learned it)*.


