[proofplan] The proof is semantic. Given an assignment $s$, the term $t$ denotes an element of the structure; this element will be the witness for the existential quantifier. The only point requiring care is that $A[t/x]$ must really express the formula $A$ evaluated after assigning $x$ the value of $t$, and this is exactly what the capture-free substitution condition guarantees. [/proofplan]

[step:Use the denotation of the substituted term as the witness]Let $\mathcal{L}$ be a first-order language, let $\operatorname{Var}$ denote the set of variables of $\mathcal{L}$, let $x\in\operatorname{Var}$, let $A$ be an $\mathcal{L}$-formula, and let $t$ be an $\mathcal{L}$-term that is free for $x$ in $A$ in the sense of [capture-free substitution](/page/Capture-Free%20Substitution). Let $\mathcal{M}$ be an $\mathcal{L}$-[structure](/page/Structure) with universe $M$, and let $s:\operatorname{Var}\to M$ be a variable assignment. Define the element \begin{align*} a := \llbracket t \rrbracket_{\mathcal{M},s} \in M, \end{align*} where $\llbracket t \rrbracket_{\mathcal{M},s}$ denotes the [term denotation](/page/Term%20Denotation) of $t$ in $\mathcal{M}$ under the assignment $s$. Assume, in the [satisfaction relation](/page/Satisfaction), that \begin{align*} \mathcal{M},s\models A[t/x]. \end{align*} The [Substitution Lemma for Capture-Free Substitution](/page/Substitution%20Lemma) states that if $t$ is free for $x$ in $A$, then for every $\mathcal{L}$-structure $\mathcal{N}$, every variable assignment $r:\operatorname{Var}\to N$ into the universe $N$ of $\mathcal{N}$, and the element $c:=\llbracket t\rrbracket_{\mathcal{N},r}\in N$, one has \begin{align*} \mathcal{N},r\models A[t/x] \quad\Longleftrightarrow\quad \mathcal{N},r[x:=c]\models A. \end{align*} Its hypotheses are satisfied here because $t$ is free for $x$ in $A$ by assumption. Applying the lemma with $\mathcal{N}=\mathcal{M}$, $r=s$, and $c=a$ gives \begin{align*} \mathcal{M},s\models A[t/x] \quad\Longleftrightarrow\quad \mathcal{M},s[x:=a]\models A, \end{align*} where $s[x:=a]:\operatorname{Var}\to M$ is the assignment defined by \begin{align*} s[x:=a](y)= \begin{cases} a, & y=x,\\ s(y), & y\ne x. \end{cases} \end{align*} Hence \begin{align*} \mathcal{M},s[x:=a]\models A. \end{align*} By the [semantics of the existential quantifier](/page/Existential%20Quantifier), \begin{align*} \mathcal{M},s\models \exists x\,A \end{align*} holds exactly when there exists some $b\in M$ such that \begin{align*} \mathcal{M},s[x:=b]\models A. \end{align*} Taking $b=a$ gives the required witness. Therefore \begin{align*} \mathcal{M},s\models \exists x\,A. \end{align*} This proves the semantic soundness of the existential introduction rule.[/step]

[guided]Let $\mathcal{L}$ be a first-order language, let $\operatorname{Var}$ denote the set of variables of $\mathcal{L}$, let $x\in\operatorname{Var}$, let $A$ be an $\mathcal{L}$-formula, and let $t$ be an $\mathcal{L}$-term that is free for $x$ in $A$ in the sense of [capture-free substitution](/page/Capture-Free%20Substitution). Let $\mathcal{M}$ be an $\mathcal{L}$-[structure](/page/Structure) with universe $M$, and let $s:\operatorname{Var}\to M$ be a variable assignment. The premise says, in the [satisfaction relation](/page/Satisfaction), that the substituted formula $A[t/x]$ is true under $s$: \begin{align*} \mathcal{M},s\models A[t/x]. \end{align*} The existential conclusion requires a witness for $x$. The natural witness is the object denoted by the term $t$ under the current assignment. Define \begin{align*} a := \llbracket t \rrbracket_{\mathcal{M},s}\in M, \end{align*} where $\llbracket t \rrbracket_{\mathcal{M},s}$ is the [term denotation](/page/Term%20Denotation) of $t$ in $\mathcal{M}$ under $s$. Now define the modified assignment $s[x:=a]:\operatorname{Var}\to M$ by \begin{align*} s[x:=a](y)= \begin{cases} a, & y=x,\\ s(y), & y\ne x. \end{cases} \end{align*} The capture-free substitution hypothesis is used here. The [Substitution Lemma for Capture-Free Substitution](/page/Substitution%20Lemma) states that if $t$ is free for $x$ in $A$, then for every $\mathcal{L}$-structure $\mathcal{N}$, every variable assignment $r:\operatorname{Var}\to N$ into the universe $N$ of $\mathcal{N}$, and the element $c:=\llbracket t\rrbracket_{\mathcal{N},r}\in N$, one has \begin{align*} \mathcal{N},r\models A[t/x] \quad\Longleftrightarrow\quad \mathcal{N},r[x:=c]\models A. \end{align*} We may apply this lemma because $t$ is free for $x$ in $A$ by assumption: replacing free occurrences of $x$ by $t$ does not cause any variable of $t$ to become bound inside $A$. Applying the lemma with $\mathcal{N}=\mathcal{M}$, $r=s$, and $c=a$ gives \begin{align*} \mathcal{M},s\models A[t/x] \quad\Longleftrightarrow\quad \mathcal{M},s[x:=a]\models A. \end{align*} Since the left-hand side holds by hypothesis, we obtain \begin{align*} \mathcal{M},s[x:=a]\models A. \end{align*} Finally, by the [semantics of the existential quantifier](/page/Existential%20Quantifier), \begin{align*} \mathcal{M},s\models \exists x\,A \end{align*} means that there exists an element $b\in M$ such that \begin{align*} \mathcal{M},s[x:=b]\models A. \end{align*} The element $a=\llbracket t \rrbracket_{\mathcal{M},s}$ is such an element. Hence \begin{align*} \mathcal{M},s\models \exists x\,A. \end{align*} This establishes the soundness of the rule.[/guided]