Listing Subjudgments.

We define a map returning the list of subjudgments of a given judgment.

In[161]:=

SF[A_, s_] := {Lin[A, s], PSF[A, s]} ;

In[162]:=

(* For implication and negation, the first subformula is taken with the opposite sign *)ᡝ ... [A_], s_]             := {SF[A, Dual[s]]} ;

In[165]:=

(* In all other cases, the sign of the subformula is the sign of the formula . *)PSF[C ... ormulas *)PSF[A_String, s_]           := {} ;

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

In[170]:=

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

An example of a subjudgments list.

In[171]:=

SubformulaList[F3, PosSign]

Out[171]=

{.∃x.(((¬A∨C)∧B)), .(((¬A∨C)∧B)& ... 743;B), .(¬A∨C), .¬A, .A, .C, .B, .}

Created by Mathematica  (October 17, 2006)