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.
New to topics? Read the docs here!