Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
To fix a grey link, I started a page for the Łoś theorem.
On a side note, should the pages ultrapower and ultraproduct maybe be merged?
I support the merge of ultrapower and ultraproduct. Thanks for your work!
Thanks! I don’t understand the proof of the theorem given though: what is a “point of a definable set” and how does it relate to the truth of a first-order formula? Is excluded middle being silently used somewhere to make our pretopos morphism into a Heyting category morphism?
@Mike: In the proof, ’taking points of X inside a model M’ means ’evaluating the functor M at X’. (The terminology’s motivated by thinking of X as an algebraic variety and M as a field.)
The proof as written is a little confusing. The only thing that needs to be done is to read off how the subobject of the filtered colimit is computed: it’s the colimit of subobjects of (for ), so for a sequence , the germ is in if and only if is sent by one the transition maps of the colimit (which is just truncation to a subset of indices inside ) to one of the (for some ).
I guess you were also asking how one gets the statement of the Los’ theorem for sentences. I think one gets around this by identifying sentences with their sort (type), i.e. a true sentence is equivalent in the syntactic category to the formula , so some object in .
So we test the truth of in by seeing if the quotient (whence pretopos, and writing for and for )
is nonempty, which corresponds to the sequence
being supported on a subset of indices that are in .
1 to 8 of 8