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.5, Feb 8, 2005. The ability to handle multi-line formulas was added.

## Version

Version 0.5, Feb 8, 2005

## Author

Peter Selinger, University of Ottawa

A similar package by another author is