What is the “essential use” of the principle of excluded middle applied to infinite collections in Gödel’s completeness proof? Gödel writes:
[L]et me make a remark about the means of proof used in what follows. Concerning them, no restriction whatsoever has been made. In particular, essential use is made of the principle of the excluded middle for infinite collections (the nondenumerable infinite, however, is not used in the main proof). It might perhaps appear that this would invalidate the entire completeness proof. For what is to be proved can, after all, be viewed as a kind of decidability (every expression of the restricted functional calculus either can be recognized as valid through finitely many inferences or its validity can be refuted by a counterexample). (Gödel 1929, p. 63 in Collected Works Vol. I)
Initially I understood this to refer to the proof of König’s lemma, since the latter uses proof by contradiction (equivalent to excluded middle) to guarantee an adjacent vertex at each step of the construction of the infinite path through the tree.
But Gödel never references König explicitly, and at the point in his proof where the lemma is required, he simply appeals to “familiar arguments” (Gödel, 1930, p. 117 in ibid.)
Is there another (explicit) application of excluded middle to which Gödel could be referring? In particular, is the principle needed to establish that what van Heijenoort calls the “basic alternative”:
Either, for every n, $A_n$, which is quantifier-free, is truth-functionally satisfiable or, for some n, it is not. (ibid. p. 52)
$A_n$ is a conjunction of the substitution instances $M_1$, $M_2$, …, $M_n$ formed up to the nth level. The nth substitution instance of a formula A is obtained as follows: first instantiate the r-many universal variables of A by the nth r-tuple of integers in some pre-given ordering. Then replace each existential variable by variables $x_i$ indexed by as-yet unused integers in numerical order. The resulting $M_n$ is a quantifier-free, truth-functional formula of propositional logic.