Subformula

Subformula is a formula that occurs within another formula as part of its syntactic structure. In a formal language of logic, a subformula of a formula φ is any formula that appears in φ, including φ itself. The concept is used to analyze the complexity of formulas and to study properties of proofs and proof systems.

Subformulae can be defined recursively. If φ is atomic, then the only subformula is φ. If φ is a negation ¬ψ, then subformula(φ) = {φ} ∪ subformula(ψ). If φ is a binary connective, such as ψ ∧ θ or ψ → θ, then subformula(φ) = {φ} ∪ subformula(ψ) ∪ subformula(θ). If φ is a quantified formula ∀x ψ or ∃x ψ, then subformula(φ) = {φ} ∪ subformula(ψ). The proper subformulas of φ are the subformulas excluding φ itself.

Example: Let φ be (p ∧ q) → r. The subformulas are p, q, r, p ∧ q, and (p ∧ q) → r. Notably, each piece that appears inside φ, down to atomic formulas, is included.

Significance and use. The subformula concept underpins the subformula property, a key feature in many analytic proof systems (such as sequent calculi and analytic tableaux), where every formula appearing in a proof is a subformula of the initial assumptions or the conclusion. This property supports proof search termination, normalization, and structural induction arguments, and it extends to first-order logic with predicates and quantifiers through the same recursive idea.