Thanks to the kindness of strangers — not to mention some friends and relations (special thanks to The Daughter) — I have an improved version of the four chapters on propositional natural deduction for IFL2. LINK NOW REMOVED — revised version to follow. (Exercises to be added, which will fill some gaps, like noting the equivalence of DN and Classical Reductio, given the other rules, or dealing with biconditionals.)
One advantage about basing an intro logic book on trees (as in IFL1) is that people don’t get very exercised about how a tree system should be developed. By contrast, people get decidedly heated about the best form of natural deduction to adopt. So I’m probably not going to satisfy even half of those who urged me to go for natural deduction in the second edition. But there’s no pleasing everyone! What I propose is a standard enough Fitch-style system, with one deviation — the v-Elim rule is a Fitchian version of the liberalized rule recommended for Gentzen systems by Neil Tennant (who will get credit in the endnotes for the book!). That way we get disjunctive syllogism without relying on explosion. Which has always seemed more “natural” to me.
All comments (other than variants on “you have written the wrong book!”) and all corrections will of course be very gratefully received, as always.
The text treats the asterisk as if it were an item of the object language when officially it is no more than an annotation drawing attention to what one has done at certain places in derivations. This, in my view, is a terrible fudge. Even if doing it may sometimes streamline presentation a little, it invites deep conceptual confusion, just as would treating the letters “QED” or the box signalling that the proof is over as if they were parts of the proof itself.
Of course one could avoid the fudge by treating the asterisk as a zero-ary connective (or propositional constant) and thereby as a genuine item of the object language. That would have the further advantage of forcing one to be clearer about what is really going on in rules where the asterisk figures. In particular, it would make it clear that there simply is no introduction rule, in the strict sense of the term, for negation (or any other contrarian connective such as exclusive-or, not-both, neither-nor) in a natural deduction system where rules take us from sets of propositions to individual propositions. The asymmetry that is inherent in the set/proposition format induces an ineliminable asymmetry in the pattern of admissible rules, which one should not try to hide as as if it were a shameful blemish on the face of a beautiful lady.
p 187, last sentence in the next to last paragraph in section 20.2: If we can already infer γ from θ, and also infer θ from β, …
Presumably that should be: If we can already infer θ from α, and also infer θ from β, …
Ooops. Thanks, yes, now corrected.