wellfounded induction on formulas
Let $L$ be a firstorder 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 wellfounded 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  wellfounded induction on formulas 

Canonical name  WellfoundedInductionOnFormulas 
Date of creation  20130322 12:42:49 
Last modified on  20130322 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 