Tony Roy has kindly alerted me to the existence of his freely available Symbolic Logic: An Accessible Introduction to Serious Mathematical Logic.
It is now in version 7.1, so I guess I should have discovered this before! It looks, at a quick first glance, a remarkable resource; still work in progress but looking very polished. There are no less than 746 pages together with another almost 200 pages of answers to exercises. It goes from an introduction to sentential logic, through the usual topics in first order logic (presented both axiomatically and in a natural deduction system) getting as far as e.g. a discussion of compactness and the downward L-S theorem, and then moving on to some quite detailed work on Gödel’s incompleteness theorems. And Tony writes that “it’s aimed especially at accessibility and so builds in a level of explanation and detail that may be missing from other sources.” So I’ll certainly be taking a look at this for TYL2016, and probably commenting there. In the meantime you can take a look yourself on the book’s website here.