Let be nonempty first-order structures in one language and let be an ultrafilter on . In the ultraproduct , identify functions when , interpret functions coordinatewise and relations by their coordinate truth sets. The Łoś theorem states that for every first-order formula ,All interpretations are independent of representatives: changing finitely many arguments on -small sets changes truth only on their finite union, also -small.
Prove the theorem by structural induction on formulas. Terms evaluate coordinatewise by induction on terms. This proves the atomic cases of logical equality and relation symbols. For conjunction, intersect the two truth sets and use the filter laws. For negation, the truth set is complemented, and an ultrafilter contains exactly one of a set and its complement. These cases supply the other Boolean connectives too.
For the existential step, a witness in the ultraproduct makes the coordinate truth set for belong to by the induction hypothesis. That set is contained in the coordinate truth set of , so the latter is in . Conversely, if that existential truth set belongs to , choose a witness in for each , and any element of elsewhere. The axiom of choice supplies this function. The induction hypothesis makes a witness in the ultraproduct. Universal quantification follows by negation. This completes the proof.
For the compactness theorem, take to be the set of finite subsets of the given theory . For each , choose . For , the cone is nonempty, and any finite intersection of such cones contains their union as an index. Extend the filter they generate to an ultrafilter . By the proved Łoś theorem, the ultraproduct satisfies every , because its coordinate truth set contains . Thus . This proves compactness without assuming it in the ultraproduct construction.
Articles by others on the same topic
There are currently no matching articles.