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}$ without $\operatorname{TC5}$ has a decidable extension, 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.)
