What is the theory for the quaternions?

Question

The axiomatic theory for the natural numbers is PA. For the reals it's RCF and for the complex numbers it's ACF. What's the theory for the quaternions?

Answer 1

The quaternions have the nice feature that we can recover the reals inside them in a definable way - in stark contrast to the situation with $\mathbb{C}$. Specifically, $\mathbb{R}$ sits inside $\mathbb{H}$ as the latter's center, the set of elements which (multiplicatively) commute with everything. Consequently the whole theory $Th(\mathbb{H})$ is generated by the (noncommutative unital) ring axioms, + $\mathsf{RCF}$ relativized to the center, + the existence of a triple of elements $i,j,k$ which multiply appropriately and together with $1$ span the whole ring over the center.

The proof that this works is similar to this answer where the same idea develops a complete axiomatization for the field $\mathbb{C}$ together with a predicate naming $\mathbb{R}$. Note that per the first sentence of this answer, there's no model-theoretic difference between $\mathbb{H}$ and "$\mathbb{H}$-with-$\mathbb{R}$-labelled."