格式化逻辑 (PD) 推导

Question

我正在尝试格式化 PD 派生，但无法很好地显示子派生。本质上，我想实现的是：

1 | P          Assumption
2 | Q          Assumption
  ------------
3 | P v Q      1, 2 vI
4 | | P        A / vE
  | --------
5 | | R
6 | R

以上内容全是废话，但它显示了我需要的格式。基本上，我需要一列行号，后面跟着一条垂直线、一条水平线（表示假设（“A” 也表示假设），第三列解释我使用的推导规则和相应的行号。如果没有子推导，我可以用这样的表格来做：

\begin{tabular}{l | l l}
  1 & P & Assumption \\
  2 & Q & Assumption \\ [0.5ex] \cline{2-2} \\ [-1.9ex]
  3 & P v Q & 1, 2 vI \\
\end{tabular}

更详细地说，垂直条和其相关的水平条应该连接起来，并且子派生的垂直条应该间隔开，以便它们非常接近位于其上方行的第一个字符下方。我考虑过在整个表格中为每个子派生创建一个新表格，但我觉得这会弄乱行号，因为它只占用一个单元格。任何关于我应该如何布局的建议都将不胜感激。

这是所需布局的图像（由 Gonzalo Medina 添加，来自评论中链接的图像）：

Answer 1

网站LaTeX for logicians提到了各种可用的包；以下示例是使用fitch.sty由 Johan Klüwer 编写（该包不​​在 CTAN 上，但您可以按照我提供的链接下载它）。为了获得所需的水平规则，我定义了一个\fgh类似于原始\fh命令的命令；的强制参数\fgh给出了规则长度：

\documentclass{article}
\usepackage{fitch}

\newcommand{\fgh}[1]{\fvline%
  \makebox[0pt][l]{{%
      \raisebox{-1.4ex}[0pt][0pt]{\rule{#1}{\arrayrulewidth}}}}%
  \hspace*{\fitchindent}}
\begin{document}

\begin{equation*}
  \begin{fitch}
    \fgh{14.5em} \forall y\lnot P(y)    & Assumption \\
    \fa\fh \exists xP(x)        &  \\
    \fa\fa\fitchmodalh{u}  P(u) & \\
    \fa\fa\fa \forall y\lnot P(y) & R, 1                \\
    \fa\fa\fa \lnot P(u)          & $\forall$E, 4       \\
    \fa\fa\fa \bot                & $\lnot$E, 3,5       \\
    \fa\fa \bot                   & $\exists$E, 2, 3--6 \\
    \fa \lnot\exists xP(x)        & $\lnot$I, 2--7
  \end{fitch}
\end{equation*}

\end{document}

以下是图中扣除的代码：

\documentclass{article}
\usepackage{graphicx}
\usepackage{fitch}

\newcommand\Impl{\mathbin{\rotatebox[origin=c]{270}{$\cap$}}}
\newcommand{\fgh}[1]{\fvline%
  \makebox[0pt][l]{{%
      \raisebox{-1.4ex}[0pt][0pt]{\rule{#1}{\arrayrulewidth}}}}%
  \hspace*{\fitchindent}}

\begin{document}

\begin{equation*}
  \begin{fitch}
    \fa\forall x (Fx \vee Rx)    & Assumption \\
    \fa\forall x (Fx \Impl Wx)    & Assumption \\
    \fgh{22em} \forall x (Rx \Impl Px) \land \forall x (Px \Impl Wx) & Assumption  \\
    \fa Fa \vee Ra & 1,$\forall$E \\
    \fa\fgh{8em} Fa & A / $\vee$E \\
    \fa\fa Fa \Impl Wa & 2 $\forall$E \\
    \fa\fa Wa & 5,6 $\Impl\,$E \\
    \fa\fgh{8em} Ra & A / $\vee$E \\
    \fa\fa \forall x (Rx \Impl Px) & 3 $\land$E \\
    \fa\fa Ra \Impl Pa & 9 $\forall$E \\
    \fa\fa Pa & 8,10 $\Impl\,$E \\
    \fa\fa \forall x (Px \Impl Wx) & 3 $\land$E \\
    \fa\fa Pa \Impl Wa & 12 $\forall$E \\
    \fa\fa Wa & 11,13 $\Impl\,$E \\
    \fa Wa & 4,5--7,8--14 $\vee$E \\
    \fa\forall x Wx & 15, $\forall$I
  \end{fitch}
\end{equation*}

\end{document}