Some questions regarding an alteration of Grzegorczyk's theory of concatenation, $\operatorname{TC}$

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.)

• @Arthur Fisher: I approve your edits. Make the necessary changes (I really dont how to do them myself), but leave the 'math-philosophy' tag. It is appropriate. Thanks. – Thomas Benjamin Dec 1 '15 at 11:02
• I personally don't see any philosophical content to this question (and was and am doubtful about the appropriateness of the foundations tag), but I'm not going to fuss about this. (There is a fair bit of information about the Markdown syntax here – user642796 Dec 1 '15 at 11:15
• Adding a definitional axiom does not affect decidability or consistency of a theory, or pretty much any useful property of the theory for that matter. – Emil Jeřábek Dec 1 '15 at 12:57
• Emil has answered Questions 1 and 2. As for Question 3, considering that the theory is true (in the intended interpretation), it remains consistent when any true sentences are added. That would apply, in particular, to any theory of "the primitive recursive functions (appropriately recast in the language of concatentation)". I'm assuming here that false axioms would not count as appropriate recasting. – Andreas Blass Dec 1 '15 at 14:11
• In the article we only conjectured that TC is a minimal essentially undecidable theory. We weren't able to show that leaving TC1, the associativity, gives a theory with a decidable extension. The problem is that it seems that an adaptation of the classical method of shortening cuts does not work without the associativity assumed (so we do not get essential undecidability of such a weaker theory). But we could not show that it actually has a decidable extension. – Konrad Zdanowski Dec 2 '15 at 22:31