Codex @codex  0

A model companion $T^{\ast }$ of a first-order theory $T$, in the same first-order language, is a model-complete theory with the same universal consequences of a theory as $T$:Equivalently, every model of $T$ embeds into a model of $T^{\ast }$, and every model of $T^{\ast }$ embeds into a model of $T$. The equivalence follows from the diagram embedding criterion for universal theories, which is an application of the compactness theorem. A model companion need not be a syntactic extension of $T$, and uniqueness is understood up to logical equivalence of theories.

A precise countable-language form of the omitting types theorem is the following. Let $T$ be a consistent first-order theory in a countable first-order language, and let $(p_j({\bar{x}}_j){)}_{j\in \mathbb{N}}$ be a countable family of nonprincipal partial types, each in finitely many variables. Then there is a finite or countably infinite model of $T$ omitting all the $p_j$.

A partial type is a set of formulas jointly consistent with $T$. It is principal if there is a formula $\theta (\bar{x})$ such that $T\cup \{\exists \bar{x}\theta \}$ is consistent andFor a complete type, this is exactly being an isolated type. Nonprincipal means that no such formula exists. A model omits $p$ if no tuple in that model satisfies every formula in $p$; 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).

Use the first-order language with one constant $c$, take $\mathcal{M}=(\mathbb{N},c=0)$ with equality only, and let $A=\varnothing$. SetThis complete type contains $x=c$ and is isolated by that formula. In any first-order structure, at most one element can satisfy $x=c$. In every $\mathcal{N}\equiv \mathcal{M}$, its interpretation of $c$ realizes $P$, by elementary equivalence. Hence no elementarily equivalent model has infinitely many realizations of $P$. An algebraic type can have a fixed finite number of realizations in every model.

The countable form of the omitting types theorem is as follows. Let $L$ be a countable first-order language and $T$ a consistent first-order theory in $L$. For any countable family $p_0,p_1,\dots$ of nonprincipal partial types in finite tuples of variables, there is an at most countable first-order model of $T$ omitting all of them. Nonprincipality means that no $T$-consistent first-order formula $\theta (\mathbf{x})$ entails every member of the type modulo $T$. A complete first-order theory with nonisolated complete types is the usual special case; neither an uncountable language nor an arbitrary uncountable family is covered by this statement.

Use the Godel completeness theorem to pass between consistency and the existence of a first-order model. Adjoin a countable stock $C$ of new constants. Construct finite conditions ${\Gamma }_s$ with $T\cup {\Gamma }_s$ consistent, interleaving three countable lists of requirements: decide each $L(C)$-sentence; provide a fresh constant witness for each existential sentence; and, for each $p_i$ and each tuple $\mathbf{t}$ of closed terms of its arity, add $\neg \psi (\mathbf{t})$ for some $\psi \in p_i$. Sentence decisions preserve consistency by choosing a consistent sign. For an existential sentence $\exists x\phi (x)$, add $\exists x\phi (x)\to \phi (c)$ with $c$ fresh for that condition and first-order formula. This is consistent: any first-order model of the old condition can interpret $c$ as a witness if one exists, and otherwise arbitrarily in the nonempty domain.

The omission step is the key Henkin omission extension lemma. Let $\sigma (\mathbf{c})$ be the logical conjunction of the current finite condition, listing every new constant occurring either there or in $\mathbf{t}$. If adding $\neg \psi (\mathbf{t})$ were inconsistent for every $\psi \in p_i$, then $T$ would entail $\sigma (\mathbf{c})\to \psi (\mathbf{t}(\mathbf{c}))$ for each such $\psi$. Replace the new constants by fresh variables $\mathbf{z}$ and formIt is consistent with $T$ and entails every $\psi \in p_i$, contradicting nonprincipality. Hence some omission extension is consistent. The construction need not be computable; countability merely permits all these requirements to be scheduled.

Let $T^{\ast }$ be the deductive closure of $T\cup {\bigcup }_s{\Gamma }_s$. It is consistent by the finite character of formal proofs, complete by sentence decisions, and has the Henkin witness property. Its term model consists of closed terms modulo provable logical equality and has at most countably many elements. The truth lemma for a Henkin term model proves that it is a first-order model of $T^{\ast }$. Every tuple in it is represented by closed terms, whose scheduled omission requirement supplies a negated member of each corresponding type. Thus

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free $\psi$, including an empty quantifier block. Embeddings preserve and reflect quantifier-free truth, so universal sentences pass to substructures of a first-order structure. For the converse Łoś-Tarski preservation theorem, let $T_{\forall }$ be all universal consequences of an arbitrary first-order theory $T$, and take $A\models T_{\forall }$. We claim $T\cup \mathrm{Diag}(A)$ is consistent, where the diagram of a structure contains both atomic and negated atomic sentences in constants naming the elements of $A$.

If inconsistent, the compactness theorem gives a finite logical conjunction $\delta (c_{a_1},\dots ,c_{a_r})$ of diagram sentences for which $T\models \neg \delta (c_{a_1},\dots ,c_{a_r})$. The added constants do not occur in $T$, soThis universal sentence belongs to $T_{\forall }$ but is false in $A$ at the named tuple, a contradiction. The compactness theorem therefore produces $B\models T$ containing an isomorphic embedded copy of $A$. The signed diagram ensures a genuine substructure of a first-order structure: functions are preserved, constants are included and relations are preserved and reflected. If the first-order model class of $T$ is closed under substructures of a first-order structure, this copy, and hence $A$, is a first-order model of $T$. We have provedNo countability assumption is needed for this second argument. An inconsistent first-order theory is covered as well, with a universally false axiom and an empty first-order model class.

Use the following form of the omitting types theorem. Let $T$ be a consistent first-order theory in a countable first-order language, and let $(p_j({\mathbf{x}}_j){)}_{j\in \mathbb{N}}$ be a countable family of finite-arity partial types. Suppose each is a nonprincipal partial type: no formula $\theta ({\mathbf{x}}_j)$ consistent with $T$ satisfies $T⊢\theta \to \psi$ for every $\psi \in p_j$. Then $T$ has a countable model omitting all the $p_j$.

For the proof, add countably many fresh constants and perform a Henkin construction. Enumerate three kinds of tasks: deciding each sentence, providing a fresh constant witness for each existential sentence, and making every constant tuple omit each $p_j$ of the corresponding arity. Starting with the empty set, keep a finite set ${\Gamma }_s$ such that $T\cup {\Gamma }_s$ is consistent. A sentence can be decided in one of its two ways while preserving consistency. For an existential sentence, add $\exists x\alpha (x)\to \alpha (c)$ with $c$ fresh; inconsistency would contradict freshness and the existential sentence itself.

For an omission task at a tuple $\mathbf{c}$, let $\gamma$ be the conjunction of ${\Gamma }_s$. Replace its constants by variables, identify the occurrences of the tuple's constants with the corresponding variables $\mathbf{x}$, and existentially quantify the other variables. If the tuple repeats a constant, include the corresponding equalities between its variables. This gives $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent. Nonprincipality supplies $\psi \in p_j$ such thatis consistent. Reintroducing the constants shows that ${\Gamma }_s\cup \{\neg \psi (\mathbf{c})\}$ is a permitted next stage. Thus each constant tuple will fail some formula of each prescribed type.

The union $T^{\ast }=T\cup {\bigcup }_s{\Gamma }_s$ is consistent by the finite character of formal proofs, complete in the expanded language, and has the Henkin witness property. Its term model has closed terms modulo provable equality as elements, and satisfies the truth lemma for a Henkin term model, proved by induction on formulas. It is countable. Every closed term $t$ equals a constant in this model: apply the witness task to $\exists x(x=t)$. Consequently every tuple is represented by a constant tuple and fails a formula of each $p_j$. This proves simultaneous omission.

For arithmetic, the nonstandard element type isIn a model of Peano arithmetic, an element omits this type precisely when it is one of the standard numerals: arithmetic proves that every element at most $\overline{n}$ equals one of $\overline{0},\dots ,\overline{n}$. A model omitting $p_{\infty }$ everywhere is therefore isomorphic to the standard structure $\mathbb{N}$.

For a complete consistent theory $T\supseteq \mathrm{PA}$, this gives the particularly useful equivalenceThe first implication is the omitting types theorem. For the converse, if a consistent $\theta$ over the theory of true arithmetic implied every $x>\overline{n}$, completeness would give $\mathbb{N}\models \exists x\theta (x)$. A standard witness $m$ contradicts the implication $\theta \to x>\overline{m}$.

Completeness matters in this formulation. One must not claim that $p_{\infty }$ is automatically nonprincipal over an arbitrary incomplete arithmetic theory. For example, assuming consistency of Peano arithmetic, the formula saying that $x$ is the least code of a proof of a contradiction is consistent with that theory, by Gödel second incompleteness theorem, and implies $x>\overline{n}$ for each standard $n$. It makes $p_{\infty }$ principal over that incomplete theory, although its standard model still omits the type. The theorem is a sufficient omission criterion, not a necessary one for arbitrary partial types over incomplete theories.

For a first-order theory $T$ in a first-order language $L$, a complete $n$-type is a maximal $T$-consistent set $p(x_1,\dots ,x_n)$ of formulas whose free variables lie among $x_1,\dots ,x_n$. Equivalently, it chooses exactly one of $\phi$ and $\neg \phi$ for every such formula while remaining consistent with $T$.

An isolated type $p$ is isolated by a formula $\theta (\bar{x})$ when $T\cup \{\exists \bar{x}\theta (\bar{x})\}$ is consistent andfor every $\phi \in p$. The type is an omitted type in an $L$-structure $M$ when no tuple $\bar{a}\in M^n$ satisfies every formula in $p$.

The omitting types theorem states that if $T$ is a consistent theory in a countable language and $(p_i{)}_{i\in \mathbb{N}}$ is a countable family of nonisolated finite-arity types, then $T$ has a countable model omitting every $p_i$.

A sufficient condition is that $T$ be first-order consistent, complete, and full in its own first-order language. Work in the allowed function-free setting. Since $T$ proves the logically valid first-order sentence $\exists x(x=x)$, fullness guarantees at least one constant and a nonempty collection of names.

Form the carrier from equivalence classes $[c]$ of constant symbols underLogical equality logic makes this an equivalence relation. Interpret a constant by its class and interpret each relation symbol bySubstitution of equals makes this independent of representatives. This defines a canonical first-order structure because every carrier element is named by a constant.

The truth lemma, proved by induction on logical formulas with constants substituted for their free variables, saysAtomic formulas hold by construction; completeness and first-order consistency give the Boolean steps. For the existential step, a witness in the first-order structure is a named class, so its truth gives a proved instance and hence a proved existential sentence. Conversely a proved existential sentence has a constant witness by fullness, and the induction hypothesis realizes that instance in the first-order structure. The universal case follows by negation. Thus $\mathcal{M}\models T$, provingThe witness condition is needed in the original first-order language; adding new constants produces a canonical first-order structure in an expanded first-order language, which is a different assertion.

A canonical first-order structure is generated by its names: every element is the value of a closed term. In the function-free setting permitted here, this means every element is the interpretation of a constant symbol. Equivalently, the natural map from closed terms modulo logical equality in the first-order structure onto its carrier is surjective. When canonical is defined specifically using constant names, the same definition and all the arguments below apply in this function-free setting.

A full set of first-order sentences has the witness property in its own first-order language: whenever it proves an existential sentence $\exists x\varphi (x)$, some closed term $t$ satisfies that the set proves $\varphi (t)$. In a deductively closed set, one can equivalently state this using membership of the first-order sentences. In the function-free setting the witness first-order term is a constant symbol. This is the Henkin witness property; fullness does not by itself replace the separate requirements of first-order consistency and completeness.

A first-order theory is a set of first-order sentences in a fixed first-order language, often identified with its deductive closure. It is $\kappa$-categorical if it has a first-order model of cardinality $\kappa$ and all first-order models of that cardinality are isomorphic as first-order structures in that same first-order language. In particular, an isomorphism must preserve the named constants as well as the order.

A first-order theory is complete if it is first-order consistent and decides every first-order sentence: for each $\sigma$ it entails either $\sigma$ or $\neg \sigma$. Equivalently all its first-order models satisfy exactly the same first-order sentences. First-order consistency is included to exclude the vacuous first-order theory with no first-order models. The distinctions matter here: naming infinitely many ordered points changes countable categoricity without destroying completeness.

Use the completeness of the first-order theory of dense linear orders without endpoints and its quantifier elimination. After naming finitely many increasing constants, quantifier elimination still holds in the expanded first-order language: treat these constants as fixed parameters when eliminating quantifiers. Every quantifier-free sentence is a Boolean combination of logical equalities and order comparisons of the named constants, all decided by their stated strict increasing order. Hence ${\mathrm{DLO}}_n$ is complete.

An alternative formal proof of this finite case uses the stated general theorem that a first-order theory in a countable first-order language with only infinite first-order models and a unique countable first-order model is complete: if first-order models disagreed on a first-order sentence, downward Löwenheim-Skolem would give disagreeing countable first-order models. Part (iii) supplies the uniqueness.

Every first-order sentence of $L_{\omega }$ mentions only finitely many constant symbols, hence belongs to some $L_n$. Its truth is decided by ${\mathrm{DLO}}_n$, and every first-order model of ${\mathrm{DLO}}_{\omega }$ has a reduct satisfying that finite first-order theory. Thus the larger first-order theory also decides every first-order sentence. The rational-order examples in (ii) establish first-order consistency. ConsequentlyThere is no contradiction with (ii): completeness is agreement on individual finite first-order sentences, while categoricity requires a global isomorphism respecting all constants simultaneously.

Let $\vec{a}\in A^n$, with $A$ finite, and put $T=\mathrm{Th}(\mathcal{A})$. There are only finitely many competing tuples $\vec{b}\in A^n$. For each whose complete type differs from that of $\vec{a}$, choose a logical formula ${\varphi }_{\vec{b}}$ true at $\vec{a}$ and false at $\vec{b}$. Such a logical formula exists by the inequality of their complete types, negating a distinguishing logical formula if necessary.

Let $\theta$ be the conjunction of this finite list, or logical truth if the list is empty. It is true at $\vec{a}$, and every tuple satisfying it has the same partial type as $\vec{a}$. For each $\psi \in \mathrm{tp}(\vec{a})$, the first-order sentenceis therefore true in $\mathcal{A}$ and belongs to $T$. The logical formula $\theta$ is first-order consistent with $T$ because it is realized at $\vec{a}$. It is consequently a principal formula of a type of the partial type, proving every partial type realized in a finite first-order structure is principal. Finiteness of the first-order structure, rather than finiteness of the first-order language, is what makes the conjunction finite.

An $n$-type over a first-order theory $T$ is a set of logical formulas in the displayed $n$ free variables first-order consistent with $T$. A complete type chooses exactly one of $\varphi$ and $\neg \varphi$ for each such logical formula. Equivalently it is a maximal consistent such set. For parameter-free partial types the logical formulas use the original first-order language; partial types over parameters use additional names for those parameters.

A partial type $p(\vec{x})$ is principal if some logical formula $\theta (\vec{x})$ first-order consistent with $T$ implies every member of $p$ modulo $T$:Such a $\theta$ is a principal formula of a type of the partial type. For a complete type it isolates that partial type, so principal complete types are exactly isolated types.

For a tuple $\vec{a}$ in a first-order structure $\mathcal{A}$, its parameter-free partial type isIt is a complete type over $\mathrm{Th}(\mathcal{A})$ because the first-order structure decides the truth of every logical formula at that tuple.

Use the first-order language with one equivalence relation $E$. Let $\mathcal{A}$ have exactly two equivalence classes, one countably infinite and one uncountable, with no further first-order structure. Its complete theory says that there are exactly two classes and both are infinite.

This first-order theory has quantifier elimination. To eliminate one existential logical variable from a conjunction of atomic formulas and negated atomic formulas, a logical equality either fixes its value, or finitely many inequalities exclude finitely many points. Its required equivalence-class membership is determined by the finitely many existing classes represented among the parameters. A required unused class exists exactly when fewer than two classes have already been used. Once its class is possible, infinitude supplies a point avoiding the finite exclusions. These tests are quantifier-free logical equality and equivalence conditions on the parameters. Disjunctive normal form and induction eliminate all quantifiers and also show completeness.

Thus a finite tuple's complete type is isolated by its finite equality-and-equivalence pattern. Every realized finite-tuple partial type is principal, so $\mathcal{A}$ is atomic. In particular all individual elements have the same complete one-type, isolated by $x=x$.

Choose $a$ in the countable class and $b$ in the uncountable class. Any automorphism taking $a$ to $b$ would give a bijection from their whole equivalence classes, impossible because their cardinalities differ. ThereforeIts uncountability is precisely what avoids the conclusion of (iii).

The set of closed-term values is nonempty because the first-order language has a constant. It contains the value of every constant. If $f$ is an $r$-ary function symbol and $t_1,\dots ,t_r$ are closed terms, thenwhich is another closed-term value. Hence the set is closed under every operation. Restrict the operations and relations of $\mathcal{A}$ to it; this defines a substructure $\mathcal{B}$ whose carrier is exactly the specified set.

Part (i) now applies to the universal first-order theory, givingIt is the substructure generated by the first-order language's constants, often called the ground-term substructure. The source's constant-symbol assumption ensures its nonemptiness, even when no other elements can be generated.

An $L$-structure has a nonempty underlying set $A$. It assigns to each constant symbol $c_k$ an element $c_k^{\mathcal{A}}\in A$, to each $n$-ary function symbol $f_j$ a function $A^n\to A$, and to each $n$-ary predicate symbol $P_i$ a relation contained in $A^n$. Logical equality, when included as logical equality, is interpreted as actual identity.

The arities belong to the specification of the first-order language. An assignment of logical variables to elements of $A$ then evaluates first-order terms recursively and determines satisfaction of logical formulas through the logical connectives and quantifiers. A first-order sentence has no free variables, so its truth in the first-order structure is independent of the assignment.

Expand the ring first-order language by a new constant $c$ and considerEvery finite subset is satisfiable in the integer ring itself. Only finitely many divisibility conditions occur; interpret $c$ as a nonzero common multiple of their positive integer indices, using $1$ if none occur. All first-order sentences from $\mathrm{Th}(\mathbb{Z})$ are automatically true there.

Compactness theorem therefore gives a first-order model. Its reduct $R$ to the original ring first-order language satisfies the complete theory of $\mathbb{Z}$, so $R\equiv \mathbb{Z}$. Its element $c^R$ is nonzero and divisible by every positive standard integer. ThusSuch an element cannot be an ordinary nonzero integer, since an integer of absolute value less than $n$ cannot be a nonzero multiple of $n$. The statement concerns each standard integer index separately; it does not assert divisibility by every internally nonzero element of $R$.

The Downward Lowenheim-Skolem theorem says that for an $L$-structure $M$ and a subset $S\subseteq M$, there is an elementary substructure $N\preccurlyeq M$ containing $S$ withIf an infinite cardinal $\kappa$ satisfies $\max (|L|,{\aleph }_0)\le \kappa \le |M|$, one can in particular obtain size exactly $\kappa$ by starting with a subset of that size.

Choose a default element $a_0\in M$. For every logical formula $\exists x\varphi (x,\vec{y})$ choose a Skolem function $F_{\varphi }$ which returns a witness in $M$ when one exists, and returns $a_0$ otherwise. Begin with $S$, the interpretations of the first-order language's constants, and $a_0$. Successively adjoin the values of all the original functions and these Skolem functions on finite tuples already chosen. Let $N$ be the union of the resulting countable sequence of closure stages.

There are at most $\max (|L|,{\aleph }_0)$ logical formulas, and each function has finite arity. With $\kappa =\max (|S|,|L|,{\aleph }_0)$, each closure stage has size at most $\kappa$, and so does their countable union. Closure under the original functions makes $N$ an $L$-substructure. Whenever $M\models \exists x\varphi (x,\vec{a})$ for parameters in $N$, its chosen Skolem witness belongs to $N$, since the finitely many parameters lie in some common stage. The Tarski–Vaught test therefore gives $N\preccurlyeq M$.

For the exact-cardinality version, choose an initial set of $\kappa$ elements, enlarged to contain any prescribed subset of size at most $\kappa$. The construction gives an upper bound $\kappa$ while containment gives the matching lower bound.

If $\mathcal{A}\subseteq \mathcal{B}$, interpret each new constant $c_a$ in $\mathcal{B}$ as the same element $a$. Atomic logical formulas and their negations then have exactly their truth values in ${\mathcal{A}}_A$, so the expansion satisfies the diagram of a structure. If the inclusion is elementary, every logical formula with those named parameters has the same truth value, so the expansion satisfies the elementary diagram.

Conversely, from any expansion ${\mathcal{B}}^{+}$ satisfying the diagram of a structure defineThe diagram of a structure contains $c_a\ne c_{a^{\prime }}$ whenever $a\ne a^{\prime }$, so $e$ is injective. It contains every true function-value equation, so $e$ commutes with all operations and constants. Positive and negative relation instances ensure both preservation and reflection of the relations. Thus $e$ is an embedding of first-order structures. If the expansion satisfies the elementary diagram, for every logical formula $\varphi$ and tuple $\vec{a}$ it also givesso $e$ is an elementary embedding of first-order structures.

The precise conclusion for an arbitrary expansion is an embedding of first-order structures, rather than a literal inclusion of the original carriers. The source's inclusion notation is correct when one uses the customary identification of $\mathcal{A}$ with its embedded copy, or requires the expansion to interpret $c_a$ as the actual element $a$ of a carrier already containing $A$. With that naming convention, $e$ is the inclusion and the requested two equivalences follow exactly.

Without the convention the literal wording fails, even in the first-order language of logical equality: singleton first-order structures with carriers $\{0\}$ and $\{1\}$ have a diagram-satisfying expansion by sending the first first-order structure's named point to $1$, but the first carrier is not a subset of the second. The embedding of first-order structures formulation proved above states the invariant result and makes the intended inclusion formulation precise.

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.

Apply downward Löwenheim-Skolem to the extension from part (i), keeping all standard integers and the new prime $c$. The first-order language and this prescribed subset are countable, so there is a countable elementary substructure $N$ containing them. In particular $N\equiv \mathcal{Z}$ and contains an element outside the standard copy of $\mathbb{Z}$.

No ring isomorphism $N\to \mathcal{Z}$ can exist. Such an isomorphism fixes $0$ and $1$, hence every nonnegative integer numeral. It also fixes each negative integer, which is the unique solution of $x+\bar{n}=0$ for the corresponding positive $n$. Consequently it fixes the whole standard copy. The image of $c$ would be some standard integer $a$, already the image of that same named standard element, violating injectivity.

Thus $N$ and $\mathcal{Z}$ are two nonisomorphic countably infinite first-order models of $T$, so