well-founded induction on formulas

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 $\le$ defined on formulas by $\phi \le \psi$ if and only if $\phi$ 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 $\phi$, if $P$ is true for every subformula of $\phi$, then $P$ is true for $\phi$.