• English only

# 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] (current) Both sides previous revision Previous revision 2008/03/11 16:11 vkuncak 2008/03/11 16:11 vkuncak 2008/03/11 16:09 vkuncak 2008/03/11 14:57 vkuncak 2008/03/10 19:35 vkuncak 2008/03/06 13:26 vkuncak 2008/03/06 11:19 vkuncak 2008/03/06 11:18 vkuncak 2008/03/06 11:18 vkuncak 2008/03/06 11:05 vkuncak 2008/03/06 11:05 vkuncak 2008/03/06 10:59 vkuncak 2008/03/05 21:08 vkuncak 2008/03/05 21:08 vkuncak 2008/03/05 20:47 vkuncak created Next revision Previous revision 2008/03/11 16:11 vkuncak 2008/03/11 16:11 vkuncak 2008/03/11 16:09 vkuncak 2008/03/11 14:57 vkuncak 2008/03/10 19:35 vkuncak 2008/03/06 13:26 vkuncak 2008/03/06 11:19 vkuncak 2008/03/06 11:18 vkuncak 2008/03/06 11:18 vkuncak 2008/03/06 11:05 vkuncak 2008/03/06 11:05 vkuncak 2008/03/06 10:59 vkuncak 2008/03/05 21:08 vkuncak 2008/03/05 21:08 vkuncak 2008/03/05 20:47 vkuncak created 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*} ++++ ++++ - 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.++

sav08/substitution_theorems_for_propositional_logic.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice