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.