IssacNewton said:
I would recommend Elliott Mendelson's "Introduction to Mathematical Logic" . also Herbert Enderton's "A mathematical introduction to logic"
These books are not bad, although there are some things I don't like about Mendelson. I had one of the early editions, and it only had Hilbert calculus as a deductive system. Also, its proofs, especially of Gödel's incompleteness theorems, were pretty dense. Finally, it described Von Neumann-Bernays-Gödel set theory instead of a much more popular ZFC. Newer editions may be better.
It seems you have studied the beginning of proof theory. The next logical step is Gödel's incompleteness theorems, which is described in the two books above. One classical and very good book is "Computability and Logic" by Boolos, Burgess and Jeffrey. Another classical book is "Mathematical Logic" by Shoenfield. There are also many other books about Gödel's theorems, such as "The Incompleteness Phenomenon" by Goldstern and Judah. Speaking about this, I would recommend a book for a wide audience (not really a math textbook) "Meta Math!: The Quest for Omega" by one of the founders of algorithmic complexity Chaitin. It gives a different view on Gödel's theorem.
Speaking about proof theory, another important area is non-classical logics, such as intuitionistic, modal and linear logics, which is a subject closely related to computer science. There is a classical book "Proofs and Types" by Girard, Taylor and Lafont, which is available online. There is also "Lectures on the Curry-Howard Isomorphism" by Sørensen and Urzyczyn, whose previous version is available online.
Proof theory is one of the four main parts of mathematical logic. There is a "Handbook of Mathematical Logic" edited by Barwise, which also includes parts on set theory, model theory and computability. There are many textbooks on set theory, such as "Intermediate Set Theory" by Drake and Singh. Classic books in model theory include "Model Theory" by Chang and Keisler. A couple of classic books on computability are "Theory of Recursive Functions and Effective Computability" by Rogers and "Recursion Theory" by Shoenfield.
One topic that is closely related to logic and computer science is category theory, or "abstract nonsense," as it is called by mathematicians. It plays an increasingly important role in the theory of programming languages, for example. "Conceptual Mathematics: A First Introduction to Categories" by Lawvere and Schanuel is a very gentle introduction. Another good classical book is "Topoi: The Categorial Analysis of Logic" by Goldblatt (available online).
Unfortunately, most of these books are pretty old, and I am not familiar with modern logic textbooks. For newer books, I would recommend asking a professor who teaches logic or looking through textbooks reviews in the "Bulletin of Symbolic Logic."
