在 Latex 中编写自然演绎证明

Question

在有人问之前，我已经检查了其他问题，但证明的风格似乎略有不同，我应该遵守我所使用的惯例。

我的问题是如何在 Latex 中创建如附图所示的证明：

（抱歉灯光不好，我来晚了）

这是不是Fitch 风格的证明，因为没有缩进，或者那些条。我可以使用有序列表，但我想知道是否有一个包允许我自动缩进行和旁注/操作，因为这对于原始列表来说可能很麻烦（尽管如果有人对此有任何指点，我会很高兴听到他们）。

有什么想法吗？我很惊讶我找不到任何使用这种证明的软件包，这是门德尔松《数理逻辑导论》中使用的风格，所以也许它是老派的。感谢大家提供的任何指导。

Answer 1

另一种解决方案基于listliketab：

\documentclass{article}
\usepackage[showframe]{geometry}
\usepackage{listliketab}

\begin{document}

\storestyleof{enumerate}
\begin{listliketab}%
\newcounter{tabenum}\setcounter{tabenum}{0}
\newcommand{\step}{\refstepcounter{tabenum}\thetabenum.}
\noindent \begin{tabular}{L >{$}l <{$}@{\hskip4em}l}
\multicolumn{2}{c}{$ \vdash P\lor\lnot P $} \\
\step & \lnot(P\land\lnot P) & Hyp \\
\step & P & {Hyp}\\
\step & P\lor\lnot P & 2, $\lor$-introduction \\
\step & \bot & 1, 3, contradiction \\
\step & \lnot P & 2, 4, negation-introduction \\
\step & P\lor\lnot P & 5, $\lor$-introduction \\
\step & \bot & 1, 6, contradiction \\
\step & \lnot\lnot(P\lor\lnot P) & 1, 7, negation-introduction \\
\step & P\lor\lnot P & 8, double negation elimination
\end{tabular}
\end{listliketab}

\end{document} 

Answer 2

您可以基于以下内容构建环境flalign*：

\documentclass{article}
\usepackage{amsmath}
\usepackage{showframe}

\newcounter{formalproofline}
\newenvironment{formalproof}[1]
 {%
  \setcounter{formalproofline}{0}%
  \csname flalign*\endcsname
  &\makebox[0pt][l]{$\displaystyle#1$}
 }
 {\endflalign}
\newcommand{\step}[2]{%
  \\
  \stepcounter{formalproofline}%
  \theformalproofline.\quad & #1 &\qquad& \text{#2}%
}

\begin{document}

\begin{formalproof}{\vdash P\lor\lnot P}
\step{\lnot(P\land\lnot P)}{Hyp}
\step{P}{Hyp}
\step{P\lor\lnot P}{2, $\lor$-introduction}
\step{\bot}{1, 3, contradiction}
\step{\lnot P}{2, 4, negation-introduction}
\step{P\lor\lnot P}{5, $\lor$-introduction}
\step{\bot}{1, 6, contradiction}
\step{\lnot\lnot(P\lor\lnot P)}{1, 7, negation-introduction}
\step{P\lor\lnot P}{8, double negation elimination}
\end{formalproof}

\end{document}

该showframe包仅绘制页面边框，以检查对齐情况。