Listing subformulas.

We recursively define the list of subformulas of a given formula A. Subformulas are listed in preorder. That is, we write A first, then the subformulas of each immediate subformula of A. For ∀x.A, ∃x.A, we include only one sample subformula, A[x0/x]. If we consider constructive implication, we add a subformula A→B between A⇒B and A,B. We skip all subformulas of any abbreviation, for short.

In[149]:=

SF[A_]               &nb ... roper subformulas *) PSF[A_String]           := {} ;

The previous map returns a nested list. We define a map returning a flat list.

In[158]:=

SubformulaList[F_] := Map[Size, Flatten[SF[F]]] ;

Some example of a list of subformulas.

In[159]:=

SubformulaList["MP"]

Out[159]=

{MP}

In[160]:=

SubformulaList[Unfold["MP"]]

Out[160]=

{∃x.∀y.f(x)≤f(y), ∀y.f(x0)≤f(y), f(x0)≤f(y0)}

Created by Mathematica  (October 17, 2006)