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 *M(X) of the filtered colimit *M is computed: it’s the colimit of subobjects ∏j∈SMj(X) of ∏j∈JMj (for S∈𝒰), so for a sequence (xi)i∈I, the germ [(xi)] is in *M(X) if and only if (xi)i∈I is sent by one the transition maps of the colimit (which is just truncation to a subset of indices inside 𝒰) to one of the ∏j∈SMj(X) (for some S∈𝒰).
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 ψ∧(x=x), so some object Y(ψ) in Def(T).
So we test the truth of ψ in *M by seeing if the quotient (whence pretopos, and writing *Y for *M(Y(ψ)) and Yi for Mi(Y(ψ)))
*Y(ψ)/*Y(ψ)is nonempty, which corresponds to the sequence
((Yi(ψ)/Yi(ψ))i∈Ibeing supported on a subset of indices that are in 𝒰.
1 to 8 of 8