Logic

I’m still half-buried under tripos marking, but the end is in sight. And I’m Chair of the Examining Board for Parts IB and II this year, which is also not exactly an anxiety-free job. But between times, I’m trying to reorganize and finish the chapters of my book on the Second Theorem. I’m stuck for the moment wondering what exactly to say about “the best and most general version of the unprovability of consistency in the same system” which Gödel so briefly alludes to in the first part of his 1972a note (which repeats a footnote from 1967). Feferman in his editor’s introduction explains things by bringing to bear Jeroslow’s 1973 result. But it isn’t entirely clear to me that this rather esoteric result must be what Gödel had in mind.

Meanwhile, a nerdy footnote. There’s an even better new version out of NoteBook just out (if you are a Mac user, it really is just indispensable, and the academic price is absurdly low).

One of the many things I want to do once I’ve got my Gödel book finished is to slowly trawl through the first twenty years (say) of JSL to see what what our ancestors knew and we’ve forgotten.

I was put in mind of this project again by finding that John Myhill in JSL 1952 (‘A derivation of number theory from ancestral theory’) already had answers to some questions that came up in re-writing a section of the book last week.

As is entirely familiar, we can define the ancestral of a relation R using second-order ideas: but it doesn’t follow from that that the idea of the ancestral is essentially second-order (as if the child who cottons on to the idea of someone’s being one of her ancestors has to understand the idea of arbitrary sets of people etc.) Which in fact is another old point made by e.g. R. M. Martin in JSL 1949 in his ‘Note on nominalism and recursive functions’. So there is some interest in considering what we get if we extend first-order logic with a primitive logical operator that forms the ancestral of a relation.

It’s pretty obvious that the semantic consequence relation for such an ‘ancestral logic’ won’t be compact, so the logic isn’t axiomatizable. But we can still ask whether there is a natural partial axiomatization (compare the way we consider natural partial axiomatizations of second-order logic). And Myhill gives us one. Suppose R* is the ancestral of R, and H(F, R) is the first-order sentence which says that F is hereditary down an R-chain, i.e. AxAy((Fx & Rxy) –> Fy). Then, putting it in terms of rules, Myhill’s formal system comes to this:

• From Rab infer R*ab
• From R*ab, Rbc infer R*ac
• From H(F, R) infer H(F, R*)

where the last rule is equivalent to the elimination rule

• From R*ab infer (Fa & H(F, R)) –> Fb

which is an generalized induction schema. Myhill shows that these rules added to some simple axioms for ordered pairs give us first-order Peano Arithmetic. But do they give us more?

Suppose PA* is first-order PA plus the ancestral operator plus the axiom

• Ax(x = 0 v S*0x)

i.e. every number is zero or a successor of zero. Then — if we treat the ancestral operator as a logical constant with a fixed interpretation — this is a categorical theory whose only model is the intended one (up to isomorphism). But while semantically strong it is deductively weak. It is conservative over PA. To see this note that we can define in PA a proxy for R*ab by using a beta-function to handle the idea of a finite sequence of values that form an R-chain, and then Myhill’s rules and the new axiom apply to this proxy too. And hence any proof in PA* can be mirrored by a proof in plain PA using this proxy. (Thanks to Andreas Blass and Aatu Koskensilta for that proof idea.)

So the situation is interesting. Arguably, PA doesn’t reflect everything we understand in understanding school-room arithmetic: we pick up the idea that the numbers are the successors of zero and nothing else. In other words, we pick up the idea that the numbers all stand to zero in the ancestral of the successor relation. So arguably something like PA* does better at reflecting our elementary understanding of arithmetic. Yet this theory’s extra content does nothing for us by way of giving us extra proofs of pure arithmetic sentences. Which is in harmony with Dan Isaacson’s conjecture that if we are to give a rationally compelling proof of any true sentence of basic arithmetic which is independent of PA, then we will need to appeal to ideas that go beyond those which are constitutive of our understanding of basic arithmetic.

To blog or not to blog? I’m in two minds. But why not just dive in and see how it goes?

Today was my second outing this academic year to talk to non-philosophers in Cambridge about Gödel, incompleteness and the like. The first time was at a meeting of the Trinity Math. Society. Rather staggeringly, there were more than eighty people there. Perhaps not a brilliantly judged talk, but I did have good fun e.g. telling them about Goodstein’s Theorem. (Having a lot of bright mathmos getting the point and smiling at the cheek of the Goodstein proof made a nice change.)

Today’s outing was to give a talk at CMS to the slightly unfortunately named CUSPOMMS. A very mixed audience, we meet there approximately fortnightly for talks on the philosophy of mathematics, broadly construed. Rather perversely, I suppose, there was less philosophy than in the Trinity talk. In the event, I was explaining one pretty way of proving (a version of) Gödel’s First Theorem without explicitly constructing a Gödel sentence that codes up ‘I am unprovable’. The point of doing this is to counteract that familiar tendency to think that the Gödelian result must be fishy because it depends on something too close to the Liar paradox for comfort.

Paul Erdös had the fantasy of a Book in which God records the smartest and most elegant proofs of mathematical results (have a look at the terrific Proofs from the Book by Aigner, Hofmann and Ziegler). So I was aiming to outline one Book proof: here is a version of the talk.