# How to create a correctly aligned tree proof in logic with 4 branches, columns of line numbers and justifications?

I'm looking for a way to make a Logic Tree with three columns (line number, tree itself and commentary). I've tried using a tikz matrix, and it worked very well, except when I get more than two branches, then the edge draw command stops working and I have to draw manually. Is there a way to adjust for the amount of columns in tikz? Is there a different package I might use?

Thanks a lot

@Johannes_B, Here is the code I have so far

\documentclass{article}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{tikz}
\usepackage{tikz-qtree}

\begin{document}

\def\shoe{$\supset$}
\def\nee{$\mathord{\sim}$}
\def\nein{$\neg$}
\def\lub{$\lor$}

\noindent
\checkmark 1 \hspace{10ex} A \shoe B \hspace{8ex} (premise) \\
\checkmark 2 \hspace {10ex} B \shoe C \hspace{8ex}  (premise) \\
\checkmark 3 \hspace{8.5ex} \nee(C \shoe A) \hspace{5.5ex} (conclusion) \\
\hspace{2ex} 4 \hspace{14ex} C \hspace{11ex} (3, \nee \shoe) \\ 5 \hspace{4.5ex}
\Tree [.{\nee A} [.{\nee B} {\nee A} {B} ] [.{C}  {\nee A} {B} ]]
\hspace{4ex} (3, \nee \shoe) \\
6

\end{document}


OR

    \documentclass{article}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{amsmath}
\usepackage{tikz}
\usetikzlibrary{matrix}

\begin{document}

\def\shoe{$\supset$}
\def\nee{$\mathord{\sim}$}
\def\nein{$\neg$}
\def\lub{$\lor$}

\begin{tikzpicture}
\matrix (m)[matrix of nodes, row sep=0.2em,
column sep=0.1em, text height=1.5ex, text depth=0.25ex]
{
1   &                                       &   A \shoe B             &                                      & (premise) \\
2   &                                       &   B \shoe C    &                                  & (premise) \\
3   &                                       &   \nee(C \shoe A)    &                               & (conclusion) \\
4   &                                       &   C            &                               & (3, \nee \shoe) \\
5   &                                       &   \nee A                                                        &                               & (3, \nee \shoe) \\ [2em]
6   &        \nee B           &                    &   C                                                & (3, \nee \shoe) \\ [2em]
7   &  \nee A   \hspace{0.5cm} B  & &  \nee A   \hspace {0.5cm}   B & (2, \shoe) \\ [2em]
};

\draw [-] (-3,3) -- (-0.5, 2);
\path[-]    (m-5-3.south) edge (m-6-2.north)
(m-5-3.south) edge (m-6-4.north)
(m-6-2.south)

\end{tikzpicture}

\end{document}


The problem is that when there are more than 2 nodes, path no longer works and I have to draw by hand, which does not strike me as very efficient

Problem is, in the code below the tree inserts a vertical line before branching. Do you guys have any idea why?

    \documentclass[tikz,border=5pt]{standalone}
\usepackage{forest}

\def\shoe{$\supset$}
\def\nee{$\mathord{\sim}$}
\def\nein{$\neg$}
\def\lub{$\lor$}

\begin{document}
\forestset{
ass/.append style={
before computing xy={l=\baselineskip},
no edge
},
}
\begin{forest}
for tree={
parent anchor=south,
child anchor=north,
align=center,
},
[(P \lub (G \& \nee D)) \& (P \shoe (\nee P \& (S \lub \nee Q), ass, name=n1
[P \lub (G \& \nee D),ass, name=n2
[P \shoe (\nee P \& (S \lub \nee Q)), ass, name=n3
[[P
[\hspace{0.005pt}, ass, name=n5
[\hspace{0.05pt}, ass, name=n6
[[\nee P, name=n7]
[\nee P \& (S \lub \nee G)
[\nee P, ass, name=n8
[S \lub \nee Q, ass, name=n9]]]]]]]
[G \& \nee D, name=n4
[G, ass
[\nee D, ass
[ [\nee P]
[\nee P \& (S \lub \nee G)
[\hspace{0.05pt}, ass
[\hspace{0.05pt}, ass
[\nee P, ass, name=n10
[S \lub \nee Q, ass, name=n11
[ [S,name=n12] [\nee Q]]]]]]]]]]]
]
]
]
]
\foreach \i in {1,...,12}
\node [xshift=-100pt, anchor=east] at (n\i -| n1) {\i.};
\foreach \i/\j in {2/{(1, \&)}}
\node [xshift=100pt, anchor=west] at (n\i -| n1) {\j};
\end{forest}
\end{document}

• HI and welcome, you could give oour tikz experts with what you got so far and they can make the adjustments on your example. – Johannes_B May 5 '15 at 11:56
• Is this really a duplicate? This question specifically asks about problems when trees include more branches, using the method explained in the accepted solution to that question. Although Ignasi's solution could be used. (Or mine but Ignasi's is better.) – cfr May 5 '15 at 15:24
• @MikeKhokhlovych Also note that you can 'ping' people with the @ symbol. Type that and the start of a name -- you can tab-complete :) Formally, welcome to TeX.SX! You can have a look at our starter guide to familiarize yourself further with our format. – Sean Allred May 5 '15 at 15:29
• Although I didn't think this was a duplicate, I thought the link was useful since the question was certainly closely related. But it has disappeared! – cfr May 8 '15 at 16:53

A later version of this package is now on CTAN - updated answer to reflect current usage etc.

I finally got fed up with not having a better solution to offer people. Logic is not well served, particularly for teaching lower level classes.

My solution is a new package. It certainly contains bugs and it is not altogether automatic. However, it is more automatic than earlier versions and contains fewer bugs than at least some of them.

# Caveat emptor...

The package is called prooftrees and depends on forest. It defines a new environment prooftree and provides various facilities for global and local configuration. It can resolve cross-references, merge conflicting justifications and move lines (sometimes automatically; sometimes using move by=<positive integer>). Line numbering and layout is automatic. Various options are provided for local and global configuration.

Here is an example trees using the cross-referencing system for justifications and inferences. This can use either name to name wffs or relative node names, as Forest defines them, or a mixture. If you don't use a :, the annotation will be typeset as is so you can also write just=From 2 if you prefer or close={4,5} and forgo the cross-referencing support.

\documentclass[tikz,border=5pt,multi]{standalone}
\usepackage{prooftrees}
\usepackage{amssymb}
\usepackage{mathtools,turnstile}
\begin{document}
\begin{prooftree}{}% default preamble - note this argument is REQUIRED
[P \vee (Q \vee \lnot R), grouped,  just=Ass
[P \supset \lnot R, grouped,  just=Ass
[Q \supset \lnot R, grouped,  just=Ass
[\lnot\lnot R, grouped, just={Negated conclusion}, name=nc
[P,  just={$\vee$ Elim:!r1}
[\lnot P, close={:!u,!c}
]
[\lnot R,  close={:nc,!c}, just={$\supset$ Elim:!r11}
]
]
[Q \vee \lnot R
[Q, just={5 $\vee$ Elim:!u}
[\lnot Q, , close={:!u,!c}
]
[\lnot R,  close={:nc,!c}, just={$\supset$ Elim:!r111}
]
]
[\lnot R, close={:nc,!c}
]
]
]
]
]
]
\end{prooftree}
\end{document}


This will produce a proof tree with line numbers and justifications:

The documentation contains further examples, including a worked example which explains how to turn a tree into Forest's bracket notation which may be familiar to linguists but is not so familiar, I think, to logicians. (Or perhaps I've just led an overly sheltered life.)

Here's the example worked step-by-step in the documentation, which includes use of move by to avoid the merging of justifications:

\documentclass[tikz,border=5pt,multi]{standalone}
\usepackage{prooftrees}
\usepackage{amssymb}
\usepackage{mathtools,turnstile}
\begin{document}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\newcommand*{\liff}{\ensuremath{\mathbin{\leftrightarrow}}}
\newcommand*{\elim}{\,\text{E}}
\begin{prooftree}
{
to prove={(\exists x)((\forall y)(Py \lif x = y) \land Px) \sststile{}{} (\exists x)(\forall y)(Py \liff x = y)}
}
[{(\exists x)((\forall y)(Py \lif x = y) \land Px)}, checked=a, just=Pr., name=pr
[{\lnot (\exists x)(\forall y)(Py \liff x = y)}, subs=a, just=Conc.~neg., name=neg conc
[{(\forall y)(Py \lif a = y) \land Pa}, checked, just=$\exists\elim$:pr
[{(\forall y)(Py \lif a = y)}, subs=b, just=$\land\elim$:!u, name=mark
[Pa, just=$\land\elim$:!uu, name=simple
[{\lnot (\forall y)(Py \liff a = y)}, checked=b, just=$\lnot\exists\elim$:neg conc
[{\lnot (Pb \liff a = b)}, checked, just=$\lnot\forall\elim$:!u
[Pb, just=$\liff\elim$:!u, name=to Pb or not to Pb
[a \neq b, just=$\liff\elim$:!u
[{Pb \lif a = b}, checked, just=$\forall\elim$:mark, move by=1
[\lnot Pb, close={:to Pb or not to Pb,!c}, just=$\lif\elim$:!u
]
[{a = b}
[a \neq a, close={:!c}, just={$=\elim$:{!uuu,!u}}
]
]
]
]
]
[\lnot Pb
[{a = b}
[Pb, just={$=\elim$:{simple,!u}}, close={:to Pb or not to Pb,!c}
]
]
]
]
]
]
]
]
]
]
\end{prooftree}
\end{document}


• Thanks, cfr! I'm extremely new to Latex, so would you mind telling me what \i and \j refer to? – Mike Khokhlovych May 5 '15 at 13:06
• @MikeKhokhlovych See edited answer where I try to explain the \foreach loop. I've also added an alternative which doesn't require this. – cfr May 5 '15 at 13:18
• Thank you so much! This actually works! Now, one last question I have is do you know if there's a way to put x-s underneath closed branches? Again, thanks so much – Mike Khokhlovych May 5 '15 at 15:00
• @MikeKhokhlovych Which method are you using? The first or the second? – cfr May 5 '15 at 15:03
• @MikeKhokhlovych See second edit. I've applied it to the second method but you can use the same style etc. with the first if that's what you are using. Hope this helps! It is a pain there is no good packaged solution for this. – cfr May 5 '15 at 15:19