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$.

Title	well-founded induction on formulas
Canonical name	WellfoundedInductionOnFormulas
Date of creation	2013-03-22 12:42:49
Last modified on	2013-03-22 12:42:49
Owner	jihemme (316)
Last modified by	jihemme (316)
Numerical id	6
Author	jihemme (316)
Entry type	Definition
Classification	msc 03B10
Classification	msc 03C99