A precise countable-language form of the omitting types theorem is the following. Let be a consistent first-order theory in a countable first-order language, and let be a countable family of nonprincipal partial types, each in finitely many variables. Then there is a finite or countably infinite model of omitting all the .
A partial type is a set of formulas jointly consistent with . It is principal if there is a formula such that is consistent and
For a complete type, this is exactly being an isolated type. Nonprincipal means that no such formula exists. A model omits if no tuple in that model satisfies every formula in ; different tuples may fail different members of the type. The model in the theorem need not omit each individual formula everywhere.
For parameter types, use the expanded language naming the parameters. Countability then applies to that expanded language, and hence requires a countable parameter set as well. There is no countability restriction in the finite-satisfiability argument of part (a).

Articles by others on the same topic (0)

There are currently no matching articles.