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

## Web links

A similar package by another author is

## LICENSE

Copyright (C) 2002-2005 Peter Selinger

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.

Back to Homepage:

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