I have been mightily distracted from this blog by, first, trying to get the Gödel book into a state where it could go to CUP’s proof-reader and then, second, by the beginning of term. But the book is off, and life is settling into what passes for normality in term-time.

The high point so far is our new Mathematical Logic Reading Group (started by popular request). We are starting by working through the opening chapter of Simpson’s Subsystems of Second Order Arithmetic. The trouble we are having–wearing our philosophical hats–is to get the five key subsystems that Simpson highlights aligned to clear philosophical motivations. We can do that for ACA0; but not, for example, for the base system RCA0 with its curious mismatch between its Delta1 comprehension axiom and Sigma1 induction. And it is worrying–isn’t it?–that the chosen base system resists a clear conceptual defence. I’ll report back if we come to any less inchoate conclusions.