Universal Instantiation/Model

From ProofWiki
Jump to navigation Jump to search


Let $\map {\mathbf A} x$ be a WFF of predicate logic.

Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.

Then $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$ is a tautology.


Let $\AA$ be a structure on a set $A$, and let $\sigma$ be an assignment for $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$.


$a_\tau := \mathop {\map {\operatorname{val}_\AA} \tau} \sqbrk \sigma$

the value of $\tau$ under $\sigma$.

From the definition of value under $\sigma$:

$\map {\mathrm {val}_\AA} {\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau} \sqbrk \sigma = \map {f^\to} {\map {\mathrm {val}_\AA} {\forall x: \map {\mathbf A} x} \sqbrk \sigma, \map {\mathrm {val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma}$

where $f^\to$ is the truth function of $\implies$.

We thus need to ascertain that if:

$\map {\mathrm {val}_\AA} {\forall x: \map {\mathbf A} x} \sqbrk \sigma = T$

then also:

$\map {\mathrm {val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma = T$

By definition of value under $\sigma$, the former amounts to:

$\map {\mathrm {val}_\AA} {\map {\mathbf A} x} \sqbrk {\sigma + \paren {x / a} } = T$

for all $a \in A$.

By the Substitution Theorem for Well-Formed Formulas:

$\map {\mathrm {val}_\AA} {\map {\mathbf A} \tau} \sqbrk \sigma = \map {\mathrm {val}_\AA} {\mathbf A} \sqbrk {\sigma + \paren {x / a_\tau} }$

Since $a_\tau \in A$, the conclusion follows, and $\forall x: \map {\mathbf A} x \implies \map {\mathbf A} \tau$ is a tautology.