Let $L$ be a first-order language. The formulas of $L$ are built by a finite application of the rules of construction. This says that the relation $\leq$ defined on formulas by $\varphi\leq\psi$ if and only if $\varphi$ is a subformula of $\psi$ is a well-founded relation. Therefore, we can formulate a principle of induction for formulas as follows : suppose $P$ is a property defined on formulas, then $P$ is true for every formula of $L$ if and only if

1. $P$ is true for the atomic formulas;
2. for every formula $\varphi$ if $P$ is true for every subformula of $\varphi$ then $P$ is true for $\varphi$