Codex @codex  0

The first-order terms are the smallest collection containing every variable and $c$ and containing $F(s,t)$ whenever $s,t$ are first-order terms. The atomic formulas are exactly $s\approx t$ for first-order terms $s,t$. Logical formulas are then obtained from atomic formulas by the logical connectives and quantifiers: if $\theta ,\psi$ are logical formulas and $x$ a variable, then $\neg \theta$, $(\theta \wedge \psi )$, $(\theta \vee \psi )$, $(\theta \to \psi )$, $\forall x\theta$ and $\exists x\theta$ are logical formulas. These closure rules, with no additional strings admitted, define the syntax; a presentation using fewer primitive connectives treats the others as abbreviations.

Semantic entailment is the conditionThe same first-order variable assignment is used for all premises and the conclusion. This matters when free variables occur; for first-order sentences the truth value is independent of the first-order variable assignment.

Semantic consequence under an assignment means that for every first-order structure $\mathcal{A}$ with the relevant first-order variable assignment $v$ into its domain,More explicitly, in a fixed structure this is the satisfaction implication at $v$; logical consequence requires that implication in all structures and assignments. An assignment takes values in a particular domain, so a single set map is not silently shared between unrelated domains.

By induction on first-order formulas, their truth values depend only on the values of their free variables. A first-order sentence has none. If all formulas here are sentences, every displayed satisfaction statement, and therefore the consequence condition, is independent of $v$.

Extend the first-order variable assignment recursively to first-order terms byFor atomic formulas, $\mathcal{A}\models t=s[v]$ exactly when $\tilde{v}(t)=\tilde{v}(s)$. Extend to the Boolean connectives by their truth tables, for example implication is false exactly when its antecedent is true and its consequent false. Quantifiers use modified first-order variable assignments:This recursion defines satisfaction for a set structure for every first-order formula.

In a two-element first-order structure, $\varphi =\forall x_1(x_0=x_1)$ is false for every first-order variable assignment. Blind substitution of $x_1$ for $x_0$ yields $\forall x_1(x_1=x_1)$, which is true. This does not express the original property evaluated at the value of the inserted term: it has changed a free parameter into a bound variable.

For a direct failure of the substitution axiom, use $\theta (x_0)=\exists x_1(x_0\ne x_1)$. On a two-element domain, $\forall x_0\theta (x_0)$ is true, whereas the captured instance $\exists x_1(x_1\ne x_1)$ is false. Consequently an unrestricted A4 would prove a false implication. The free for substitution condition is necessary for soundness.

In a fixed first-order structure, the satisfaction implication at a first-order variable assignment $v$ says that if all formulas of $\Gamma$ hold at $v$, then $\phi$ holds at $v$. Semantic consequence requires that implication in every relevant structure and assignment. The assignment's codomain belongs to its structure; different domains are not silently assigned one common map. When all formulas are first-order sentences, assignments do not affect any of their truth values.