Give a semantic proof of $\alpha(x/t)\rightarrow\exists x \alpha$.

Question

Give a semantic proof of the following conclusion:

$\alpha(x/t)\rightarrow\exists x \alpha$ is a tautology, where $t$ is free in $\alpha$ for $x$.

I've already proved it directly in $K_{\mathcal{L}}$ as follows, but I'm not familiar with the method of semantic proof.

Direct proof:

$\because (\neg\alpha)(x/t)=\neg(\alpha(x/t))$, then we have

$\vdash \forall x (\neg\alpha)\rightarrow(\neg\alpha)(x/t)\quad(K4)$

$\vdash \forall x (\neg\alpha)\rightarrow\neg(\alpha(x/t))$

$\vdash (\forall x (\neg\alpha)\rightarrow\neg(\alpha(x/t)))\rightarrow(\alpha(x/t)\rightarrow\neg\forall x(\neg \alpha))\quad(tautology)$

$\vdash\alpha(x/t)\rightarrow\neg\forall x(\neg \alpha)$

That is $\vdash\alpha(x/t)\rightarrow\exists x\alpha$

Answer 1

Semantic proofs are all about reasoning about models (and variable assignments). In particular, a formula $\varphi$ with free variables $z_1,...,z_n$ is a semantic tautology (usually the term "validity" is used here instead, but I think this is more understandable) iff for every structure $\mathcal{M}$ and every variable assignment $f:\{z_1,...,z_n\}\rightarrow M$ (where $M$ is the underlying set of $\mathcal{M}$) we have $$(\mathcal{M},f)\models\varphi$$ (remember that the definition of $\models$ is a recursive one, so we understand complicated $\varphi$s by breaking them down into simpler expressions). Also, a good rule of thumb is that it's generally easier to understand the special case with as few free variables as possible.

So suppose $t$ is a closed term (= no free variables) and $\alpha$ has only the variable $x$ free. We want to show that $$\alpha(x/t)\rightarrow\exists x\alpha$$ is a semantic validity. Since there are no free variables in that expression, that means that we want to show $$\mathcal{M}\models\alpha(x/t)\rightarrow\exists x\alpha$$ for every structure $\mathcal{M}$.

Looking at the $\rightarrow$-clause in the definition of $\models$, this means that we need to show the following:

For any structure $\mathcal{M}$, if $\mathcal{M}\models\alpha(x/t)$ then $\mathcal{M}\models\exists x\alpha$.

So suppose $\mathcal{M}\models\alpha(x/t)$. In $\mathcal{M}$, the closed term $t$ refers unambiguously (since it has no free variables) to some object $m\in M$. In particular, we get $$(\mathcal{M}, \{x\mapsto m\})\models\alpha.$$ And this immediately (looking at the $\exists$-clause in the definition of $\models$ this time) gives us $\mathcal{M}\models\exists x\alpha$ as desired.

(The same basic shape of argument will work even when more free variables are involved, but I think it will be easier to understand on its own.)