Differences
This shows you the differences between two versions of the page.
sav08:substitution_theorems_for_propositional_logic [2008/03/11 16:11] vkuncak |
sav08:substitution_theorems_for_propositional_logic [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Substitution Theorems for Propositional Logic ====== | ||
- | |||
- | Relate syntax and semantics. | ||
- | |||
- | 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, | ||
- | \[ | ||
- | \sigma : D \to {\cal F} | ||
- | \] | ||
- | where $D \subseteq {\cal F}$ is the domain of substitution, usually finite. We write it | ||
- | \[ | ||
- | \sigma = \{F_1 \mapsto G_1,\ldots, F_n \mapsto G_n\} | ||
- | \] | ||
- | Let ${\cal S}$ be set of all substitutions. | ||
- | |||
- | Substitution operator //subst// takes such a map and a formula and returns a new formula. | ||
- | |||
- | Recursive definition of //subst//: | ||
- | |||
- | For $F \in {\cal F}$ we write $F \sigma$ instead of $subst(\sigma)(F)$, so | ||
- | \[ | ||
- | subst : {\cal S} \to ({\cal F} \to {\cal F}) | ||
- | \] | ||
- | |||
- | //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\}$, | ||
- | \[ | ||
- | e(subst(\{p_1 \mapsto F_1,\ldots,p_n \mapsto F_n\})(F))(I) = | ||
- | \] | ||
- | ++++| | ||
- | \[ | ||
- | e(F)(I[p_1 \mapsto e(F_1)(I),\ldots,p_n \mapsto e(F_n)(I)]) | ||
- | \] | ||
- | ++++ | ||
- | |||
- | 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)$. | ||
- | |||
- | 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))$. | ||
- | |||
- | Does the theorem hold if $\sigma$ is ++not a variable substitution?|No, because a general substitution could produce an arbitrary formula.++ | ||
- | |||
- | 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))$. | ||