3

This is my first question on TeX.SE.

I need to typeset several dozen modal logic trees; unlike typical first-order trees these require an additional index to indicate worlds in the model.

Here is a typical example, inelegantly forced using qtree:

\documentclass[11pt]{article} 
\usepackage{amssymb}
\usepackage{qtree}
\begin{document}

 \,\,\,\,\,\,\,\,\,\,\,\, \Tree
    [.{ $\,\,\,\,\, \,\,\,\,\,1. \,\,\,\Box P \,\lor\, \Box Q \,\,\,\,\,\,\,\,\,\, w \,\,\,\, \checkmark$ \\ 
    $ \,\,\,\, \,\,\,\,\,\, 2. \,\,\, \neg \Box (P \,\lor\, Q) \,\,\,\,\,\,w \,\,\,\,\checkmark $ \\ 
    $ \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, \,\,\, \,\,\, \,\,\, 3. \,\,\,  \neg (P \,\lor\, Q)\,\,\,\,\,\,\,\,\,\,\,x   \,\,\,\,\checkmark  \,\,\,\,\,\,\, [2 \,\,\neg \Box]$ \\ 
    $  \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,4.  \,\,\,\neg P \,\,\,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,x \,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\, [3 \,\,\neg \lor] \,$ \\ 
    $ \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,5.  \,\,\,\neg Q \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, x \,\,\,\,\,\,\,\,\,\, \,\,\,\,\,\, [3 \,\,\neg \lor] \,$}
      [.{ $6. \,\,\, \Box P \,\,\,\,\,w \,\,\,\,\,\,\,\, [1\,\,\,\lor ]$ \\   
      $7. \,\,\,  P \,\,\,\,\,\,\,\,\,x  \,\,\,\,\,\,\,\,\, [6 \,\,\,\Box ]$ \\ 
      $  \,\,\,\,\,\,\,\,\,\times \,\,\,\,\, \,\, \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, [4, 7 ] \,\,\,$ }
      ]
      [.{ $ \,\,\,\,\, \,\,\,\,\, \,\,\,\,\, \,\,\,\,\, \,\,6'. \,\,\, \Box Q  \,\,\,\,\,w  \,\,\,\,\,\,\,\, [1\,\,\,\lor ]$  \\ 
      \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,$ \,\,\,\,\,\,\, 7'. \,\,\,Q \,\,\,\,\,\,\,\,\,\,x  \,\,\,\,\,\,\,\, [6' \,\,\,\Box ]$ \\ 
      $\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\times \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, [5, 7']$} 
      ]
 ]     

% Note: I am not the original author of this code; used with permission.

\end{document}

which produces the following result:

enter image description here

where the offset w's and x's are the indices at issue.

Obviously this is an ad hoc solution. Certainly it gets the point across, but it's mighty inconvenient and unacceptable for professional publication, which is the goal.

Now for non-modal (propositional and predicate logic) trees, I'm a huge fan of prooftrees. That's what I've been using for everything else. Here's effectively the same tree using prooftrees:

\documentclass[11pt]{article} 
\usepackage{prooftrees}
\forestset{subs with={\,\, | \,}}
\forestset{check right=false}
\forestset{close with={\ensuremath{\times}}}
\forestset{close sep= .75\baselineskip}

\begin{document}

\begin{prooftree}
{to prove={\Box P\lor\Box Q\vdash\Box(P\lor Q)}}
[\Box P\lor\Box Q, subs=w, checked
[\lnot\Box(P\lor Q), subs=w, checked
[\lnot(P\lor Q), subs=x, checked, just={2 $\lnot\Box$}
[\lnot P, subs=x, just={3 $\lnot\lor$}
[\lnot Q, subs=x, just={3 $\lnot\lor$}
    [\Box P, subs=w, just={1 $\lor$}
    [P, subs=x, just={6 $\Box$}, close={(4,7)}
    ]]
    [\Box Q, subs=w
    [Q, subs=x, just={6' $\Box$}, close={(5,7')}
    ]]
]]]]]
\end{prooftree}

 \end{document}

which produces the following result:

enter image description here

Notice I've used the substitution feature for the world indices, which is less than ideal. (The line numbers and justifications are also affected, but I'm less concerned about that.) I'm pretty happy with this method, all things considered; but I'd really prefer a separate column for the indices if it's possible, because that's how we do the trees by hand. I experimented with placing the indices in the justification, which works well for trees that don't branch, but obviously that still won't work for left or subsequent branches.

I know this is possible in something like tikz or forest, but I confess I still find those packages rather formidable. I suspect something along the lines of the answer here will be required, but I hope there is a more straightforward solution. I don't have the technical expertise to implement a more elegant solution, so I'd appreciate whatever help is on offer. Please and thank you!

UPDATE 1

Based on this answer I devised the following solution for the tree above, using forest:

\documentclass[11pt]{article} 
\usepackage{amssymb, amsmath, amstext, forest}

\begin{document}

\begin{forest}
    for tree={for tree={parent anchor=south,
            child anchor=north,
            align=center,
            inner sep=2.5pt}}
[
\begin{tabular}{p{1ex}p{0ex}cp{1em}p{0em}}
1. & $\checkmark$ & $\Box P\lor \Box Q$ & $w$ &\\
2. & $\checkmark$ & $\lnot\Box (P\lor Q)$ & $w$ &\\
3. & $\checkmark$ & $\lnot(P\lor Q)$ & $x$ & {[2$\,\lnot\Box$]}\\
4. & & $\lnot P$ & $x$ & {[3$\,\lnot\lor$]}\\
5. & & $\lnot Q$ & $x$ & {[3$\,\lnot\lor$]}
\end{tabular}, s sep=3em
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    6. & $\Box P$ & $w$ & {[1$\,\lor$]}\\
    8. & $P$ & $x$ & {[6$\,\Box$]}\\
     & $\times$ & & {[4{,\,}8]}\\
    \end{tabular}
    ]
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    7. & $\Box Q$ & $w$ & {[1$\,\lor$]}\\
    9. & $Q$ & $x$ & {[7$\,\Box$]}\\
    & $\times$ & & {[5{,\,}9]}\\
    \end{tabular}
    ]
]
\end{forest}

\bigskip

Suppose line 9 was absent:

\bigskip

\begin{forest}
    for tree={for tree={parent anchor=south,
            child anchor=north,
            align=center,
            inner sep=2.5pt}}
[
\begin{tabular}{p{1ex}p{0ex}cp{1em}p{0em}}
1. & $\checkmark$ & $\Box P\lor \Box Q$ & $w$ &\\
2. & $\checkmark$ & $\lnot\Box (P\lor Q)$ & $w$ &\\
3. & $\checkmark$ & $\lnot(P\lor Q)$ & $x$ & {[2$\,\lnot\Box$]}\\
4. & & $\lnot P$ & $x$ & {[3$\,\lnot\lor$]}\\
5. & & $\lnot Q$ & $x$ & {[3$\,\lnot\lor$]}
\end{tabular}, s sep=3em
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    6. & $\Box P$ & $w$ & {[1$\,\lor$]}\\
    8. & $P$ & $x$ & {[6$\,\Box$]}\\
    & $\times$ & & {[4{,\,}8]}\\
    \end{tabular}
    ]
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    7. & $\Box Q$ & $w$ & {[1$\,\lor$]}\\
    & $\times$ & & {[5{,\,}9]}\\
    \end{tabular}
    ]
]
\end{forest}

\bigskip

Remediable in this specific case by adding an empty line under the right branch closure:

\bigskip

\begin{forest}
    for tree={for tree={parent anchor=south,
            child anchor=north,
            align=center,
            inner sep=2.5pt}}
[
\begin{tabular}{p{1ex}p{0ex}cp{1em}p{0em}}
1. & $\checkmark$ & $\Box P\lor \Box Q$ & $w$ &\\
2. & $\checkmark$ & $\lnot\Box (P\lor Q)$ & $w$ &\\
3. & $\checkmark$ & $\lnot(P\lor Q)$ & $x$ & {[2$\,\lnot\Box$]}\\
4. & & $\lnot P$ & $x$ & {[3$\,\lnot\lor$]}\\
5. & & $\lnot Q$ & $x$ & {[3$\,\lnot\lor$]}
\end{tabular}, s sep=3em
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    6. & $\Box P$ & $w$ & {[1$\,\lor$]}\\
    8. & $P$ & $x$ & {[6$\,\Box$]}\\
     & $\times$ & & {[4{,\,}8]}\\
    \end{tabular}
    ]
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    7. & $\Box Q$ & $w$ & {[1$\,\lor$]}\\
    & $\times$ & & {[5{,\,}9]}\\
    & & &
    \end{tabular}
    ]
]
\end{forest}

\bigskip

But what if line 7 branched?

\bigskip

\begin{forest}
    for tree={for tree={parent anchor=south,
            child anchor=north,
            align=center,
            inner sep=2.5pt}}
[
\begin{tabular}{p{1ex}p{0ex}cp{1em}p{0em}}
1. & $\checkmark$ & $\Box P\lor \Box Q$ & $w$ &\\
2. & $\checkmark$ & $\lnot\Box (P\lor Q)$ & $w$ &\\
3. & $\checkmark$ & $\lnot(P\lor Q)$ & $x$ & {[2$\,\lnot\Box$]}\\
4. & & $\lnot P$ & $x$ & {[3$\,\lnot\lor$]}\\
5. & & $\lnot Q$ & $x$ & {[3$\,\lnot\lor$]}
\end{tabular}, s sep=3em
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    6. & $\Box P$ & $w$ & {[1$\,\lor$]}\\
    8. & $P$ & $x$ & {[6$\,\Box$]}\\
     & $\times$ & & {[4{,\,}8]}\\
    \end{tabular}
    ]
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    7. & $\Box Q$ & $w$ & {[1$\,\lor$]}\\
    \end{tabular}
        [blah
        ]
        [blah
        ]
    ]
]
\end{forest}

\bigskip

The previous remedy delivers inferior results:

\bigskip

\begin{forest}
    for tree={for tree={parent anchor=south,
            child anchor=north,
            align=center,
            inner sep=2.5pt}}
[
\begin{tabular}{p{1ex}p{0ex}cp{1em}p{0em}}
1. & $\checkmark$ & $\Box P\lor \Box Q$ & $w$ &\\
2. & $\checkmark$ & $\lnot\Box (P\lor Q)$ & $w$ &\\
3. & $\checkmark$ & $\lnot(P\lor Q)$ & $x$ & {[2$\,\lnot\Box$]}\\
4. & & $\lnot P$ & $x$ & {[3$\,\lnot\lor$]}\\
5. & & $\lnot Q$ & $x$ & {[3$\,\lnot\lor$]}
\end{tabular}, s sep=3em
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    6. & $\Box P$ & $w$ & {[1$\,\lor$]}\\
    8. & $P$ & $x$ & {[6$\,\Box$]}\\
     & $\times$ & & {[4{,\,}8]}\\
    \end{tabular}
    ]
    [
    \begin{tabular}{p{1ex}cp{1em}p{0em}}
    7. & $\Box Q$ & $w$ & {[1$\,\lor$]}\\
    & & & \\
    & & &
    \end{tabular}
        [blah
        ]
        [blah
        ]
    ]
]
\end{forest}

\end{document}

which produces the following result:

enter image description here

This is much better! However, this method cannot accommodate more complex trees with multiple branches that don't run in parallel, which is what I'd ultimately like to do. (In the code above I've also included some basic problems I don't understand how to solve [not pictured here].)

I haven't tried to code the more complex trees yet, but I can share some examples of the kind of tree I'm interested in typesetting.

These examples are all taken from Girle's Modal Logics and Philosophy (2000). This first example is nicely aligned:

enter image description here

[Source: Girle (2000), p. 25]

Compare to these next few examples, where he abandons good alignment:

enter image description here

[Source: Girle (2000), p. 184]

enter image description here

[Source: Girle (2000), p. 185]

Regarding the above examples, after giving it some thought I think I no longer care for the line numbers and annotations justified to the left and right edges respectively, as prooftrees does. I think I'd prefer the line numbers and annotations attached to the individual formulas, as with my original tree and my updated attempt. What's important is that the formulas, indices, etc. are aligned with other instances on the same branch.

Also, I note that for 2-D and impossible worlds semantics an additional index is needed; but I figure if I can get the issue for one index resolved, then I could just pair the two indices together with a little space between them.

I suspect the solution will be along the lines of this awesome answer. But whatever's going on there is as yet far beyond my grasp, and I have no clue how to adapt it to my purposes.

I really appreciate any and all help!

UPDATE 2

cfr's solution works very well in many cases. Thank you again!

However, a large tree such as the following causes problems:

\documentclass[11pt]{article} 
\usepackage{amssymb, amsmath, amstext,array}
\usepackage[linguistics]{forest}
\newcolumntype{C}[1]{>{\centering $}p{#1}<{$}}
\forestset{
  declare toks register={claim},
  declare autowrapped toks={just}{},
  declare toks={close}{},
  Autoforward={close}{closing},
  declare autowrapped toks={world}{},
  declare boolean={align me}{0},
  declare dimen={my width}{0pt},
  declare dimen register={lmeas},
  lmeas/.pgfmath=width("99."),
  declare dimen ={rmeas}{0pt},
  rmeas/.pgfmath={width("[99.]")},
  declare dimen register={wmeas},
  wmeas/.pgfmath=width("$w$"), 
  declare dimen={cmeas}{0pt},
  cmeas/.pgfmath=width("\ensuremath{\checkmark}"),
  claim=,
  declare toks register={check with},
  check with={\ensuremath{\checkmark}}, 
  declare toks register={close with},
  close with={\times}, 
  declare autowrapped toks={discharge}{},
  declare boolean={checked}{0},
  declare boolean={closed}{0},
  ml proof/.style={
    for tree={
      math content,
    },
    for root=align me,
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
    },
    for root={align me},
    where n children>=2{
      for children={align me}}{},
    before packing={
      where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip},}{},
      where align me={%
        tempdima/.max={>{OOw2+d}{max x}{min x}{##1-##2}}{%
          walk and save={temptoksa}{current,
             until={> O_=!{n children}{1}}{first}}%
        },
        tempdimb/.max={>{ROO?w2+P}{check with}{discharge}{checked}{width("##1##2")}{0pt}}{%
          load=temptoksa%
        },
        tempdimc/.max={>{OSl+tt=?w+P}{just}{}{0pt}{width("[##1]")}}{%
          load=temptoksa%
        },
        if tempdimb={0pt}{}{tempdimb'+=2.5pt},
        for nodewalk={load=temptoksa}{my width/.register=tempdima, cmeas/.register=tempdimb, rmeas/.register=tempdimc}, 
      }{},
      tempcounta'=0,
      for tree breadth-first={
        align=p{\foresteregister{lmeas}}@{}p{\foresteoption{cmeas}}@{}C{\foresteoption{my width}}C{\foresteregister{wmeas}}p{\foresteoption{rmeas}},
        if closed={
          content/.process={ ROSl+tt= ? w  w2 {close with}{!u.close}{}{}{[##1]}{ && ##1  && ##2} },
        }{
          tempcounta'+=1,
          content/.process={ ORO OSl+tt= ? w ROO ? w2  w5 {content}{tempcounta}{world}{just}{}{}{[##1]}{check with}{discharge}{checked}{##1##2}{}{##2. & ##5 & ##1 & ##3 & ##4} },
        },
        typeset node,
      }
    },
  },
  discharged/.style={
    checked,
    discharge=\,#1,
  },
  closing/.style={delay={append={[, closed]}}},
}

\begin{document}
\begin{forest}
claim={\Box P\lor\Box Q\vdash\Box(\Diamond P\land\Diamond Q)},
ml proof,
[\Box P\lor\Box Q, world=w, checked
 [\lnot\Box(\Diamond P\land\Diamond Q), world=w, checked
  [\lnot(\Diamond P\land\Diamond Q), world=v, checked, just={2 $\lnot\Box$}
   [\lnot\Diamond P, world=v, just={3 $\lnot\land$}
    [\Box P, world=w, just={1 $\lor$}
     [P, world=w, just={6 $\Box$}
      [\lnot P, world=w, just={4 $\lnot\Diamond$}, close={10,\,14}]
     ]
    ]
    [\Box Q, world=w, just={1 $\lor$}
     [Q, world=w, just={7 $\Box$}
      [Q, world=v, just={7 $\Box$}
       [\lnot P, world=w, just={4 $\lnot\Diamond$}
        [\lnot P, world=v, just={4 $\lnot\Diamond$}]
       ]
      ]
     ]
    ]
   ]
   [\lnot\Diamond Q, world=v, just={3 $\lnot\land$}
    [\Box P, world=w, just={1 $\lor$}
     [P, world=w, just={8 $\Box$}
      [P, world=v, just={8 $\Box$}
       [\lnot Q, world=w, just={5 $\lnot\Diamond$}
        [\lnot Q, world=v, just={5 $\lnot\Diamond$}]
       ]
      ]
     ]
    ]
    [\Box Q, world=w, just={1 $\lor$}
     [Q, world=w, just={9 $\Box$}
      [\lnot Q, world=w, just={5 $\lnot\Diamond$}, close={13,\,17}]
     ]
    ]
   ]
  ]
 ]
]
\end{forest}
\end{document}

Obviously flushleft/noindent isn't enough and tiny is overkill. Condensing the horizontal space or vertically offsetting the right branches would both be acceptable solutions, but I don't (yet) understand the method well enough to accomplish them. Any advice?

8
  • Welcome! I didn't know people used tableaux for modal logic. It would be possible to do better with prooftrees, but I don't know if that's the best approach. Can you describe exactly which differences between the two outputs matter? For example, in the first tableau, justifications for closure are aligned with other justifications. That would be tricky. Moreover, if you need double numbering & justifications prooftrees is out. The code isn't going to produce 6 and 6' and two justifications on a single line. If you want that,plain forest would be better.
    – cfr
    Dec 10, 2020 at 6:13
  • That is: I'm pretty sure I can adapt prooftrees to do the indices, but there's no point in doing that if you really want a tree of a kind better done with forest.
    – cfr
    Dec 10, 2020 at 6:14
  • Does your second example compile without error for you? I get an error, which I suspect is my fault ....
    – cfr
    Dec 10, 2020 at 6:19
  • Definitely a bug - thanks.
    – cfr
    Dec 10, 2020 at 6:25
  • @cfr Thanks so much for taking a look! I've updated my answer with more information. I'm grateful for any and all assistance you might provide.
    – poot
    Dec 10, 2020 at 13:38

1 Answer 1

3

The following provides automatic numbering. close=<arg> adds closure, checked checks, discharged=<arg> should check <arg> (untested as not used in these examples), world=<arg> adds a world, just=<arg> adds a justification. ml proof in a forest preamble triggers the style and claim=<arg> sets a proof statement/theorem.

Aside from the initial statement, if any, all nodes are tabulars with 5 columns:

  1. line number (auto)
  2. checked/discharged variables (checked, discharged=<arg>
  3. wff
  4. world (world=<arg>)
  5. justification (just=<arg> except that close=<arg> will produce the justification for an appended closure mark in the child node.

The widths of the second, third and fifth columns are adjusted based on the content of nodes from a node with exactly one child to the next branch. The first and fourth columns are set to the width of something roughly expected and are not adjusted further. (If you have a lot of these, compilation time can quickly become an issue. So I'd avoid setting all columns to optimal widths unless you really need to. The coding for doing that is straightforward, but --- at least sans Sašo --- every additional adjustment requires parsing through the various chunks of the tableau.

No special shenanigans are required for the examples in the question. However, a sample size of 3 is offers scant confidence for the population as a whole. (This is exacerbated by the fact I've never used tableaux for modal logic.)

Caveat emptor ...

% ref.: https://tex.stackexchange.com/q/574099/
\documentclass[11pt]{article} 
\usepackage{amssymb, amsmath, amstext,array}
% ref.: https://tex.stackexchange.com/q/570449/
\usepackage[linguistics]{forest}
\newcolumntype{C}[1]{>{\centering $}p{#1}<{$}}
\forestset{
  declare toks register={claim},
  declare autowrapped toks={just}{},
  declare toks={close}{},
  Autoforward={close}{closing},
  declare autowrapped toks={world}{},
  declare boolean={align me}{0},
  declare dimen={my width}{0pt},
  declare dimen register={lmeas},
  lmeas/.pgfmath=width("99."),
  declare dimen ={rmeas}{0pt},
  rmeas/.pgfmath={width("[99.]")},
  declare dimen register={wmeas},
  wmeas/.pgfmath=width("$w$"),
  declare dimen={cmeas}{0pt},
  cmeas/.pgfmath=width("\ensuremath{\checkmark}"),
  claim=,
  declare toks register={check with},
  check with={\ensuremath{\checkmark}}, 
  declare toks register={close with},
  close with={\textsf{x}},
  declare autowrapped toks={discharge}{},
  declare boolean={checked}{0},
  declare boolean={closed}{0},
  ml proof/.style={
    for tree={
      math content,
    },
    for root=align me,
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
    },
    for root={align me},
    where n children>=2{
      for children={align me}}{},
    before packing={
      where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip},}{},
      where align me={%
        tempdima/.max={>{OOw2+d}{max x}{min x}{##1-##2}}{%
          walk and save={temptoksa}{current,
             until={> O_=!{n children}{1}}{first}}%
        },
        tempdimb/.max={>{ROO?w2+P}{check with}{discharge}{checked}{width("##1##2")}{0pt}}{%
          load=temptoksa%
        },
        tempdimc/.max={>{OSl+tt=?w+P}{just}{}{0pt}{width("[##1]")}}{%
          load=temptoksa%
        },
        if tempdimb={0pt}{}{tempdimb'+=2.5pt},
        for nodewalk={load=temptoksa}{my width/.register=tempdima, cmeas/.register=tempdimb, rmeas/.register=tempdimc}, 
      }{},
      tempcounta'=0,
      for tree breadth-first={
        align=p{\foresteregister{lmeas}}@{}p{\foresteoption{cmeas}}@{}C{\foresteoption{my width}}C{\foresteregister{wmeas}}p{\foresteoption{rmeas}},
        if closed={
          content/.process={ ROSl+tt= ? w  w2 {close with}{!u.close}{}{}{[##1]}{ && ##1  && ##2} },
        }{
          tempcounta'+=1,
          content/.process={ ORO OSl+tt= ? w ROO ? w2  w5 {content}{tempcounta}{world}{just}{}{}{[##1]}{check with}{discharge}{checked}{##1##2}{}{##2. & ##5 & ##1 & ##3 & ##4} },
        },
        typeset node,
      }
    },
  },
  discharged/.style={
    checked,
    discharge=\,#1,
  },
  closing/.style={delay={append={[, closed]}}},
}

\begin{document}
\begin{forest}
  claim={\vdash(\Box P\lor \Box Q) \rightarrow \Box(P\lor Q)},
  ml proof,
  [\Box P \lor \Box Q, checked, world=w
    [\lnot\Box(P\lor Q), checked, world=w
      [\lnot(P\lor Q), checked, world=x, just=2$\,\lnot\Box$
      [\lnot P, world=x, just=3$\,\lnot\lor$
      [\lnot Q, world=x, just=3$\,\lnot\lor$
      [\Box P, world=w, just={1$\,\lor$} [P, world=x, just=6$\,\Box$, close={4,8}]]
        [\Box Q, world=w, just={1$\,\lor$} [Q, world=x, just=7$\,\Box$, close={5,9}]]
      ]]]
    ]
  ]
\end{forest}

\bigskip

Suppose line 9 was absent:

\begin{forest}
  claim={\vdash(\Box P\lor \Box Q) \rightarrow \Box(P\lor Q)\text{ *}},
  ml proof,
  [\Box P \lor \Box Q, checked, world=w
    [\lnot\Box(P\lor Q), checked, world=w
      [\lnot(P\lor Q), checked, world=x, just=2$\,\lnot\Box$
      [\lnot P, world=x, just=3$\,\lnot\lor$
      [\lnot Q, world=x, just=3$\,\lnot\lor$
      [\Box P, world=w, just={1$\,\lor$} [P, world=x, just=6$\,\Box$, close={4,8}]]
        [\Box Q, world=w, just={1$\,\lor$}, close={5,9}]
      ]]]
    ]
  ]
\end{forest}

\bigskip

But what if line 7 branched?

\begin{forest}
  claim={\vdash(\Box P\lor \Box Q) \rightarrow \Box(P\lor Q)\text{ *}},
  ml proof,
  [\Box P \lor \Box Q, checked, world=w
    [\lnot\Box(P\lor Q), checked, world=w
      [\lnot(P\lor Q), checked, world=x, just=2$\,\lnot\Box$
      [\lnot P, world=x, just=3$\,\lnot\lor$
      [\lnot Q, world=x, just=3$\,\lnot\lor$
      [\Box P, world=w, just={1$\,\lor$} [P, world=x, just=6$\,\Box$, close={4,8}]]
        [\Box Q, world=w, just={1$\,\lor$}[Q \lor R][Q \lor \lnot R]]
      ]]]
    ]
  ]
\end{forest}

\end{document}

three tableaux w/o special remedies

That is, there are bugs. I just don't know which ones they are yet.

Addendum

If a proof is too wide, you can reduce the spacing within the tree. For example, you can add

for tree={inner sep=1pt}

to the tree's preamble. Or you could reduce the space between columns in the tabulars. However, some proofs will remain too wide and you may not wish to use such reduced spacing. In these cases, turning the proof using sidewaysfigure from the rotating package may be a better option. That's what I'd recommend for the proof added to your question.

proof turned on page

\documentclass[11pt]{article} 
\usepackage{amssymb, amsmath, amstext,array,rotating}
\usepackage[linguistics]{forest}
\newcolumntype{C}[1]{>{\centering $}p{#1}<{$}}
\forestset{
  declare toks register={claim},
  declare autowrapped toks={just}{},
  declare toks={close}{},
  Autoforward={close}{closing},
  declare autowrapped toks={world}{},
  declare boolean={align me}{0},
  declare dimen={my width}{0pt},
  declare dimen register={lmeas},
  lmeas/.pgfmath=width("99."),
  declare dimen ={rmeas}{0pt},
  rmeas/.pgfmath={width("[99.]")},
  declare dimen register={wmeas},
  wmeas/.pgfmath=width("$w$"), 
  declare dimen={cmeas}{0pt},
  cmeas/.pgfmath=width("\ensuremath{\checkmark}"),
  claim=,
  declare toks register={check with},
  check with={\ensuremath{\checkmark}}, 
  declare toks register={close with},
  close with={\times}, 
  declare autowrapped toks={discharge}{},
  declare boolean={checked}{0},
  declare boolean={closed}{0},
  ml proof/.style={
    for tree={
      math content,
    },
    for root=align me,
    before typesetting nodes={
      if claim={}{}{
        replace by/.process={Rw{claim}{[##1, math content, append]}},
        no edge,
        before computing xy={l'=2\baselineskip},
      },
    },
    for root={align me},
    where n children>=2{
      for children={align me}}{},
    before packing={
      where n children=1{!1.no edge, before computing xy={!1.l'=\baselineskip},}{},
      where align me={%
        tempdima/.max={>{OOw2+d}{max x}{min x}{##1-##2}}{%
          walk and save={temptoksa}{current,
             until={> O_=!{n children}{1}}{first}}%
        },
        tempdimb/.max={>{ROO?w2+P}{check with}{discharge}{checked}{width("##1##2")}{0pt}}{%
          load=temptoksa%
        },
        tempdimc/.max={>{OSl+tt=?w+P}{just}{}{0pt}{width("[##1]")}}{%
          load=temptoksa%
        },
        if tempdimb={0pt}{}{tempdimb'+=2.5pt},
        for nodewalk={load=temptoksa}{my width/.register=tempdima, cmeas/.register=tempdimb, rmeas/.register=tempdimc}, 
      }{},
      tempcounta'=0,
      for tree breadth-first={
        align=p{\foresteregister{lmeas}}@{}p{\foresteoption{cmeas}}@{}C{\foresteoption{my width}}C{\foresteregister{wmeas}}p{\foresteoption{rmeas}},
        if closed={
          content/.process={ ROSl+tt= ? w  w2 {close with}{!u.close}{}{}{[##1]}{ && ##1  && ##2} },
        }{
          tempcounta'+=1,
          content/.process={ ORO OSl+tt= ? w ROO ? w2  w5 {content}{tempcounta}{world}{just}{}{}{[##1]}{check with}{discharge}{checked}{##1##2}{}{##2. & ##5 & ##1 & ##3 & ##4} },
        },
        typeset node,
      }
    },
  },
  discharged/.style={
    checked,
    discharge=\,#1,
  },
  closing/.style={delay={append={[, closed]}}},
}

\begin{document}
\begin{sidewaysfigure}
\begin{forest}
claim={\Box P\lor\Box Q\vdash\Box(\Diamond P\land\Diamond Q)},
ml proof,
% for tree={inner sep=0pt},
[\Box P\lor\Box Q, world=w, checked
 [\lnot\Box(\Diamond P\land\Diamond Q), world=w, checked
  [\lnot(\Diamond P\land\Diamond Q), world=v, checked, just={2 $\lnot\Box$}
   [\lnot\Diamond P, world=v, just={3 $\lnot\land$}
    [\Box P, world=w, just={1 $\lor$}
     [P, world=w, just={6 $\Box$}
      [\lnot P, world=w, just={4 $\lnot\Diamond$}, close={10,\,14}]
     ]
    ]
    [\Box Q, world=w, just={1 $\lor$}
     [Q, world=w, just={7 $\Box$}
      [Q, world=v, just={7 $\Box$}
       [\lnot P, world=w, just={4 $\lnot\Diamond$}
        [\lnot P, world=v, just={4 $\lnot\Diamond$}]
       ]
      ]
     ]
    ]
   ]
   [\lnot\Diamond Q, world=v, just={3 $\lnot\land$}
    [\Box P, world=w, just={1 $\lor$}
     [P, world=w, just={8 $\Box$}
      [P, world=v, just={8 $\Box$}
       [\lnot Q, world=w, just={5 $\lnot\Diamond$}
        [\lnot Q, world=v, just={5 $\lnot\Diamond$}]
       ]
      ]
     ]
    ]
    [\Box Q, world=w, just={1 $\lor$}
     [Q, world=w, just={9 $\Box$}
      [\lnot Q, world=w, just={5 $\lnot\Diamond$}, close={13,\,17}]
     ]
    ]
   ]
  ]
 ]
]
\end{forest}
\end{sidewaysfigure}
\end{document}
6
  • 1
    Amazing! I'll play around with this later today to learn how it works and see if I can't fish out any bugs. Thank you so so much for your help.
    – poot
    Dec 11, 2020 at 15:09
  • Forgive me, I don't know the proper protocol for engaging answers. I've updated my question with an example of a bug.
    – poot
    Dec 12, 2020 at 8:17
  • @poot Hmm... That's not really a bug. I agree the output is unacceptable, but it's wrong in a way my code didn't try to address ;). Have you considered turning the tree so it's in landscape mode? That would be my first thought, but may not be what you need.
    – cfr
    Dec 13, 2020 at 6:37
  • @poot I will try playing with it. I can't do it right now, but will try to get to it shortly.
    – cfr
    Dec 13, 2020 at 6:38
  • Another question: it seems one cannot employ some features in the justifications, like hspace or, more importantly, mathcal. Would you please help me understand why this is the case?
    – poot
    Jan 23, 2021 at 5:31

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .