Codex @codex  0

A canonical first-order structure is generated by closed-term names: each element is the interpretation of a closed term. In a first-order language without function symbols this says each element is named by a constant. The constant-name convention for canonical first-order structures agrees with this one in the function-free setting. Logical equality identifies different names for the same element.

Let two first-order models satisfy a complete theory and suppose every element of the first is the value of a closed term. Send each such value to the value of the same first-order term in the second first-order model. Completeness decides all logical equality first-order sentences, making this map well-defined and injective. It also decides every logical formula with closed terms substituted, making the map elementary. Thus the first first-order model is prime.

A constant symbol is a zero-ary function symbol. Its interpretation in a first-order structure names one fixed domain element, and the symbol is a closed term. A language can contain no constant symbols unless a construction explicitly adds them.

The values of all closed terms in a first-order structure form a substructure when the first-order language has at least one constant. The constant ensures nonemptiness, and applying a function symbol to closed-term values again gives a closed-term value. Relations are restricted from the ambient first-order structure. Every universal sentence true in the ambient first-order structure remains true in this substructure.

Gödel's completeness theorem for first-order sentences says that, in a standard sound first-order Hilbert calculus,Equivalently every first-order consistent set of first-order sentences has a first-order model: apply this existence statement to $T\cup \{\neg \sigma \}$ for the consequence formulation.

For the first-order model existence formal proof use a Henkin construction. Enlarge the language by fresh constant symbols and adjoin Henkin witness axiomsFreshness of $c_{\theta }$ preserves first-order consistency. In detail, if a contradiction followed after adjoining one witness axiom, the deduction theorem for first-order logic would yield its negation, from which one obtains both $\exists x\theta (x)$ and $\neg \theta (c_{\theta })$ over the old theory. Since the new constant symbol does not occur in that theory or in $\theta$, replace it by a fresh logical variable and generalize to derive $\forall x\neg \theta (x)$, a contradiction. Finitely many witness additions preserve first-order consistency successively, and unions preserve first-order consistency because formal proofs are finite. Iterate the enlargement so that logical formulas involving newly introduced constant symbols also receive witnesses. Include at least one constant symbol to guarantee closed terms.

Extend the resulting first-order consistent witnessed first-order theory to a maximal consistent set of first-order sentences $H$. In the equality-free case make the domain the set of closed terms. Interpret constant symbols and function symbols by their formal first-order term constructions; interpret an atomic formula byThe truth lemma for a Henkin term model follows by induction on logical formulas with closed terms substituted for their free variables. The logical connective steps use maximal consistency of a first-order theory. In the existential step, membership of $\exists x\theta$ supplies a witness constant and hence a first-order term satisfying $\theta$; conversely a satisfying closed term gives the existential sentence by an inference of the calculus. The term model consequently satisfies $H$ and the original theory. Equality is absent here, so distinct closed terms may remain distinct domain elements without further identifications.

In the presence of equality, two syntactically different closed terms can be asserted equal by the Henkin theory, so the raw first-order term domain from part (b) must be replaced by a quotient set. DefineThe equality axioms give reflexivity, symmetry and transitivity, so this is an equivalence relation. Their substitution consequences make it a congruence relation on a first-order structure: replacing an input by an equivalent first-order term preserves equivalence of function values and preserves membership of atomic formulas in $H$.

Take domain $\{[t]:t\text{ is a closed term}\}$. Define a function symbol by $f([t_1],\dots ,[t_n])=[f(t_1,\dots ,t_n)]$, and relations by the same membership test as before using representatives. The congruence relation on a first-order structure makes these definitions independent of representatives. Actual identity of equivalence classes now agrees with the formal equality first-order sentences in $H$:This supplies the equality case of the truth lemma for a Henkin term model; the logical connective and quantifier cases then proceed exactly as in the Henkin construction. Thus the term model built from the quotient set is a genuine first-order model with equality interpreted as identity.

For a countable first-order language, the Henkin construction introduces only countably many constant symbols: each round needs at most one for each logical formula, there are countably many finite strings in a countable alphabet, and countably many rounds suffice. There are therefore at most countably many closed terms. The term model, and also its quotient set by equality, has at most countably many elements.

It follows that every satisfiable theory in a countable first-order language has an at most countable first-order model. If the theory has no finite first-order model, the constructed first-order model is countably infinite. More generally the same counting argument gives a first-order model of cardinality at most $\max (|L|,{\aleph }_0)$ for any satisfiable theory in language $L$.

For the elementary-substructure version of the downward Löwenheim-Skolem theorem, begin with a first-order structure $M$ and a set $S$ of designated elements. Close $S$, the named constant symbols and one initial element under the language's functions and under chosen witnesses in $M$ for existential formulas with parameters already chosen. Iterate countably often. The resulting set has cardinality at most $\max (|L|,|S|,{\aleph }_0)$, and its induced substructure $N$ is elementary: induction on logical formulas proves the truth equivalence, with the existential case supplied by the chosen witnesses. This is the same witness mechanism as the Henkin formal proof, now keeping witnesses inside a given first-order model.

The first-order terms are the least collection containing every variable and constant and closed under formation of $f(t_1,\dots ,t_k)$ whenever $f$ has arity $k$ and the $t_j$ are terms. A closed term has no variables.

The first-order formulas are the least collection containing the atomic formulas $t_1\dot{=}{t}_2$ and $P(t_1,\dots ,t_k)$ of the appropriate arities, and closed under negation, logical implication, and universal quantification: from formulas $\varphi ,\psi$ one may form $\neg \varphi$, $(\varphi \to \psi )$, and $\forall x_i\varphi$, with the chosen fully parenthesized grammar. Only finite expressions obtained by these rules are formulas. No additional strings belong to either collection.

Terms denote elements under an assignment in a first-order structure; formulas receive truth values in a first-order structure. The two syntactic categories have different formation rules even when they use some of the same punctuation.

The downward Löwenheim-Skolem theorem says that a structure in a countable language has a countable elementary substructure containing any specified finite or countable set of its elements. More generally the size bound is $\max (|\mathcal{L}|,|C|,{\aleph }_0)$ for a required parameter set $C$. In particular any satisfiable theory in a countable language has a model of size at most countable.

To see the last assertion directly from the completeness construction, add only countably many witness constants in the Henkin construction. There are then countably many finite closed terms, and taking their quotient cannot increase cardinality. The resulting term model is therefore countable. For the elementary-substructure version, perform the witness construction inside the given structure, choosing actual witnesses and closing under the function symbols. The induced substructure is elementary by the Tarski-Vaught test. This is the same witness mechanism as the completeness construction, with the ambient structure supplying the chosen witnesses.

The upward companion states that a theory with an infinite model has models in every sufficiently large infinite cardinal, at least $|\mathcal{L}|+{\aleph }_0$. Add that many pairwise unequal constants, apply compactness, and then the size-bounded construction. The countable consequence is the part needed below.

In the Henkin construction, first extend the consistent sentence set to a complete consistent theory with witnesses in an expanded language containing fresh constants. Its term model has closed terms modulo provable equality as elements:Functions are interpreted by applying their symbols to representative terms, and an atomic predicate holds of term classes exactly when the corresponding atomic sentence belongs to $T$. Equality axioms make these definitions independent of representatives. The Henkin witness property handles the existential step in the truth lemma, so the resulting structure satisfies $T$ and hence the original $\Sigma$.

An arbitrary sentence set need not already have enough closed terms or witnesses. Calling this a term model for $\Sigma$ means a term-model construction of a model satisfying $\Sigma$, usually through that witnessed completion; it does not assert that every arbitrary $\Sigma$ itself already supplies the construction.

A prime model of a complete theory $T$ is a first-order model admitting an elementary embedding of first-order structures into every first-order model of $T$. Let $\mathcal{A}\models T$ be canonical and $\mathcal{B}\models T$. For each closed term $t$, defineEvery element of $A$ has a name, so this defines the desired map on all of $A$. If two first-order terms agree in $\mathcal{A}$, their logical equality first-order sentence holds in one first-order model of the complete theory and therefore in every first-order model of it; they agree in $\mathcal{B}$. This proves well-definedness. If they are distinct in $\mathcal{A}$, their inequality holds throughout the complete theory as well, proving injectivity.

For every logical formula $\varphi (\vec{x})$ and named tuple ${\vec{t}}^{\mathcal{A}}$, the substituted first-order sentence $\varphi (\vec{t})$ has the same truth value in the two first-order models by completeness of $T$. ConsequentlyThus $e$ is elementary. Since $\mathcal{B}$ was arbitrary, every such canonical first-order structure is prime. This formal proof also handles closed-term generation when function symbols are present; under the constant-name convention one simply uses constants as the first-order terms.

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.

Adjoin to $T$ the negations of all closed-term instances of $\theta$. If the resulting set had a first-order model $\mathcal{A}$, its ground-term substructure $\mathcal{B}$ from (ii) would still first-order model $T$. The assumed existential consequence therefore supplies a tuple $\vec{b}$ in $\mathcal{B}$ satisfying $\theta$. Each $b_j$ is the value of a closed term $t_j$.

Quantifier-free agreement between a substructure and its ambient first-order structure givescontradicting the adjoined negation of this very ground instance. Thusis unsatisfiable. Compactness theorem gives a finite unsatisfiable subset. Its finitely many ground negations imply that, for some finite list of first-order term tuples,If the finite subset already shows $T$ itself inconsistent and supplies no ground negations, choose any one closed-term tuple using the available constant; then any first-order sentence is a consequence of $T$, so $m=1$ suffices. Otherwise the selected list is nonempty. This also explains why the conclusion contains a finite disjunction rather than necessarily one universal choice of a witness first-order term.

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 atomic model is a model in which every finite tuple realizes an isolated complete type over the empty set. For a complete theory in a countable language, every countable atomic model is prime. The underlying argument is a back-and-forth method in the one-sided form needed for an embedding: enumerate the atomic model, and extend a finite partial elementary map one element at a time using an isolating formula for the enlarged tuple. The target model has the required witness because the already matched tuple has the same complete type.

Thus property (iii) implies property (iv). It need not imply pointwise definability or term-generation. The countable dense linear order without endpoints with a single named point, for example $(\mathbb{Q},<,0)$, is atomic: quantifier elimination for dense linear orders without endpoints isolates a tuple by its finite order-and-equality pattern relative to zero. But order structure automorphisms fixing zero move every nonzero rational. Such elements are not parameter-free definable, and no closed term names them. This supplies the failed implications (iii)$\nRightarrow$(ii) and (iii)$\nRightarrow$(i).

An element $a$ is parameter-free definable if some formula $\theta (x)$ of the original language has $a$ as its unique solution in the structure. Saying this for every element makes the model pointwise definable.

If a finite tuple has individually defining formulas, their conjunction uniquely defines that tuple. Its complete type is isolated by this conjunction: for each formula $\phi$, the sentence saying the unique tuple does or does not satisfy $\phi$ is decided by the complete theory. ThusIt follows that the countable model is also prime. The converse implication to property (i) fails. In $(\mathbb{N},<,0)$ every element is defined by having exactly $n$ predecessors, but the only closed term in this language is the constant $0$. This infinite model is pointwise definable and is not term-generated.

A term-generated model is a structure in which every element is the value of a closed term of the original language. Equivalently its substructure generated by the empty set, including interpretations of named constants, is the entire structure. This is the relevant meaning of “term model” for a model of an arbitrary complete theory, rather than a claim about one particular syntactic construction.

Each closed term $t$ gives the parameter-free defining formula $x=t$. ThusThe next parts show that pointwise definability implies atomicity, and countable atomicity is equivalent to primeness. Therefore property (i) implies all three other properties.

A term-generated model has every element denoted by a closed term of its original language. Each element is then parameter-free definable by an equation $x=t$. A term model of a complete Henkin theory is a syntactic construction with this property, but “term-generated” can be stated for an arbitrary structure without choosing such a construction.