As Sylvain Peyronnet already mentioned, logic is an important part of theoretical computer science. However, it is not enough to learn logic from textbooks tailored for pure mathematicians. In other words, it's also important to learn logic from a more "computer science" perspective.
Finite Model Theory
We want to learn techniques that deal with finite structures. It is well-known that many traditional tools from model theory, e.g., compactness and Löwenheim-Skolem theorem, are not applicable to finite models. This leads us to the study of Finite Model Theory. For this area, I recommend the following excellent books:
A sub-area of finite model theory is descriptive complexity, where we want to characterizes complexity classes by the type of logic needed to define the languages. The definitive reference for descriptive complexity is:
Proof Complexity
Another important area of logic in computer science is Proof Complexity, a study of three way relationship among complexity classes, weak logical systems, and propositional proof system. The following two related aspects are considered: (i) the complexity of of proofs of propositional formulas, and (ii) the study of weak theories of arithmetic, called bounded arithmetic.
Aspect (i) has to do with the following question: "Is there a propositional proof system in which every tautology has a proof of size polynomial in the size of the tautology?"
Aspect (ii) studies logical systems which use restricted reasoning based on concepts from computational complexity. In other words, we assign with each complexity class $C$ a logical theory $VC$, where the provably total functions in $VC$ are exactly the functions in the complexity class $C$. One recent development is a new research program called "bounded reverse mathematic" proposed by Stephen Cook and Phuong Nguyen, where the goal is to classify theorems (of interest in computer science) based on the (minimal) computational complexity of concepts needed to prove them.
Aspects (i) and (ii) are closely related by the notion of propositional translation proposed in Cook's 1975 paper, which introduced the equation theory $\mathsf{PV}$ for polytime functions and showed how theorems in $\mathsf{PV}$ can be translated into families of tautologies which have polynomial length proofs in the extended Frege proof system.
For excellent surveys on proof complexity, I recommend the following two books:
The book by Cook and Nguyen is essentially self-contained, and all the necessary logic background is given in Chapters 2 and 3. Chapter 9 is particularly interesting since the authors introduced an extremely easy method to define your own theory for any complexity classes within $\mathsf{P}$. In this method, we only need to add one additional axiom to a base theory $V_0$, where the axiom simply states the existence of a solution to a complete problem of the complexity class. Pretty amazing!
The book by Krajíček is a bit more challenging since he assumed the readers are already familiar with mathematical logic and model theory (or willing enough to learn the background needed along the way). But you will learn a lot from reading and understanding this book.
