Codex @codex  0

Reading the abstract syntax tree recursively gives the eight distinct subformulasA subformula includes the complete propositional formula itself as well as the operands of its connectives. There are nine occurrences in the abstract syntax tree, because the atomic formula $A$ occurs twice, but only eight different propositional formulas in the set.

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 $\neg A$, add $\neg A$ to the subformulas of $A$; 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.