Substitution for Equivalent Subformula is Equivalent

From ProofWiki
Jump to navigation Jump to search


It has been suggested that this page be renamed.
In particular: Couldn't think of anything better
To discuss this page in more detail, feel free to use the talk page.


Theorem

Let $\mathbf B$ a WFF of propositional logic.

Let $\mathbf A, \mathbf A'$ be equivalent WFFs.

Let $\mathbf A$ be a subformula of $\mathbf B$.

Let $\mathbf B' = \map {\mathbf B} {\mathbf A \,//\, \mathbf A'}$ be the substitution of $\mathbf A'$ for $\mathbf A$ in $\mathbf B$.


Then $\mathbf B$ and $\mathbf B'$ are equivalent.


Proof

Let $v$ be an arbitrary boolean interpretation.

Then $\map v {\mathbf A} = \map v {\mathbf A'}$.


It is to be shown that $\map v {\mathbf B} = \map v {\mathbf B'}$.

We proceed by induction.

Let $\map n {\mathbf B}$ be the number of WFFs $\mathbf C$ such that:

$\mathbf A$ is a subformula of $\mathbf C$, and $\mathbf C$ is a subformula of $\mathbf B$.

Note that $\map n {\mathbf B} \ne 0$, for $\mathbf C = \mathbf A$ is a valid choice.


Suppose now that $\map n {\mathbf B} = 1$.

Because we have the valid choices $\mathbf C = \mathbf A$ and $\mathbf C = \mathbf B$, it follows that these choices must be identical, i.e. $\mathbf A = \mathbf B$.

Hence $\mathbf B' = \mathbf A'$, and so:

$\map v {\mathbf B} = \map v {\mathbf B'}$


Suppose now that the assertion is true for all $\mathbf B$ with $\map n {\mathbf B} \le n$.

Let $\map n {\mathbf B} = n + 1$.


Suppose $\mathbf B = \neg \mathbf B_1$.

Then obviously $\map n {\mathbf B_1} = n$, so by hypothesis:

$\map v {\mathbf B_1} = \map v {\map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} }$

Also, by definition of substitution:

$\mathbf B' = \neg \map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'}$

Now, by definition of boolean interpretation:

\(\ds \map v {\mathbf B}\) \(=\) \(\ds \map {f^\neg} {\map v {\mathbf B_1} }\)
\(\ds \) \(=\) \(\ds \map {f^\neg} {\map v {\map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} } }\)
\(\ds \) \(=\) \(\ds \map v {\neg \map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} }\)
\(\ds \) \(=\) \(\ds \map v {\mathbf B'}\)


Suppose now that $\mathbf B = \mathbf B_1 \mathbin{\mathsf B} \mathbf B_2$ for a binary connective $\mathsf B$.

Then $\map n {\mathbf B_1}, \map n {\mathbf B_2} \le n$, so:

$\map v {\mathbf B_1} = \map v {\map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} }$
$\map v {\mathbf B_2} = \map v {\map {\mathbf B_2} {\mathbf A \,//\, \mathbf A'} }$

This follows by either the induction hypothesis, or when $\mathbf A$ is not a subformula of $\mathbf B_1$ or $\mathbf B_2$, is entirely trivial, considering the substitution does not change anything.

Also, by definition of substitution:

$\mathbf B' = \map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} \mathbin {\mathsf B} \map {\mathbf B_2} {\mathbf A \,//\, \mathbf A'}$


Now, by definition of boolean interpretation:

\(\ds \map v {\mathbf B}\) \(=\) \(\ds \map {f^{\mathsf B} } {\map v {\mathbf B_1}, \map v {\mathbf B_2} }\)
\(\ds \) \(=\) \(\ds \map {f^{\mathsf B} } {\map v {\map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} }, \map v {\map {\mathbf B_2} {\mathbf A \,//\, \mathbf A'} } }\)
\(\ds \) \(=\) \(\ds \map v {\map {\mathbf B_1} {\mathbf A \,//\, \mathbf A'} \mathbin {\mathsf B} \map {\mathbf B_2} {\mathbf A \,//\, \mathbf A'} }\)
\(\ds \) \(=\) \(\ds \map v {\mathbf B'}\)


By definition of the language of propositional logic, $\mathbf B$ must have either of the above forms.

Hence the result, from the Second Principle of Mathematical Induction.

$\blacksquare$


Sources

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