Printing the Subformula tree.

We recursively define a map turning a subformula tree into a tree in the Mathematica format. We replace each constant constructor with a leaf, each unary constructor with the unary constructor of trees, each binary constructor with the binary constructor of trees. We count quantifiers as unary construction (their first argument is a variable, not a formula, and it is ignored).

In[221]:=

The first subformula of A, which is A itself, is defined as the root of the subformula tree. Vertices are labelled by the list of subformulas, with or without sign, with or without color.

In[229]:=

In[230]:=

We choose some options for printing the subformula tree.

1. We make vertices very small with VertexStyle→Disk[0.06] (there is already too much information on the display).
2. We center each subformula with the corresponding node with VertexLabelPosition→Center.
3. We decide the size in pixels of the image with ImageSize→... and AspectRatio→...
4. We print the entire tree with PlotRange→All (otherwise some labels are cut off from the image).
5. As default, we draw the background PaleGoldenRod (a golden pale yellow) in order to make pink color more evident.
6. As default, we draw edges thin to avoid superpositions with formulas.

In[232]:=

In[233]:=

We define functions printing the subformula tree with and without sign, with and without colors.

In[235]:=

In[236]:=

In[237]:=

Created by Mathematica  (October 17, 2006)