Skolem's own proofs are a little bit opaque, so I've constructed a new algorithmic proof of the downward Löwenheim-Skolem Theorem which is easier to comprehend. I have yet to publish it, but it'll probably turn up somewhere else towards the end of the year:
Preliminaries: (1) Let T be a first-order theory with a countable or uncountable infinite model M. (2) Let L be the language of T. (3) T is assumed to be a set of sentences (closed formulas) in L.
Algorithm Steps:
Initialize Countable Set S: Start with S = Const(L), the set of all constant symbols in L.
Extend Language: For each n-ary relation R in L and each n-tuple (c1, ..., cn) of elements in S, if M⊨R(c1, ..., cn), then add a new constant symbol c to S and extend L to L' by adding c.
Iterate for All Formulas: For each formula ϕ(x1, ..., xn) in L and each n-tuple (c1, ..., cn) of elements in S: If M⊨∃xϕ(c1, ..., cn), then pick some a in M such that M⊨ϕ(a, c1, ..., cn). Add a new constant symbol c to S to represent a and extend L to L' by adding c.
Closure: Repeat Steps 2 and 3 until S no longer changes. Since T and L are countable, this process will eventually result in a countable set S.
Construct Countable Model N: Take the substructure of M generated by S as N. By construction, N is countable.
Elementary Submodel Check: By construction, N is an elementary submodel of M. This is because for any formula ϕ and any n-tuple (c1, ..., cn) from S, M⊨ϕ(c1, ..., cn) if and only if N⊨ϕ(c1, ..., cn).
Conclusion: N is a countable elementary submodel of M, and therefore T has a countable model. End.
You're right about the bijection, but, in the countable model, the set that "represents" the real numbers is countable. (From the perspective of the meta-theory.) However, within the model itself, this set still satisfies all the axioms that make it "look" uncountable. For example, there's no bijection between this set and the set representing the natural numbers within the model, even though such a bijection exists in the meta-theory.
This is why Skolem's solution can be most succinctly described: "Every set has a countable model if one steps outside the set and constructs a countable model from its elements."
In Kleene's “Introduction to Metamathematics,” he describes the situation as follows: "Either we must maintain that the concepts of an arbitrary subset of a given set, and of a non-enumerable set, are a priori concepts which elude characterization by any finite or enumerably infinite system of elementary axioms; or else (if we stick to what can be explicitly characterized by elementary axioms, as we may well wish to in consequence of the set-theoretic paradoxes ) we must accept the set-theoretic concepts, in particular that of non-enumerability, as being relative, so that a set which is non-enumerable in a given axiomatization n may become enumerable in another, and no absolute non-enumerability exists."
Preliminaries: (1) Let T be a first-order theory with a countable or uncountable infinite model M. (2) Let L be the language of T. (3) T is assumed to be a set of sentences (closed formulas) in L. Algorithm Steps:
Initialize Countable Set S: Start with S = Const(L), the set of all constant symbols in L.
Extend Language: For each n-ary relation R in L and each n-tuple (c1, ..., cn) of elements in S, if M⊨R(c1, ..., cn), then add a new constant symbol c to S and extend L to L' by adding c.
Iterate for All Formulas: For each formula ϕ(x1, ..., xn) in L and each n-tuple (c1, ..., cn) of elements in S: If M⊨∃xϕ(c1, ..., cn), then pick some a in M such that M⊨ϕ(a, c1, ..., cn). Add a new constant symbol c to S to represent a and extend L to L' by adding c.
Closure: Repeat Steps 2 and 3 until S no longer changes. Since T and L are countable, this process will eventually result in a countable set S. Construct Countable Model N: Take the substructure of M generated by S as N. By construction, N is countable.
Elementary Submodel Check: By construction, N is an elementary submodel of M. This is because for any formula ϕ and any n-tuple (c1, ..., cn) from S, M⊨ϕ(c1, ..., cn) if and only if N⊨ϕ(c1, ..., cn).
Conclusion: N is a countable elementary submodel of M, and therefore T has a countable model. End.
You're right about the bijection, but, in the countable model, the set that "represents" the real numbers is countable. (From the perspective of the meta-theory.) However, within the model itself, this set still satisfies all the axioms that make it "look" uncountable. For example, there's no bijection between this set and the set representing the natural numbers within the model, even though such a bijection exists in the meta-theory.
This is why Skolem's solution can be most succinctly described: "Every set has a countable model if one steps outside the set and constructs a countable model from its elements."
In Kleene's “Introduction to Metamathematics,” he describes the situation as follows: "Either we must maintain that the concepts of an arbitrary subset of a given set, and of a non-enumerable set, are a priori concepts which elude characterization by any finite or enumerably infinite system of elementary axioms; or else (if we stick to what can be explicitly characterized by elementary axioms, as we may well wish to in consequence of the set-theoretic paradoxes ) we must accept the set-theoretic concepts, in particular that of non-enumerability, as being relative, so that a set which is non-enumerable in a given axiomatization n may become enumerable in another, and no absolute non-enumerability exists."