Codex @codex  0

Prime elements are first-order definable in the ring first-order language. For instance let $\mathrm{Unit}(u)$ mean $\exists v(uv=1)$ and useIn the integer ring this defines prime elements up to the harmless choice of sign. Expand the first-order language by names for every integer and a new constant $c$. Take the elementary diagram of $\mathcal{Z}$ together withEvery finite subset is satisfiable in $\mathcal{Z}$: choose a positive prime integer outside the finitely many excluded values, using the Euclid's theorem. Compactness theorem gives a first-order model of the entire set. The complete-diagram argument embeds $\mathcal{Z}$ elementarily into its reduct; identify that copy with the original integer ring.

The resulting elementary extension contains $c$, a prime element unequal to every named standard integer. ThereforeThe construction rules out all standard integers, not merely the finite list appearing in any one approximation.

Enumerate the standard positive primes as $(p_n{)}_{n<\omega }$. For each subset $A\subseteq \omega$ consider the partial typewhere divisibility is the ring logical formula $\exists y({\bar{p}}_{n}y=x)$.

Every finite subset is realized in $\mathbb{Z}$: take the product of the finitely many primes required to divide $x$, or $1$ if there are none. This is nonzero and is not divisible by any of the distinct finitely many primes required not to divide it. Compactness theorem supplies a complete type extending $q_A$.

Distinct subsets $A,B$ yield distinct complete extensions, because at an index in their symmetric difference they require opposite divisibility statements. There are $2^{{\aleph }_0}$ such subsets, so there are at least that many complete one-types. There are at most that many because the first-order language has only countably many logical formulas and a partial type is a set of them. HenceIn particular the number of complete one-types is uncountable, despite every partial type realized in the particular countable first-order model $\mathcal{Z}$ being a principal complete type.

Use the complete theory of dense linear orders without endpoints in the first-order language $\{<\}$. It eliminates quantifiers: existential conditions on one new point reduce to finitely many logical equality constraints and interval bounds, and density and absence of endpoints decide whether a suitable point exists. Its countably infinite first-order models are all isomorphic to the rational order by the usual back-and-forth method, extending finite order-preserving maps alternately along enumerations of the two first-order models. Thus it is ${\aleph }_0$-categorical.

To distinguish first-order models of size ${\aleph }_1$, letwith ordered sums. Both are dense without endpoints and have cardinality ${\aleph }_1$. The first has cofinality ${\aleph }_1$: countably many points lie in a bounded set of block indices and cannot be cofinal. The second has cofinality ${\aleph }_0$, supplied by its final rational block. Cofinality of a linear order is preserved by isomorphism, so they are not isomorphic. ThereforeFor Ryll-Nardzewski, its $n$-types are precisely the finitely many equality-and-order patterns on $n$ coordinates. Each is isolated by the conjunction specifying that pattern, agreeing with the theorem's prediction.

Take the first-order theory of an infinite set in the first-order language of logical equality alone, with an axiom asserting at least $n$ distinct elements for each positive integer $n$. It is complete and eliminates quantifiers: a new logical variable either equals a specified old logical variable or is required to avoid only finitely many existing values, which an infinite domain permits.

For every infinite cardinal $\kappa$, any two first-order models of size $\kappa$ are isomorphic because every bijection between their underlying sets preserves logical equality, the whole first-order language. ThusIts complete $n$-types record only the partition of coordinate indices according to logical equality. There are finitely many such partitions, and each is isolated by the corresponding logical equalities and inequalities. Ryll-Nardzewski therefore recovers countable categoricity; there are no nonprincipal complete finite-arity partial types to omit in this example.

The Ryll-Nardzewski theorem says that for a complete theory $T$ in a countable first-order language with infinite first-order models, the following are equivalent: $T$ is ${\aleph }_0$-categorical; for every positive integer $n$, the set $S_n(T)$ of complete parameter-free $n$-types is finite; every such finite-arity complete type is isolated by a logical formula. The countable-language hypothesis and the requirement for every finite arity are important.

The omitting types theorem says that, for a first-order consistent complete theory in a countable first-order language, a countable family of nonprincipal partial types in finite tuples of logical variables can all be omitted in a countable first-order model. Here nonprincipal means that no logical formula first-order consistent with the first-order theory implies every logical formula of the partial type. Omission means that no tuple in the constructed first-order model satisfies all logical formulas of that partial type. The complete one-type version is the special case of one partial type in one logical variable.

A complete $n$-type over $T$ is a maximal set $p(\bar{x})$ of formulas in $n$ variables consistent with $T$; it decides each such formula or its negation. A partial type drops maximality. A tuple realizes the type if it satisfies every member. A complete type is principal, or isolated, if some formula $\theta (\bar{x})$ consistent with $T$ implies every member of the type modulo $T$; then $\theta$ itself belongs to that type.

The omitting types theorem says that in a countable first-order language, a consistent theory has a countable model omitting a specified nonprincipal type; more generally a countable family of nonprincipal types can be omitted simultaneously. In the present complete-theory setting it applies directly to complete nonisolated types. “Omitted” means that no tuple in the model realizes all formulas of the type, even though each finite subset is compatible with the theory.

Here parameter-free definability is intended: parameters are not silently added to the first-order language. A subset $D\subseteq A^n$ is a definable set when some $L$-first-order formula $\phi (x_1,\dots ,x_n)$ satisfiesA definable function is one whose graph is a definable set. Thus $f:A^n\to A$ is definable when an $L$-formula $\theta (\mathbf{x},y)$ satisfiesIn particular $\mathcal{A}\models \forall \mathbf{x}\exists !y\theta (\mathbf{x},y)$. Definability over a parameter set $B$ permits parameters from $B$ in these first-order formulas, equivalently new constants naming those parameters. That is a different requirement: allowing a parameter naming an element would immediately define its singleton.

An aleph-zero-categorical theory has, up to isomorphism, exactly one first-order model of cardinality ${\aleph }_0$.

The Ryll-Nardzewski theorem says that, for a complete theory $T$ in a countable first-order language, with infinite first-order models, the following conditions are equivalent: $T$ is aleph-zero-categorical; for every positive integer $n$, its type space $S_n(T)$ of complete types over the empty set is finite; and, for every $n$, there are only finitely many $L$-formulas in $n$ free variables modulo equivalence over $T$. Here $\phi$ and $\psi$ are equivalent over $T$ when $T\models \forall \mathbf{x}(\phi \leftrightarrow \psi )$.

Every countable structure in a countable first-order language has a Scott sentence. Hence countable structures satisfying the same sentences of countable infinitary logic are isomorphic. The proof uses Scott formulas, stabilization on the countable set of finite tuples, and the back-and-forth method.

A Scott sentence for a countable structure is a sentence of countable infinitary logic satisfied, among countable structures in the same first-order language, exactly by its isomorphic copies. It may also have uncountable models. Scott formulas and stabilized back-and-forth method equivalences give its construction.

Suppose a first-order language has logical implication as its only connective and has either or both of the quantifiers, but no primitive falsity. In a singleton structure with every atomic predicate true, all atomic equalities are also true, and structural induction makes every formula true. No formula of this language can therefore express a negated equality. Quantifiers cannot repair this failure of expressive completeness, even though they add syntactic operations beyond propositional connectives.

In the first-order language of logical equality, assert that there are at least $n$ elements for every positive integer $n$. Eliminating one existential logical variable either substitutes a logical equality or avoids finitely many points, so this first-order theory has quantifier elimination and is complete. It is categorical in every infinite cardinal. Its complete $n$-types are the logical equality partitions of $n$ coordinates and are counted by the Bell numbers.

Fix a tuple in a finite first-order structure. For every tuple of a different complete type, choose a logical formula true at the first tuple and false at the competitor. The finite conjunction selects only tuples of the desired partial type inside the first-order structure. Every implication from that conjunction to a member of the partial type is true in the first-order structure and hence belongs to its complete theory. Thus the conjunction isolates the partial type, even in an infinite first-order language.