first-order-logic Definition Proper Subformula (First-Order Logic) A formula is a proper subformula of if and .