 Syntax tree of a formula

The syntax tree of a logical formula records its recursive construction. A propositional variable is a leaf, negation has one child, and binary implication has an ordered pair of children. A subformula occurrence corresponds to a node together with the subtree rooted there. Different occurrences may have identical formula strings.