我如何将步骤与证明树左对齐？

Question

我正在尝试使用 LaTeX 和软件包编写自然演绎，prooftrees从各方面来看，效果都很好。唯一的问题是我希望我的推导步骤左对齐，而不是居中对齐（这在我做真值树时很有意义，但对于 ND 来说就没那么好了）。

\renewcommand*\linenumberstyle[1]{(#1)}
    \begin{prooftree}
      {
        close with={\ensuremath{\ast}},
      }
      [(A \land B), just=P
        [(A \to C), just=P
            [(B \to D), just=P
                [A, just=(1) Simp.
                    [B, just=(2) Simp.
                        [C, just=(2) MP
                            [D, just=(3) MP
                                [(C \land D), just=(6-7) Conj. Intro.
                                    [\text{QED}, just=\text{1, 2, 3, 8, CP.}]
                                ]
                            ]
                        ]
                    ]
                ]
            ]
        ]
      ]
    \end{prooftree}

例子：

Answer 1

prooftrees不适合这种格式的自然演绎证明。我强烈建议不是使用它来达到这个目的。因此，这个答案应该被理解为探索反事实的含义，而不是举例说明现实世界中的某事。

买者自负 ...

请注意，您不需要\text在参数中，just因为这些默认为文本。但是，您需要完成代码才能编译，这需要amstextQED。

我还删除了你的序言行，因为在这个例子中你没有任何封闭的分支，并且永远不会有任何此类证明。这种类型的证明不使用封闭符号。

请注意，最后一行看起来很奇怪。我并不指望QED这是应用推理规则的结果，但是，嘿，这是一个 TeX 网站，而不是逻辑网站，所以就这样吧...

\documentclass{standalone}
\usepackage{amstext}
\usepackage{prooftrees}

\begin{document}
    
\renewcommand*\linenumberstyle[1]{(#1)}
\begin{prooftree}
  {
    wff format={anchor=base west}
  }
  [(A \land B), just=P
    [(A \to C), just=P
        [(B \to D), just=P
            [A, just=(1) Simp.
                [B, just=(2) Simp.
                    [C, just=(2) MP
                        [D, just=(3) MP
                            [(C \land D), just=(6-7) Conj. Intro.
                                [\text{QED}, just={1, 2, 3, 8, CP.}]
                            ]
                        ]
                    ]
                ]
            ]
        ]
    ]
  ]
\end{prooftree}

\end{document}

但同样，很多更好的方法。这种格式非常简单，只需简单操作tabular即可。例如，

\documentclass{standalone}
\usepackage{amstext}
\usepackage{array}
\newcounter{mylineno}
\setcounter{mylineno}{0}
\newcolumntype{W}{!{\stepcounter{mylineno}(\themylineno)}>{$}l<{$}}
\newenvironment{simpleproof}{\setcounter{mylineno}{0}\begin{tabular}{Wl}}{\end{tabular}}

\begin{document}
\begin{simpleproof}
  A \land B & P\\
  A \to C & P\\
  B \to D & P\\
  A & (1) Simp.\\
  B & (1) Simp.\\
  C & (2,4) MP\\
  D & (3,5) MP\\
  (C \land D) & (6,7) Conj.\ Intro.\\
  \text{QED} & (1,2,3,8,CP.)\\
\end{simpleproof}

\end{document}

这并没有实现交叉引用，prooftrees但你似乎并没有使用这个功能。如果你需要编译一个或两个以上的非常简单的证明，那么像这样的东西就可以编译很多更快。prooftrees是慢着因为，基本上forest是慢的。prooftrees使用各种方法来加快速度（forest作者提供），但这仍然是一个费力的过程。如果你需要它，我认为这是值得的。如果你不需要它，你最好使用更直接的方法。