I'm looking at this now. It's a bit idiosyncratic but looks good. It covers standard topics in proof and recursion theory but from a more contemporary approach using natural deduction instead of Hilbert-style proof systems, and it also does complexity theory with various computation models. There are a fair number of exercises and problems, always a good thing. But it covers specialized topics at the expense of some standard ones. For example, I didn't spot any mention of the compactness theorem. So it's hard to call the book a usable general introduction to logic, despite it starting at a relatively beginner level.
It's a draft and it has some typos and some long-winded passages that could use editing, but I'm glad it is out there, and it looks to me like a good way for computer people to learn some logic and computability theory if that strikes their fancy. I've only looked at the first couple chapters but the TOC mentions that Girard's polymorphic lambda calculus makes an appearance, so there must be some type theory in there. But, my preference would be to increase the coverage of that even if it means trimming back some of the computability stuff. Another improvement might be to include some coverage and exercises in mechanized proof checking using Coq, in the spirit of Software Foundations (also by authors at Penn, https://softwarefoundations.cis.upenn.edu/ ).
Well, it depends on what you are looking for, but the traditional-style book that I'm used to is H. B. Enderton, "A Mathematical Introduction to Logic", and Enderton also has an accompanying book on set theory. I guess I'd suggest those as a companion rather than an alternative to the Gallier and Quaintance book. The G&Q book is imho more modern and more interesting from a CS-oriented perspective. It just leaves out too many important fundamentals. Alternatively, since it is still a work in progress, maybe some of the missing stuff could be added.
Boolos and Jeffrey "Logic and Computability", whatever the current edition is, is supposed to be good, but I haven't read it yet.
The G&Q book is weird in that it is about interesting topics that I'd consider slightly advanced, but written in a way that assumes almost no background, so if it's the only thing you read, you'll still be missing important background. I'd like a book that uses the G&Q approach but that includes the background. If it kept all the current contents and was expanded, it would probably end up as 2 volumes, which is fine. Or it could leave out some of the specialized stuff, but I think that stuff is there because that was what the authors wanted to write about, so I won't judge ;-).
It's a draft and it has some typos and some long-winded passages that could use editing, but I'm glad it is out there, and it looks to me like a good way for computer people to learn some logic and computability theory if that strikes their fancy. I've only looked at the first couple chapters but the TOC mentions that Girard's polymorphic lambda calculus makes an appearance, so there must be some type theory in there. But, my preference would be to increase the coverage of that even if it means trimming back some of the computability stuff. Another improvement might be to include some coverage and exercises in mechanized proof checking using Coq, in the spirit of Software Foundations (also by authors at Penn, https://softwarefoundations.cis.upenn.edu/ ).
Thanks to whoever posted this link!