Peter Selinger: LaTeX macros for Fitch style natural deduction

LaTeX macros for Fitch style natural deduction

Fitch-style natural deduction is a system for writing proofs in propositional logic and predicate logic. We use it in our logic courses at the University of Ottawa. This is a set of easy-to-use LaTeX macros that I wrote for making handouts for my classes.

With these macros, one can typeset natural deduction proofs in Fitch style, as in the following example:

\begin{nd}
  \hypo {1} {\forall y \neg P(y)}
  \open
  \hypo {2} {\exists x P(x)}
  \open[u]
  \hypo {3} {P(u)}
  \have {4} {\forall y \neg P(y)}  \r{1}
  \have {5} {\neg P(u)}            \Ae{4}
  \have {6} {\bot}                 \ne{3,5}
  \close
  \have {6a}{\bot}                 \Ee{2,3-6}
  \close
  \have {7} {\neg \exists x P(x)}  \ni{2-6a}
\end{nd}

The output is shown on the left, and the corresponding LaTeX code on the right.

News

Version 0.6, Sep 5, 2023. The fitch package is now maintained by Richard Zach, University of Calgary. It's available from GitHub and CTAN.

Version 0.5, Feb 8, 2005. The ability to handle multi-line formulas was added.

Download

GitHub: https://github.com/OpenLogicProject/fitch
CTAN: https://ctan.org/pkg/fitch
Previous versions: fitch-0.4.tgz, fitch-0.5.tgz.

Version

Version 0.6, Sep 5, 2023

Author

Peter Selinger, Dalhousie University (original author)
Richard Zach, University of Calgary (current maintainer)

LICENSE

This work may be distributed and/or modified under the conditions of the LaTeX Project Public License, either version 1.3 of this license or (at your option) any later version. The latest version of this license is in https://www.latex-project.org/lppl.txt and version 1.3c or later is part of all distributions of LaTeX version 2008 or later.

Back to Homepage:

Peter Selinger / Department of Mathematics and Statistics / Dalhousie University
selinger@mathstat.dal.ca / PGP key