# Extending the sequential calculus (logic over words) to allow a hierarchy of languages like the arithmetical hierarchy

Let $$\Sigma$$ be some finite alphabet. Then consider the logical language $$\mathcal L = \{ R_a : a \in \Sigma \} \cup \{ <,= \}$$ and first order formulas. For a given first order formula $$\varphi$$ a word $$w \in \Sigma^*$$ is a structure for it in the sense that the variables range over $$\{ 1, \ldots, |w| \}$$, where $$|w|$$ denotes the length of $$w$$ and $$R_a = \{ 1 \le i \le |w| : \mbox{ the word w has symbol a at position i } \}$$. For example for $$a \in \Sigma$$ $$\exists x ( R_ax)$$ describes the language of all words with at least one $$a$$ in it.

This is the usual approach to logic on words which goes back to Büchi, see this survey, or this survey, or these slides.

This generalizes the logic over $$\mathbb N$$ (special case of $$|\Sigma|=1$$) with $$<$$ and $$=$$.

But this logic does not allow me to describe languages (sets of words) similar as the Arithmetical Hierarchy allows me to describe subsets of $$\mathbb N$$, the problem is that the variables are over the positions of a word, not the words itself. Hence I can just use them to define subsets of $$\mathbb N$$.

Is there any logic or variation such that the variables run over words and I can us formulas to built up a hierarchy like the Arithmetical Hierarchy? I somehow think about a multi-sorted logic where I can quantify over words and positions, such that the above set could be defined by $$\varphi(w) = \exists x R_a(w,x)$$ with free word variable $$w$$, i.e. we have $$w \in \Sigma^* a \Sigma^* \Leftrightarrow \varphi(w).$$ Is there anything done in that direction? Or are there other approaches with similar goals?

• I’m not sure if this is what you are asking, but you can easily formulate arithmetic in such a way that the basic objects are finite strings rather than natural numbers. This is in fact commonly done for systems of bounded arithmetic, in the two-sorted set-up. – Emil Jeřábek Jun 6 '19 at 19:19
• @EmilJeřábek Thanks for comment; could you give more specific details or points to literature? – StefanH Jun 6 '19 at 21:57
• I would start with Cook & Nguyen, Logical foundations of proof complexity. – Emil Jeřábek Jun 7 '19 at 6:11