Consider Grzegorczyk's concatenation theory $\operatorname{TC}$, a "weak theory of words over the two letter alphabet $\Sigma=\{a,b\}$" (this from Grzegorczyk and Zdanowski's paper _Undecidability and Concatenation_, pp.72-91 in _Andrzej Mostowski and Foundational Studies_, A. Ehrenfeucht, V.W. Marek, M. Srebrny (eds.)).

* **TC1:** $x{\frown}(y\frown z)=(x\frown y)\frown z$
* **TC2:** $x{\frown}y=z{\frown}w \Rightarrow \\ ((x=z \land y=w) \lor \exists u((x{\frown}u=z \land y=u{\frown}w) \lor (x=z{\frown}u \land u{\frown}y=w))$
* **TC3:** $\lnot (\alpha =x \frown y)$
* **TC4:** $\lnot (\beta =x \frown y)$

* **TC5:** $\lnot (\alpha = \beta )$, 

(where in TC3-5 $\alpha$ and $\beta$ denote the one letter words $a$ and $b$ respectively).

It should be noted that in the aforementioned paper Grzegorczyk and Zdanowski prove $\operatorname{TC}$ essentially undecidable, however, they also note that $\operatorname{TC}$ is also minimally essentially undecidable, e.g., from p.85 of the article:

> Indeed, if we drop TC5 then we can interpret all axioms in the model for arithmetic without zero $(\omega \setminus \{0\}, +, 1,1)$.  By Presburger['s] theorem this model has a decidable theory.

Suppose now that one drops TC5 and adds the following axiom introducing the notion of _subtext_ $x \lt y$,  i.e. '$x$ is a subtext of $y$':

* **TC5a:**  $x \lt y \Longleftrightarrow y=x \lor (\exists z,w )(x=y \frown z  \lor x=z \frown y \lor x=z \frown y \frown w)$

---

* **Question 1:**  Is this new theory also decidable?

* **Question 2:**  Is this theory also consistent?

* **Question 3:**  If this theory is consistent, can the primitive recursive functions (appropriately recast in the language of concatenation) be consistently added? Can the first-order predicate calculus with only bounded numerical quantification be consistently added as well?

* **Question 4.** How much of 'contentual number theory' does the resulting theory capture?

(It should be noted that semantical (i.e. model theoretic) methods can be used here, much as Hilbert and Bernays did in the _Grundlagen_, vol I,ch. 2, "Elementary Number Theory--Finitistic Inference and its Limits.)