真值树中的连词

Question 1

以下代码显示如何定义一个append wffs=<integer>采用整数参数的新样式。它应添加到要括在一起的 wff 的最后一个选项中，并且值应等于要与此 wff 括在一起的其他 wff 的数量。例如，如果您希望将第 3 行和第 4 行的 wff 括在一起，请将其添加append wffs=1到第 4 行的 wff 中。

使用标准just=<whatever>语法来指定理由。例如，append wffs=1, just={1,2,MP}或其他。因此，对于您的示例，您可以编写

                [{Ha}, no line no
                [{Fa}, no line no, my text={6}, just=(5), append wffs=1

这会将两个 wff 括起来并放置(5)在行的右侧。

即使要括起来的 wff 比当前（最终）wff 长，这也应该有效，因为代码使用的forest选项fit to来获取一个包含所有受影响 wff 的框并使用它来绘制括号。

\forestset{
  append wffs/.style={
    before typesetting nodes={%
      for nodewalk={fake=c,*{#1}u}{just=}%
    },
    before drawing tree={
      tikz+/.process={Ow1{name}{%
          \node (##1 append box) [inner sep=0pt, fit to={c*{#1}u}] {};
          \draw (##1 append box.north east) ++(-2.5pt,0pt) -| (##1 append box.south east) -- ++(-2.5pt,0pt);
        }%
      },
      tempdima/.max={>O{max x}}{c*{#1}u},
      for nodewalk/.process={%
        O Rw1+d OOw2+d w3 {proof tree proof line no}{tempdima}{##1+2.5pt}{y}{!*{#1}u.y}{(##1+##2)/2}
        {%
          {name=just ##1}{x'=##2,y'=##3}%
        }%
      },
    },
  },
}

just请注意，这将覆盖为附加的 wff 设置的任何理由，因此为相同的 wff指定非常重要append wffs。

\documentclass[10pt]{article}
\usepackage[edges]{forest}
\usepackage{prooftrees}
\usepackage{amsmath}
\usepackage{mathtools}
\usepackage{newpxtext,newpxmath}
\usepackage{mathastext}
\usepackage[paperwidth=160mm, paperheight=240mm]{geometry}
\geometry
{
  total={120mm,200mm},
}
\forestset{
  branchcomment/.style={
    my text/.style={
      label={[yshift=-5pt]below:{##1}},
      l sep'+=5pt,
    },
  },
  append wffs/.style={
    before typesetting nodes={%
      for nodewalk={fake=c,*{#1}u}{just=}%
    },
    before drawing tree={
      tikz+/.process={Ow1{name}{%
          \node (##1 append box) [inner sep=0pt, fit to={c*{#1}u}] {};
          \draw (##1 append box.north east) ++(-2.5pt,0pt) -| (##1 append box.south east) -- ++(-2.5pt,0pt);
        }%
      },
      tempdima/.max={>O{max x}}{c*{#1}u},
      for nodewalk/.process={%
        O Rw1+d OOw2+d w3 {proof tree proof line no}{tempdima}{##1+2.5pt}{y}{!*{#1}u.y}{(##1+##2)/2}
        {%
          {name=just ##1}{x'=##2,y'=##3}%
        }%
      },
    },
  },
}
\begin{document}
\renewcommand*\linenumberstyle[1]{(#1)}%
\begin{prooftree}
  {
      to prove={\forall x(Fx \rightarrow \lnot Gx),\, \exists x(Hx \wedge Fx) \therefore \exists x(Hx \wedge \lnot Gx)},
      auto move=false,
      single branches=false,
      for tree={s sep'=10mm},
      just sep'=2.5em,
      close with={\ensuremath{\bigtimes}},
      branchcomment,
  }
  [{\forall x(Fx \rightarrow \lnot Gx)},just={(Ön)}, line no override={3}
    [{\exists x(Hx \wedge Fx)},just={(Ön)}, line no override={2}
      [{\lnot \exists x(Hx \wedge \lnot Gx)},just={($\lnot$Sn)}, line no override={1}
        [{\forall x \lnot (Hx \wedge \lnot Gx)},just={(1. N.D.K)}, line no override={4}
          [{Ha \wedge Fa},just={(2. Özelleme)}, line no override={5}
            [{Fa \rightarrow \lnot Ga}, just={(3. Özelleme)}, line no override={6}
              [{\lnot (Ha \wedge \lnot Ga)},just={(4. Özelleme)}, line no override={7}
                [{Ha}, no line no
                [{Fa}, no line no, my text={6}, just=(5), append wffs=1
                    [{\lnot Fa}, no line no, close]
                    [{\lnot Ga}, no line no, my text={7}
                      [{\lnot Ha}, no line no, close]
                      [{Ga}, no line no, close]]]]]]]]]]]
\end{prooftree}
\end{document}

目前，如果您做了一些“奇怪的”事情，例如将论证居中或切换它们的锚点，east或者将论证放在树的另一侧，这将失败。但是，它“应该”可以合理地稳健地适用于与您的示例大致相同的表，即使您append wffs在同一棵树中使用多个表、括号多个 wff 或括号长度不同的 wff。

Answer