Closed rzach closed 7 years ago
Need to decide if this should be done for milestone Fall 2017
I don't find this pressing. The main advantage of this (I think) is to have classical logic as an easy extension of intuitionistic logic. The difference becomes exactly one additional rule for classical logic (and for minimal logic, you can just drop one more.) But since that's not how (this part of) the book it build, perhaps let's postpone this until we include (a) proper intuitionism chapter(s)?
Just my ¢2. (Obviously, no strong objection to changing the rules for Fall 2017! Just doesn't strike me as a priority.)
I'm hoping to have an intuitionistic logic chapter by Winter 2018 (it'll be part of my modal logic course). In fact there already is a draft of a beginning of one in a branch which I hope to merge into master soon.
Fixed in commit b5feb38e2a22ff9d7ed7021e4170b6a53732701b
The current version of content/fol/natural-deduction has the rules for \lnot and \lfalse just like eg Language, Proof, and Logic (eg A, \lnot A \proves \lfalse is called \lfalse Intro and not \lnot Elim, and what we call \lnot Elim is actually double-\lnot elim). Replace with Prawitz's rules (ie, \lfalse Elim is \lfalse_I and \lnot Elim is \lfalse_C) & standard names? Make this a configurable choice? (If so has downstream effects for arithmetization of syntax!)