well-founded induction on formulas

Let L be a first-order language. The formulasMathworldPlanetmath of L are built by a finite application of the rules of construction. This says that the relationMathworldPlanetmath defined on formulas by φψ if and only if φ is a subformula of ψ is a well-founded relation. Therefore, we can formulate a principle of inductionMathworldPlanetmath 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. 1.

    P is true for the atomic formulas;

  2. 2.

    for every formula φ, if P is true for every subformula of φ, then P is true for φ.

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