Ancestral logic

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.