CTAN Comprehensive TeX Archive Network

Directory macros/latex/contrib/fitch



macros for Fitch style natural deduction


Fitch-style natural deduction is a system for writing proofs in propositional logic and predicate logic. This is a set of easy-to-use macros originally written by Peter Selinger. It is used, e.g., in the various versions of forall x by PD Magnus (e.g., the original, Cambridge, and Calgary versions)

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

  \hypo {1} {\forall y \neg P(y)}
    \hypo {2} {\exists x P(x)}
      \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}
    \have {6a} {\bot}                 \Ee{2,3-6}
  \have {7} {\neg \exists x P(x)}     \ni{2-6a}

The output is shown above, and the corresponding code below.


v1.0-beta, October 15, 2023 Adds outerline option; improves \by; fixes spacing when using tabular

v1.0-alpha, Sept 30, 2023 This is an alpha release that adds key-value options to the package and commands for customization. It is not fully compatible with the 0.x versions (see documentation). Please report any issues or suggestions.

v0.6, Sept 4, 2023. Updated the documentation and license (from GPL to LPPL). The code is essentially unchanged.

v0.5, Feb 8, 2005. The ability to handle multi-line formulas was added.


The package is available on CTAN as fitch.

The code is maintained on Github.

Related packages

  • logicproof: natural deduction with boxed subproofs in the style of Huth and Ryan's Logic in Computer Science.
  • lplfitch: Fitch-style proofs in the format used in Barwise & Etchemendy's textbook Language, Proof, and Logic.
  • natded: natural deduction proofs in the style of Jaśkowski, or that of Kalish and Montague.
  • synproof: natural deduction proofs in the style of Gamut's Logic, Language, and Meaning.

Additional packages for proofs, including Johan Klüwer's, are available at a page maintained by Alex Kocurek


Peter Selinger, Dalhousie University, is the original author.

Richard Zach, University of Calgary, it the current maintainer.


Copyright (C) 2002-2023 Peter Selinger

This work may be distributed and/or modified under the conditions of the 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


and version 1.3c or later is part of all distributions of version 2008 or later.

Download the contents of this package in one zip archive (290.3k).

fitch – macros for Fitch-style natural deduction

The package provides macros for typesetting natural deduction proofs in Fitch style, with subproofs indented and offset by scope lines.

Bug trackerhttps://github.com/OpenLogicProject/fitch/issues/
Version1.0 2023-12-17
LicensesThe Project Public License 1.3
Copyright2002–2023 Peter Selinger
MaintainerRichard Zach
Contained inTeX Live as fitch
MiKTeX as fitch
Guest Book Sitemap Contact Contact Author