在 LaTeX 中排版逻辑证明答案

【问题标题】：Typesetting logic proofs in LaTeX在 LaTeX 中排版逻辑证明
【发布时间】：2010-03-01 15:54:53
【问题描述】：

我正在尝试在 LaTeX 中排版一些基本的逻辑证明。我需要一个多列布局，并且我需要右侧编号的行。我想重置每个证明的编号。输出应如下所示：

1) (x)¬F      A

2) (Ex)F

3) ...

最简单的方法是什么？ enumerate 似乎不是一个好主意，因为它不会喜欢多列的东西。我也需要一切都处于数学模式。

有没有简单的方法可以做到这一点？

[编辑] 到目前为止，这是我设法做到的，但它远非优雅。

\begin{minipage}{\linewidth}
\boldmath \center{$ \forall x \neg F \to \neg \exists x F $} \unboldmath

\begin{math}
  \begin{array}{llr}
    1. &\forall x \neg F &   \\
    2. &\exists x F & A  \\
    3. &F[\alpha / x ] & ES 2  \\
    4. &\neg F[\alpha / x] & US  \\
    5. &\exists x F \to F[\alpha / x ] & CP 2,4  \\
    6. &\neg \exists x F & TI 4,5 
  \end{array}
\end{math}
\end{minipage}

理想情况下，我想要自动编号步骤并使“标题”行更容易...

【问题讨论】：

minipage 是这样的，当我把这一切都放在一个 multicols 中时，“标题”不会与证明分开。
如果对这个问题投反对票的人解释了它的问题所在，我将不胜感激。请记住，它是在 tex.stackexchange.com 存在之前被询问的......

标签： latex

【解决方案1】：

请参阅包装以获取 Fitch 式样张 here。您根本不需要任何子证明。 LaTeX for Logicians 还涵盖了其他证明方式、逻辑符号等。

【讨论】：

+1: Latex for Logicians 是一个很好的资源，很好地组合在一起。不过，我认为 Alexey M 的建议是如此简短，以至于我更愿意为此任务而不是可避免的导入另一个包。
两个链接现在都断开了。

【解决方案2】：

\newcount\mycount
\def\nextnum{\global\advance\mycount 1 \the\mycount.}
\def\logicx#1{\halign{$\nextnum##$\quad \hfil&$##$\hfil
      &\qquad\hfil##\crcr#1\crcr}\endgroup}
\def\logic{\begingroup \global\mycount 0 \let\\\cr \logicx}

\logic{
    &\forall x \neg F &   \\
    &\exists x F & A  \\ 
    &F[\alpha / x ] & ES 2  \\ 
    &\neg F[\alpha / x] & US  \\ 
    &\exists x F \to F[\alpha / x ] & CP 2,4  \\ 
    &\neg \exists x F & TI 4,5  \\
}

【讨论】：

我想你应该在证明开始时重置\mycount，而不是在每个\logic。
@Vlad: Alexey 的\logic#1 一次排版了整个证明。
@Charles：证明通常包含更多单词，而不仅仅是计算。类似于：“假设 x > 0。设 y = |x| + 1，我们得到：（方程列表）。对于 x
@Vlad：不在形式逻辑中。很明显，这些证明是某种 Hilbert 风格的证明系统（US 我承认 - 它是统一替换），其中诸如“假设 x>0 之类的非正式陈述被转换为内部正式表示。我'希望任何英语讨论都是在证明结尾处进行的注释，指的是步骤编号 1 到 6 的推论。
好吧，开头可能有一些介绍性文字，例如：“我们使用 [1] 中稍微修改的方法”，中间像“这是最难的部分，现在我们只需要证明 X 的 foobarability”。证明不应该太干。

【解决方案3】：

查看amsmath 包文档中的section 3.6。

【讨论】：

我希望每列左对齐，并且我想要一种简单（即自动）的方法来重置每个证明的编号。

【解决方案4】：

抱歉，现在没有 \LaTeX 编译器，所以我的代码可能无法编译或包含愚蠢的错误。

您的线路需要一个新的计数器：

\newcount\logicproofline

然后，你需要一个命令来启动它：

\def\proofline#1{
    \global\advance\logicproofline by 1
    \shoveright{\text{\the\logicproofline}\qquad#1}
}

现在，您需要重新定义 proof 来重置您的计数器：

\AtBeginDocument{
    \let\myoldproof=\proof
    \def\proof{\myoldproof\logicproofline=0\relax}
}

需要重新定义，因为证明与任何计数器都没有关联，因此我们不能将其设为主计数器。

【讨论】：