Notes on Interpretability between Weak First-order Theories: Theories of Sequences

We introduce a first-order theory Seq which is mutually interpretable with Robinson's Q. The universe of a standard model for Seq consists of sequences. We prove that Seq directly interprets the adjuctive set theory AST, and we prove that Seq interprets the tree theory T and the set theory AST + EXT.