Nonprincipal complete type 2026-10-31
A nonprincipal complete type has no first-order consistent first-order formula implying all its members. In a complete countable first-order theory such a partial type can be omitted in a countable first-order model by the omitting types theorem. A partial type realized by a parameter-free definable tuple is principal.
Take the parameter-free complete typeof the nonstandard prime constructed in part (i). It is first-order consistent and complete because it consists of exactly the logical formulas true of an actual element in a first-order model of . It contains for every integer , and consequently no element of realizes it. ThusIt is necessarily a nonprincipal complete type. If a first-order consistent logical formula isolated it, completeness of would force the existential closure of that logical formula to hold in every first-order model of , including ; a witness there would realize the partial type, a contradiction. This connects the explicit omission with the hypothesis of the omitting types theorem.
Use , the complete theory of algebraically closed fields of characteristic zero. Its quantifier elimination is a standard characterization of this complete theory. Algebraically closed fields of a fixed characteristic are classified up to isomorphism by transcendence degree over their prime field.
For such a field ,when the transcendence degree is infinite, while finite transcendence degree also gives a countable field. This follows by counting rational functions in a transcendence basis and then algebraic elements over that field. Thus every first-order model of cardinality has transcendence degree , and the classification gives a unique such first-order model.
On the other hand and an algebraic closure of are countably infinite first-order models with transcendence degrees zero and one, so are not isomorphic. HenceThe transcendental complete one-type consists of for every nonzero polynomial over . Quantifier elimination makes it complete. It is nonprincipal: any parameter-free one-variable logical formula containing a transcendental element defines a cofinite set, hence contains algebraic elements as well and cannot isolate this partial type. The first-order model omits it, concretely illustrating the omitting types theorem. The existence of infinitely many algebraic complete one-types, together with this nonprincipal complete type, also agrees with the failure of the Ryll-Nardzewski finiteness condition.
Reuse the complete free-bijection theory from part (e). Quantifier elimination shows that every one-variable atomic statement is already decided by the no-finite-cycle axioms. Thus there is exactly one complete one-type, isolated by .
For two logical variables, each integer gives a different complete type isolated byThere is also the complete typesaying that the two elements lie in different orbits. These exhaust the possibilities by quantifier elimination. In particularThe last complete type is a nonprincipal complete type. Any logical formula uses only finitely many integer offsets after quantifier elimination; a pair in a single orbit with a sufficiently different offset agrees with a different-orbit pair on those tests. Hence no single logical formula can isolate .
The one-orbit first-order model omits , while a two-orbit first-order model realizes it. This illustrates the omitting types theorem and shows concretely why finitely many complete one-types alone cannot replace the all-arities condition in Ryll-Nardzewski.