= Subformula replacement theorem
Replacing one designated <subformula>[subformula occurrence] in a <propositional formula> by another <propositional formula> preserves well-formedness. Induct on the context surrounding the occurrence: at the root the result is the <subformula replacement theorem>[replacement] <logical formula>[formula]; under a <logical connective>[connective] apply the induction hypothesis to the affected child and rebuild the parent using its <formal grammar>[formation rule].
Back to article page
