Differences

This shows you the differences between two versions of the page.

--- sav08:substitution_theorems_for_propositional_logic [2008/03/06 13:26]
vkuncak
+++ sav08:substitution_theorems_for_propositional_logic [2015/04/21 17:30] (current)
@@ Line 4: / Line 4: @@
 Called metatheorems, because they are not formulas //within// the logic, but formulas //about// the logic.
+From semantics we can prove the following lemma by induction.
+Lemma: if $I_1(p) = I_2(p)$ for every $p \in FV(F)$, then $e(F)(I_1)=e(F)(I_2)$.
 ===== Substitutions =====
 Substitution is a maping formulas to formulas,
-\[
+\begin{equation*}
    \sigma : D \to {\cal F}
-\]
+\end{equation*}
 where $D \subseteq {\cal F}$ is the domain of substitution, usually finite.  We write it
-\[
+\begin{equation*}
    \sigma = \{F_1 \mapsto G_1,\ldots, F_n \mapsto G_n\}
-\]
+\end{equation*}
 Let ${\cal S}$ be set of all substitutions.
@@ Line 22: / Line 26: @@
 For $F \in {\cal F}$ we write $F \sigma$ instead of $subst(\sigma)(F)$, so
-\[
+\begin{equation*}
    subst : {\cal S} \to ({\cal F} \to {\cal F})
-\]
+\end{equation*}
 //Variable substitution// is substitution where the domain is a subset of $V$ - it only replaces variables, not complex formulas.
 **Theorem:** For formula $F$, interpretation $I$ and variable substitution $\sigma = \{p_1 \mapsto F_1,\ldots,p_n \mapsto F_n\}$,
-\[
+\begin{equation*}
    e(subst(\{p_1 \mapsto F_1,\ldots,p_n \mapsto F_n\})(F))(I) =
-\]
+\end{equation*}
 ++++|
-\[
+\begin{equation*}
    e(F)(I[p_1 \mapsto e(F_1)(I),\ldots,p_n \mapsto e(F_n)(I)])
-\]
+\end{equation*}
 ++++
-Corollary: if $\models F$, then $\models (subst(\sigma)(F))$ for every substitution $\sigma$.
+**Corollary (tautology instances):** if $\models F$, then $\models (subst(\sigma)(F))$ for every variable substitution $\sigma$.
 We say that two formulas are equivalent if $\models (F \leftrightarrow G)$.
-**Lemma**: If $\models (F \leftrightarrow G)$ then for every interpretation $I$ we have $e(F)(I) = e(G)(I)$.
+**Lemma:** If $\models (F \leftrightarrow G)$ then for every interpretation $I$ we have $e(F)(I) = e(G)(I)$.
+From the tautology instances Corrolary we obtain.
+**Corollary:** if $\models (F \leftrightarrow G)$ and $\sigma$ is a variable substitution, then $\models (subst(\sigma)(F) \leftrightarrow subst(\sigma)(G))$.
-**Theorem on instantiating equivalences**: if $\models (F \leftrightarrow G)$ and $\sigma$ is a variable substitution, then
+Does the theorem hold if $\sigma$ is ++not a variable substitution?|No, because a general substitution could produce an arbitrary formula.++
-\[
-    \models (subst(\sigma)(F) \leftrightarrow subst(\sigma)(G)
-\]
-Does the theorem hold if $\sigma$ is not variable substitution?
 This theorem was about transforming formulas from the outside, ignoring the structure of certain subformulas.