Lemmon-style natural deduction proofs in LaTeX

Recently I had to typeset a natural deduction argument in \LaTeX. I looked around for a package that does it, but couldn’t find any (which doesn’t mean that it’s not there somewhere). So, I wrote one myself. It doesn’t do fancy things, but at least it figures out the width the various columns should have by itself and a few other things that are described in the ‘manual‘ (which, admittedly, sounds a bit grand).

So, in case you have always wanted a package that typesets natural deduction proofs, you’re very welcome to try it. The file can be downloaded here (you should use “save link as”, since opening it with Word et al. will change the formatting). Currently, the file has a “.doc” extension, since WordPress did not let me upload it with its proper one. It should be renamed to “ND.sty” (lose the “.doc” extension). Then you can simply copy the file either to your local texmf folder or to the folder of the document in which it is to be used, and load the package with “\usepackage{ND}” in the preamble of your document.

A word of caution. I’m not a \LaTeX expert and I haven’t extensively tested the  package (unfortunately, I don’t need to typeset too many natural deduction proofs), so it probably does some things it shouldn’t. In particular, it may give you unexpected (and unexplained) error messages. But that should be about it. Happy \TeXing.

12 comments

  1. Yes, thanks for reminding me of the LaTeX for Logicians site where they have three packages for typesetting Fitch-style proofs. I should have said that I unsuccessfully looked for a package for typesetting Lemmon-style natural deduction proofs (it always takes me a while to figure out how to introduce assumptions so that I can lose them in the right order).

  2. Graeme Forbes: Modern Logic, perhaps? It has the rules in Lemmon-style printed on the inside of the front and back cover for quick reference. Although I don’t have it here, I suppose Lemmon: Beginning Logic would be a natural place to start as well. I don’t know any places that assume that you’re already familiar with Fitch-style systems and build on that, however.

  3. Can you start a proof at some list number other than (1)? In particular, I want to write out one half of my proof, discuss some implications, then continue with that same proof.

  4. Thanks for your question. You have figured this out yourself in the meantime, so I leave this reply merely for the sake of completeness.
    What needs to be done is to set the internal counter @NDlines to an appropriate value. In order to avoid having to deal with “@” expressions in the document body, I would suggest adding the following command definition to the end of the style-file:
    \newcommand\linenumber[1]{\setcounter{@NDlines}{#1-2}\refstepcounter{@NDlines}}
    You can then use, e.g., “\linenumber{26}” before an \ndl command which will then set line number 26.

  5. Hi Alex,

    Thanks for creating this package! It’s been really useful for me.

    Is there any way to replace a line number or dependency number with a letter? For instance, I wish I could use the \linenumber command to manually change a line number to (n) or (n-1). E.g.:

    1,2 (n) P & Q &I

    Or have a line with something like this:

    n-1 (n) P & Q &I

    I wouldn’t expect the package to be able to automatically increment the counter in such a case, but it would be nice to be able to manually change a couple of lines at the end of a proof.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s