Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:substitution_theorems_for_propositional_logic [2008/03/11 16:11] vkuncak |
sav08:substitution_theorems_for_propositional_logic [2008/03/11 16:11] vkuncak |
||
|---|---|---|---|
| Line 42: | Line 42: | ||
| ++++ | ++++ | ||
| - | Corollary (tautology instances): if $\models F$, then $\models (subst(\sigma)(F))$ for every variable 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)$. | 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. | 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))$. | + | **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.++ | Does the theorem hold if $\sigma$ is ++not a variable substitution?|No, because a general substitution could produce an arbitrary formula.++ | ||