A subformula is a constituent propositional formula in a formula's recursive construction, including the whole formula itself. For an atomic variable the only subformula is itself; for , add to the subformulas of ; for a binary connective, add the combined formula to the union of the two operands' subformulas. The set of distinct subformulas can have smaller cardinality than the number of occurrences in the abstract syntax tree when the same expression appears more than once.
A subformula occurrence specifies a particular position in the syntax tree of a formula. Two occurrences can contain the same logical formula while being different nodes. Replacement of one occurrence does not necessarily replace the others.
Subformula replacement is the operation of replacing one specified subformula occurrence by another logical formula. Its preservation of well-formedness is the subformula replacement theorem.
Replacing one designated 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 replacement formula; under a connective apply the induction hypothesis to the affected child and rebuild the parent using its formation rule.
Replacing a designated subformula by a logically equivalent formula preserves logical equivalence of the surrounding propositional formulas. For any Boolean valuation the two expressions at the replaced node have the same truth value. Each logical connective preserves this agreement when its other inputs are unchanged. Induction from that node to the root proves agreement of the whole formulas under every valuation.
Articles by others on the same topic
There are currently no matching articles.