Here is a tranche of draft chapters for IFL2. Chapters 25–30 are revised chapters on QL languages (informal syntax and semantics, how to translate in and out). Chapters 31–34 are newly drafted chapters on natural deduction for QL proofs (the system is standard, and I hope contains no surprises).
The following chapters will give a more formal semantic story, define q-validity etc.; but I think it is good to get natural deduction proofs up and running in an intuitive way first (after all, they are supposed to be fairly natural!).
All comments, especially on the new Chapters 31–34. In particular, chapter 34 is a stand-alone short chapter on empy domains, which significantly revises an earlier draft section in response to some very just comments.
Concerning page 287, the statement of the rule for elimination: “…we can infer gamma”.
The word “infer” is very misleading. Gamma does not logically follow from the given material, even with the provisos satisfied. This is not a rule of inference, but rather a procedural wlog step: given the material, with the provisos satisfied, we may assume without loss of generality that gamma.
It is natural to respond (a) this is a minor verbal quibble, (b) the students are not going to understand the difference; they will merely be confused.
Re (a): It is not a verbal quibble at all, but a fundamental conceptual distinction at the heart of logic, reflected more clearly in the articulation of sequent calculi.
Re (b): Indeed, but with sufficiently careful explanation, it should be possible to get the point across. One would not attempt to explain when first stating the rule, but merely write “proceed to” instead of “infer” in the enunciation. Then later, when they have got routines under their belts, one could place a short section of careful explanation of why one said “proceed to” instead of “infer”.
Thanks, I take the basic point — though the place to highlight the distinction you want to emphasize is the first time a deductive move involving subproofs appears, back in the treatment of propositional logic. OK: I smudged over that, and need to think again how best to handle this. Your remarks make me think I should have said more. (Though I’m not myself inclined to hang too much on “infer” once it is explained that the rules of inference come in two flavours, without and with the appeal to subproofs.)
I like the point, though I’m trying to think of something better than “proceed to”. How about “we’re allowed to write”? (We need a word that implies both allowed and recommended.)