Soundness of universal instantiation

We argue directly from Tarski's satisfaction semantics, which defines truth in a structure recursively on formula structure.

By the semantic clause for $\forall$: $\mathcal{M} \models_s \forall x\, P(x) \iff \text{for every } d \in M,\ \mathcal{M} \models_{s[x \mapsto d]} P(x)$. Assume the hypothesis $\mathcal{M} \models_s \forall x\, P(x)$; by this clause, $\mathcal{M} \models_{s[x \mapsto d]} P(x)$ holds for every $d \in M$, with no exception.

Since the claim holds for every $d \in M$, it holds in particular for $d = t^{\mathcal{M},s}$, the element that the term $t$ denotes in $\mathcal{M}$ under $s$. Substituting this specific $d$ gives $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$.

By the Substitution Lemma (a standard result relating variable assignment to term substitution, provable by induction on the structure of $P$): $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x) \iff \mathcal{M} \models_s P(t)$, valid precisely because $t$ is substitutable for $x$ in $P(x)$ (no free variable of $t$ becomes accidentally bound). Applying the lemma converts $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$ into $\mathcal{M} \models_s P(t)$.

Since $\mathcal{M}$, $s$, and $t$ were arbitrary, the inference from $\forall x\, P(x)$ to $P(t)$ preserves truth in every structure under every assignment: the rule is sound.