I'm reviewing the books on the MIRI course list. After putting down Model Theory partway through I picked up a book on logic. Computability and Logic, specifically.

Computability and Logic

This book is not on the MIRI course list. It was recommended to me by Luke along with a number of other books as a potential way to learn provability logic.

Computability and Logic is a wonderful book. It's well written. It's formal, but pulls off a conversational tone. It demonstrates many difficult concepts with ease. It even feels nice — it's got thick pages, large text, and a number of useful diagrams.

That said, I didn't find it very useful to me personally.

This book is a wonderful introduction to computability, incompleteness, unsatisfiability, and related concepts. It masterfully motivates the connection between computability and logic (a subject near and dear to my heart). It could be an invaluable resource for anyone in computer science looking to branch out into logic. It starts with the basic concept of enumeration and takes you all the way through Löb's theorem: quite an impressive feat, for one textbook.

For me, though, it was on the easy side. I already knew all the computability stuff quite well, and skimmed over much of it. The logic sections were a good refresher, though they were somewhat rudimentary by comparison to Model Theory. (Actually, this book would have been a great precursor to Model Theory: It spent quite a bit of time motivating and fleshing out concepts that Model Theory dumps on your head.)

Still, while this book was not exactly what I needed, I highly recommend it for other purposes. Its contents are summarized below.

Contents

1. Enumerability
2. Diagonalization
3. Turing Computability
4. Uncomputability
5. Abacus Computability
6. Recursive Functions
7. Recursive Sets and Relations
8. Equivalent Definitions of Computability
9. A Précis of First-Order Logic: Syntax
10. A Précis of First-Order Logic: Semantics
11. The Undecidability of First-Order Logic
12. Models
13. The Existence of Models
14. Proofs and Completeness
15. Arithmetization
16. Representability of Recursive Functions
17. Indefinability, Undecidability, and Incompleteness
18. The Unprovability of Consistency
19. Normal Forms
20. The Craig Interpolation Theorem
21. Monadic and Dyadic Logic
22. Second-Order Logic
23. Arithmetical Decidability
24. Decidability of Arithmetic without Multiplication
25. Nonstandard Models
26. Ramsey's Theorem
27. Modal Logic and Provability

Enumerability

This chapter introduces enumerability, and some of the cooler results. If any of the below sounds surprising to you, you'd be well served by reading this chapter:

If there's a one-to-one mapping between two sets, those sets are "the same size". By this measure, the following sets are the same size:

1. The natural numbers 0, 1, 2, 3, … (We call any one-to-one mapping between a set and the natural numbers an "enumeration".)
2. All integers: we can enumerate them 0, 1, -1, 2, -2, …
3. All even numbers: we can enumerate them 0, 2, 4, 6, …
4. All fractions. See if you can find your own enumeration of the fractions — It's a fun exercise, if you've never done it before.

This leads to a discussion of the "size" of infinite sets, which can be somewhat surprising the first time through. Knowledge of enumerability is central to many issues in computer science, and is integral in any study of infinities. I highly recommend you familiarize yourself with these concepts at some point in your life, if only for fun.

Diagonalization

When you realize how much can be enumerated (there's a one-to-one mapping between natural numbers and all finite subsets of the natural numbers!) it's easy to get excited, and feel like you can enumerate anything.

But you can't.

Diagonalization stops the buck. It's a tool for finding a set that defies a given encoding. Diagonalization is incredibly important if you want to play with infinities or learn about decidability. If you haven't yet seen diagonalization, you're in for a treat.

I won't ruin the fun here: The second chapter of Computability and Logic is a clever and easy introduction to diagonalization, and I highly recommend it to newcomers. Again, if this sounds new, I highly recommend picking up Computability and Logic: you're in for a treat.

Turing Computability

This chapter introduces Turing Computability, which is literally the bedrock of computer science. We focus on the question of what can (in principle) be computed. For those of you who don't know, the Turing Machine is an idealized computation engine which can compute answers to a very large class of problems.

If you're not familiar with the concept, this chapter is a great introduction. Even if you're vaguely familiar with the concept, but you're not quite sure how a Turing machine works ("wait, it only has a fixed number of states?"), then this chapter is a great way to beef up your understanding. It walks you through the implementation of a Turing machine, and shows you a number of clever algorithms by which a Turing machine computes simple algorithms. You'll find yourself actually walking through the actions of the machine in your head, which is a great way to get a feel for the idealized basics of computation.

Again, if any of this sounds new to you, I highly recommend picking up this book and reading the first few chapters.

Uncomputability

After seeing Turing machines, it is again easy to grow overconfident and feel like you can compute anything.

As before, you can't.

As a matter of fact, the proof that you can't compute everything with a Turing machine is exactly the same as the proof that you can't enumerate every set. It turns out Turing programs are enumerable (as is anything you can write out with symbols from a finite alphabet). So we can use the exact same technique — diagonalization — to construct problems that a Turing machine cannot solve.

Again, if any of this sounds foreign (or even if you're just rusty), this chapter is a delightful introduction to uncomputability. For example, it constructs the halting problem from a diagonalization of an encoding of Turing machine instructions. This smoothly unifies diagonalization with the intuitive impossibility of the halting problem. The chapter even touches on the busy beaver problem. I can't do it justice in a few mere paragraphs: if any of this sounds fun, don't hesitate to pick up this book.

Abacus Computability

This chapter introduces another formalism that has more machinery available to it than a Turing machine. If you don't already know how this story goes, I won't ruin the surprise. Again, this chapter is clever and fun to read. It has lots of diagrams and gives you a good feel for what sort of power an "abacus machine" (something that can do real math) has as a computational engine. If computability is a new field to you, you'll enjoy this chapter.

Recursive Functions

We now step to the math side of things. This transition is motivated computationally: we discuss five functions that are trivial to compute, and which turn out to be quite powerful when taken together. Those functions are:

• Zero: The function that always returns 0.
• Successor: The function that, given n, returns n+1.
• Identity: Functions that return something they are given.
• Composition: The function that performs function composition.

These four functions are called the "primitive recursive" functions, and some time is spent exploring what they can do. (Answer: quite a bit. Readers of Gödel, Escher, Bach will recognize BlooP.) If we allow use of a fifth function:

• Minimization: Given f, finds the arguments for which f returns 0.

we get the "recursive" functions. (Readers of Gödel, Escher, Bach will recognize this as unbounded search, and thus FlooP.)

These are a set of building blocks for some pretty interesting functions, and we are now firmly in math land.

Recursive Sets and Relations

The above definitions are extended to define recursive sets and relations. Generally speaking, we can define sets and relations by indicator functions which distinguish between elements that are in a set from elements that are not. Sets and relations are called "primitive recursive" if their indicator functions can be constructed from primitive recursive building blocks. They are "recursive" if their indicator functions can be constructed from recursive building blocks. They are called "semirecursive" if there is a recursive function which at least says "yes" to elements that are in the set, even if it cannot say "no" to elements that are not in the set.

Note that the indicator function for recursive sets must be total — i.e., must terminate — even though not all recursive functions are total. Also, note that semirecursive sets are more commonly known as "recursively enumerable" sets.

This may all seem a bit abstract, especially following all the computationally-motivated content above. However, these distinctions are good to know. This chapter is perhaps less fun than the others, but no less important. (It's easy to get recursive and semirecursive sets mixed up, when you're starting out.)

Equivalent Definitions of Computability

This is where the magic happens. This chapter shows that a function is recursive iff it is Turing computable. Turing machines and recursive functions are computational engines of precisely the same power. This is one of my favorite results in mathematics, and it's a beautiful (and the original) bridge between the lands of math and computer science.

This chapter actually shows you how to build a recursive function that computes the result of a Turing machine, and how to encode recursive functions as Turing-machine instructions. Even if you know the results, you may find it useful (or just fun) to toy with an actual bridge between the two formalisms. That's one thing I really like about this book: it doesn't just say "and these are equivalent, because [brief proof]". It actually shows you an encoding. It lets you see the guts of the thing.

If you're casually interested in math or computer science (or if you need a brush up, or you just want a good time) then I highly recommend reading this book at least through chapter 8. It's good clean fun to see these things play out in front of you, instead of just hearing the results secondhand.

A Précis of First-Order Logic: Syntax

We now dive in to the logic side of things. This chapter introduces the syntax of first order logic. It's a pretty solid introduction, and a good way to brush up on the precise syntax if you're feeling rusty.

A Précis of First-Order Logic: Semantics

Here we start getting into a little bit of model theory, binding the syntax of first order logic to semantics. This chapter would have been valuable before I started reading Model Theory. It is a solid introduction to the concepts.

The Undecidability of First-Order Logic

This chapter is dedicated to encoding a Turing machine as a logical theory. The fact that this can be done is incredibly cool, to say the least.

As before, the chapter provides actual examples for how to encode Turing machines as logical theories. You get to play with sentences that describe a specific Turing machine and the state of its tape. You get to see the chain of implications that represent the computation of the Turing machine. As before, this is an awesome way to get a hands-on feel for a theoretical result that is commonly acknowledged but seldom explored.

The end result, of course, is that you can encode the halting problem as a decision problem, and therefore the decision problem (checking whether a set of sentences Γ implies some sentence D) is uncomputable. However, this book doesn't just tell you that result, it shows it to you. You actually get to build a set of sentences Γ encoding a Turing machine, and construct a sentence D that expresses "this Turing machine halts". Even if you're already familiar with the result, reading this chapter is quite a bit of fun. There's something magical about seeing the connections between computation and logic laid bare before you.

Models

This chapter goes into basic model theory, discussing concepts like isomorphism, model size, and compactness. (Compactness is explained, but not proven.) This chapter would have been invaluable a month and a half ago, before I started Model Theory. If you're interested in model theory, this is a great place to get a feel for the ideas. It illustrates the basic concepts that I tried to cover in my very basic model theory post, but it covers them in a much more complete and approachable manner.

The Existence of Models

This chapter is entirely devoted to a proof of the compactness theorem. The chapter walks you through the whole thing and makes it easy. Again, this would have been good preliminaries for Model Theory, in which compactness is proved about a paragraph. I personally found this chapter a bit slow, but I imagine it would be useful to someone new to the idea of compactness.

Proofs and Completeness

This chapter is about formalizing a system of proofs. It also introduces the concepts of soundness and completeness. Readers of Gödel, Escher, Bach and others familiar with the subject matter will see where this is going, and the chapter very much feels like it's setting up all the right pieces and putting things in place.

If you're new to the ideas of arithmetization and representability, then you don't want to read the next three chapters without reading this. Otherwise, it's skippable.

Arithmetization

This chapter develops an arithmetization of the syntax first-order logic, and of the proof system sketched in the previous chapter. This involves developing a numeric encoding of first-order formulas, and recursive functions that can manipulate formulas so encoded. If you've never experienced such an encoding before, this chapter is a fun read: otherwise, it's skippable.

Representability of Recursive Functions

This chapter shows how any recursive function can be expressed as a formula in the language of arithmetic (a theory of first-order logic). This closes our loop: all functions may be encoded as arithmetical formulas, which may themselves be encoded as numbers. This is the mechanism by which we will embed arithmetic in itself.

The chapter then discusses formal systems of arithmetic. PA is mentioned, but a more minimal (and easier to reason about) arithmetic is the focus of conversation.

Indefinability, Undecidability, and Incompleteness

This is the climax of the book. The previous three chapters have been leading here. We construct a function that does diagonalization, then we represent it as a formula, and show how, given any formula A(x), we can construct a sentence G ↔ A('G') via some clever uses of our diagonalization function and the diagonalization formulas. From there, indefinability, undecidability, and incompleteness are just a hop, skip, and jump away.

Diagonalization in arithemtic is always a pleasure to run your mind over, in my experience. This is a result that's assumed in many other texts ("and, by diagonalization, we can construct…"), but rarely explored in full. It's quite fun to pop the thing open and see the little gears. Even if you're pretty comfortable with diagonalization, you may enjoy this chapter for its crisp treatment of the device.

This chapter comes highly recommended, even if just for fun.

The Unprovability of Consistency

This chapter breaks down Löb's theorem and proves it in detail. If you've made it this far in the book, Löb's theorem won't even seem difficult. If you already know Löb's theorem well, this chapter is skippable. But if the theorem has always seemed somewhat confusing to you (even after the cartoon guide) then this chapter may well be enlightening.

Normal Forms

We now move to the "further topics" section of the book. This section was a bit faster, a bit less motivated, and more prone to dump proofs on you and say "isn't that neat".

First, we discuss a variety of normal forms into which we can put logical sentences, each of which makes particular proofs easier. For example, you can do everything with only ∃, ¬, and ∧. Alternatively, you can resolve to deal only with sentences where all the quantifiers come first. Or you can decide to work without function symbols, and so on.

It's good to know your normal forms, this chapter is worth a read.

The Craig Interpolation Theorem

Craig's interpolation theorem lets us construct a sentence that is "between" an implication and has some nice properties. (If A→C, then the Craig interpolation theorem lets us construct a B such that A→B, B→C, and B contains only logical symbols contained in both A and C.) This is a result used often in model theory, and a good tool to have in the toolbox. Read it if you're curious, skip it if you're not.

Monadic and Dyadic Logic

This chapter is pretty neat. It turns out that "monadic" logic (first order logic in a language logic with only one-place relation symbols) is decidable. However, it also turns out that "dyadic" logic (first order logic in a language with only two-place relation symbols) is undecidable. (We can actually make that stronger: a language in first order logic with exactly one two-place relation symbol is undecidable.)

This is interesting, because it shows us precisely where undecidability sets in. First order logic becomes undecidable when you add the first two-place relation symbol. This is a fun chapter to read if you feel like exploring the boundaries of undecidability.

The latter result is proved by showing that we can put any logic into a "normal form" where it has at most one two-place relation symbol (and no relation symbols of higher arity). This result was surprising, and the proof is a fun one.

Second-Order Logic

This chapter introduces second order logic, and shows some basic results (it's not compact, etc.). It's not a very in-depth introduction. If you're interested in exploring second order logic, I'd recommend finding a text that focuses on it for longer than a chapter. This chapter left me a bit unsatisfied.

Arithmetical Decidability

This discusses some results surrounding the definability of truth in arithmetic: for example, the chapter shows that for each n and any sane measure of complexity, the set of sentences of complexity at most n which are true is arithmetically definable.

The results here were somewhat boring, in my opinion.

Decidability of Arithmetic without Multiplication

It turns out that arithmetic without multiplication is decidable. This is another interesting exploration of the boundaries of undecidability. The result is shown in this chapter by elimination of quantifiers: this is nice, but I feel like the chapter could have had more impact by exploring the mechanism by which multiplication brings about undecidability to arithmetic. I plan to explore this subject more in my free time.

Nonstandard Models

This section discusses nonstandard models of arithmetic, and the usual wacky results. If you've never played with nonstandard models before, this chapter is a nice introduction.

Ramsey's Theorem

This chapter introduces Ramsey's theorem (a result in combinatorics) and uses it to obtain an undecidable sentence that doesn't do any overt diagonalization. This chapter is kind of fun, and it's nice to see an undecidable sentence that doesn't come from direct self-reference trickery, but you won't miss much if you skip it.

Modal Logic and Provability

This chapter introduces provability logic (and is the reason I picked up this textbook, initially). I was somewhat disappointed with it: it introduces modal logic well enough, but it just sort of dumps a lot of proofs and results on you. This is all well and good, but I was expecting much more detail and motivation, given the impressive motivation found elsewhere in the book. Overall, this chapter felt somewhat rushed.

---

That concludes the summary. As a minor note, this textbook had way more typos than any other textbook I've read. There was one every few chapters. It was especially bad in the "Further Topics" section (ch. 19 and up), where there was a typo every chapter or so. However, the writing quality is otherwise top-notch, so I won't complain too loudly.

Who should read this?

This book comes highly recommended, especially to people just getting interested in the fields of computability and logic. If you're interested in computation or logic, this book introduces some of the coolest results in both fields in a very approachable way.

This book excels at showing you the actual mechanisms behind results that are often mentioned but seldom exposed. Even if you know that the deduction problem is equivalent to the halting problem, it's illuminating to play directly with an encoding of Turing machines as logical theories.

This book is a great way to shore up your understanding of some of the most fun proofs in computability theory and in logic. It would make an excellent companion to a computer science curriculum, and a great follow up to Gödel, Escher, Bach by someone hungry for more formalism.

That said, it's not a good introduction to (modal) provability logic. Don't pick it up for that reason, no matter what Luke tells you :-)

What should I read?

You should definitely read chapters 1-8 if you get the chance, especially if you're not already familiar with the bridge between Turing machines and recursive functions.

Chapters 9-18 also come highly recommended if you want to really understand incompleteness and undecidability. Readers of Gödel, Escher, Bach will find these chapters to be familiar, albeit more formal. They're a great way to brush up on your understanding of incompleteness, if you think you have to.

Chapter 18 in particular is quite relevant to some of MIRI's recent work, and is good to know in the LessWrong circles.

Chapters 19-27 are optional. They're less polished and less motivated, and more likely to just dump a proof on you. Read the ones that seem interesting, but don't be afraid to skip the ones that seem boring.

Final notes

This book wasn't the most useful book I've read in this series. I was already quite comfortable with most of these subjects. In fact, I planned to skim the first two sections (up through chapter 18): I only slowed down and gave the book more time when it turned out to be a lot of fun.

I highly recommend reading this book before Model Theory, if you're planning to read both. Chapters 9-13 would have made Model Theory quite a bit easier to tackle.

This book is not on the MIRI course list, but I recommend putting it on the course list. The subject matter may start out a little basic for much of the audience (I expect people who approach the course list to already know enumerability, the halting problem, etc.), but chapters 9-18 are a good introduction to fields that are important to MIRI's current research.

I mean, this book takes readers all the way through a proof of Löb's theorem, and it does it at an easy pace. That's no small feat. It also sets up Model Theory nicely and has a brief intro to modal logic. It feels a little easy, but that's not a bad thing. I think this would be a great way to get people familiar with the type of logic problems they'll have to be comfortable with if they're going to tackle the rest of the course list (and eventually MIRI research).

If anyone else is thinking of reading the course list, Computability and Logic is a great place to start. It introduces you to all the right concepts. It may not be the fastest way to get up to speed, but it's definitely entertaining.