[Tex/LaTex] Formatting a logical (PD) derivation

spacingtables

I'm trying to format a PD derivation but I'm having trouble getting subderivations to display well. Essentially what I'm trying to accomplish is this:

1 | P          Assumption
2 | Q          Assumption
  ------------
3 | P v Q      1, 2 vI
4 | | P        A / vE
  | --------
5 | | R
6 | R

The above is all nonsense but it shows the format I need. Basically, I need one column for line numbers followed by a vertical line, a horizontal line under assumptions ("A" also means assumption) and a third column explaining the derivation rule I used with the corresponding line numbers. Without the subderivation I can do it with tables like this:

\begin{tabular}{l | l l}
  1 & P & Assumption \\
  2 & Q & Assumption \\ [0.5ex] \cline{2-2} \\ [-1.9ex]
  3 & P v Q & 1, 2 vI \\
\end{tabular}

For a little more detail, the vertical bars and their associated horizontal bar should be connected and the vertical bars for the subderivations should be spaced so they're pretty close to being underneath the first character of the line above it. I thought about making a new table inside the whole table for each subderivation, but I feel like that would mess up the line numbering since it would only occupy a single cell. Any suggestions as to how I should lay this out are greatly appreciated.

Here's an image of the desired layout (added by Gonzalo Medina, from an image linked in a comment):

enter image description here

Best Answer

The site LaTeX for logicians mentions various packages availables; the following example was obtained using fitch.sty by Johan Klüwer (the package is not on CTAN, but following the link I provided you can download it). To get the desired horizontal rule I defined a \fgh command similar to the original \fh command; the mandatory argument for \fgh gives the rule length:

\documentclass{article}
\usepackage{fitch}

\newcommand{\fgh}[1]{\fvline%
  \makebox[0pt][l]{{%
      \raisebox{-1.4ex}[0pt][0pt]{\rule{#1}{\arrayrulewidth}}}}%
  \hspace*{\fitchindent}}
\begin{document}

\begin{equation*}
  \begin{fitch}
    \fgh{14.5em} \forall y\lnot P(y)    & Assumption \\
    \fa\fh \exists xP(x)        &  \\
    \fa\fa\fitchmodalh{u}  P(u) & \\
    \fa\fa\fa \forall y\lnot P(y) & R, 1                \\
    \fa\fa\fa \lnot P(u)          & $\forall$E, 4       \\
    \fa\fa\fa \bot                & $\lnot$E, 3,5       \\
    \fa\fa \bot                   & $\exists$E, 2, 3--6 \\
    \fa \lnot\exists xP(x)        & $\lnot$I, 2--7
  \end{fitch}
\end{equation*}

\end{document}

enter image description here

An here's the code for the deduction in the image:

\documentclass{article}
\usepackage{graphicx}
\usepackage{fitch}

\newcommand\Impl{\mathbin{\rotatebox[origin=c]{270}{$\cap$}}}
\newcommand{\fgh}[1]{\fvline%
  \makebox[0pt][l]{{%
      \raisebox{-1.4ex}[0pt][0pt]{\rule{#1}{\arrayrulewidth}}}}%
  \hspace*{\fitchindent}}

\begin{document}

\begin{equation*}
  \begin{fitch}
    \fa\forall x (Fx \vee Rx)    & Assumption \\
    \fa\forall x (Fx \Impl Wx)    & Assumption \\
    \fgh{22em} \forall x (Rx \Impl Px) \land \forall x (Px \Impl Wx) & Assumption  \\
    \fa Fa \vee Ra & 1,$\forall$E \\
    \fa\fgh{8em} Fa & A / $\vee$E \\
    \fa\fa Fa \Impl Wa & 2 $\forall$E \\
    \fa\fa Wa & 5,6 $\Impl\,$E \\
    \fa\fgh{8em} Ra & A / $\vee$E \\
    \fa\fa \forall x (Rx \Impl Px) & 3 $\land$E \\
    \fa\fa Ra \Impl Pa & 9 $\forall$E \\
    \fa\fa Pa & 8,10 $\Impl\,$E \\
    \fa\fa \forall x (Px \Impl Wx) & 3 $\land$E \\
    \fa\fa Pa \Impl Wa & 12 $\forall$E \\
    \fa\fa Wa & 11,13 $\Impl\,$E \\
    \fa Wa & 4,5--7,8--14 $\vee$E \\
    \fa\forall x Wx & 15, $\forall$I
  \end{fitch}
\end{equation*}

\end{document}

enter image description here

Related Question