Tính đúng đắn của quy tắc thay thế phổ dụng

Ta lập luận trực tiếp từ ngữ nghĩa thỏa mãn Tarski, định nghĩa tính đúng trong một cấu trúc theo đệ quy trên cấu trúc công thức.

Theo mệnh đề ngữ nghĩa cho $\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)$. Giả sử giả thiết $\mathcal{M} \models_s \forall x\, P(x)$; theo mệnh đề này, $\mathcal{M} \models_{s[x \mapsto d]} P(x)$ đúng với mọi $d \in M$, không ngoại lệ.

Vì khẳng định đúng với mọi $d \in M$, nó đúng đặc biệt với $d = t^{\mathcal{M},s}$, phần tử mà hạng tử $t$ biểu thị trong $\mathcal{M}$ dưới $s$. Thay $d$ cụ thể này cho ta $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$.

Theo Bổ đề Thay thế (một kết quả chuẩn liên hệ phép gán biến với phép thay thế hạng tử, chứng minh được bằng quy nạp theo cấu trúc của $P$): $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x) \iff \mathcal{M} \models_s P(t)$, đúng chính xác vì $t$ thay thế được cho $x$ trong $P(x)$ (không biến tự do nào của $t$ bị buộc ngoài ý muốn). Áp dụng bổ đề biến $\mathcal{M} \models_{s[x \mapsto t^{\mathcal{M},s}]} P(x)$ thành $\mathcal{M} \models_s P(t)$.

Vì $\mathcal{M}$, $s$, $t$ tùy ý, nên suy luận từ $\forall x\, P(x)$ tới $P(t)$ bảo toàn tính đúng trong mọi cấu trúc dưới mọi phép gán: quy tắc là đúng đắn.