subformula


Let L be a first order language and suppose φ is a formulaMathworldPlanetmath of L. A subformula of φ is defined as any of the following:

  1. 1.

    φ is a subformula of φ;

  2. 2.

    if ¬⁢ψ is a subformula of φ for some L-formula ψ, then so is ψ;

  3. 3.

    if α∧β is a subformula of φ for some L-formulas α,β, then so are α and β;

  4. 4.

    if ∃x⁢(ψ) is a subformula of φ for some L-formula ψ, then so is ψ⁢[t/x] for any t free for x in ψ.

Remark. And if the languagePlanetmathPlanetmath contains a modal connective, say □, then we also have

  1. 5.

    if □⁢α is a subformula of φ for some L-formula α, then so is α.

The phrase “t is free for x in ψ” means that after substituting the term t for the variable x in the formula ψ, no free variablesMathworldPlanetmathPlanetmath in t will become bound variables in ψ⁢[t/x].

For example, if φ=α∨β, then α and β are subformulas of φ. This is so because α∨β=¬⁡(¬⁢α∧¬⁢β), so that ¬⁢α∧¬⁢β is a subformula of φ by applications of 1 followed by 2 above. By 3 above, ¬⁢α and ¬⁢β are subformulas of φ. Therefore, by 2 again, α and β are subformulas of φ.

For another example, if φ=∃x(∃y(x2+y2=1)), then ∃y(t2+y2=1) is a subformula of φ as long as t is a term that does not contain the variable y. Therefore, if t=y+2, then ∃y((y+2)2+y2=1) is not a subformula of φ. In fact, if y∈ℝ, the equation (y+2)2+y2=1 is never true.

Finally, it is easy to see (by inductionMathworldPlanetmath) that if α is a subformula of ψ and ψ is a subformula of φ, then α is a subformula of φ. “Being a subformula of” is a reflexiveMathworldPlanetmathPlanetmath transitive relation on L-formulas.

Remark. There is also the notion of a literal subformula of a formula φ. A formula ψ is a literal subformula of φ if it is a subformula of φ obtained in any one of the first three ways above, or if ∃x⁢(ψ) is a literal subformula of φ.

Note that any literal subformula of φ is a subformula of φ, for if φ=∃x⁢(ψ), then x occurs free in ψ and ψ=ψ⁢[x/x].

In the second example above, ∃y(x2+y2=1) and x2+y2=1 are both literal subformulas of φ=∃x(∃y(x2+y2=1)).

Title subformula
Canonical name Subformula
Date of creation 2013-03-22 12:42:52
Last modified on 2013-03-22 12:42:52
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 13
Author CWoo (3771)
Entry type Definition
Classification msc 03C07
Classification msc 03B10
Related topic Substitutability
Defines literal subformula