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 [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 12: | Line 12: | ||
Substitution is a maping formulas to formulas, | Substitution is a maping formulas to formulas, | ||
- | \[ | + | \begin{equation*} |
\sigma : D \to {\cal F} | \sigma : D \to {\cal F} | ||
- | \] | + | \end{equation*} |
where $D \subseteq {\cal F}$ is the domain of substitution, usually finite. We write it | 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\} | \sigma = \{F_1 \mapsto G_1,\ldots, F_n \mapsto G_n\} | ||
- | \] | + | \end{equation*} |
Let ${\cal S}$ be set of all substitutions. | Let ${\cal S}$ be set of all substitutions. | ||
Line 26: | Line 26: | ||
For $F \in {\cal F}$ we write $F \sigma$ instead of $subst(\sigma)(F)$, so | 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}) | 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. | //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\}$, | **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) = | 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)]) | e(F)(I[p_1 \mapsto e(F_1)(I),\ldots,p_n \mapsto e(F_n)(I)]) | ||
- | \] | + | \end{equation*} |
++++ | ++++ | ||