[Tex/LaTex] Need help with making Logic Trees in qtree/tikz-qtree (i.e. aligning, numbering lines)

Question

I would like to make something similar to the logic tree below. I've tried using tikz-qtree, but I can't figure out how to number every line in the tree. I did however find something else doable in qtree. Here's a sample of my code (note that it's not the same tree as below)

    \documentclass[a4paper, english, 12pt, reqno]{article}\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[norsk]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage[shortlabels]{enumitem}
\usepackage{bm}
\usepackage{qtree}

\begin{document}
\maketitle{}

\section{}
\begin{center}
\begin{tabular}{c  c  c}
\Tree[.{1\\2\\ 3\\4} [.5  [.6 ] ] ] &
\Tree[.$A\supset B$\\$C\vee A$\\$\sim\sim C$\,\checkmark\\$C$ [.$C$ $s$ $s$ ][.$A$ $c$ $c$ ] ] &
\Tree[.SM\\SM\\SM\\3$\sim\sim$D [.3$\vee$D [.1$\supset$D ] ] ]
\end{tabular}
\end{center}

\end{document}

So I have some questions, which I hope will be able to help me get closer to a similar tree as in the picture.

1) My lines are not aligned horizontally, any ideas on how to fix that?

2) How can I remove the lines that connects the numbers, and the notation on the right side of the tabular enviroment?

3) This question is not about my code, but I will have this problem later. As you see on line 9 in the picture, there is a node all the way down to the 12th line, skipping the lines in between. How do I do this?

I'm open for using tikz-qtree too, and I probably missed something in the manual, so I will try to read more, as I'm quite new to using qtree in LaTeX. Thanks in advance!

Answer 1

This is a variant of Ignasi's answer. It uses a new package based on forest. The advantage is that the lines are automatically numbered, the justifications are added as annotations with their nodes using the key just (no need for a separate tree) and the vertical spacing between lines which should be grouped together (as when listing assumptions) is corrected automatically. In addition, styles are provided to move nodes (move by) to lower lines in the tree without the need to set special tier names or enter empty nodes. Cross-referencing support is provided in justifications and closure annotations (using either named nodes or relative node names), so that line numbers need not be hard-coded. Further options and details are explained in the package documentation.

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage{prooftrees,amsmath,turnstile}
\newcommand*{\tnot}{\ensuremath{\mathord{\sim}}}
\begin{document}
\begin{prooftree} % uses Ignasi's code for the main tree (https://tex.stackexchange.com/a/233576/)
  {
    to prove={(\exists x)Fx \supset (\forall x)Fx \sststile{}{} (\forall x) (Fx \supset (\forall y) Fy)}
  }
    [(\exists x) Fx \supset (\forall x) Fx, checked, just=SM, name=pr
      [\tnot (\forall x) (Fx \supset (\forall y) Fy), checked, grouped, just=SM
        [(\exists x) \tnot (Fx \supset (\forall y) Fy), checked=a, just={$\tnot\forall$D:!u}
          [\tnot (Fa \supset (\forall y) Fy), checked, just={$\exists$D:!u}
            [Fa, just={$\tnot\supset$D:!u}, name=fa
              [\tnot (\forall y) Fy, checked, grouped, just={$\tnot\supset$D:!uu}
                [(\exists y) \tnot Fy, checked=b, just={$\tnot\forall$D:!u}
                  [\tnot Fb, just={$\exists$D:!u}, name=nofb
                    [\tnot (\exists x) Fx, checked, just={$\supset$D:pr}
                      [(\forall x) \tnot Fx, subs=a, just={$\tnot\exists$D:!u}
                        [\tnot Fa, close={:fa,!c}, just={$\forall$D:!u}
                        ]
                      ]
                    ]
                    [(\forall x) Fx, subs=b
                      [Fb, close={:nofb,!c}, just={$\forall$D:!u}, move by=2
                      ]
                    ]
                  ]
                ]
              ]
            ]
          ]
        ]
      ]
    ]
\end{prooftree}
\end{document}