The theory of concatenation (TC) can be equivalently expressed as the following assumptions:
- Closure of strings under concatenation $+$.
- Existence of an empty string $e$, namely $e+x = x = x+e$ for any string $x$.
- Associativity of $+$ on strings, namely $(x+y)+z = x+(y+z)$ for any strings $x,y,z$.
- Existence of distinct symbols $p,q$, namely distinct strings $p,q$ such that
$p \ne u+v$ and $q \ne u+v$ for any non-empty strings $u,v$.
- Given any strings $a,b,c,d$ such that $a+b = c+d$, there is a string $x$ such that
either ( $a+x = c$ and $b = x+d$ ) or ( $a = c+x$ and $x+b = d$ ).
Formally in first-order logic, TC is axiomatized as the theory with a binary function-symbol $+$ and constant-symbol $e$ and the following axioms:
- $∃e ∀x ( x+e = x = e+x )$.
- $∀x,y,z ( (x+y)+z = x+(y+z) )$.
- $∃x,y ( x≠y ∧ ¬∃u,v ( u≠e ∧ v≠e ∧ ( x=u+v ∨ y=u+v ) ) )$.
- $∀a,b,c,d ( a+b = c+d ⇒ ∃x ( a+x=c ∧ b=x+d ∨ a=c+x ∧ x+b=d ) )$.
Someone asked me (essentially) whether TC proves the cancellation property. This can be split into left-cancellation (LC) and right-cancellation (RC):
- (LC) $∀x,y,c ( c+x = c+y ⇒ x=y )$.
- (RC) $∀x,y,c ( x+c = y+c ⇒ x=y )$.
Of course, finite strings (the intended model of TC) satisfy cancellation (both LC and RC). So the question can be understood as asking whether these are independent over TC. Incidentally, LC and TC can be proven by TC plus a suitable induction schema.
I came up with countable binary-labelled linear orders modulo isomorphism (with $+$ interpreted as concatenation modulo isomorphism) as a model of TC that fails to satisfy cancellation. I also realize that countable binary-labelled well-orders modulo isomorphism is a model of TC and LC but not RC, because for any well-ordering every prefix embeds uniquely into itself, but not suffixes. An explicit counter-example for RC is $(0)+(0,0,0,\cdots) = ()+(0,0,0,\cdots)$.
My questions are:
What are other simple models of TC+LC+¬RC?
Is there a more systematic way of finding a model? (Mine was ad-hoc.)
I think TC and PA$^-$ are bi-interpretable. If so, can we utilize that to find nice models?