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 Both sides next revision
sav08:substitution_theorems_for_propositional_logic [2008/03/11 14:57]
vkuncak 		sav08:substitution_theorems_for_propositional_logic [2008/03/11 16:09]
vkuncak
Line 4: Line 4:
  
 Called metatheorems,​ because they are not formulas //within// the logic, but formulas //about// the logic. Called metatheorems,​ because they are not formulas //within// the logic, but formulas //about// the logic.
 +
 +From semantics we can prove the following lemma by induction.
 +
 +Lemma: if $I_1(p) = I_2(p)$ for every $p \in FV(F)$, then $e(F)(I_1)=e(F)(I_2)$.
  
 ===== Substitutions ===== ===== Substitutions =====
Line 37: Line 41:
 \] \]
 ++++ ++++
- 
-Corrollary: if $I_1(p) = I_2(p)$ for every $p \in FV(F)$, then $e(F)(I_1)=e(F)(I_2)$. 
  
 Corollary: if $\models F$, then $\models (subst(\sigma)(F))$ for every variable substitution $\sigma$. Corollary: 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 +Corollary: if $\models (F \leftrightarrow G)$ and $\sigma$ is a variable substitution,​ then $\models (subst(\sigma)(F) \leftrightarrow subst(\sigma)(G)$.
-\[ +
-    ​\models (subst(\sigma)(F) \leftrightarrow subst(\sigma)(G) +
-\]+
  
-++Does the theorem hold if $\sigma$ is not variable substitution?​|No.+++Does the theorem hold if $\sigma$ is ++not a variable substitution?​|No, because a general substitution could produce an arbitrary formula.++
  
 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)$. 
- 
  
 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)$.
  
-**Theorem on Substituting Equivalent Subformulas**: if $\sigma$ is equivalence-preserving, ​then for every formula ​$F$ we have $\models ​(F \leftrightarrow (subst(\sigma)(F))$.+**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))$.