How to improve my semantic tableau?

Question

I have to typeset some semantic tableaux in my document, looking similar to the example underneath.

My first idea was to use tikz for this, so I created the following monster:

\documentclass[convert]{standalone}
\usepackage{tikz,amssymb}
\usetikzlibrary{positioning}
\newcommand{\lnec}{\Box}
\begin{document}
  \begin{tikzpicture}[scale=2]
    \node[label=right:$(\lnec p\to\lnec q)\to\lnec(p\to q)$] (n1) {$\circ_1$};
    \node[label=left:$\lnec p\to\lnec q$, label=right:$\lnec(p\to q)$, below=of n1] (n2) {$\circ_1$};
    \node[label=left:$\lnec q$, label=right:$\lnec(p\to q)$, below left=of n2] (n3) {$\circ_1$};
    \node[label=right:{$\lnec p, \lnec(p\to q)$}, below right=of n2] (n4) {$\circ_1$};
    \node[label=left:$q$, label=right:$\lnec(p\to q)$, below=of n3] (n5) {$\circ_2$};
    \node[label=right:$p$, below left=of n4] (n6) {$\circ_3$};
    \node[label=right:$p\to q$, below right=of n4] (n7) {$\circ_4$};
    \node[label=left:$p$, label=right:$q$, below=of n7] (n8) {$\circ_4$};

    \draw[-] (n1) to (n2);
    \draw[-] (n2) to (n3);
    \draw[-] (n2) to (n4);
    \draw[-, dotted] (n3) to (n5);
    \draw[-, dotted] (n4) to (n6);
    \draw[-, dotted] (n4) to (n7);
    \draw[-] (n7) to (n8); 
  \end{tikzpicture}
\end{document}

It's clear that this is not the desired result. The edges should start underneath and end above the \circs, and they should have right angles, such that the diagram can be compressed a bit.

Drawing these kind of diagrams is completely new to me, so can you give me some useful guidelines? Do you have any tips or tricks for producing these semantic tableaux in general? Are packages like forest or qtree produce easier to use for this kind of tree?

---

Edit: @cfr's answer underneath is promising, so I'd like to work on with forest and fine-tune his style tableaux. I've tried to do it myself during the past two days, but understanding all of forest's advanced options in the documentation turned out to be impossible for a beginner like me. Therefore, I'd like to award a bounty to the person who can do the fine-tuning for me. That means

• the space between the wffs and the \circ separator should be decreased,
• the edges should be aligned with the center of the \circ separators, ignoring the possible subscripts,
• the above should also work when no subscript for the \circ separator is given.

Answer 1

This answer uses a completely different approach since the code was unfortunately lost from the original version of the question. It may be less helpful since it is not based on that code, but I will leave it here since it may be of use to somebody at some point.

Here's a basic Forest style, tableaux, which might be used for this kind of diagram.

The trouble with using label is that it doesn't get taken into account when positioning the nodes relative to each other. tableaux creates additional nodes for this content instead which are specified together with the 'main' node. This makes it possible to align things correctly with the 'main' circle while leaving sufficient space for the wffs.

The one real disadvantage of this is that it is necessary to create an additional phantom root node as we'd otherwise end up with 2 or 3 roots (the main node at the top level and wffs on each side). That's not possible. Hence the phantom root node.

If you are doing a lot of these, it is possible to avoid having to add the phantom root yourself by creating a new environment which does this automatically. (The environ package can be used for this with a custom name for the environment body.)

Forest's edges library is used to provide the forked edges style.

Fine-tuning is left as an exercise for the reader. For example, it might look better to adjust the sibling distances to bring the wffs closer in.

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage[edges]{forest}
\usepackage{amssymb}
\begin{document}
\forestset{%
  declare toks={F}{},
  declare toks={T}{},
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      delay={%
        content/.wrap value={\circ_{##1}},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}
\newcommand*{\necc}{\ensuremath{\mathbin{\Box}}}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{forest}
  tableaux
  [
    [1, F=(\necc p \lif \necc q) \lif \necc (p \lif q)
      [1, T=\necc p \lif \necc q, F=\necc (p \lif q)
        [1, T=\necc q, F=\necc (p \lif q)
          [2, T=q, F=p \lif q, edge=densely dotted
            [2, T={p, q}, F=q, label=below:$\otimes$]
          ]
        ]
        [1, F={\necc p, \necc(p \lif q)}
          [3, F=p, edge=densely dotted]
          [4, F=p \lif q, edge=densely dotted
            [4, F=q, T=p]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\end{document}

EDIT

This addresses the 3 desiderata added to the question. We avoid the effect of the subscripts on alignment by rendering them as labels rather than part of the nodes. We adjust the distance to the wffs before drawing the tree as we do not want to reduce the sibling distances generally but only the distance between the circles and associated wffs. This fine with and without the subscripts.

Depending on your actual usage, font family and size etc., you may want to adjust the particular dimensions used in the adjustments. These are -3.5pt and 3.5pt for the subscripts and 7.5pt and -7.5pt for the wffs in the MWE below.

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage[edges]{forest}
\usepackage{amssymb}
\begin{document}
\forestset{%
  declare toks={T}{},
  declare toks={F}{},
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      before typesetting nodes={%
        content/.wrap value={\circ},
      },
      delay={%
        my label/.wrap pgfmath arg={{[inner sep=0pt, xshift=-3.5pt, yshift=3.5pt, anchor=north west, font=\scriptsize]-45:$##1$}}{content()},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}
\newcommand*{\necc}{\ensuremath{\mathbin{\Box}}}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{forest}
  tableaux
  [
    [1, F=(\necc p \lif \necc q) \lif \necc (p \lif q)
      [1, T=\necc p \lif \necc q, F=\necc (p \lif q)
        [1, T=\necc q, F=\necc (p \lif q)
          [2, T=q, F=p \lif q, edge=densely dotted
            [2, T={p, q}, F=q, label=below:$\otimes$]
          ]
        ]
        [1, F={\necc p, \necc(p \lif q)}
          [3, F=p, edge=densely dotted]
          [4, F=p \lif q, edge=densely dotted
            [4, F=q, T=p
              [99, F=X!, T=XX!!
                [, F=XXX!!!, T=XXXX!!!!]
              ]
            ]
          ]
        ]
      ]
    ]
  ]
\end{forest}
\end{document}

EDIT EDIT

As pointed out in a comment, my Edit has caused the closures to disappear. This is because they are created using label and the numbers at the top right of the nodes have also been added using label. Although the labels are requested in different places and would be fine in usual TikZ code, Forest defines label in such a way that only one is permitted per node. Moreover, label also overwrites any earlier annotations specified using tikz or pin. From forest.sty:

 label/.style={tikz={\path[late options={%
        name=\forestoption{name},label={#1}}];}},
 pin/.style={tikz={\path[late options={%
        name=\forestoption{name},pin={#1}}];}},

Each call to tikz overrides any previous setting. Hence, code does not accumulate, but instead replaces existing code.

I'm not sure what reason the author had for this choice, so I'm not entirely sure how best to address it. One option would be to use afterthought for the numbers, which should allow the use of label in the tree itself. In that case, however, we couldn't specify the numbers as TikZ labels without essentially reproducing the code Forest uses for label in the first place. Since there doesn't seem to be any advantage in doing that, it is tempting to redefine label instead by adding the following code to the document's preamble:

\forestset{% Sašo Živanović won't like this ...
  label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  },
}

The + here is what makes the difference. Now labels will accumulate rather than overwriting each other and/or any prior uses of pin, tikz or tikz+. As indicated, I can't imagine this is the kind of thing I'm meant to do, so I'm not recommending it, even though it works:

A more complex alternative is to use this:

\forestset{%
  my label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  }
}

Then the placement of the numbers simply uses my label in place of label. Complete configuration:

\forestset{%
  declare toks={T}{},
  declare toks={F}{},
  my label/.style={%
    tikz+={%
      \path[late options={%
        name=\forestoption{name},label={#1}}
      ];
    }
  },
  tableaux/.style={%
    forked edges,
    for tree={
      math content,
      parent anchor=children,
      child anchor=parent,
    },
    where level=0{%
      for children={no edge},
      phantom,
    }{%
      before typesetting nodes={%
        content/.wrap value={\circ},
      },
      delay={%
        my label/.wrap pgfmath arg={{[inner sep=0pt, xshift=-3.5pt, yshift=3.5pt, anchor=north west, font=\scriptsize]-45:$##1$}}{content()},
        insert before/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'+=7.5pt}]
        }{T()},
        insert after/.wrap pgfmath arg={%
          [{##1}, no edge, math content, before drawing tree={x'-=7.5pt}]
        }{F()},
      },
      if={n_children("!u")==1}{%
        before packing={calign with current edge},
      }{}
    },
  }
}

which produces the same result as above without redefining Forest's label style.