first-order-logic Definition Subformula (First-Order Logic) The set of subformulas of a formula is defined inductively: