You probably already know about the two packages that you can use to typeset Fitch-style natural deducation proofs in LaTeX. Here's another, which you may be interested in if you use Barker-Plummer, Barwise, and Etchemendy's popular logic text Language, Proof, and Logic. It makes proofs like this:
I've taken Etch's original style file and Dave's documentation, put it together in standard docstrip format, cleaned up the code a bit and added a few features. You can download the beta from
I've also attached the documentation here.
Please file any problem reports on github, if you could, or email me directly. (The comment system here is unreliable.) I'm hoping to put it on CTAN in a month.
UPDATE: CTAN upload done.