Fix any Boolean valuation . Logical equivalence of and means for this Boolean valuation and every other one. Follow the unique path from the replaced node to the root of the formula syntax tree. At a negation node, equal input truth values have equal negations. At a logical implication node, the unaffected child has the same truth value before and after subformula replacement, while the affected child has the same truth value by induction; the resulting logical implications therefore agree as well.
Induction along that finite path yields . Since was arbitrary,This is the replacement theorem for logical equivalence: the semantics of each logical connective depends only on the truth values of its immediate inputs.
Articles by others on the same topic
There are currently no matching articles.