Lowenheim-Skolem and Constructive

Bacle2

Hi,

Just curious as to wether the Lowenheim-Skolem theorem is constructive , in the sense

that , while it guarantees the existence of a model of infinite cardinality -- given the

existence of any infinite model -- does it give a prescription for constructing them?

I was thinking mostly of the ( 1st order theory of) the reals: the standard model is

the one given in most books. Then we can construct the hyperreals using, e.g.,

ultraproducts. What if we had any other infinite cardinal κ : is there a method for

constructing a model of cardinality κ ?

Thanks.

AKG

One can give an explicit set of instructions to construct the model, but the process is rather indirect and might not be what you're looking for. That is, there's a positive answer to your question about whether there is a prescription, you just might not like the taste of it. At any rate, here it is:

(I'm omitting details, hopefully you're familiar with Henkin's proof of the Completeness Theorem. I'm basically just stepping through that proof and observing that every step is an explicit construction.)

Expand the language of your theory T to include [itex]\kappa[/itex] distinct constants [itex]c_\alpha, \alpha < \kappa[/itex]. Extend T to include assertions that the [itex]c_\alpha[/itex] are distinct. It's easy to explicitly well-order the sentences of the expanded language. We can then extend this extension of T to a consistent complete theory in the expanded language by going through the sentences one-by-one (in the aforementioned well-order) and adding them to the theory if it's consistent to do so. Next we do the usual thing to add Henkin constants (so that every existential sentence in the theory has a witness among these constants), and this process is explicit. In the end we get a language and a complete consistent theory in that language, and the model we want consists of the variable-free terms in the final language, modulo provable equality in the final theory, with the obvious interpretation for the function and relation symbols. This last step too is also clearly explicit.

Bacle2

Excellent, AKG, thanks.

dcpo

With regard the OP, remember that the existence of non-principal ultrafilters does not follow from ZF, so an ultraproduct construction is non-constructive in your sense (or trivial).

Bacle2

Thanks; I was using the word in a very loose sense, so it works out fine. Sorry for being too loose/ambiguous in my usage.