Need help with making Logic Trees in qtree/tikz-qtree (i.e. aligning, numbering lines)
Here's one way. This is somewhat of a hack because it requires manual adjustment to get the spacing right.
The code works by creating three trees - the main tree, the line numbers and the justifications. To create the latter two without lines, we temporarily redefine the commands used for branches, making use of qtree's ! feature.
The best work flow involves setting the tree itself first. Then copy that tree above it in your code and replace every instance of [.{single formula i.e. no line break} by [.n for the appropriate line number, n. Then replace [.{several formulae with line breaks} by [.{n\\m\\...} for the relevant line numbers n, m, .... Now compile and check the spacing. Add spacing as required. Get the lines to line up at this point as well as you can. Then copy your line number tree below the code for the main tree. Simply replace the line numbers by the relevant justifications. The spacing should be right as you've already adjusted it.
Getting the long branch down for the twelfth line is actually covered (kind of) in qtree's documentation where it explains how to create nodes without labels. However, it might not be obviously applicable here since the example concerns an unlabelled branching node whereas your example needs extra non-branching nodes.
\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}
\usepackage{turnstile}
% set up a more semantically pleasing command for not
\newcommand*{\tnot}{\ensuremath{\mathord{\sim}}}
\makeatletter
\newcommand{\nounibranches}[1]{% One-branching only
\begin{picture}(0,1)
\put(0,0){\line(0,1){0}}
\end{picture}}%
\newcommand{\nobibranches}[1]{% Two-branching only
\begin{picture}(2,0.5)
\put(0,0){\line(2,1){0}}
\put(2,0){\line(-2,1){0}}
\end{picture}}%
\let\qdrawReal=\qdraw@branches
\def\dimbr#1{\ifcase#1\relax % zero case is unused
\or % One-branching
\let\qdraw@branches=\nounibranches
\or % Two-branching
\let\qdraw@branches=\nobibranches
\else \typeout{error --- Can't handle #1-way branching}
\fi}
\newcommand\breto{\let\qdraw@branches=\qdrawReal}
\makeatother
\begin{document}
\hspace*{-\parindent}
{$(\exists x)Fx \supset (\forall x)Fx \sststile{}{} (\forall x) (Fx \subset (\forall y) Fy)$}\bigskip\\
\Tree
[.{1\\2}
[.3
[.4
[.{5\\6}
[.7
[.{8\\[-.75em]\mbox{ }}
[.9
[.10
[.11
[.12
!{\dimbr1}
]
]
]
]
]
]
]
]
]
] {\breto}
\Tree
[.{$(\exists x) Fx \supset (\forall x) Fx\ \checkmark$\\
$\tnot (\forall x) (Fx \subset (\forall y) Fy)\ \checkmark$}
[.{$(\exists x) \tnot (Fx \subset (\forall y) Fy)\ \checkmark$}
[.{$\tnot (Fa \subset (\forall y) Fy)\ \checkmark$}
[.{$Fa$\\$\tnot (\forall y) Fy\ \checkmark$}
[.{$(\exists y) \tnot Fy\ \checkmark$}
[.{$\tnot Fb$}
[.{$\tnot (\exists x) Fx\ \checkmark$}
[.{$(\forall x) \tnot Fx\ \checkmark$}
[.{$\tnot Fa$\\$\otimes$}
]
]
]
[.{$(\forall x) Fx\ \checkmark$}
[
[
[
[
[
[.{$Fb$\\$\otimes$}
]
]
]
]
]
]
]
]
]
]
]
]
]
\Tree
[.{SM\\SM}
[.{2 $\tnot\forall$D}
[.{3 $\exists$E}
[.{4 $\tnot\supset$D\\4 $\tnot\supset$D}
[.{6 $\tnot\forall$D}
[.{7 $\exists$D}
[.{1 $\supset$D}
[.{9 $\tnot\exists$D}
[.{10 $\forall$D}
[.{9 $\forall$D}
!{\dimbr1}
]
]
]
]
]
]
]
]
]
] {\breto}
\end{document}
This produces the following tree:
If you're open to a different approach, I would actually go about this by \usetikzlibrary{matrix} instead. I think this solution might be preferable to @cfr's solution, as one does not have to manually adjust the spacing for this solution.
That is, one can specify the matrix options of column sep and row sep globally in order to get some default spacing that one wants for all rows and columns. Yet, at the same time, if one wants to manipulate some of the spacing individually, one can do so by, for example, using the optional argument to \\, as I have done in line 8 of the matrix in order to provide more separation for the branching part of the 'tree'.
\documentclass{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{amssymb}
\newcommand*{\tnot}{\ensuremath{\mathord{\sim}}} % following @cfr's suggestion
\usepackage{tikz}
\usetikzlibrary{matrix}
\begin{document}
\begin{tikzpicture}
\matrix (m) [matrix of nodes, row sep=0.2em,
column sep=0.1em, text height=1.5ex, text depth=0.25ex]
{
1 & & $(\exists x) Fx \supset (\forall x) Fx\ \checkmark$ & & SM \\
2 & & $\tnot (\forall x) (Fx \subset (\forall y) Fy)\ \checkmark$ & & SM \\
3 & & $(\exists x) \tnot (Fx \subset (\forall y) Fy)\ \checkmark$ & & 2 $\tnot\forall$D \\
4 & & $\tnot (Fa \subset (\forall y) Fy)\ \checkmark$ & & 3 $\exists$E \\
5 & & $Fa$ & & 4 $\tnot\supset$D \\
6 & & $\tnot (\forall y) Fy\ \checkmark$ & & 4 $\tnot\supset$D \\
7 & & $(\exists y) \tnot Fy\ \checkmark$ & & 6 $\tnot\forall$D \\
8 & & $\tnot Fb$ & & 7 $\exists$D \\[2em] % here I've added some space so the tree can branch
9 & $\tnot (\exists x) Fx\ \checkmark$ & & $(\forall x) Fx\ \checkmark$ & 1 $\supset$D \\
10 & $(\forall x) \tnot Fx\ \checkmark$ & & & 9 $\tnot\exists$D \\
11 & $\tnot Fa$ & & & 10 $\forall$D \\
12 & $\otimes$ & & $Fb$ & 9 $\forall$D \\
& & & $\otimes$ & \\
};
\path[-] (m-8-3.south) edge (m-9-2.north)
(m-8-3.south) edge (m-9-4.north)
(m-9-4) edge (m-12-4);
\end{tikzpicture}
\end{document}
Just for fun I wanted to try with forest and with all columns being branches from the same tree.
The main problem was how to adjust horizontal alignment between columns. forest documentation mention (page 17) that when text includes parenthesis, the alignment will look strange because it's a very special situation. But, as usual, it also provides a solution consisting in defining a new \forestStandardNode.
So, a possible solution with forest could be:
\documentclass[tikz,border=2mm]{standalone}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage[norsk]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{qtree}
\usepackage{forest}
\newcommand*{\tnot}{\ensuremath{\mathord{\sim}}} % following @cfr's suggestion
\begin{document}
\forestStandardNode[(dj)]
{%
\forestOve{\csname forest@id@of@standard node\endcsname}{content},%
\the\ht\strutbox,\the\pgflinewidth,%
\pgfkeysvalueof{/pgf/inner ysep},\pgfkeysvalueof{/pgf/outer ysep},%
\pgfkeysvalueof{/pgf/inner xsep},\pgfkeysvalueof{/pgf/outer xsep}%
}
{
l sep={\the\ht\strutbox+\pgfkeysvalueof{/pgf/inner ysep}},
l={l_sep()+abs(max_y()-min_y())+2*\pgfkeysvalueof{/pgf/outer ysep}},
s sep={2*\pgfkeysvalueof{/pgf/inner xsep}}
}
{l sep,l,s sep}
\begin{forest}
[,phantom, for descendants={no edge}
[1, [2[3[4[5[6[7[8[9[10[11[12]]]]]]]]]]]]
[$(\exists x) Fx \supset (\forall x) Fx\ \checkmark$
[$\tnot (\forall x) (Fx \subset (\forall y) Fy)\ \checkmark$
[$(\exists x) \tnot (Fx \subset (\forall y) Fy)\ \checkmark$
[$\tnot (Fa \subset (\forall y) Fy)\ \checkmark$
[$Fa$
[$\tnot (\forall y) Fy\ \checkmark$
[$(\exists y) \tnot Fy\ \checkmark$
[$\tnot Fb$
[$\tnot (\exists x) Fx\ \checkmark$, edge={draw}
[$(\forall x) \tnot Fx\ \checkmark$
[$\tnot Fa$
[$\otimes$, tier=otimes]]]]
[$(\forall x) Fx\ \checkmark$, edge={draw}
[$Fb$,tier=otimes, edge={draw}
[$\otimes$]]]]]]]]]]]
[SM [SM[2 $\tnot\forall$D[3 $\exists$E[4 $\tnot\supset$D[6 $\tnot\forall$D
[7 $\exists$D[1 $\supset$D[9 $\tnot\exists$D[10 $\forall$D
[9 $\forall$D]]]]]]]]]]]
]
\end{forest}
\end{document}
