Kevin Klement has done up a prototype of his online natural deduction proof builder/checker that works with the natural deduction system of the Cambridge and Calgary versions of forall x. The system was originally written for UMass’s Intro Logic course, based on Gary Hardegree’s online textbook. Kevin writes:
Earlier I mentioned making some online exercises for the “forall x” book. Not sure how far I’ll follow through with it, but I did go ahead and mock up a proof builder and checker, and sample exercises using them. That seems like the most fun/interesting part. I wasn’t intending to target the Calgary remix, but that’s the version I was looking at when I made it. I realized only later that the proof system and notation is different from the original, but I left it stand. Anyway, I thought I’d post a demo before taking it any further, so others can take a look, make suggestions, and help identify bugs. The user interface was the hardest part, and I’m not entirely happy with it as is, but not sure how to improve. Let me know what you think.
If you find a bug or have suggestions for improvements, please let Kevin know! The code is open source (download link at the bottom of the page).
I’m teaching the incompleteness theorems (and related material) this term, and of course I’m using the Open Logic Project as a text. The relevant sections are based on Jeremy Avigad’s notes, which originally were meant as a supplement to Epstein & Carnielli’s textbook Computability. I’ve spent a fair bit of time revising them, and making them independent of that text. That meant adding a bunch of material, reformatting things, adding explanations and examples, etc. I think it’s now in sufficiently good shape that I can share it. However, it’s by no means done (we’re only halfway through the semester). I’m waiting to hear what else my students want to hear about; and I’ll update the project with additional chapters from the OLP (perhaps yet to be written). The most unusual aspect of it so far is perhaps that I’m doing everything in natural deduction, including arithmetization of provability.
The most recent PDF version should be available here, but I’ll also attach the current version to this post. All the actual material (with the exception of the chapter summaries and the front matter) comes from the Open Logic Text. The code to produce the text in this version is on GitHub. As usual, suggestions more than welcome!
Incompleteness and Computability