How to typeset axiomatic logic proofs in list form?

Question

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}

Answer 1

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.