We study first-order concatenation theory with bounded quantifiers. We give axiomatizations with interesting properties, and we prove some normal-form results. Finally, we prove a number of decidability and undecidability results.

In the language \(\lbrace 0, 1, \circ, \preceq \rbrace \), where 0 and 1 are constant symbols, \(\circ \) is a binary function symbol and \(\preceq \) is a binary relation symbol, we formulate two theories, \( \textsf {WD} \) and \( {\textsf {D}}\), that are mutually interpretable with the theory of arithmetic \( {\textsf {R}} \) and Robinson arithmetic \({\textsf {Q}} \), respectively. The intended model of \( \textsf {WD} \) and \( {\textsf {D}}\) is the free semigroup generated (...) by \(\lbrace {\varvec{0}}, {\varvec{1}} \rbrace \) under string concatenation extended with the prefix relation. The theories \( \textsf {WD} \) and \( {\textsf {D}}\) are purely universally axiomatised, in contrast to \( {\textsf {Q}} \) which has the \(\varPi _2\) -axiom \(\forall x \; [ \ x = 0 \vee \exists y \; [ \ x = Sy \ ] \ ] \). (shrink)

We show that we can interpret concatenation theories in arithmetical theories without coding sequences by identifying binary strings with \(2\times 2\) matrices with determinant 1.