in yesterday’s notes I mentioned Robinson Arithmetic () as a subsystem of the axiom system in Hellman’s example. Just because it’s so much fun, let’s talk about . The axioms are listed below. The dot notation distinguishes between the symbol used and the relation it represents (this notation was used earlier without explanation here and here). indicates the successor function that returns the successor of .
These axioms are from Hinman and correspond to what Boolos, Burgess and Jeffrey (in chapter 16 of Computability and Logic) call “minimal arithmetic”. Since the Boolos et al book is so widely studied, here is a map linking both axiomatizations.
This is going to be as confusing as keeping track of names in One Hundred Years of Solitude. Boolos et al compare /minimal arithmetic to the system , which has historically been called “Robinson Arithmetic”. differs from in that it contains,
And it replaces - with,
In their comparison Boolos et al conclude that and have a lot in common (e.g., some of the same theorems are provable), but in some cases is stronger than –e.g., in the non-standard ordinal model of some simple laws (like ) fail to hold, in addition to and . At the same time, howerver, is in some cases stronger than . For example, there is a model (with domain and non standard elements and and natural interpretations of , , , of where basic laws like fail to hold.
While it’s easier to represent all recursive functions in is than it is to do so in than in , any one of these will do for Hellman’s example. What’s interesting is that in theories like and which lack an induction schema (and thus fall just short of Peano Arithmetic) the truth predicate is undefinable.
Hopefully in the next update I’ll be able to get to Hellman’s second definability example.