3. Natural deduction and sequent 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

  • Some prefer the following similar package: ebproof (Emmanuel Beffara, 2015/17).
  • 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

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 table than are actually used.)

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

Links checked 28 February 2017

One Response to 3. Natural deduction and sequent 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 *