In the Study Guide entry on First-Order Logic, after the list of main reading suggestions, there is a further list of suggested parallel/additional reading which ends by warmly recommending Melvin Fitting’s First-Order Logic and Automated Theorem Proving (Springer, 2nd edn 2012). Although published in a series aimed at compsci students, this should certainly appeal to logicians who are primarily philosophers or mathematicians but who want to know a little more about some themes (e.g. resolution proof systems) of special interest to computer science, and who want to re-encounter some familiar ideas approached from a slightly different angle. You can, if you want, skip some of the bits on Prolog and still get a particularly elegantly and clearly written account.
I’ve been wondering whether there are other books also written for computer scientists which could similarly appeal to the Guide’s intended readers. I know, of course, Michael Huth and Mark Ryan’s Logic in Computer Science (CUP, 2nd edn 2004). I haven’t reread this recently, but I recall it as being attractively and clearly written — the long first two chapters on propositional and predicate logic are well done, with a few interesting extras for the philosophical or mathematical reader (e.g. on SAT solvers). But then the later chapters go off in directions no doubt of key concern to computer scientist, but less interesting for the rest of us (for me, anyway!).
I’ve had Mordechai Ben-Ari’s Mathematical Logic for Computer Science (Springer 3rd edn 2012) recommended to me. But I thought this pretty second-rate. 
The level of exposition is poor, and indeed at points seemingly outright confused (e.g. about the status of the Deduction Theorem for a Hilbert system). Someone who already has a grip on the standard math logic approaches could, I guess, get something out of the book by diving straight into the chapters on propositional resolution, SAT solvers, and first-order resolution, for example. But I didn’t find this material well explained: it is surely treated more pleasingly elsewhere.
To repeat, then, I’m interested in locating logic books coming from a compsci angle which will however also appeal to someone whose main interest remains in philosophy or mathematics. Luis Augusto’s book is advertised as aimed at such readers, but you know what I think of that. So are there other options? I’d be very interested to hear!
I know I’m a bit late to this post, but one book I quite like and you may appreciate having brought to your attention is John Harrison’s Handbook of Practical Logic and Automated Reasoning
I’m not sure that the title accurately describes the contents, but I think it contains a few topics that make it of interest at least to mathematicians, and possibly even philosophers.
https://www.cl.cam.ac.uk/~jrh13/atp/
https://www.cambridge.org/core/books/handbook-of-practical-logic-and-automated-reasoning/EB6396296813CB562987E8C37AC4520D
I was wondering about the opposite direction, i.e. whether there are introductions to computer science/programming from a logician’s point of view. Thanks!
Zhaohui Luo’s “Computation and Reasoning – A Type Theory for Computer Science”?
or perhaps “Derivation and Computation: Taking the Curry-Howard Correspondence Seriously” from Harold Simmons. I think they were not mentioned.
I don’t know Luo’s book, so thanks for the pointer — I’ll check it out. I do ratherlike some of Harold Simmons’s other books: this one I found disappointing when I read some of it a while back — but maybe I should take another look.
There are some good textbooks on modal logic from a computer science perspective that are also of interest to philosophers:
1. Fagin et al.: ‘Reasoning about knowledge’. This book is a great exposition of the standard relational semantics of various epistemic logics and contains applications to distributed systems, complexity results on knowledge and time and fixed-point theorems about common knowledge.
2. van der Hoek / Meyer: ‘Epistemic Logic for AI and Computer Science’. Another attractive intro to Kripke-style semantics for epistemic logics adding more intricate systems like default logics and autoepistemic logic.
3. Manna / Pnueli: ‘The Temporal Logic of Reactive and Concurrent Systems: Specifications’. This book uses temporal logic as a means to specify certain computing systems, but it has some chapters that present temporal logic in a very illuminating way.
4. Demir et al: ‘Temporal Logics in Computer Science’. Contains many valuable chapters on the expressive power of various temporal logics and has an accessible treatment of the mu-calculus.
Thanks! — I’ll check out these references when I get round to rewriting the Guide chapter on modal logic.
I have thought about this question a lot and the only answer I feel totally confident in giving would be Fitting’s book.
A distant second would be *Computability, Complexity, and Languages*, the second edition, by Martin Davis et al. It is in the same genre of theory of computation books as Michael Sipser’s and *Introduction to Automata Theory, Languages, and Computation* by Hopcroft, Motwani, and Ullman; that is, it covers computation in general, formal language and automata theory, and computational complexity theory, however it also delves into programming language semantics, both denotational and operational, which I really appreciate. Out of those three, which are the standard three books on the subject, Davis’ comes the closest to the type of book your asking for. It deals with logic and the relevant theorems and results in its own chapter instead of relegating it to a few subsections like in Sipser and it feels much more like a book written for mathematicians and logicians than for software engineers who are trying to get through a theory course in their undergrad.
However, if any philosopher or mathematician readers are put off by the elegant Prolog in Fitting’s book, they will be horrified by the macros-and-jumps filled register machine language in parts of Davis’. There are also minor references to software that might go over the head of some readers who aren’t programmers (if I recall correctly there’s a reference to grep and yacc when discussing grammars, and there is passing mention and analysis of the behavior of a Fortran compiler), but they are not critical to understanding or even working through the text. So all things considered I’d argue it is the best out of the three and I think the theory of computation is a very good way to get some core mathematical logic from a compsci view, as it were.
Then, to add to what Matt mentioned about type theory, one book I very much recommend you check out is *Lectures on the Curry-Howard Isomorphism* by Sørensen and Urzyczyn. When type theory people and programming language people say ‘type theory’ they mean typed lambda calculi, and when they say ‘logic’ they mean intuitionistic natural deduction and this book is a fantastic series of lectures outlining the field. Not only does it work its way up through the different sorts of typed lambda calculi, but it also gives a very algebraic view of first order model theory and an illuminating account of the incompleteness and undecidability results. There is also a great discussion of Gentzen’s hauptsatz and a lot of related proof theory topics as well. One of the highlights for me is that under the propositions-as-types correspondence, continuation passing style, a style of functional programming that is very important in compiler optimization and programming language theory, corresponds to the double negation interpretation of classical logic in intuitionistic logic (and when category theory is brought in, they both correspond to the Yoneda embedding (!)) and there is an entire chapter on that.
For anyone who does want to just test the waters of type theory and its place in the greater area of mathematical logic and proof theory, my recommendation would be to read Hindley and Seldin’s *Lambda-Calculus and Combinators* (unfortunately it is expensive) for a very steady and full introduction to the untyped and then typed lambda calculus as well as combinatory logic, and then follow it with Sørensen and Urzyczyn for the complete picture. If you do want to eventually put something about type theory into the guide, I highly recommend starting out by looking into those two books.
Sørensen and Urzyczyn looks like a great book. I’m disappointed it’s so expensive. As Peter has written before it’s really unfortunately that, in this age of print-on-demand, some of these older works cost so much. I know that Elsevier can do print-on-demand since I’ve ordered two books from them directly.
I wholeheartedly concur. A particularly egregious example to me is the Oxford Logic Guides series; it is mindboggling that Kaye’s book, the de facto standard reference for models of PA is sitting at almost $200, even used.
In terms of a free alternative to Sørensen and Urzyczyn for anyone interested, there is Girard’s Proofs and Types. Paul Taylor, one of the translators, hosts a pdf of it on his website http://www.paultaylor.eu/stable/Proofs+Types.html due to it being out of print. It is less thorough and much shorter (being the spawn of lecture notes for a one semester course) but it covers a lot of the same topics. However, it stops before getting to dependent types. And again for anyone who is interested in type theory, I would be remiss to not mention Pierce’s book Types and Programming Languages which is the go to for type systems and how to implement them, though its much more firmly in the programming language theory space than the logic through type theory space. Pierce’s book is still relatively expensive, so in a mirror case to the above, a free alternative that covers a lot of the same material but is not as thorough is Type Theory and Functional Programming by Simon Thompson which he hosts as a PDF on his webpage https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ due to it being out of print, but as I said these are less logic and more functional programming focused.
The Oxford Logic Guides all seem outrageously expensive, even now that they’re print on demand. Yet somehow Smullyan and Fitting’s Set Theory and the Continuum Problem managed to escape and become an inexpensive Dover. I don’t know why the others remain captive, or why OUP doesn’t offer them itself at a reasonable price.
(There is actually one other escapee that I know of: An Introduction to Stability Theory, by Anand Pillay, also rescued by Dover.)
Anyway, a curious addition to the literature on dependent types is The Little Typer, by Daniel P. Friedman, David Thrane Christiansen, Duane Bibby, Robert Harper, and Conor Mcbride.
Like other The Little books (The Little LISPer, The Little Schemer, The Little Prover, …), it’s written in a style that at least used to be known as ‘programmed learning’. Each page is in two columns, with questions on the left and the answer to each question opposite it on the right. The reader is meant to read each question, think about how to answer it, then look at the answer and go on to the next question. Another book in this style is Bobby Fischer Teaches Chess.
This approach does not appeal to everyone; it nonetheless appeals to enough people that Friedman has written 8 or so of these books, with various co-authors, starting with the original Little LISPer back in 1974. (It’s now in its 4th edition.)
(I’d temporarily forgotten that OUP does offer some Logic Guides at relatively reasonable, though still questionable, prices — 30-something pounds — Shapiro’s Foundations without Foundationalism, Awodey’s Category Theory, Bell’s Set Theory: Boolean-Valued Models and Independence Proofs, and some others.)
Yes, I just don’t understand their principle of selection for deciding what to paperback! Why not paperback Kaye? And the two volumes of that bible, the Elephant, will set the category theorist back over 400 pounds … which is crazy.
Indeed, I was going to mention Smullyan at first, it is jarring to see so many of his books as cheap dover editions and then see e.g. Diagonalization and Self-Reference at $270. I do not understand how there could possibly be an invisible $255 line between that book and his Forever Undecidable.
The Little series of books are all very good. I like to make the analogy between that series and Halmos’ Naive Set Theory (which is even recommended at the end of The Little Schemer): they are lighthearted and rather informal, but you end up learning a lot more than you realize at first.
There are some other great introductions to dependent types which are free, Samuel Mimram’s Program = Proof https://www.lix.polytechnique.fr/Labo/Samuel.Mimram/teaching/INF551/ starts with functional programming in OCaml and goes all the way through homotopy type theory with Agda; the online book Wadler et al.’s Programming Language Foundations in Agda https://plfa.github.io/ and its provenance The Software Foundation series https://softwarefoundations.cis.upenn.edu/lf-current/index.html the first book of which does similar work in Coq; and of course there is Programming in Per Martin-Löf’s Type Theory http://www.cse.chalmers.se/research/group/logic/book/ but I personally have always found that monograph to be fairly difficult to follow in many places.
My biggest challenge with free e-copies is that I really prefer a nicely bound paper version to learn from. If we could just bridge that gap to a reasonably price print-on-demand that would be wonderful. I have tried spiral bound from the local print store but I don’t like it nearly as much. I too love the “Little” books. The Little Schemer was my best introduction to how to write recursive function.
I think chapter 5 in Huth Ryan’s Logic in Computer Science — Modal logics and agents — is a good introduction to modal logics and how to understand and use them, and that it’s especially useful on the accessibility relation. Though much of the chapter is described as ‘Logic engineering’, I think it would suit philosophical and mathematical readers, not only computer scientists.
Good point. Though I guess I was setting aside modal logic for the time being (coming back to the in the relevant section of the Study Guide).
I first found this blog when I searched for reviews of David Makinson’s Sets, Logic and Maths for Computing.
I like this book a great deal, and it indeed gets a recommendation in the next version of the Guide. But it is at a more introductory level than I was looking for here in this post — the philosopher or mathematician who has followed the standard math logic curriculum will not find many surprises here.
I realize that this might not quite what you’re looking for but have you looked Type Theory and Formal Proof?
Type Theory and Formal Proof: An Introduction https://g.co/kgs/EuCYV1
Ah yes indeed — there’s the whole area of type theory which isn’t in the usual core math logic curriculum for philosophers or mathematicians. The Nedepelt and Geuvers book is pretty hard-core, though. (I’ve wondered before about adding a section on type theory to the Guide, but confess I’m not sure how to structure it or what exactly to recommend, which reflects my lack of grip on the area!)
The best way to start with type theory is to read the chapter “A gradual introduction to type theory” in Aarne Ranta’s book “Type-Theoretical Grammar,” OUP 1995, out of print but maybe the file is out there somewhere… The only prerequisite is some natural deduction. Then there is a chapter about higher-level type theory to continue with.
I have a copy of Aarne Ranta’s book, and indeed agree that his “gradual introduction” is rather helpful — helpful at any rate in setting out the a certain story. But I’m left with the suspicion that various things are being run together in a potentially confusing way. I should try to set down my worries sometime.