Concatenation theory

Concatenation theory, string theory, or more fully character-string theory, also called theoretical syntax, studies character strings over finite alphabets of characters, signs, symbols, or marks. The most basic operation on strings is concatenation, connecting two strings to form a longer string whose length is the sum of the lengths of the operands: abcde is the concatenation of ab with cde, in symbols abcde = ab ^ cde. String theory is foundational for formal linguistics, computer science, logic, and metamathematics especially proof theory. A generative grammar can be seen as a recursive definition in string theory. Mathematically inclined logicians noticed that string concatenation resembled number addition: both are homogeneous, associative, totally defined, two-place operations. This leads to discovery that strings-under-concatenation gives rise to mathematical theories analogous to theories of numbers-under-addition. Logicians then realized that the axiomatic tradition traced to Euclid’s predecessors required such theories be treated axiomatically. In 1956 Alonzo Church wrote: "Like any branch of mathematics, theoretical syntax may, and ultimately must, be studied by the axiomatic method". Church was evidently unaware that string theory already had two axiomatizations from the 1930s: one by Hans Hermes and one by Alfred Tarski. Coincidentally, the first English presentation of Tarski’s 1933 axiomatic foundations of string theory appeared in 1956 - the same year that Church called for such axiomatizations. As Tarski himself noted using other terminology, serious difficulties arise if strings are construed as tokens rather than types in the sense of Pierce's type-token distinction, not to be confused with similar distinctions underlying other type-token distinctions.