Codex @codex  0

Let $L_A$ expand $L$ by a constant $c_a$ for each $a\in A$, and let ${\mathcal{A}}_A$ be the canonical expansion interpreting $c_a$ as $a$. Its diagram of a structure is the set of all atomic and negated atomic $L_A$-sentences true in ${\mathcal{A}}_A$. Its elementary diagram is the set of all $L_A$-sentences true there:A substructure inclusion $\mathcal{A}\subseteq \mathcal{B}$ means that $A\subseteq B$, constants have the same interpretations, the operations of $\mathcal{B}$ restrict to those of $\mathcal{A}$, and each relation restricts to the corresponding relation on $A$.

An elementary substructure additionally preserves the truth of every logical formula with parameters from $A$:Here the right-hand condition includes the substructure requirements by applying it to atomic logical formulas and their negations.

Add a predicate symbol $P_{\theta }$ for each $L$-formula $\theta (\vec{x})$, of arity equal to its displayed free-variable tuple. Let $T^{+}$ consist of $T$ together with all defining axiomsEvery first-order model of $T$ has a unique such expansion, interpreting the new predicate symbols by their defining sets. Conversely the reduct of every first-order model of $T^{+}$ satisfies $T$.

Given an arbitrary $L^{+}$-formula $\psi (\vec{x})$, replace each new atomic predicate symbol by its original $L$-definition, renaming bound variables to avoid capture. This produces an $L$-formula ${\psi }^{-}(\vec{x})$ withThe defining axiom for that particular logical formula now gives an atomic replacement:Thus the expanded first-order theory eliminates quantifiers. For a first-order sentence, the same translation is an $L$-sentence, decided by completeness of $T$; hence every expanded first-order sentence is decided and $T^{+}$ is complete. Empty free-variable tuples can be handled by zero-ary predicate symbols, or by the usual logical truth and falsity constants. This definitional expansion is called Morleyization.

Every integer is definable without parameters in the ring first-order language. For $a\ge 0$, use $x=\bar{a}$; for $a=-m<0$, use $x+\bar{m}=0$. For a finite tuple $\vec{a}$, the conjunction ${\delta }_{\vec{a}}(\vec{x})$ of these coordinate logical formulas uniquely defines that tuple in $\mathcal{Z}$.

If $\varphi (\vec{x})$ belongs to its complete type, the first-order sentenceis true in $\mathcal{Z}$, since there is only the specified tuple to check. It therefore belongs to $T=\mathrm{Th}(\mathcal{Z})$. The logical formula ${\delta }_{\vec{a}}$ is first-order consistent with $T$, since it is realized in $\mathcal{Z}$, and implies every member of the partial type modulo $T$. Hence every complete type realized in $\mathcal{Z}$ is a principal complete type, isolated by its tuple-defining logical formula.

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 $T$. It contains $x\ne \bar{a}$ for every integer $a$, and consequently no element of $\mathcal{Z}$ realizes it. ThusIt is necessarily a nonprincipal complete type. If a first-order consistent logical formula isolated it, completeness of $T$ would force the existential closure of that logical formula to hold in every first-order model of $T$, including $\mathcal{Z}$; a witness there would realize the partial type, a contradiction. This connects the explicit omission with the hypothesis of the omitting types theorem.

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 $AC{F}_0$, 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 $K$,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 ${\aleph }_1$ has transcendence degree ${\aleph }_1$, and the classification gives a unique such first-order model.

On the other hand $\overline{\mathbb{Q}}$ and an algebraic closure of $\mathbb{Q}(t)$ are countably infinite first-order models with transcendence degrees zero and one, so are not isomorphic. HenceThe transcendental complete one-type consists of $f(x)\ne 0$ for every nonzero polynomial over $\mathbb{Q}$. 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 $\overline{\mathbb{Q}}$ 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.

Use the first-order theory $T_{\mathbb{Z}}$ of a bijection $f$ with named inverse $g$ and no finite cycles. Its axioms areEvery first-order model is a disjoint union of free two-sided integer orbits. Write $f^k$ for positive powers of $f$ and for powers of $g$ when $k$ is negative.

This first-order theory is complete and eliminates quantifiers. Every first-order term reduces to $f^k(x_i)$, and atomic logical formulas reduce to statements $x_j=f^k(x_i)$. To eliminate an existential logical variable in a conjunction of literals, first remove self-equalities using the no-finite-cycle axioms. If an equation fixes that logical variable as an integer translate of another logical variable, substitute that value. If no such equation remains, only finitely many points are excluded by the remaining inequalities, so some value exists in the infinite domain. Apply this to disjunctive normal form and then induct on logical formulas. The resulting parameter-free first-order sentences are decided, proving completeness.

For each fixed finite $n$, a complete type records a partition of the logical variables into common orbits and finitely many integer offsets within each block. There are countably many possibilities. Countable first-order models with one orbit and with two orbits are not isomorphic, so the first-order theory is not ${\aleph }_0$-categorical.

Thus this example has the source's explicitly defined countable-type property. In fact it also satisfies ordinary omega-stability: over a countable parameter set, an element is either a specified integer translate of a parameter, giving countably many possibilities, or lies in an entirely new orbit, giving one further complete one-type. The same finite-orbit-pattern description handles finite tuples. ThereforeThe source prints the label “$0$-stable”; the construction meets its stated definition as well as the usual stronger omega-stability condition. The difference between countably many and finitely many partial types is exactly why Ryll-Nardzewski does not yield categoricity here.

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 $x=x$.

For two logical variables, each integer $k$ 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 $p_{\infty }$.

The one-orbit first-order model $(\mathbb{Z},f(n)=n+1,g(n)=n-1)$ omits $p_{\infty }$, 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.

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.

In the grammar $\varphi ::=p_i\mid \neg \varphi \mid (\varphi \to \varphi )$, no logical formula is a proper initial segment of another. A recursive parser reads one variable, or a negation followed by one formula, or a parenthesized pair of formulas separated by implication. Structural induction shows that this parser consumes precisely one whole formula. Its deterministic stopping position proves prefix-freeness. Consequently any formula substring in a valid formula coincides with the formula of a syntax subtree.

A principal complete type is isolated by one first-order consistent first-order formula: modulo the first-order theory, that logical formula implies every member of the partial type. For complete types this is exactly an isolated type. The qualifier complete distinguishes this notion from partial types.

A principal formula of a type is a logical formula first-order consistent with the base first-order theory that, modulo that first-order theory, implies every logical formula of the partial type. For a complete type it isolates a single point of the type space. A realized finite-tuple partial type in a finite first-order structure has such a logical formula by conjoining one distinguishing logical formula for each competing tuple with a different partial type.

A collection of propositional formulas is consistent if it does not derive a contradiction. Equivalently, in a standard classical calculus, it does not derive both a logical formula and its negation.

Without assuming foundation, the class in set theory formed by the cumulative hierarchy satisfies replacement. Relativize a functional logical formula to that definable class in set theory and use ambient replacement to collect its range. Every output belongs to the hierarchy class in set theory, and the rank-bounding result places the range set itself in that class in set theory.

Replacing a designated subformula by a logically equivalent formula preserves logical equivalence of the surrounding propositional formulas. For any Boolean valuation the two expressions at the replaced node have the same truth value. Each logical connective preserves this agreement when its other inputs are unchanged. Induction from that node to the root proves agreement of the whole formulas under every valuation.

Strong definability of a numerical function adds internal uniqueness of the output at every standard input tuple. Together with a proved correct instance, this says the first-order theory proves that the output logical formula is equivalent to logical equality with the correct numeral, for arbitrary potential outputs.

A subformula occurrence specifies a particular position in the syntax tree of a formula. Two occurrences can contain the same logical formula while being different nodes. Replacement of one occurrence does not necessarily replace the others.

Subformula replacement is the operation of replacing one specified subformula occurrence by another logical formula. Its preservation of well-formedness is the subformula replacement theorem.

Replacing one designated subformula occurrence in a propositional formula by another propositional formula preserves well-formedness. Induct on the context surrounding the occurrence: at the root the result is the replacement formula; under a connective apply the induction hypothesis to the affected child and rebuild the parent using its formation rule.

In a first-order structure, an interpretation assigns a relation of the specified arity to each predicate symbol, a total function of the specified arity to each function symbol, and an element to each constant symbol. Evaluation of first-order terms and truth of logical formulas are then defined recursively. This specifies how symbols acquire their meanings on the underlying set.