述語論理

$\forall x\, P(x)$ は「$x$ に何を代入しても $P$ が成り立つ」ことを意味する——だから特定の項 $t$ を代入しても $P(t)$ は成り立たなければならない。これは一般法則を具体的な事例に変える規則である。「$\forall x\, (\text{Human}(x) \to \text{Mortal}(x))$」から $t = \text{Socrates}$ で例化すると「$\text{Human}(\text{Socrates}) \to \text{Mortal}(\text{Socrates})$」が得られる。これは古典的三段論法の第一前提である。

構造における真理性を論理式の構造に関する帰納で定義するタルスキの充足意味論から直接論じる。

$\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)$。仮定 $\mathcal{M} \models_s \forall x\, P(x)$ を仮定する。この節により、$\mathcal{M} \models_{s[x \mapsto d]} P(x)$ がすべての $d \in M$ について例外なく成り立つ。

この主張はすべての $d \in M$ について成り立つので、特に $d = t^{\mathcal{M},s}$(項 $t$ が $s$ のもとで $\mathcal{M}$ において表す元)についても成り立つ。この特定の $d$ を代入すると $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$ が得られる。

代入補題(変数割り当てと項代入を結びつける標準的な結果で、$P$ の構造に関する帰納法で証明できる)により:$\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x) \iff \mathcal{M} \models_s P(t)$。これは $t$ が $P(x)$ の $x$ に代入可能である(すなわち $t$ の自由変数が意図せず束縛されない)ときに正確に成り立つ。この補題を適用すると $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$ は $\mathcal{M} \models_s P(t)$ になる。

$\mathcal{M}$、$s$、$t$ は任意だったので、$\forall x\, P(x)$ から $P(t)$ への推論はすべての構造・すべての付値において真理性を保存する。すなわちこの規則は健全である。

$\exists y\, \forall x\, R(x,y)$ はすべての $x$ に対して通用する単一の証拠 $y$(「固定された」証拠)を要求するのに対し、$\forall x\, \exists y\, R(x,y)$ は各 $x$ に対して何らかの証拠があればよく、$x$ ごとに異なっていてもよい(「動く」証拠)。固定された証拠は自動的に動く証拠にもなる(そのまま使い回せる)が、逆は成り立たない——これはまさに「みんなを愛する人がいる」(一人の普遍的な恋人)と「みんな誰かに愛されている」(相手は人によって違うかもしれない)の違いであり、述語論理が明確化する自然言語の古典的な曖昧さの一例である。

順方向。 $\mathcal{M} \models_s \exists y\, \forall x\, R(x,y)$ を仮定する。$\exists$ に対する意味論的節により、$\mathcal{M} \models_s \exists y\, \varphi \iff \text{there is } d \in M \text{ with } \mathcal{M} \models_{s[y \mapsto d]} \varphi$。これをここに適用すると、ある $d_0 \in M$ が存在して $\mathcal{M} \models_{s[y \mapsto d_0]} \forall x\, R(x,y)$。

これに $\forall$ に対する節を適用すると、$\mathcal{M} \models_{s[y \mapsto d_0][x \mapsto a]} R(x,y)$ がすべての $a \in M$ について成り立つ。なぜなら $\forall x$ は後でどの $a$ を選ぼうと $M$ 全体にわたるからである。

ここで $\forall x\, \exists y\, R(x,y)$ を確認するため任意の $a \in M$ を固定する。前段落から $x \mapsto a$ を取ると $\mathcal{M} \models_{s[y \mapsto d_0][x \mapsto a]} R(x,y)$ が得られ、これは $x \mapsto a$ のもとで $\exists y\, R(x,y)$ に対する証拠として $d_0$ 自身を示している。したがって $\mathcal{M} \models_{s[x \mapsto a]} \exists y\, R(x,y)$。

$a \in M$ は任意だったので、$\mathcal{M} \models_{s[x \mapsto a]} \exists y\, R(x,y)$ はすべての $a$ について成り立ち、これはまさに $\mathcal{M} \models_s \forall x\, \exists y\, R(x,y)$ の意味論的節である。これで $\exists y\, \forall x\, R(x,y) \Rightarrow \forall x\, \exists y\, R(x,y)$ が証明された。

逆は成り立たない:反例。 $\mathcal{M}$ の領域を $M = \mathbb{Z}$(整数)とし、$R(x,y)$ を「$x < y$」と解釈する。このとき $\forall x\, \exists y\, R(x,y)$ は真である:任意の整数 $x$ に対して $y = x+1$ を取れば $x < y$。しかし $\exists y\, \forall x\, R(x,y)$ は偽である:これはすべての整数 $x$ より大きい単一の整数 $y$ を要求するが、そのような最大の整数は存在しない(どの候補 $y$ についても、整数 $y+1$ は $y+1 < y$ に違反する)。よって $\forall x\, \exists y\, R(x,y)$ は成り立つが $\exists y\, \forall x\, R(x,y)$ は成り立たず、逆の含意が一般には偽であることが示された。