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

<p>This is the usual approach to logic on words which goes back to Büchi, see <a href="https://link.springer.com/article/10.1007/BF02127803" rel="nofollow noreferrer">this survey</a>, or <a href="https://arxiv.org/abs/1011.6491" rel="nofollow noreferrer">this survey</a>, or these <a href="https://www7.in.tum.de/um/courses/auto/ws1718/slides1718/10-MSOL.pdf" rel="nofollow noreferrer">slides</a>.</p>

<p>This generalizes the logic over <span class="math-container">$\mathbb N$</span> (special case of <span class="math-container">$|\Sigma|=1$</span>) with <span class="math-container">$&lt;$</span> and <span class="math-container">$=$</span>.</p>

<p>But this logic does not allow me to describe languages (sets of words) similar as the <a href="https://en.wikipedia.org/wiki/Arithmetical_hierarchy" rel="nofollow noreferrer">Arithmetical Hierarchy</a> allows me to describe subsets of <span class="math-container">$\mathbb N$</span>, 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 <span class="math-container">$\mathbb N$</span>.</p>

<p>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 <span class="math-container">$\varphi(w) = \exists x R_a(w,x)$</span> with free word variable <span class="math-container">$w$</span>, i.e. we have 
<span class="math-container">$$
 w \in \Sigma^* a \Sigma^* \Leftrightarrow \varphi(w).
$$</span>
Is there anything done in that direction? Or are there other approaches with similar goals?</p>

CC BY-SA 4.0
2019-06-06T19:19:17.837Z
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
CC BY-SA 4.0
2019-06-06T21:57:50.017Z
@EmilJeřábek Thanks for comment; could you give more specific details or points to literature?
StefanH
CC BY-SA 4.0
2019-06-07T06:11:17.727Z
I would start with Cook & Nguyen, Logical foundations of proof complexity.
Emil Jeřábek
<lo.logic><fl.formal-languages><first-order-logic>
Extending the sequential calculus (logic over words) to allow a hierarchy of languages like the arithmetical hierarchy
StefanH
# Extending the sequential calculus (logic over words) to allow a hierarchy of languages like the arithmetical hierarchy

(Asked by: username_0 on 2019-06-06)

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](https://link.springer.com/article/10.1007/BF02127803), or [this survey](https://arxiv.org/abs/1011.6491), or these [slides](https://www7.in.tum.de/um/courses/auto/ws1718/slides1718/10-MSOL.pdf).

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](https://en.wikipedia.org/wiki/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?

**Tags:** lo.logic, fl.formal-languages, first-order-logic

> **Comments:**
> **username_1**: 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.  
> **username_0**: @EmilJeřábek Thanks for comment; could you give more specific details or points to literature?  
> **username_1**: I would start with Cook & Nguyen, Logical foundations of proof complexity.  

---

## 0 answers

