In papers published 1920 and 1922, Skolem offered two separate proofs of a result due to Lowenheim. On this basis we can distinguish a strong and a weak version of the Lowenheim-Skolem theorem as follows:
The weak (1922) version states that if a closed formula $\phi$ of quantification theory is satisfiable, then it is satisfiable in a countable domain. This version does not require the Axiom of Choice; a model of $\phi$ is built up from below using numerals to instantiate the variables.
The (1920) "subdomain" version states that if $\phi$ is satisfiable in an (infinite) domain D, then it is satisfiable in a countable subdomain D' of D, where the predicates retain the same meaning in D' as in D (modulo the restriction).
Skolem (1922) gives no formal proof procedure. However, the level-by-level construction of the denumerable model implicitly supplies an effective procedure for refuting a formula in a finite number of steps. This occurs if we reach a level for which no satisfying truth-value assignment exists for the approximation to the formula considered at that level, thus implying the formula's negation. This explains why Godel (Coll. Wrks. Vol 1, p. 52) writes that Skolem's weak theorem implies completeness: "Skolem...could justly claim...that, in his 1922 paper, he implicitly proved: 'Either A is provable or $\neg$A is satisfiable” (“provable” taken in an informal sense).'
What about the subdomain version? In this version, Skolem starts with $\phi$ in normal form (i.e. $\forall x \exists y\psi$, where $\psi$ quantifier-free) and uses the axiom of choice to find witnesses $f(x)$ for the existential quantifier, taken from a domain D in which $\phi$ is assumed to be satisfied. Let $a$ be an arbitrary element from D. The proof continues by closing $a$ under the following operation. Consider all the classes $X\subseteq $D such that $a \in X$ and if $x \in X$, then $f(x) \in X$. Skolem then applies a result from Dedekind's chain theory to conclude that the intersection of all such classes $X$ must be denumerable (cf. Dedekind 1888).
By omission, Godel implies that this subdomain version cannot be interpreted so as to yield completeness. I assume this is because the method Skolem uses does not, as in the weak version, implicitly describe a refutation procedure for $\phi$ since the assumption of $\phi$'s satisfiability in D is crucial in the description of the submodel.
Question:
(a) Is that the correct reading?
(b) Does it mean that the weak version, in order to provide a refutation procedure, does not make use of the antecedent in its statement?
Main references
Skolem 1920, Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen, Videnskapsselskapet Skrifter, translated in (3) as Logico-combinatorical investigations in the satisfiability or provabilitiy of mathematical propositions: A simplified proof of a theorem by L. Löwenheim and generalizations of the theorem
Skolem 1922, Einige Bemerkungen zu axiomatischen Begründung der Mengenlehre, 5th Scand. Math. Congress, translated in (3) as Some remarks on axiomatized set theory
Jean van Heijenoort (ed.) 1977, From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931, Harvard University Press
