[proofplan] We prove the semantic soundness of universal instantiation. The key technical point is the substitution lemma: evaluating the capture-free substitution $A(t)$ under an assignment $s$ is the same as evaluating $A(x)$ under the assignment obtained from $s$ by sending $x$ to the value denoted by $t$. Once this is established, the universal hypothesis immediately gives the desired instance because that denoted value is one of the elements over which the universal quantifier ranges. [/proofplan] [step:Record the semantic notation for assignments and term values] Let $M$ denote the domain of the $\mathcal{L}$-structure $\mathcal{M}$. Let $\operatorname{Var}(\mathcal{L})$ denote the set of variables of the first-order language $\mathcal{L}$. An assignment in $\mathcal{M}$ is a map \begin{align*} s : \operatorname{Var}(\mathcal{L}) &\to M. \end{align*} For an assignment $s : \operatorname{Var}(\mathcal{L}) \to M$ and an element $a \in M$, define the updated assignment \begin{align*} s[x \mapsto a] : \operatorname{Var}(\mathcal{L}) &\to M \end{align*} by sending $x$ to $a$ and agreeing with $s$ on every variable distinct from $x$. Let \begin{align*} \llbracket t \rrbracket_{\mathcal{M},s} \in M \end{align*} denote the value of the term $t$ in $\mathcal{M}$ under the assignment $s$. Since every term denotes an element of the domain under every assignment, the element \begin{align*} a := \llbracket t \rrbracket_{\mathcal{M},s} \end{align*} is a well-defined element of $M$. [/step] [step:Prove the capture-free substitution lemma] [claim:Substitution lemma] For every $\mathcal{L}$-formula $B$, every variable $x$, every $\mathcal{L}$-term $t$ that is free for $x$ in $B$, every $\mathcal{L}$-structure $\mathcal{M}$, and every assignment $s$ in $\mathcal{M}$, \begin{align*} \mathcal{M},s \models B[t/x] \quad \Longleftrightarrow \quad \mathcal{M},s[x \mapsto \llbracket t \rrbracket_{\mathcal{M},s}] \models B. \end{align*} [/claim] [proof] We prove the claim by structural induction on $B$. First consider the atomic case. Let $B$ be either an equality formula $u_1 = u_2$ or a relation formula $R(u_1,\dots,u_n)$, where $u_1,\dots,u_n$ are $\mathcal{L}$-terms. We use the corresponding term-substitution fact: for every term $u$, \begin{align*} \llbracket u[t/x] \rrbracket_{\mathcal{M},s} = \llbracket u \rrbracket_{\mathcal{M},s[x \mapsto \llbracket t \rrbracket_{\mathcal{M},s}]}. \end{align*} This term-substitution fact is proved by induction on the construction of the term $u$: it is immediate for variables, and the function-symbol case follows by applying the induction hypothesis to each argument term and then using the interpretation of the relevant function symbol in $\mathcal{M}$. For equality, the displayed identity gives \begin{align*} \mathcal{M},s \models u_1[t/x] = u_2[t/x] \quad \Longleftrightarrow \quad \llbracket u_1 \rrbracket_{\mathcal{M},s[x \mapsto a]} = \llbracket u_2 \rrbracket_{\mathcal{M},s[x \mapsto a]}, \end{align*} where $a := \llbracket t \rrbracket_{\mathcal{M},s}$. This is exactly \begin{align*} \mathcal{M},s[x \mapsto a] \models u_1 = u_2. \end{align*} The relation-symbol case is identical: the tuple of values of the substituted terms under $s$ equals the tuple of values of the original terms under $s[x \mapsto a]$, so membership in the interpretation $R^{\mathcal{M}} \subseteq M^n$ is preserved. The Boolean connectives follow directly from their truth definitions and the induction hypothesis. For example, \begin{align*} \mathcal{M},s \models (C \wedge D)[t/x] \end{align*} holds iff both $\mathcal{M},s \models C[t/x]$ and $\mathcal{M},s \models D[t/x]$ hold, which by the induction hypothesis is equivalent to both \begin{align*} \mathcal{M},s[x \mapsto a] \models C \quad \text{and} \quad \mathcal{M},s[x \mapsto a] \models D. \end{align*} This is precisely \begin{align*} \mathcal{M},s[x \mapsto a] \models C \wedge D. \end{align*} Negation, disjunction, implication, and biconditional are handled by the same truth-functional argument. It remains to treat quantifiers. Consider $B = \forall y\,C$. If $y = x$, then no free occurrence of $x$ in $C$ is free in $\forall x\,C$, so $(\forall x\,C)[t/x] = \forall x\,C$. Also, for every $b \in M$, \begin{align*} s[x \mapsto a][x \mapsto b] = s[x \mapsto b]. \end{align*} Hence \begin{align*} \mathcal{M},s[x \mapsto a] \models \forall x\,C \quad \Longleftrightarrow \quad \mathcal{M},s \models \forall x\,C. \end{align*} Now suppose $y \neq x$. We separate the case in which the substitution under the $\forall y$-binder is vacuous. If $x$ is not free in $C$, then $C[t/x] = C$, and $x$ is not free in $\forall y\,C$. We use the free-variable invariance fact for formulas: if a variable $z$ is not free in a formula $E$, then changing only the value assigned to $z$ does not change whether $E$ is satisfied. This fact is proved by structural induction on $E$, using the corresponding free-variable invariance fact for terms in the atomic case. Applying it with $z = x$ and $E = \forall y\,C$, we obtain \begin{align*} \mathcal{M},s \models \forall y\,C[t/x] &\Longleftrightarrow \mathcal{M},s \models \forall y\,C \\ &\Longleftrightarrow \mathcal{M},s[x \mapsto a] \models \forall y\,C. \end{align*} This proves the quantified case when no free occurrence of $x$ occurs in $C$. It remains to consider the case where $x$ is free in $C$. Since $t$ is free for $x$ in $\forall y\,C$ and the binder $\forall y$ scopes every occurrence of $C$, the variable $y$ is not free in the term $t$; otherwise a free occurrence of $y$ in $t$ would be captured by the quantifier $\forall y$ after substitution. We use the free-variable invariance fact for terms: if a variable $z$ is not free in a term $u$, then changing only the value assigned to $z$ does not change the value of $u$. This fact is proved by induction on the construction of $u$. Applying it with $z = y$ and $u = t$, for every $b \in M$ we have \begin{align*} \llbracket t \rrbracket_{\mathcal{M},s[y \mapsto b]} = \llbracket t \rrbracket_{\mathcal{M},s} = a. \end{align*} Also, $t$ is free for $x$ in $C$, so the induction hypothesis is available for the formula $C$. Using the definition of satisfaction for the universal quantifier and the induction hypothesis applied to $C$ with the assignment $s[y \mapsto b]$, we get \begin{align*} \mathcal{M},s \models \forall y\,C[t/x] &\Longleftrightarrow \text{for every } b \in M,\ \mathcal{M},s[y \mapsto b] \models C[t/x] \\ &\Longleftrightarrow \text{for every } b \in M,\ \mathcal{M},s[y \mapsto b][x \mapsto a] \models C. \end{align*} Because $x \neq y$, the assignments $s[y \mapsto b][x \mapsto a]$ and $s[x \mapsto a][y \mapsto b]$ agree on every variable. Thus the last condition is equivalent to \begin{align*} \text{for every } b \in M,\ \mathcal{M},s[x \mapsto a][y \mapsto b] \models C, \end{align*} which is exactly \begin{align*} \mathcal{M},s[x \mapsto a] \models \forall y\,C. \end{align*} The existential quantifier is handled in the same way, replacing “for every $b \in M$” by “there exists $b \in M$”. This completes the structural induction. [/proof] [guided] The purpose of the substitution lemma is to make precise what capture-free substitution means semantically. If we write $B[t/x]$, we want this formula to say: evaluate $B$ as though the variable $x$ had been assigned the object denoted by $t$. The lemma states exactly that equivalence: \begin{align*} \mathcal{M},s \models B[t/x] \quad \Longleftrightarrow \quad \mathcal{M},s[x \mapsto \llbracket t \rrbracket_{\mathcal{M},s}] \models B. \end{align*} We prove it by structural induction on $B$. In atomic formulas, the only issue is how terms behave under substitution. For every term $u$, substitution satisfies \begin{align*} \llbracket u[t/x] \rrbracket_{\mathcal{M},s} = \llbracket u \rrbracket_{\mathcal{M},s[x \mapsto \llbracket t \rrbracket_{\mathcal{M},s}]}. \end{align*} This is proved by induction on terms: variables are immediate, and if $u$ is obtained by applying a function symbol to smaller terms, then the induction hypothesis applies to each argument before the interpretation of the function symbol is evaluated. For an equality formula $u_1 = u_2$, the term identity says that both sides of the substituted equality under $s$ have the same values as the original terms under the updated assignment. Thus \begin{align*} \mathcal{M},s \models u_1[t/x] = u_2[t/x] \quad \Longleftrightarrow \quad \mathcal{M},s[x \mapsto a] \models u_1 = u_2, \end{align*} where $a := \llbracket t \rrbracket_{\mathcal{M},s}$. The same reasoning applies to a relation formula $R(u_1,\dots,u_n)$, because the tuple of interpreted substituted terms under $s$ is exactly the tuple of interpreted original terms under $s[x \mapsto a]$. Boolean connectives preserve the lemma because their semantics are truth-functional. For instance, conjunction satisfies \begin{align*} \mathcal{M},s \models (C \wedge D)[t/x] \end{align*} iff both substituted formulas $C[t/x]$ and $D[t/x]$ hold under $s$. By the induction hypothesis, this is equivalent to both $C$ and $D$ holding under $s[x \mapsto a]$, which is precisely \begin{align*} \mathcal{M},s[x \mapsto a] \models C \wedge D. \end{align*} The quantifier step is where the capture-free condition is used. Let $B = \forall y\,C$. If $y = x$, then the quantifier $\forall x$ binds every occurrence of $x$ inside its scope, so substituting for free occurrences of $x$ does not enter the formula. Moreover, updating an assignment at $x$ before evaluating $\forall x$ has no effect, because the universal quantifier immediately ranges over all possible values of $x$: \begin{align*} s[x \mapsto a][x \mapsto b] = s[x \mapsto b]. \end{align*} If $y \neq x$, there is one subtlety: the side condition that $t$ is free for $x$ in $\forall y\,C$ does not by itself imply that $y$ is absent from $t$ when no free occurrence of $x$ occurs in $C$. We therefore split into two cases. First suppose $x$ is not free in $C$. Then substituting for $x$ inside $C$ changes nothing, so $C[t/x] = C$ and hence $\forall y\,C[t/x] = \forall y\,C$. Also $x$ is not free in $\forall y\,C$. We use the free-variable invariance fact for formulas: if a variable $z$ is not free in a formula $E$, then changing only the value assigned to $z$ does not affect satisfaction of $E$. This fact is proved by structural induction on $E$; in atomic formulas it uses the corresponding free-variable invariance fact for terms, and the quantifier cases follow from the semantic clauses for quantifiers. Applying this fact with $z = x$ and $E = \forall y\,C$, we obtain \begin{align*} \mathcal{M},s \models \forall y\,C[t/x] &\Longleftrightarrow \mathcal{M},s \models \forall y\,C \\ &\Longleftrightarrow \mathcal{M},s[x \mapsto a] \models \forall y\,C. \end{align*} So the lemma holds in the vacuous-substitution case without making any claim about whether $y$ occurs in $t$. Now suppose $x$ is free in $C$. In this case substitution really occurs under the binder $\forall y$. Since $t$ is free for $x$ in $\forall y\,C$, a free occurrence of $y$ in $t$ would be captured by that binder after substitution. Therefore $y$ is not free in $t$. We use the free-variable invariance fact for terms: if a variable $z$ is not free in a term $u$, then changing only the value assigned to $z$ does not change the value of $u$. This fact follows by induction on the construction of $u$. Applying it with $z = y$ and $u = t$, for every $b \in M$ we have \begin{align*} \llbracket t \rrbracket_{\mathcal{M},s[y \mapsto b]} = \llbracket t \rrbracket_{\mathcal{M},s} = a. \end{align*} Also, $t$ is free for $x$ in the matrix $C$, so the induction hypothesis applies to $C$ under the assignment $s[y \mapsto b]$. We obtain \begin{align*} \mathcal{M},s \models \forall y\,C[t/x] &\Longleftrightarrow \text{for every } b \in M,\ \mathcal{M},s[y \mapsto b] \models C[t/x] \\ &\Longleftrightarrow \text{for every } b \in M,\ \mathcal{M},s[y \mapsto b][x \mapsto a] \models C \\ &\Longleftrightarrow \text{for every } b \in M,\ \mathcal{M},s[x \mapsto a][y \mapsto b] \models C \\ &\Longleftrightarrow \mathcal{M},s[x \mapsto a] \models \forall y\,C. \end{align*} The commutation of the two assignment updates is valid because $x \neq y$. The existential case is identical except that the universal quantifier over $b \in M$ is replaced by an existential quantifier. Hence the substitution lemma is proved. [/guided] [/step] [step:Apply universal truth to the object denoted by the substituted term] Assume \begin{align*} \mathcal{M},s \models \forall x\,A(x). \end{align*} By the semantic clause for the universal quantifier, this means that for every $b \in M$, \begin{align*} \mathcal{M},s[x \mapsto b] \models A(x). \end{align*} Apply this with the particular element \begin{align*} a := \llbracket t \rrbracket_{\mathcal{M},s} \in M. \end{align*} Then \begin{align*} \mathcal{M},s[x \mapsto a] \models A(x). \end{align*} [guided] The universal hypothesis says more than truth at the current assignment. It says that the matrix $A(x)$ remains true after assigning $x$ to any element of the domain $M$. The term $t$ denotes one such element, namely \begin{align*} a := \llbracket t \rrbracket_{\mathcal{M},s}. \end{align*} Since $a \in M$, the universal quantifier allows us to instantiate $x$ with this specific element. Therefore, \begin{align*} \mathcal{M},s[x \mapsto a] \models A(x). \end{align*} This is the semantic core of universal instantiation: the value of the term is among the objects over which the universal quantifier ranges. [/guided] [/step] [step:Convert the updated-assignment truth back into the substituted formula] Since $t$ is free for $x$ in $A(x)$, the substitution lemma applies to $B = A(x)$. Thus \begin{align*} \mathcal{M},s \models A(t) \quad \Longleftrightarrow \quad \mathcal{M},s[x \mapsto \llbracket t \rrbracket_{\mathcal{M},s}] \models A(x). \end{align*} The right-hand side was proved in the previous step. Therefore \begin{align*} \mathcal{M},s \models A(t). \end{align*} This proves that from $\forall x\,A(x)$ one may infer $A(t)$ whenever $t$ is free for $x$ in $A(x)$. [guided] We have already proved the semantic fact needed for the instance. Namely, with \begin{align*} a := \llbracket t \rrbracket_{\mathcal{M},s}, \end{align*} the previous step established \begin{align*} \mathcal{M},s[x \mapsto a] \models A(x). \end{align*} To translate this back into the syntactic formula obtained by substitution, we apply the substitution lemma with $B = A(x)$. The hypothesis needed for that lemma is exactly the side condition in the theorem statement: $t$ is free for $x$ in $A(x)$. Hence \begin{align*} \mathcal{M},s \models A(t) \quad \Longleftrightarrow \quad \mathcal{M},s[x \mapsto \llbracket t \rrbracket_{\mathcal{M},s}] \models A(x). \end{align*} Since $a = \llbracket t \rrbracket_{\mathcal{M},s}$, the right-hand side is precisely the statement already proved. Therefore \begin{align*} \mathcal{M},s \models A(t). \end{align*} Thus every structure and assignment satisfying $\forall x\,A(x)$ also satisfies $A(t)$, provided $t$ is free for $x$ in $A(x)$. This is the soundness of the universal elimination rule. [/guided] [/step]