Subformula relation, conjunctive and disjunctive formulas.

We define two constant T,F for true and false atomic formula.

In[148]:=

Subformula relations (for closed formulas).
   1. If A is atomic, then A has no subformulas.
   2. Then only subformula of ¬A is A.
   3. Immediate subformulas of A∨B, A∧B, A⇒B are A, B.
   4. Immediate subformulas of ∃x.A, ∀x.A are all A[t], with t closed term of the language.
A is a subformula of B if there is a chain of immediate subformulas from B to A.

Subformula relations (enriched with T,F).
There is an enriched subformula relation as well. In the enriched subformula relation, we slightly modify point 1 above (for atomic formulas) as follows:
   0. T,F have no subformulas.
   1. If A≠T,F is atomic, the only subformula of A is T if A is true, and F if A is false.
A is a subformula of B if there is a chain of immediate subformulas from B to A.

About the "enriched" subformula relation. In the enriched subformula relation we added T, F as subformula of all true atomic formulas ≠T,F. In this way truth and falsity for any atomic formula is evident from the subformula relation. This little trick makes easier to understand the picture of the subformula tree, as we will see.

Conjunctive formulas are the formulas equivalent to a conjunction of all their immediate subformulas. We also call conjunctive formulas Abelard's formulas. Conjunctive formulas are:

    T,            A∧B,        ∀x.A

Disjunctive formulas are the formulas equivalent to a disjunction of all their immediate subformulas. We also call disjunctive formulas Eloise's formulas. Disjunctive formulas are:

    P(x,y,...) (≠T),        A∨B,        A⇒B,        ¬A    ∃x.A
    
Some explanations. We first recall that the disjunction of the empty set is =F, and the conjunction of the empty set is =T.
   1. T is conjunctive because its set of subformulas is empty, hence the conjunction of its subformulas is =T.
   2. F is conjunctive because its set of subformulas is empty, hence the conjunction of its subformulas is =F.
   3. An atom P≠T,F is disjunctive because its set of its subformula is {T} if it is true, it is {F} if it is false. The disjunction of this singleton set is, according to the case, T or F. Remark that we could also consider P conjunctive. We made an arbitrary choice here.
   4. ¬A can be considered both the unary disjunction and the unary conjunction of its subformula set {A}. We considered ¬A as a disjunction in order to have negation as a particular case of implication.
   5. In all other cases, the choice between disjunctive and conjuctive is forced by the connective.

Created by Mathematica  (October 17, 2006)