On this page, I have made available a set of LaTeX macros useful for anybody who is typesetting Fitch-style proofs. These macros are based off an earlier set by Peter Selinger, with a few minor additions to better suit use with Barker-Plummer, Barwise and Etchemendy’s Language, Proof and Logic (and, in turn, the PHIL 210 assignments). For example, I have added a ‘Reit’ function, disjunction introduction, etc., as well as the ability to use the ‘AnaCon’ feature devised by the authors of the book. I am aware of the existence of the lplfitch macros, created by LPL’s authors, but I personally found Selinger’s macros to be less clunky and overcomplicated and overall simpler to use.
I don’t feel it’s necessary to write new documentation for my modifications; anything that works according to Selinger’s original documentation should still work; the new additions are meant to obviously mesh with the system as it already existed, and the source code is fairly readable as well, should you find yourself looking for one of the new justifications. You are also, of course, free to modify the macros yourself. I can confirm that the macros work in all the major engines.
© 2002 – 2005 Peter Selinger. © 2018 Daniel Benjamin Miller.
Licensed under the GNU GPL v2 or any later version of the licence.