3. Natural deduction proofs

Natural deduction and sequent proofs (Gentzen style)

  • The best, most flexible package, is surely now 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.

    Two ways of aligning sequents provided by Bussproofs

    There is an add-on by Richard Zach for adding vertical or diagonal lines of dots for “missing” parts of proofs, see here.

  • An older, less flexible but 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

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 an 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).
  • And another package, new in 2014, for setting proofs in which subproofs have boxes round them is logicproof which outputs proof in the style of e.g. Logic in Com­puter Science by Huth and Ryan.

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 19 October 2014

One Response to 3. Natural deduction proofs

Leave a Reply

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