Natural Deduction Rules in forall x: Calgary

Prompted by a good suggestion by Richard Lawrence and support from Catrin Campbell-Moore, we’ve been working on revising the natural deduction rules used in the Calgary Remix of forall x, the intro logic text by P. D. Magnus.  The proposal is to rename some rules so the nomenclature is in line with that used in the literature on natural deduction, e.g., where the rule A, \lnot A \vdash \bot is \lnot-elimination, not \bot-introduction, and \bot \vdash A is now called “explosion,” not \bot-elimination. We’re also planning to replace the tertium non datur rule with an indirect proof rule, i.e., Prawitz’s classical absurdity rule. (Tertium non datur, which we now slightly less pretentiously call “law of excluded middle” LEM,  will stay an “official” derived rule.) The proof checker recognizes both the old and the new rules.

We have an issue on GitHub tracking the progress and a branch with the revisions. The current version of the result is attached (see esp. Sections 15.7, 16.5, 19.4-5), but a few exercises elsewhere were changed, as were some of the solutions. Comments welcome!


2 thoughts on “Natural Deduction Rules in forall x: Calgary

Leave a Reply