Typesetting Fitch-style proofs with a computer is generally a difficult task. This page describes a LaTeX style I made for use in my doctoral thesis.
News: My latest paper, "Natural deduction for belief at most", contains lots of examples of the package in use; click here to download: PDF.
There is another LaTeX package that does the same, written by Peter Selinger, available here. You might want to compare the two -- since both packages are free, the choice is real! In terms of output, there is not much difference between the two; here is the example proof on Selinger's page, typeset using my macros:
The proof was typeset using the following code.
\begin{equation*}
\begin{fitch}
\fh \forall y\lnot P(y) \\
\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*}
Notable differences between this and Selinger's macros include
fitch* for unnumbered lines/manual numbering)
\open ... \close parts, subproofs are indicated with
sequences of \fa (for vertical lines) and \fh (for hypotheses)
Also note that the package automatically loads the packages
mdwtab,latexsym,amsmath,amsfonts, and ifthen,
of which mdwtab and ifthen are essential. They should be included
in every recent LaTeX distribution.
I find the input method using my macros to be quite practical in daily
use. In particular, the indentation in the source file that results
from writing \fa\fh etc. matches the subproof structure, so you get
an indication of proof structure in the source for free. Then again,
had I known about Selinger's package, I probably would never have
bothered to write my own, but I didn't at the time, so I did.
There is no documentation for the package apart from the comments in the style file itself; for many writers, this will be good enough, but I will add real documentation here before long.