Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next 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*}
 ++++ ++++
  
-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