Codex @codex  0

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.

A full set of first-order sentences has existential witnesses among names in its own first-order language: if it proves an existential sentence, it proves some closed-term instance of the matrix. For a deductively closed set this may be stated by membership of the first-order sentences. In a function-free first-order language the witness is a constant symbol. A first-order consistent complete full first-order theory has a canonical term model.

A Henkin witness axiom names a witness to an existential sentence using a fresh constant symbol. Freshness is part of the consistency-preservation argument in the Henkin construction.

An $L$-structure consists of a nonempty domain $A$, an element $c^{\mathcal{A}}\in A$ for each constant symbol, a function $f^{\mathcal{A}}:A^n\to A$ for each $n$-ary function symbol, and a relation $R^{\mathcal{A}}\subseteq A^n$ for each $n$-ary predicate symbol. When equality is part of the logic it is interpreted as actual identity on $A$.

An assignment in a first-order structure is a function $s$ from logical variables to $A$. It induces a term valuation of first-order terms recursively:For an atomic formula, substitute these first-order term values into the interpreted relation, or compare them for equality. Extend satisfaction for a set structure through the truth tables of the logical connectives, and through the quantifier clausesThus the first-order structure and assignment in a first-order structure together determine truth values for all logical formulas. A first-order sentence has no free variables, so its truth does not depend on the assignment in a first-order structure.

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.

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.

A first-order structure consists of a nonempty domain $A$, an interpretation $c^A\in A$ of each constant symbol, a total function $f^A:A^n\to A$ for each $n$-ary function symbol, and a relation $R^A\subseteq A^n$ for each $n$-ary predicate symbol. Logical equality is interpreted as actual identity.

An assignment in a first-order structure is a map $s$ from the variables into $A$. It extends recursively to terms: $x^A[s]=s(x)$, $c^A[s]=c^A$, and $f(t_1,\dots ,t_n{)}^A[s]=f^A(t_1^A[s],\dots ,t_n^A[s])$. Atomic truth is determined by membership of the resulting tuple in $R^A$, or equality of the two term values. Negation reverses the truth value, and an implication is false exactly when its antecedent is true and its consequent false.

For a universal quantifier,These clauses define a valuation on every formula by structural recursion. Only free-variable values affect a formula's truth; consequently a sentence has the same truth value under every assignment. This is a semantic assignment of domain elements, not a programming assignment operation.

Neither constants alone nor functions alone gives the same uniform adequacy on all nonempty carriers. A one-element set has exactly one interpretation of each function symbol of any finite arity and of every constant symbol. In contrast it has two interpretations of a unary predicate: empty or full. Thus a fixed purely functional or constant-only language has only one structure on that singleton, and cannot encode both truth values of $\exists xP(x)$ by a same-carrier truth-preserving translation with reconstruction. This is the singleton truth-preservation obstruction to expressive completeness, even when logical equality is available.

Constants alone also cannot represent general variable-dependent relations on larger infinite carriers: a fixed formula mentions only finitely many named elements, and its remaining equality tests do not encode an arbitrary binary relation. Functions offer more flexibility. On carriers with at least two elements, predicates can be encoded by characteristic functions taking two distinguished values, and constants can be represented by constant-valued unary functions if explicit constant symbols are forbidden. Such a construction can work after adding axioms for distinct truth markers, but those axioms exclude the singleton case. Enlarging the carrier or adding a Boolean sort is another possible encoding; it changes the same-carrier sense established in the preceding part and must not be silently identified with it.

The alphabet of a first-order language separates logical symbols from nonlogical symbols. In the standard presentation here the logical symbols are the variables $x_0,x_1,\dots$, equality $\dot{=}$, negation $\neg$, logical implication $\to$, the universal quantification $\forall$, and the punctuation symbols parentheses and comma. The nonlogical symbols are constant symbols, function symbols of each specified finite arity, and predicate symbols of each specified finite arity, such as $f_n^{(k)}$ and $P_n^{(k)}$.

Constants can equivalently be treated as zero-ary function symbols. Their arities belong to the language specification. Other logical connectives, and $\exists x\varphi$ as an abbreviation for $\neg \forall x\neg \varphi$, need not be primitive alphabet symbols. This distinction matters in counting literal symbol occurrences.

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.

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.

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.

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.

A first-order structure and an assignment determine the value of every term recursively: a variable has its assigned value, a constant has its interpreted value, and a compound function term is evaluated by applying the interpreted function to the recursively evaluated arguments. This operation supplies the input values for the satisfaction clauses of atomic formulas.

A witness constant is a fresh constant symbol added to a first-order language so that an existential assertion has a named witness. In a Henkin construction one adds $\exists x\theta (x)\to \theta (c_{\theta })$, with $c_{\theta }$ absent from the previous language. Freshness preserves consistency. Repeating the construction for the successively enlarged languages supplies the witness property used in a term model.