Introduction and elimination of quantifiers

要证明之前用的逻辑推理规则是合理的。

Theorem 1.

$$\phi[x\mapsto t]\models\exists x\phi$$

where $\phi [ x\mapsto t]$ means substituting every free occurrence $of$ $x$ in $\phi$ with $t$.

Example2.
Theorem1 的例子：

$$P(c)\vDash\exists x(P(x))$$

考虑一个更复杂一点的例子：

$$P(c)\wedge Q(g(c),c)\models\exists x(P(x)\wedge Q(g(x),c))$$

In order to prove theorem 1, we need to use the following property.
因为 Theorem1 引入了一个新的符号 $\phi[x \mapsto t]$，这个符号表示在语法上把 $\phi$ 中的 $x$ 替换成 $t$。（不包括 $\forall x, \exists x$ 包括到的这些 $x$）

Claim 3.

$$\llbracket \phi[x \mapsto t] \rrbracket_{\mathcal{J}} = \llbracket \phi \rrbracket_{\mathcal{J}[x \mapsto \llbracket t \rrbracket_{\mathcal{J}}]}$$

Claim3 可能有点复杂，再举两个例子：

Example 4.

• Let $\phi = P(x)$ and $t=c$. Then, $\llbracket P(c) \rrbracket_{\mathcal{J}} = \llbracket P(x) \rrbracket_{\mathcal{J}[x \mapsto \mathcal{J}(c)]}$
• Let $\phi = P(x)$ and $t=f(y,c)$. Then, $\llbracket P(f(y,c)) \rrbracket_{\mathcal{J}} = \llbracket P(x) \rrbracket_{\mathcal{J}[x \mapsto \llbracket f(y,c) \rrbracket_{\mathcal{J}}]}$.

上面的 Claim3 直接作为结论来用，不做证明。然后使用 Claim3 来证明 Theorem1：
Proof
For any $\mathcal{J}$, if $\llbracket \phi \mapsto t \rrbracket_{\mathcal{J}} = T$, then $\llbracket \phi \rrbracket_{\mathcal{J}[x\mapsto \llbracket t \rrbracket_{\mathcal{J}}]} = T$, so $\llbracket \exists x\phi \rrbracket_{\mathcal{J}} = T$.
Qed.

再考虑一个类似的结论，同样可以用 Claim3 证明。
Theorem 5.

$$\forall x \phi \models \phi[x\mapsto t]$$

Proof
If $\mathcal{J}$ is an interpretation, $\llbracket \forall x\phi \rrbracket_{\mathcal{J}} = T$, then for any $a$ in $\mathcal{J}$'s domain, $\llbracket \phi \rrbracket_{x\mapsto a} = T$.
$\llbracket \phi[x\mapsto t] \rrbracket_{\mathcal{J}} = \llbracket \phi \rrbracket_{\mathcal{J}\left[x\mapsto \llbracket t \rrbracket_{\mathcal{J}} \right]} = T$.
Qed.

在之前的逻辑推理中，用过这样的结论：
If $\Phi, \psi \vdash \chi$ and $x$ not mentioned in $\Phi$, then $\Phi \vdash \forall x(\psi \to \chi)$.
上述结论可以抽象为如下结论

Theorem 7.

• If $\Phi \models \psi$ and $x$ does not freely occur in $\Phi$, then $\Phi \models \forall x \psi$

Remark: “does not freely occur” is very important.

举个例子：
$\Phi = \{ P(x) \}, \psi = P(x)$，那么有 $\Phi \models \psi$，但是 $\Phi \not \models \forall x \psi$。

想要证明 Theorem7，需要引入以下 Claim

Claim9
If $\Phi$ does not mention $x$

$$\llbracket \phi \rrbracket_{\mathcal{J}} = \llbracket \phi \rrbracket_{\mathcal{J}[x\mapsto a]}$$

接下来用 Claim9 证明 Theorem7
Proof
For any $\mathcal{J}$ s.t. for any $\phi \in \Phi, \llbracket \phi \rrbracket_{\mathcal{J}} = T$.
For any $a$ in $\mathcal{J}'s$ domain, and any $\phi \in \Phi$, $\llbracket \phi \rrbracket_{\mathcal{J}[x\mapsto a]} = \llbracket \phi \rrbracket_{\mathcal{J}} = T$
So $\llbracket \psi \rrbracket_{\mathcal{J}[x\mapsto a]} = T$ ($\Phi \models \psi$), $\llbracket \forall x \psi \rrbracket_{\mathcal{J}} = T$
Qed.

Theorem7
Theorem7 还有一个对称的说法

• If $\Phi, \psi \models \chi$, and $x$ is not mentioned in $\Phi$ and $\chi$, then $\Phi, \exists x \psi \models \chi$

Proof
Suppose $\mathcal{J}$ is an interpretation s.t. (1) For any $\phi \in \Phi$, $\llbracket \phi \rrbracket_{\mathcal{J}} = T$; (2) $\llbracket \exists x \psi \rrbracket_{\mathcal{J}} = T$
So there exists $a$ s.t. $\llbracket \psi \rrbracket_{\mathcal{J}[x\mapsto a]}$
For any $\phi \in \Phi$, $\llbracket \phi \rrbracket_{\mathcal{J}[x\mapsto a]} = \llbracket \phi \rrbracket_{\mathcal{J}} = T$
Thus $\llbracket \chi \rrbracket_{\mathcal{J}[x\mapsto a]} = T$ (because $\Phi, \psi \models \chi$)
$\llbracket \chi \rrbracket_{\mathcal{J}} = \llbracket \chi \rrbracket_{\mathcal{J}[x\mapsto a]} = T$.