Differences

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

--- sav08:substitution_theorems_for_propositional_logic [2008/03/10 19:35]
vkuncak
+++ sav08:substitution_theorems_for_propositional_logic [2008/03/11 16:09]
vkuncak
@@ 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 =====
@@ Line 38: / Line 42: @@
 ++++
-Corollary: if $\models F$, then $\models (subst(\sigma)(F))$ for every substitution $\sigma$.
+Corollary: if $\models F$, then $\models (subst(\sigma)(F))$ for every variable substitution $\sigma$.
-Corrollary: if $I_1(p) = I_2(p)$ for every $p \in FV(F)$, then $e(F)(I_1)=e(F)(I_2)$.
+Corollary: if $\models (F \leftrightarrow G)$ and $\sigma$ is a variable substitution, then $\models (subst(\sigma)(F) \leftrightarrow subst(\sigma)(G)$.
+Does the theorem hold if $\sigma$ is ++not a variable substitution?|No, because a general substitution could produce an arbitrary formula.++
 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)$.
-**Theorem on instantiating equivalences**: if $\models (F \leftrightarrow G)$ and $\sigma$ is a variable substitution, then
-\[
-    \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.
 We next justify transforming formulas from inside.
 We say that $\sigma = \{F_1 \mapsto G_1,\ldots,F_n \mapsto G_n\}$ is //equivalence-preserving// iff for all $i$ where $1 \le i \le n$ we have $\models (F_i \leftrightarrow G_i)$.
-**Theorem on Substituting Equivalent Subformulas**: if $\sigma$ is equivalence-preserving, then for every formula $F$ we have $\models (F \leftrightarrow (subst(\sigma)(F))$.
+**Lemma**: If $\models (F \leftrightarrow G)$ then for every interpretation $I$ we have $e(F)(I) = e(G)(I)$.
+**Theorem on Substituting Equivalent Subformulas**: if $\sigma$ is equivalence-preserving, then for every formula $F$ we have $\models (F \leftrightarrow (subst(\sigma)(F))$.