Fitch 式谓词逻辑证明

Question

我一直在尝试以 Huth 和 Ryan 的风格排版一些谓词逻辑证明，但我不知道如何以相同的格式显示声明的变量。下面是其中一个证明的示例。

我一直在使用logicproof包来排版我迄今为止的证明，这就是我重新创建上述证明时所拥有的。

有谁知道如何声明语句左边的变量吗？

LaTeX 来源：

\documentclass{article}
\usepackage{logicproof}

\begin{document}
\begin{logicproof}{1}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\
    \begin{subproof}
        P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
\end{document}

Answer 1

您可以增加\subproofhorizspace（我的代码中的额外一对括号使更改保持局部），然后用于\llap变量：

\documentclass{article}
\usepackage{logicproof}

\begin{document}

{
\setlength\subproofhorizspace{2em}
\begin{logicproof}{1}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\\hspace*{-30pt}
    \begin{subproof}
        \llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
}

\end{document}

上述解决方案将改变两侧的水平分离；如果您想要单独控制，这里有一种可能性：

\documentclass{article}
\usepackage{logicproof}

\newlength\subproofhorizspaceright
\setlength\subproofhorizspaceright{\subproofhorizspace}
\makeatletter
\renewcommand{\lp@stop@proof@line}{%
  \whiledo{\value{lp@temp}>\value{lp@nested}}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspaceright}%
  }%
  \whiledo{\value{lp@temp}>0}{%
    \addtocounter{lp@temp}{-1}%
    \lp@amper%
    \hspace*{\subproofhorizspaceright}%
    \vline%
  }%
}
\makeatother

\begin{document}

{
\setlength\subproofhorizspace{2em}
\begin{logicproof}{1}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\\hspace*{-30pt}
    \begin{subproof}
        \llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}
}

\end{document}

现在可以\subproofhorizspace控制左侧的空间和\subproofhorizspaceright右侧的空间。

Answer 2

Gonzalo Medina 的解决方案对于嵌套子证明效果不是特别好。偶然间，我发现只需充分增加嵌套深度即可解决这个问题：

\begin{logicproof}{4}
    \forall x \, (P(x) \to Q(x)) & premise \\
    \forall x \, P(x) & premise \\\hspace*{-30pt}
    \begin{subproof}
        \llap{$x_0\quad$} P(x_0) \to Q(x_0) & $\forall x \, \mathrm{e}$ 1 \\
        P(x_0) & $\forall x \, \mathrm{e}$ 2 \\
        Q(x_0) & $\to \mathrm{e}$ 3, 4
    \end{subproof}
    \forall x \, Q(x) & $\forall x \, \mathrm{i}$ 3--5
\end{logicproof}

我不知道这个解决方案是否稳定。