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?

  • 1
    $\begingroup$ 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. $\endgroup$ – Emil Jeřábek Jun 6 '19 at 19:19
  • $\begingroup$ @EmilJeřábek Thanks for comment; could you give more specific details or points to literature? $\endgroup$ – StefanH Jun 6 '19 at 21:57
  • $\begingroup$ I would start with Cook & Nguyen, Logical foundations of proof complexity. $\endgroup$ – Emil Jeřábek Jun 7 '19 at 6:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.