# How to typeset axiomatic logic proofs in list form?

I'm trying to typeset some axiomatic logic proofs in list form. I have tried to define a new environment such that I could combine the proof environment of the amsthm package with a table, resulting in the ugly picture underneath.

What I would like to achieve is that the lines of the proof are automatically numbered (I've tried to do that with a counter), that they have the same indentation as an enumeration, that the descriptions are nicely aligned (that's why I tried to use a table) and that the QED symbol is placed properly.

How can I do that?

\documentclass{article}
\usepackage{array,amsthm,amssymb,amsmath}
\newcounter{rowcount}
\newenvironment{listproof}
{\setcounter{rowcount}{0}
\begin{proof}\mbox{}\\\\
\begin{tabular}{@{\stepcounter{rowcount}(\alph{rowcount})\hspace*{\tabcolsep}}ll}}
{\end{tabular}\end{proof}}
\newtheorem{thm}{Theorem}
\newcommand{\necc}{\ensuremath{\mathbin{\Box}}}
\newcommand{\limpl}{\ensuremath{\mathbin{\rightarrow}}}
\newcommand{\theo}{\ensuremath{\mathrel{\vdash}}}

\begin{document}
\begin{thm}
$\theo\phi\limpl\psi \implies \theo\necc\phi\limpl\necc\psi$.
\end{thm}

\begin{listproof}
$\phi\limpl\psi$ & given\\
$\necc(\phi\limpl\psi)$ & N, a\\
$\necc(\phi\limpl \psi)\limpl(\necc \phi\limpl\necc\psi)$ & $[\phi/p, \psi/q]\,$K\\
$\necc{\phi}\limpl\necc{\psi}$ & MP, b, c\\
\end{listproof}
\end{document}


You were almost there.

\documentclass{article}
\usepackage{array,amsthm,amssymb,amsmath,enumitem}

\newcounter{rowcount}
\newenvironment{listproof}
{\setcounter{rowcount}{0}%
\begin{proof}\mbox{}\\*
\begin{tabular}[b]{
@{%
\stepcounter{rowcount}%
%     \makebox[\dimexpr\leftmargini-\labelsep][r]{(\alph{rowcount})}\hspace{\labelsep}}
\makebox[\leftmargini][r]{(\alph{rowcount})\hspace{\labelsep}}}
ll@{}
}%
}
{\end{tabular}\end{proof}}

\newtheorem{thm}{Theorem}
\newcommand{\necc}{\mathbin{\Box}}
\newcommand{\limpl}{\mathbin{\rightarrow}}
\newcommand{\theo}{\mathrel{\vdash}}

\begin{document}
\begin{thm}
$\theo\phi\limpl\psi \implies \theo\necc\phi\limpl\necc\psi$.
\end{thm}

\begin{listproof}
$\phi\limpl\psi$ & given\\
$\necc(\phi\limpl\psi)$ & N, a\\
$\necc(\phi\limpl \psi)\limpl(\necc \phi\limpl\necc\psi)$ & $[\phi/p, \psi/q]\,$K\\
$\necc{\phi}\limpl\necc{\psi}$ & MP, b, c\\
\end{listproof}

\begin{enumerate}[label=(\alph*),noitemsep]
\item test
\item test
\item test
\item test
\end{enumerate}

\end{document}


With \begin{tabular}[b] the QED symbol will be aligned with the bottom row of the tabular. The labels are set in a box \leftmargini wide, the same used for first level lists.

I removed the useless \ensuremath and also the blank line; you may possibly use \\*[1ex] if you want some more vertical space. The * ensures no page break can intervene.

• Perfect! Thank you for the hints about the smaller issues too. – Jeroen Apr 11 '16 at 13:59
• I've noticed today that the first column of the table isn't perfectly aligned with the labels of an enumeration. Put a small enumeration \begin{enumerate}[(a), noitemsep] \item test \end{enumerate} before the listproof (of course, add \usepackage[shortlabels]{enumitem} to the preamble) and see for yourself. Can this be fixed somehow? – Jeroen Apr 23 '16 at 16:35
• @Jeroen Fixed: the \hspace{\labelsep} had to go inside the box, not after it. – egreg Apr 23 '16 at 16:45
• Correct, I should have seen that myself. Thanks! – Jeroen Apr 23 '16 at 16:56