Archive for September 17th, 2010

Fun With Robinson Arithmetic

September 17, 2010

in yesterday’s notes I mentioned Robinson Arithmetic (\mathsf{Q}) as a subsystem of the axiom system \textup{T} in Hellman’s example. Just because it’s so much fun, let’s talk about \mathsf{Q}.  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). \dot{\mathsf{S}}x indicates the successor function that returns the successor of x.

Robinson Arithmetic

(\textup{S1}) \ \forall x (\neg \dot{0} \ \dot{=} \ \dot{\mathsf{S}}x)
(\textup{S2}) \ \forall x \forall y (\dot{\mathsf{S}}x \ \dot{=} \ \dot{\mathsf{S}} y \rightarrow x \dot{=} y)
(\textup{L1}) \ \forall x (\neg x \dot{<} \dot{0})
(\textup{L2}) \ \forall x \forall y [x \dot{<} \dot{\mathsf{S}}y \leftrightarrow (x \dot{<} y \vee x \dot{=} y)]
(\textup{L3}) \ \forall x \forall y [(x \dot{<} y) \vee (x \dot{=} y) \vee (y \dot{<} x])
(\textup{A1}) \ \forall x (x \dot{+} \dot{0} \dot{=} x)
(\textup{A2}) \ \forall x \forall y [x \dot{+} \dot{\mathsf{S}}y \dot{=} \dot{\mathsf{S}}(x \dot{+} y)]
(\textup{M1}) \ \forall x (x \dot{\times} \dot{0} \dot{=} \dot {0})
(\textup{M2}) \ \forall x \forall y [(x \dot{\times} \dot{\mathsf{S}}y) \dot{=} (x \dot{\times} y) \dot{+} x]

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.

(\textup{S1}) \mapsto 1
(\textup{S2}) \mapsto 2
(\textup{L1}) \mapsto 7
(\textup{L2}) \mapsto 8
(\textup{L3}) \mapsto 9
(\textup{A1}) \mapsto 3
(\textup{A2}) \mapsto 4
(\textup{M1}) \mapsto 5
(\textup{M2}) \mapsto 6

This is going to be as confusing as keeping track of names in One Hundred Years of Solitude. Boolos et al compare \mathsf{Q}/minimal arithmetic to the system \mathsf{R}, which has historically been called “Robinson Arithmetic”.  \mathsf{R} differs from \mathsf{Q} in that it contains,

(\textup{Q0}) \ \forall x [x \dot{=} \dot{0} \vee (\exists y) (y \dot{=} \dot{\mathsf{S}}y)]

And it replaces \textup{L1}-\textup{L3} with,

(\textup{Q10}) \ \forall x \forall y [x \dot{<} y \leftrightarrow \exists z (\dot{\mathsf{S}}z \dot{+} x \dot{=} y)

In their comparison Boolos et al conclude that \mathsf{Q} and \mathsf{R} have a lot in common (e.g., some of the same theorems are provable), but in some cases \mathsf{R} is stronger than \mathsf{Q} –e.g., in the non-standard ordinal model of \mathsf{Q} some simple laws (like \dot{1} \dot{+} x \dot{=} x \dot{+} \dot{1}) fail to hold, in addition to (\textup{Q0}) and (\textup{Q10}).  At the same time, howerver, \mathsf{Q} is in some cases stronger than \mathsf{R}.  For example, there is a model (with domain \omega and non standard elements a and b and natural interpretations of \dot{0}, \dot{+}, \dot{\times}, \dot{\mathsf{S}}x of \mathsf{R} where basic laws like x \dot{<} \dot{\mathsf{S}}x fail to hold.

While it’s easier to represent all recursive functions in \mathsf{Q} is than it is to do so in \mathsf{Q} than in \mathsf{R}, any one of these will do for Hellman’s example.  What’s interesting is that in theories like \mathsf{Q} and \mathsf{R} 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.

Posted in Robinson Arithmetic, Undefinability of Truth | Leave a Comment »

Follow

Get every new post delivered to your Inbox.