Typesetting logic proofs in LaTeX

Question

Hi, I'm trying to typeset some basic logic proofs in LaTeX. I need a multiple column layout, and I need the lines numbered on the right. I want to reset the numbering for each proof. The output should look like this:

1) (x)¬F      A

2) (Ex)F

3) ...

What is the easiest way to do this? enumerate doesn't seem a good idea, since it's not going to like the multiple column things. I need everything to be in mathmode as well.

Is there an easy way to do this?

[edit] Here is what I've managed to do so far, but it is far from elegant.

\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}

Ideally I want something that automatically numbers steps and makes the "title" line easier...

Answer 1

Check out section 3.6 of the amsmath package documentation.

Answer 2

Sorry, don't have a \LaTeX compiler now, so my code may be not compileable or contain silly mistakes.

You need a new counter for your lines:

\newcount\logicproofline

Then, you need a command to start it:

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

Now, you would need to redefine proof to reset your counter:

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

The redefinition is needed because proof is not associated with any counter, so we cannot make that one a master counter.

Answer 3

\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  \\
}

Answer 4

See the packages for Fitch-style proofs here. You simply don't need any subproofs. LaTeX for Logicians also covers other proof styles, logical symbols, etc.