The Annotated Gödel

Some years ago, Charles Petzold published his The Annotated Turing which, as its subtitle tells us, provides a guided tour through Alan Turing’s epoch-making 1936 paper. I was prompted at the time to wonder about putting together a similar book, with an English version of Gödel’s 1931 paper interspersed with explanatory comments and asides. But I thought I foresaw too many problems. For a start, not having any German, I’d have had to use one of the existing translations, which would lead to copyright issues, and presumably extra problems if I wanted to depart from the adopted translation by e.g. rendering Bew by Prov, etc. And then I felt it wouldn’t be at all easy to find a happy level at which to pitch the commentary.

Plan (A) would be to follow Petzold, who is very expansive and wide ranging about Turing’s life and times, and is aiming for a fairly wide readership too (his book is over 370 pages long). I wasn’t much tempted to try to emulate that.

Plan (B) would be write for a much narrower audience, readers who are already familiar with some standard modern textbook treatment of Gödelian incompleteness and who want to find out how, by comparison, the original 1931 paper did things. You then wouldn’t need to spend time explaining e.g. the very ideas of primitive recursive functions or Gödel numberings, but could rapidly get down to note the quirks in the original paper, giving a helping hand to the logically ept so that they can navigate through. However, the Introductory Note to the paper in the Collected Works pretty much does that job. OK, you could say a bit more (25 pages, perhaps rather than 14). But actually the original paper is more than clear enough for that to be hardly necessary, if you have already tackled a good modern treatment and then read that Introductory Note for guidance in reading Gödel himself.

Plan (C) would take a middle course. Not ranging very widely, sticking close to Gödel’s text. But also not assuming much logical background or any prior acquaintance with the incompleteness theorems, so having to slow down to explain ideas of formal systems, primitive recursion and so on and so forth. But to be frank, I didn’t and don’t think Gödel’s original paper is the best peg on which to hang a first introduction to the incompleteness theorems. Better to write a book like GWT! So eventually I did just that, and dropped any thought of doing for Gödel something like Petzold’s job on Turing.

But now, someone has bravely taken on that project. Hal Prince, a retired software engineer, has written The Annotated Gödel, a sensibly-sized book of some a hundred and eighty pages, self-published on Amazon. Prince has retranslated the incompleteness paper in a somewhat more relaxed style than the version in the Collected Works, interleaving commentary intended for those with relatively little prior exposure to logic. So he has adopted plan (C). And the thing to say immediately — before your heart sinks, thinking of the dire quality of some amateur writings on Gödel — is that the book does look entirely respectable!


Actually, I shouldn’t have put it quite like that, because I do have my reservations about the typographical look of the book. Portions of different lengths of a translation from the 1931 paper are set in pale grey panels, separated by episodes of commentary. And Prince has taken the decidedly odd decision not to allow the grey textboxes containing the translation to split themselves over pages. This means that an episode of commentary can often finish halfway down the page, leaving blank inches before the translation continues in a box at the top of the next page. And there are other typographical choices while also unfortunately make for a somewhat  unprofessional look. That’s a real pity, and does give a quite misleading impression of the quality of the book.


Now, I haven’t read the book with a beady eye from cover to cover; but the translation of the prose seems quite acceptable to me. Sometimes Prince seems to stick a bit closer to the Gödel’s original German than the version in the Works, sometimes it is the other way about. For example, in the first paragraph of Gödel’s §2, we have

G, undefinierten Grundbegriff: W, primitive notion: P, undefined basic notion,

while in the very next sentence we have

G, Die Grundzeichen: W, The primitive signs: P, The symbols.

But such differences are relatively minor.

Where P’s translation of G departs most is not in rendering the German prose but in handling symbolism. W just repeats on the Englished pages exactly the symbolism that is in the reprint of G on the opposite page. But where G and W both e.g. have “Bew(x)”, P has “isProv(x)”. There’s a double change then. First, P has rendered the original “Bew”, which abbreviated “beweisbare Formel”, to match his translation for the latter, i.e. “provable formula”. Perhaps a good move. But Prince has also included an “is” (to indicate that what we have here is an expression attributing a property, not a function expression). To my mind, this makes for a bit of unnecessary clutter here and elsewhere: you don’t need to be explicitly reminded on every use that e.g. “Prov” expresses a property, not a function.

Elsewhere the renditions of symbolism depart further. For example, G has “A_1\mbox{-}Ax(x)” for the wff which says that x is an instance of Axiom Schema II.1. P has “isAxIIPt1(x)”. And there’s a lot more of this sort of thing which makes for some very unwieldy symbolic expressions that I don’t find particularly readable.

There are other debatable symbolic choices too. P has “\Rightarrow” for the object language conditional, which is an unfortunate and unnecessary change. And P writes “x[v \leftarrow y]” for the result of substituting y for v where v is free in x. This may be a compsci notation, but to my untutored eyes makes for mess (and I’d say bad policy too to have arrows in different directions meaning such different things).

Other choices for rendering symbolism involve more significant departures from G’s original but are also arguably happier (let’s not pause to wonder what counts as faithful enough translation!). For example, there is a moment when G has the mysterious “p = 17 Gen q”: P writes instead “p = forall(\mathbf{x_1}, q)”. In G, 17 is the Gödel number for the variable x_1: P uses a convention of bolding a variable to give its Gödel number, which is tolerably neat.

There’s more to be said, but I think your overall verdict on the translation element of Prince’s book might go either way. The prose is as far as I can judge handled well. The symbolism is tinkered with in a way which makes it potentially clearer on the small scale, but makes for some off-putting longwindedness when rendering long formulas. If you are going to depart from Gödel’s symbolism, I don’t think that P chooses the best options. But as they say, you pays your money and makes your choice.


But what about the bulk of the book, the commentary and explanations interspersed with the translation of Gödel’s original? My first impression is definitely positive (as I said, I haven’t yet done a close reading of the whole). We do get a lot of helpful framing of the kind e.g. “Gödel is next going to define … It is easier to understand these definitions if we think about what he needs and where he is going.” And Prince’s discussions as we go along do strike me as consistently sensible and accurate enough, and will indeed be helpful to those who bring the right amount to the party.

I put it like that because, although I think the book is intended for those with little background in logic, I really do wonder whether e.g. the twenty pages on the proof of Gödel’s key Theorem VI will gel with those who haven’t previously encountered an exposition of the main ideas in one of the standard textbooks. This is the very difficulty I foresaw in pursuing plan (C). Most readers without much background will be better off reading a modern textbook.

But, on the other hand, for those who have already read GWT (to pick an example at random!), i.e. those who already know something of Gödelian incompleteness, they should find this a useful companion if they want to delve into the original 1931 paper. Though some of the exposition will now probably be unnecessarily laboured for them, while they would have welcomed some more  “compare and contrast” explanations bringing out more explicitly how Gödel’s original relates to standard modern presentations.

In short, then: if someone with a bit of background does want to study Gödel’s original paper, whereas previously I’d just say ‘read the paper together with its Introductory Note in the Collected Works’, I’d now add ‘and, while still doing that, and depending quite where you are coming from and where you stumble, you might very well find some or even all of the commentary in Hal Prince’s The Annotated Gödel a pretty helpful accompaniment’.

4 thoughts on “The Annotated Gödel”

  1. It’s very interesting to see your comments, and I’m glad another useful Godel book has appeared.

    I think you’re being a bit too hard on its typographical, notational, and naming choices though, and I think you may have, perhaps unintentionally, made it seem that seem that Prince’s translation is less helpful (or at least no more helpful) than one that uses Godel’s 1931 notations and German-based vocabulary for the names in the proof — so that it’s only Prince’s commentary that might help readers. I find the translation more helpful than the commentary, but I wouldn’t be able to spot errors in it as easily as you could (so I’m glad you haven’t spotted any major ones so far).

    While I agree that some of Prince’s typographical choices might look ‘unprofessional’, I don’t think they’re actually very bad. (The only one I really don’t like is the use of grey background. Plenty of professionally produced textbooks do that, though.)

    * I think that it’s good that the translation blocks aren’t split across pages. I’d find a split quite annoying, unless perhaps it was across facing pages, and I think other readers might too. I think it’s better to have some blank inches than to split a block. (What often happens in professionally produced books is that special boxes ‘float’ a bit, to avoid splitting them while also avoiding blank space.)

    * I don’t know whether Prince’s notation for substitution is from computer science. I think it’s readable, though, and fairly concise. I certainly prefer it to the “/” that many people seem to use, and to notations that involve super- and subscripts. I don’t think it makes for mess or that it’s confusing to have different-looking arrows, pointing in different directions, mean such different things.

    * While it might not be necessary to tell the reader that ‘Prov’ is a property each time it appears, ‘is’ is a rather minimal way to do it and will be familiar to many readers from Java (and some other languages). It’s fairly common in programming languages to give predicates / boolean-valued functions names that reflect that, and it should be done consistently. So while ‘Prov” might occur so often that the reader doesn’t need to be reminded, the choice is really between having no property names indicate that they’re property names or having all of them do it.

    I think it removes a cognitive burden from the reader (remembering or figuring out each time whether a name names a property) which will help readers who aren’t already so familiar with the proof that it they don’t need it. I found it helpful anyway.

    Do you have examples of “off-putting longwindedness when rendering long formulas” other than his naming choices? Nothing else that you mention looks like it would make formulas longer, so I’m wondering if that’s all there is.

    (Mathematicians seem strongly inclined towards short names, often single-letter ones, and will resort even to unreadable alphabets to help them achieve this. (Is 𝕬 a U? (No). What on earth is 𝕰 or 𝕲? Which letter isℐ ?) That might work for people who read and write many formulas in the relevant subject area; it doesn’t work so well for other people.)

    1. My concern about some of the typographical choices was that they could give a really quite misleading impression of the quality of the book: that’s why I thought/think them a bit unfortunate.

      The use of “is” as a component of every defined predicate expression means that it can appear five times in a wff: that seems unnecessary clutter to me. If you insist on marking the difference between predicate and function expressions in the syntax, then upper case initials for predicates and lower case for functions is a classic choice.

      As for “longwindedness” that was perhaps over-egging it: but there are cases where P’s version sprawls over four lines as against G’s two.

      1. I can understand not liking ‘is’-names. I didn’t like them when I first saw them.

        However, I think that, over the years, programmers have worked out some useful conventions for names and for laying out expressions, statements, etc that are written in a formal language (such as a programming language). Mathematicians tend to use different conventions that reflect a strong preference for brevity. The mathematicians’ approach seems to work well for people who are immersed in a relevant mathematical subject. I think the programmer’s approach often produces something that’s easier for people who aren’t so immersed to read.

        Using ‘is’-names isn’t the only programming convention or one that everyone likes. It is pretty clear, though, because the name naturally suggests a yes/no question. (I see it as useful rather than clutter.) The difference between an initial capital letter and a lower case one doesn’t naturally suggest anything relevant. It’s also such a small difference that it would be easy to make a mistake when reading or writing.

        Shorter expressions aren’t necessarily clearer or easier to read. The meaning of a formula can be easier to discern when longer names are used or when written over four lines rather than two. It depends on the formula and on where the line breaks occur. For example, a disjunction with 4 disjuncts can be easier to read when written 1-per-line than when it’s 2-per-line or 3 on one line and 1 on the other.

      2. It’s interesting the ongoing cold-war between compsci and pure maths seems so centered in syntax. In anecdotal discussions with compsci people the response to maths seems almost always that “the notation is impossible”, and this DSL of Maths book ( https://chalmers.instructure.com/courses/17542 ) seems to be getting at the same.

        And, after reading this post as well, now i’m wondering how much of this syntactic divergence is just a natural property of divergent practice; in a maths setting we write informal snippets on blackboards and read books that are mostly natural language with a few formal lines interspersed, while in compsci we type into editors with autocomplete for longer keywords, and where everything is code except a few interspersed comments. This latter environment i think gives rise to practices like prefacing with “is” (or in some languages suffixing with ?) not only because we’re stuck with plain ascii but also for the sake of consistency and disambiguation, with every name unique to its namespace but also standardised. Sans surrounding commentary, the code must be able to explain itself, and, without the constraint of handwriting, there’s less emphasis placed on brevity.

        At any rate it’s interesting to think about how these differences came about, and that proof assistants might finally be bridging the gap.

Leave a Comment

Your email address will not be published. Required fields are marked *

Scroll to Top