3. Natural deduction proofs

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.

    Two ways of aligning sequents provided by Bussproofs

  • A similar package is ebproof (Emmanuel Beffara, 2015).
  • More recently still, there is another package, which is designed to be even more flexible: prftree (Marco Benini, 2016).
  • 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.

    A derivation of one of De Morgan’s Laws, set using 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.

    Using ebproof and cancel

    Using ebproof and cancel

For Fitch-style layouts, there are five packages

  • 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.

Set using Klüwer’s version of fitch.sty

  • 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.)
  • 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).

For Lemmon-style proofs

  • 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 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.

Links checked 23 January 2016

One Response to 3. Natural deduction proofs

  1. With so many versions of “natural deduction” lying around, and differences in laying them out on a page or screen, has there been any solid attempt to define a generic presentation of proofs, that a LaTeX package could present in any of various styles?

    I have the beginnings of a home-grown one, but it’s a long way from being ready for prime time. What else exists of this kind?

Leave a Reply

Your email address will not be published. Required fields are marked *