Substitution Instance of WFF is WFF

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathbf A$ be a WFF of predicate logic.

Let $\tau$ be a term of predicate logic.

Let $x \in \mathrm{VAR}$ be a variable.

Let $\mathbf A \left({x \gets \tau}\right)$ be the substitution instance of $\mathbf A$ substituting $\tau$ for $x$.


Then $\mathbf A \left({x \gets \tau}\right)$ is a WFF.


Proof

Proceed by the Principle of Structural Induction on the bottom-up specification of predicate logic, applied to $\mathbf A$.


If $\mathbf A = p \left({\tau_1, \ldots, \tau_n}\right)$, then:

$\mathbf A \left({x \gets \tau}\right) = p \left({\tau_1 \left({x \gets \tau}\right), \ldots, \tau_n \left({x \gets \tau}\right)}\right)$

where $\tau_i \left({x \gets \tau}\right)$ is the substitution instance of $\tau_i$.

By Substitution Instance of Term is Term, each such $\tau_i \left({x \gets \tau}\right)$ is again a term.

It follows that $\mathbf A \left({x \gets \tau}\right)$ is again a WFF.


If $\mathbf A = \neg \mathbf B$ and the induction hypothesis applies to $\mathbf B$, then:

$\mathbf A \left({x \gets \tau}\right) = \neg \mathbf B \left({x \gets \tau}\right)$

and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.


If $\mathbf A = \mathbf B \circ \mathbf B'$ for $\circ$ one of $\land, \lor, \implies, \iff$ and the induction hypothesis applies to $\mathbf B, \mathbf B'$:

$\mathbf A \left({x \gets \tau}\right) = \mathbf B \left({x \gets \tau}\right) \circ \mathbf B' \left({x \gets \tau}\right)$

and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.


If $\mathbf A = \exists x: \mathbf B$, and the induction hypothesis applies to $\mathbf B$:

$\mathbf A \left({x \gets \tau}\right) = \exists x: \mathbf B \left({x \gets \tau}\right)$

and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.


If $\mathbf A = \forall x : \mathbf B$, and the induction hypothesis applies to $\mathbf B$:

$\mathbf A \left({x \gets \tau}\right) = \forall x: \mathbf B \left({x \gets \tau}\right)$

and it follows from the induction hypothesis that $\mathbf A \left({x \gets \tau}\right)$ is a WFF of predicate logic.


The result follows by the Principle of Structural Induction.

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Substitution_Instance_of_WFF_is_WFF&oldid=265959"