Proofs

For a document on bussproofs for Gentzen-style proofs, two Fitch-style packages, and also mentioning Lemmon style proofs, see Proofs in LaTeX (Alex Kocurek 2019).

Natural deduction and sequent proofs, Gentzen-style

• The standard package in recent years has been bussproofs.sty (Sam Buss: download the latest version, 1.1, June 2011). Note that there is a LaTeX for Logicians User Guide to bussproofs.sty. There is an add-on by Richard Zach for adding vertical or diagonal lines of dots for “missing” parts of proofs, see here.

  

• Some prefer the following similar package: ebproof (Emmanuel Beffara, 2015-21).
• And there is another package, which is designed to be even more flexible: prftree (Marco Benini, 2016–19).
• For old times’ sake, a much older, less flexible though still highly functional, alternative is provided by proof.sty (Makoto Tatsuta, originally 1990, and now in version 3.1). Again there is an old LaTeX for Logicians User Guide to proof.sty.

  

• If you like to cancel discharged premisses by slashing through a wff, the  cancel  package is for you. Example of it in use here.

  

Natural deduction, Fitch-style

• The best of the older packages is fitch.sty (Johan Klüwer, 2003): there is also a short guide to the first steps of using this package (Ang Tong, 2005), and a demonstration here of how to set the sort of example illustrated below.  But you’ll need to dig inside the style file to see further commands. (Warning: fitch.sty loads a package which is not fully compatible with the standard tabular environment, producing unpredictable side effects; in particular, you need to ensure, if you want to make tables in the same document, that you don’t define more columns in those tables than are actually used.)

• An alternative producing similar output is fitch.sty (Peter Selinger, 2005).
• However, there is now also a new kid on the block, lplfitch, “a package for typesetting Fitch-style proofs a la Language, Proof, and Logic, a logic textbook by Jon Barwise and John Etchemendy.” It was originally written by John Etchemendy, with modifications by Dave Barker-Plummer and Richard Zach: the documentation is good and contains a section compared its output to the varieties of fitch.sty. (See here for how to change the pre-set suite of logic symbols.)
• There is also a package natded.sty  for Jaśkowski-style and Kalish-Montague-style natural deduction (similar to Fitch-style, but with boxes around subproofs).
• logicproof  is another package for setting proofs,  in which subproofs have boxes round them in the style of e.g. Logic in Com­puter Science by Huth and Ryan (Alan Davidson, 2014). See also here for how to declare variables.

Natural deduction, Lemmon-style

• There is a package nd3.sty for setting Lemmon-style proofs, with a short manual (Alex Steinberg 2010: see here for the original post about this).

Other relevant packages

• Another older available package for Gentzen-style proofs: prooftree.sty (Paul Taylor, 1996)
• mathpartir provides the mathpar environment,  a “paragraph mode for formulas”, and also the inferrule macro designed to typeset inference rules (Didier Rémy 2005)
• More flexibly (but probably also requiring a more sophisticated user), there is now Derivation trees with MetaPost (Laurent Méhats, 2010 — these don’t need a knowledge of MetaPost to use).
• The Virginia Lake package offers macros aimed at “writing papers in the area of deep inference and the calculus of structures” but which could be adopted for other proof theoretic purposes.
• The flagderiv package can be used to set the variant kind of “flag” proofs some computer scientists like.
• The logix package (Michael Finney 2001-2022) provides commands for setting Hilbert-style linear proofs.

Updated 25 January 2023