Detour: Computation and Nand2Tetris
The last five posts have been proofs from my reading of Limits Of Logic. That book is divided roughly into an introduction plus three parts — model theory, computation theory and proof theory.
My last post about Tarski’s Undefinability theorem is somewhat the peak result from pure model theory that the book explores, that the set of all true sentences in the standard string structure is undefinable i.e. there is no one formula in (such as TRUE(x)) that is true of all and only true sentences in . In other words, that “truth is undefinable”. This is the first big checkpoint in the journey towards Godel’s Incompleteness theorems, which is essentially the destination in Limits Of Logic.
I haven’t posted in a while and that’s because I’ve taken a short detour after planting a flag at this checkpoint. I read through the rest of Limits Of Logic and I realized that I don’t have the 30,000 feet overview of the landscape that’ll let me appreciate the results in the remainder of the book. But I knew where to climb to get that overview.
The remainder of Limits Of Logic first introduces the concept of computation/computability and proves results about the limits of our analysis of programs — what questions can and cannot be answered by any computer program that can possibly be written, particularly via working through the halting problem that there is no method or algorithm that can tell whether a given program will ever halt (in completion or error) or keep going on forever. It then introduces proof theory and immediately relates how all proofs are essentially computations. The reason to explicitly form this relation is that is the basis for a good, modern intuition of Godel’s Incompleteness theorem.
This intuition was a bit much for me to grasp. In an abstract way, sure I can accept results about computability and that “proofs are just computations”, but when I looked within me I knew I didn’t really get it. I’ve written software and I roughly know modern computer architecture and how it is ultimately equivalent in its computational repertoire to the tape Turing machine. But the level of obviousness with which this universality of computation is stated in Limits Of Logic and elsewhere was just not within me. In what sense is the tape Turing machine computationally equivalent to my MacBook? Seems ridiculous doesn’t it?
I knew the stop in my detour is Nand2Tetris. It’s a series of hardware and software projects where you start out with building logic gates and keep building up the hierarchy to end up with a computer that can run Tetris. (I’m at the final bit of this project series where I get to write a compiler; here’s an assembler I wrote whose job is to translate a machine/assembly language into the right 1s and 0s that’ll run on the Hack Computer chip — isn’t that cool!?) I can now see, in a very structured and understandable manner, how a MacBook does boil down to manipulating electrical charges via logic gates, and the sense in which it is computationally equivalent to the tape Turing machine.
The detour is not over just yet. I’ve been reading through the Fabric Of Reality and consuming interviews of Penrose and others on the Incompleteness theorem, computability, etc. to gain perspective on where Godel’s incompleteness theorems sit in the broader landscape of physics and math. I hope to share more soon.