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.

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 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.