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:09]
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: 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$.
  
-Corollary: ​if $\models (F \leftrightarrow ​G)$ and $\sigma$ is a variable substitution,​ then $\models (subst(\sigma)(F) \leftrightarrow subst(\sigma)(G)$.+We say that two formulas are equivalent ​if $\models (F \leftrightarrow G)$.
  
-Does the theorem hold if $\sigmais ++not a variable substitution?​|No,​ because a general substitution could produce an arbitrary formula.+++**Lemma:** If $\models (F \leftrightarrow G)$ then for every interpretation $I$ we have $e(F)(I) = e(G)(I)$.
  
-We say that two formulas are equivalent ​if $\models (F \leftrightarrow G)$.+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. This theorem was about transforming formulas from the outside, ignoring the structure of certain subformulas.
  
 We next justify transforming formulas from inside. 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)$. 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)$.
- 
-**Lemma**: If $\models (F \leftrightarrow G)$ then for every interpretation $I$ we have $e(F)(I) = e(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))$. **Theorem on Substituting Equivalent Subformulas**:​ if $\sigma$ is equivalence-preserving,​ then for every formula $F$ we have $\models (F \leftrightarrow (subst(\sigma)(F))$.