☰

更新 1

tag-icon • tag-icon tikz-trees forest trees qtree prooftrees
更新 1

这是我在 TeX.SE 上的第一个问题。

我需要排版几十棵模态逻辑树；与典型的一阶树不同，这些树需要额外的索引来指示模型中的世界。

这是一个典型的例子，不雅地强制使用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}

其结果如下：

在此处输入图片描述

其中偏移量瓦'沙X's 就是所讨论的指数。

显然，这只是一个临时解决方案。它确实传达了要点，但对于专业出版而言，这非常不方便且不可接受，而专业出版才是其目标。

现在，对于非模态（命题和谓词逻辑）树，我非常喜欢prooftrees。 这也是我在其他所有事情中都使用的方法。 以下是使用 的同一棵树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}

其结果如下：

在此处输入图片描述

请注意，我已将替换功能用于世界索引，但这并不理想。（行号和对齐方式也受到影响，但我对此不太担心。）考虑到所有因素，我对这种方法非常满意；但如果可能的话，我真的希望为索引设置一个单独的列，因为这就是我们手动制作树的方式。我尝试将索引放在对齐方式中，这对于没有分支的树很有效，但显然这对左分支或后续分支仍然不起作用。

我知道这在类似tikz或中是可能的forest，但我承认我仍然觉得这些包相当强大。我怀疑答案这里是必需的，但我希望有一个更直接的解决方案。我没有技术专长来实现更优雅的解决方案，所以我很感激任何提供的帮助。谢谢！

更新 1

基于这个答案我针对上述树设计了以下解决方案，使用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}

其结果如下：

在此处输入图片描述

这好多了！但是，这种方法无法适应具有多个不并行运行的分支的更复杂的树，而这正是我最终想要做的。（在上面的代码中，我还包括了一些我不了解如何解决的基本问题[这里没有显示]。）

我还没有尝试编写更复杂的树，但我可以分享一些我感兴趣的排版树的例子。

这些例子都取自 Girle 的模态逻辑与哲学（2000）。第一个例子很好地对齐了：

在此处输入图片描述

[来源：Girle (2000)，第 25 页]

与接下来的几个例子相比，他放弃了良好的对齐：

在此处输入图片描述

[来源：Girle (2000)，第 184 页]

在此处输入图片描述

[来源：Girle (2000)，第 185 页]

关于上述示例，经过一番思考，我认为我不再关心分别与左边缘和右边缘对齐的行号和注释，就像prooftrees我原来的树和更新的尝试一样。我认为我更喜欢附加到各个公式的行号和注释。重要的是公式、索引等。与同一分支上的其他实例对齐。

另外，我注意到，对于二维和不可能世界语义，需要一个额外的索引；但我想如果我能解决一个索引的问题，那么我就可以将两个索引配对在一起，并在它们之间留出一点空间。

我怀疑解决方案可能是这个很棒的答案。但无论那里发生什么，目前都远远超出了我的理解范围，而且我不知道如何使它适应我的目的。

我非常感谢所有帮助！

更新2

cfr 的解决方案在很多情况下都很有效。再次感谢！

然而，如下图所示的大树会带来一些问题：

\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}

显然flushleft/noindent是不够的，而且tiny有点矫枉过正。压缩水平空间或垂直偏移右分支都是可以接受的解决方案，但我（目前）还不太了解实现它们的方法。有什么建议吗？

答案1

以下提供自动编号。close=<arg>添加闭包、checked检查、discharged=<arg>应检查<arg>（未经测试，因为这些示例中未使用）、world=<arg>添加世界、just=<arg>添加理由。 ml proof 在forest序言中触发样式并claim=<arg>设置证明语句/定理。

除了初始语句（如果有）之外，所有节点都是tabular具有 5 列的：

  1. 行号（自动）
  2. 检查/释放变量（checked，discharged=<arg>
  3. 伍夫
  4. 世界 （world=<arg>）
  5. 理由（just=<arg>除了将为close=<arg>子节点中附加的闭合标记产生理由之外。

第二、第三和第五列的宽度根据从只有一个子节点到下一个分支的节点内容进行调整。第一列和第四列的宽度设置为大致预期的宽度，并且不会进一步调整。（如果您有很多这样的列，编译时间很快就会成为一个问题。因此，除非您真的需要，否则我会避免将所有列设置为最佳宽度。这样做的编码很简单，但 --- 至少无Sašo --- 每次额外的调整都需要对 tableau 的各个部分进行解析。

问题中的例子不需要特殊的诡计。但是，3 个样本量对于整个人群来说信心不足。（由于我从未使用过模态逻辑的表格，情况更加糟糕。）

买者自负 ...

% 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}

三个没有特殊补救措施的场景

也就是说，是错误。我只是还不知道它们是什么。

附录

如果校样太宽，您可以减少树内的间距。例如，您可以添加

for tree={inner sep=1pt}

到树的序言。或者您可以减少列之间的空间tabular。但是，有些证明仍然太宽，您可能不希望使用这种减小的间距。在这些情况下，使用包sidewaysfigure中的证明rotating可能是一个更好的选择。这就是我建议添加到您的问题中的证明。

证明已翻页

\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}

相关内容