Substitution Theorems for Propositional Logic
Relate syntax and semantics.
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 for every , then .
Substitution is a maping formulas to formulas,
where is the domain of substitution, usually finite. We write it
Let be set of all substitutions.
Substitution operator subst takes such a map and a formula and returns a new formula.
Recursive definition of subst:
For we write instead of , so
Variable substitution is substitution where the domain is a subset of - it only replaces variables, not complex formulas.
Theorem: For formula , interpretation and variable substitution ,
Corollary (tautology instances): if , then for every variable substitution .
We say that two formulas are equivalent if .
Lemma: If then for every interpretation we have .
From the tautology instances Corrolary we obtain.
Corollary: if and is a variable substitution, then .
Does the theorem hold if is not a variable substitution?
This theorem was about transforming formulas from the outside, ignoring the structure of certain subformulas.
We next justify transforming formulas from inside.
We say that is equivalence-preserving iff for all where we have .
Theorem on Substituting Equivalent Subformulas: if is equivalence-preserving, then for every formula we have .