代入

说明

⚠ 捕获是什么样：取 $\varphi = \exists y\, (y > x)$、$t = y$。直接代入得 $\exists y\, (y > y)$ —— 语义完全变了（原来「存在比 $x$ 大的数」，现在成了假命题）。这时要说「$t$ 对 $\varphi$ 中的 $x$ 不可代入」。

⭐ 代入在图上不是花边：替换公理模式的整个内容就是「用一个公式 $\varphi (x, y, p)$ 把 $A$ 中每个 $x$ 的像收集起来」，那里做的正是代入。

⚠ 避免捕获的标准做法是先把冲突的约束变元改名（$\alpha$-换名），再代入。这是逻辑教科书写起来最啰嗦、却绕不过去的一步。