The local omission of a partial type by a consistent first-order theory means that, for every formula consistent with , there is some such thatis consistent. Equivalently, no formula consistent with implies every member of . Thus every possible local condition has a compatible refinement excluding at least one proposed type formula.
The omitting types theorem states: in a countable first-order language, if is consistent and locally omits each of countably many finite-arity families , then it has a countable model omitting them all. Omission means that no tuple satisfies every formula in the family. In the case of a complete type, local omission is equivalent to the type being nonisolated. Countability of the language and of the list of omission requirements is essential to this formulation.
An atomic model is a model in which every finite tuple's complete type over the empty set is isolated by a formula. An omega-saturated model realizes every complete type in finitely many variables over every finite parameter set; equivalently it realizes all one-variable types over finite parameter sets, then successive realizations give the finite-tuple version.
Suppose is countable and omega-saturated. Every type in is realized by a tuple in , so is countable. This is a compact Hausdorff Stone space with a clopen basis. Its isolated points are dense. Indeed, if a nonempty clopen subset had no isolated point, split it into two disjoint nonempty clopen subsets and recursively split every resulting subset. Such splits exist because each subset has at least two points and the space is zero-dimensional. Compactness supplies a point in each nested sequence along an infinite binary branch, while disjoint siblings make different branches yield different points. This would give uncountably many points, contradicting countability.
For each , let consist of the negations of all formulas that isolate complete -types. Density of isolated types means that every consistent formula has a consistent refinement to an isolating formula ; this refinement excludes the member of . Thus locally omits every . The omitting types theorem gives a countable model omitting them all. Every tuple in therefore satisfies some isolating formula, so is atomic. If some is itself inconsistent, its omission is automatic and does not obstruct this argument.
The converse about existence is false. Here is a countable atomic model without a countable saturated model. Take a countable set with unary predicates , , such that every finite Boolean pattern of the predicates occurs infinitely often. For example, use finite binary words paired with a natural number, with recording the th bit when it exists and false otherwise. Add a constant naming each element, and put in this countable language. Every tuple of has its type isolated by equations to its named coordinates, so is a countable atomic model.
For each infinite binary sequence , the familyis finitely satisfiable in : realize its finitely many predicate requirements while avoiding finitely many named elements. By compactness theorem, it extends to a complete one-type. Different sequences give different types, so is uncountable. Any omega-saturated model must realize all these empty-parameter types, which a countable model cannot do. This disproves the existence converse, rather than merely exhibiting an atomic model that is itself nonsaturated.
The Ehrenfeucht theory of an increasing named sequence is complete and has quantifier elimination: the usual one-point cut argument for dense linear orders without endpoints works with the finitely many constants occurring in a formula. Complete types are consequently determined by order relations to the named constants and to any additional parameters.
In the model where the sequence is unbounded above, every finite tuple lies below some . Its order relations to , together with its internal equality and order pattern, determine its relations to every later constant as well. This finite condition isolates its complete type. Thus model (ii) is an atomic model. It is not omega-saturated, because the finitely satisfiable type has no realization.
In either bounded model, a point above every realizes the typeThis type is not isolated. Any formula belonging to it uses only finitely many constants after quantifier elimination, and its order condition can also be realized below a sufficiently late . That realization fails one of the later inequalities in . Hence neither bounded model is atomic.
In model (i), let be the least upper bound. The type over the single parameter is finitely satisfiable by density but unrealized, so this model is not omega-saturated.
In model (iii), the upper tail has no least element. Every consistent one-type over finitely many parameters is realizable. Indeed, it is either an equality type, a cut below or between some of the named constants, or a cut in . The first two cases are realized by equality or by density in the relevant interval. In , finitely many parameters divide the tail into finitely many intervals, each relevant nonempty interval having points by density, absence of a least element in , and absence of a last element in the order. This realizes the third case too. There is no other cut among the increasing sequence: a proper initial segment of its indices is finite. Successive one-variable realizations give all finite-tuple types. ThereforeA least upper bound is thus precisely the obstruction to filling the additional finite-parameter cut in model (i).
Articles by others on the same topic
There are currently no matching articles.