My first ‘lockdown book’ was Douglas Hofstadter’s Gödel, Escher, Bach - I can heartily recommend it! I’m completely ignorant about formal logic and still enjoyed it tremendously.
I love that book. It is mind bending, and so well-written you don’t need to be a mathematician to understand it.
Would it work in audio book form? Are there a lot of graphics?
Sadly I think it would suffer - it features some lovely hand-drawn diagrams and many Escher drawings.
Thanks for linking this article - I’ve heard of Goedel’s proof before of course, but never previously tried to understand it. It’s interesting that one of the key insights involves creating a mapping between the typographical symbols of written math proofs, and integers. This insight seems a little more obvious now that ASCII has existed for over half a century and any programmer or hardware engineer is used to treating textual symbols as numbers inside a computer. Goedel had this insight in 1931, which was before the age of the electronic computer - but not that many years before it.
Turing had many of the same insights around the same time, and everybody was, if not talking to each other, at least vaguely aware of each other. What’s really interesting to me is that around three decades later, Lawvere simplified and unified these results of Turing, Tarski, Gödel, and also Cantor and Russell, into Lawvere’s fixed-point theorem, and this unified theorem is still quite unknown, even among folks who grok Gödel’s work.