LARA

Differences

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

Link to this comparison view

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*}
 ++++ ++++