This completely self-contained study, widely considered the best book in the field, is intended to serve both as an introduction to quantification theory and as an exposition of new results and techniques in "analytic" or "cut-free" methods. Impressed by the simplicity and mathematical elegance of the tableau point of view, the author focuses on it here. After preliminary material on tress (necessary for the tableau method), Part I deals with propositional logic from the viewpoint of analytic tableaux, covering such topics as formulas or propositional logic, Boolean valuations and truth sets, the method of tableaux and compactness. Part II covers first-order logic, offering detailed treatment of such matters as first-order analytic tableaux, analytic consistency, quantification theory, magic sets, and analytic versus synthetic consistency properties. Part III continues coverage of first-order logic. Among the topics discussed are Gentzen systems, elimination theorems, prenex tableaux, symmetric completeness theorems, and system linear reasoning. Raymond M. Smullyan is a well-known logician and inventor of mathematical and logical puzzles. In this book he has written a stimulating and challenging exposition of first-order logic that will be welcomed by logicians, mathematicians, and anyone interested in the field.
This is the most dense book I've ever read, but to say it has been rewarding would be an understatement. I had to re-read several paragraphs over and over again before their obvious simplicity shone through; also, had to go back several pages to re-read previous proofs anew to understand the new developments on following pages. Let the slimness of this book not induce the slightest doubt about its richness, complexity, and, yes, readability.
NOTE: Only after understanding half of the book will you be able to appreciate Smullyan's writing style, if you are new to FOL like I was, the hard part is staying focused till then.
Extremely concise, somewhat old-fashioned presentation, focused mainly on completeness theorems for various first-order deductive systems. The author begins with the necessary stuff on Boolean logic, including König's infinity lemma, before moving into the first-order. His approach relies mostly on tableaux, which you just don't see as much anymore. There's also a somewhat frustrating decision to switch between signed and unsigned formulas (signed carry a T/F tag), which leads to some redundancy.
Extremely clear and economical, particularly in the first presentation of Hintikka sets and magic sets. If you've seen a proof of completeness à la Herbrand in a more modern logic text, this will look somewhat different. He makes no reference to functions or really languages at all: there are only predicates and parameters (no closed term universe). It's a very purely logician-feeling book, it doesn't have the algebraic or categorical flavor of newer books. The Lowenheim-Skolem theorem here is just that a consistent set of sentences can be satisfied in a denumerable domain (there's no "upward" version). Several proofs seem aimed at reducing the use of Choice in the construction of the Herbrand model to an absolute minimum, using tree ordering stuff.
He develops a unifying principle around his concept of analytic consistency principles that allows him to efficiently port the completeness theorem to various deductive systems (Gentzen, linear, etc.). After a while, I have to confess I got bored of seeing "new system, completeness for that system, new system, etc." even though this is such a short book. There are a few late standouts in the book, interesting topics like Beth definability and Craig interpolation (named after one-off characters from season 6 episode of Friends). Maybe I am just not a logician at heart because I did not thrill to the variety of systems for proving basically boring and uninteresting tautologies. Minor nitpick: There was an annoying bit when he first introduces compactness where he doesn't actually state the theorem apart from the text, only refers to it as a principle somewhat indirectly.
That being said the first seventy-five pages or so are very good; the latter half of the book moves by faster because of the Gentzen diagrams.
I enjoyed reading this book and going through (most of) its exercises (which I think is a necessary part in understanding any book on mathematics), and I learned a lot from it.
I do have a few issues with the book, though. First of all, there are some typos, but fortunately none that hinder comprehension. Second of all, I don't think the book does a good job of communicating its target audience; it is assumed that the reader is familiar with at least basic naive set theory and what is meant by a theorem and a proof (even though these terms are defined for axiom systems in part II of the book), so the reader should be a student of mathematics at least. The book is really about a small handful of results proved in a multitude of ways and for a multitude of (proof-)systems for propositional or first-order logic, and then doing a comparison between these proofs and systems and finally a search for the deeper underlying principles at play beneath these proofs. This is quite difficult to follow for someone new to the subject, so the reader should also already be familiar with propositional logic and quantification theory. I would have also liked more sections with discussions or motivating text, since (at least towards the end in part III) the material began to feel quite repetitive and unmotivated, so we conclude that the reader should also already be interested and motivated to learn about e.g. Gentzen systems and completeness theorems for linear reasoning before beginning the book. Finally, I actually read this book because I thought it would serve as a good "prologue" or introduction before reading Raymond Smullyan and Melvin Fittings book on set theory, but since this book (First Order Logic) already assumes familiarity with set theory (and uses it in defining key objects of the theory), that might not have been the case, but this is of course not the author's fault.
All in all I do think that this is a good book, but I would be wary about recommending it to anyone not already well versed and interested in propositional logic, quantification theory and axiom systems.
You want to know the nitty-gritty of FOL? Smullyan's your boy. He even has some awesome puzzle books for you to put some of the arcane theory of it into practice.