<p>FO(LFP) captures PTIME on ordered structures, and strings are ordered structures.  So the languages definable by FO(LFP) include all regular languages and much much more.
<a href="http://dx.doi.org/10.1016/S0019-9958(86)80029-8">http://dx.doi.org/10.1016/S0019-9958(86)80029-8</a></p>

<p>Ebbinghaus and Flum's textbook contains an exercise that asks to show FO(TC^1) (first-order logic extended with transitive closures of binary relations) is equivalent to MSO on strings. In the same exercise, $\{ a^n b^n \mid n \geq 1 \}$ is used as an example to show FO(TC^2) is more expressive than MSO on strings.  All FO(TC) formulas are clearly equivalent to FO(LFP) formulas.</p>

CC BY-SA 3.0
2012-01-30T22:45:34.757Z
Excellent. I don't know what you mean by TC^1 and TC^2, is that a typo? As far as I know, in the book you mention the notation used is FO(TC) for the extension of FO with *transitive closure* and FO(DTC) for the extension of FO with *deterministic transitive closure*, which is defined differently. I haven't found the exercise you mention, though. It remains to see whether there is an operator less expressive than TC that still allows to capture regular languages. I will update my question accordingly.
Janoma
CC BY-SA 3.0
2012-01-28T22:32:17.173Z
2012-01-28T22:32:17.173Z
Makoto Kanazawa
<p>This answer is a bit late, but it is known that one can obtain all and only the regular languages by adjoining a generalized group quantifier for each finite group (or equivalently for each finite simple group). Eg, see "Regular Languages Definable by Lindstrom Quantifiers" by Zoltan Esiky and Kim G. Larsen, at <a href="http://www.brics.dk/RS/03/28/BRICS-RS-03-28.pdf">http://www.brics.dk/RS/03/28/BRICS-RS-03-28.pdf</a>.</p>

<p>Moreover, this is optimal in the sense that a regular language will only be definable if the quantifiers for every group dividing its syntactic monoid are available.</p>

CC BY-SA 3.0
2012-04-11T02:28:42.593Z
2012-04-11T02:28:42.593Z
Ben Standeven
<p>It's Exercise 8.6.3 on page 221 of the second edition of Ebbinghaus and Flum's textbook, <i>Finite Model Theory</i>.  The notation FO(TC$^r$) is explained there.  FO(TC$^r$) can form the transitive closure of a $2r$-ary relation, regarded as a binary relation on $r$-tuples.</p>

<p>I found some more references you might be interested in.</p>

<p>FO(TC$^1$) is called FO(MTC) (first-order logic with monadic transitive closure) in <a href="http://dl.acm.org/citation.cfm?id=1706598">ten Cate and Segoufin's 2010 paper</a>.  It proves, among other things, FO(MTC) is strictly less expressive than MSO on finite trees.</p>

<p><a href="http://www.springerlink.com/content/5l466173q574j788/">Bargury and Makowsky's 1992 paper</a> shows that <i>deterministic</i> monadic transitive closure—FO(DTC$^1$) in Ebbinghaus and Flum's notation—suffices to define regular string languages (see Theorem 5 in this paper).</p>

CC BY-SA 3.0
2012-01-31T03:17:20.057Z
2012-01-31T03:17:20.057Z
Makoto Kanazawa
<h2>Context: relations between logic and automata</h2>

<p>Büchi's Theorem states that Monadic Second Order logic over strings (MSO) captures the class of regular languages. The proof actually shows that existential MSO ($\exists\text{MSO}$ or <em>EMSO</em>) over strings is enough to capture regular languages. This might be a bit surprising, since, over general structures, MSO is strictly more expressive than $\exists\text{MSO}$.</p>

<h2>My (original) question: a <em>minimal</em> logic for regular languages?</h2>

<blockquote>
  <p>Is there a logic which, over general structures, is strictly less expressive than $\exists\text{MSO}$, but that still captures the class of regular languages when considered over strings?</p>
</blockquote>

<p>In particular, I'd like to know what fragment of the regular languages is captured by FO over strings when extended with a least-fixed point operator (FO+LFP). It seems like a natural candidate for what I'm looking for (if it is not $\exists\text{MSO}$).</p>

<h2>A first answer</h2>

<p>As per <a href="https://cstheory.stackexchange.com/a/9968/5396">@makoto-kanazawa's answer</a>, both FO(LFP) and FO(TC) capture more than regular languages, where TC is an operator of transitive closure of binary relations. It remains to be seen whether TC can be replaced by another operator or set of operators in such a way that the extension captures exactly the class of regular languages, and no others.</p>

<p>First-order logic alone, as we know, is not enough, since it captures star-free languages, a proper subclass of the regular languages. As a classical example, the language <strong>Parity</strong>$\;\;=(aa)^*$ cannot be expressed using a FO sentence.</p>

<h2>Updated question</h2>

<p>Here is a new wording of my question, which remains unanswered.</p>

<blockquote>
  <p>What is the <em>minimal</em> extension of first-order logic such that FO + this extension, when taken over strings, captures <strong>exactly</strong> the class of regular languages?</p>
</blockquote>

<p>Here, an extension is minimal if it is the least expressive (when taken over general structures) among all extensions that capture the class of regular languages (when taken over strings).</p>

CC BY-SA 3.0
2012-01-27T22:11:22.963Z
If I am not mistaken, $\mu$-calculus is indeed equivalent to MSO over strings.
Sylvain
CC BY-SA 3.0
2012-01-27T22:15:52.837Z
@Sylvain, any reference? I don't know anything about $\mu$-calculus.
Janoma
CC BY-SA 3.0
2012-01-27T22:27:14.953Z
It appears to be proven in http://dx.doi.org/10.1109/LICS.1988.5137 for the infinite tree, and in http://dx.doi.org/10.1007/3-540-61604-7_60 for the equivalence with the bisimulation-invariant fragment of MSO over arbitrary structures.
Sylvain
CC BY-SA 3.0
2012-01-27T23:19:20.857Z
I'm taking a look at the second paper, though I'm afraid many concepts are new to me. In particular, I didn't know about bisimulation-invariant transition systems. It appears to be that DFA are particular cases of a transition system, but I don't know if they are bisimulation-invariant. If they are, that would answer part of my question (there could be yet another less expressive logic for regular languages); if they are not, I think nothing can be said, for there could still be an equivalence when considering strings only.
Janoma
CC BY-SA 3.0
2012-01-28T00:47:31.757Z
Two _finite words_, seen as transition systems, are bisimilar iff they are isomorphic.  (In the notations of the second paper, a word $a_1\cdots a_n$ in $\Sigma^\ast$ with $\Sigma=2^{\mathit{Prop}}$ can be seen as a transition system $\langle\{1,\dots,n\},1,\{(i,i+1)\mid i<n\},\{i\mid p\in a_i\}_{p\in\mathit{Prop}}\rangle$.)
Sylvain
CC BY-SA 3.0
2012-02-13T18:35:46.003Z
It's not clear to me what would make an extension _minimal_.  For instance, you could imagine that ext1 and ext2 coincide on strings but might capture incomparable classes of general structures.  Also, why should you restrict yourself to full FO+ext?  As the case of the $\mu$-calculus indicates, bisimulation-invariant logics are sufficient for strings, for instance one might venture that PDL (propositional dynamic logic) would be enough.
Sylvain
CC BY-SA 3.0
2012-02-13T18:46:55.100Z
@Sylvain Yep, it could be the case that two extensions coincide over strings but are not comparable over general structures. The reason I want to know about a minimal extension of **FO** is because I'm interested in the "gap" between FO and SO over different structures, make some kind of hierarchy. I don't have it clear myself, it is something I have to talk about with my future advisor if I ever start a PhD in TCS (possible question about career advice there as well).
Janoma
<reference-request><lo.logic><regular-language><finite-model-theory>
What is the minimal extension of FO that captures the class of regular languages?
Janoma
# What is the minimal extension of FO that captures the class of regular languages?

(Asked by: username_0 on 2012-01-27)

## Context: relations between logic and automata

Büchi's Theorem states that Monadic Second Order logic over strings (MSO) captures the class of regular languages. The proof actually shows that existential MSO ($\exists\text{MSO}$ or *EMSO*) over strings is enough to capture regular languages. This might be a bit surprising, since, over general structures, MSO is strictly more expressive than $\exists\text{MSO}$.

## My (original) question: a *minimal* logic for regular languages?

> Is there a logic which, over general structures, is strictly less expressive than $\exists\text{MSO}$, but that still captures the class of regular languages when considered over strings?

In particular, I'd like to know what fragment of the regular languages is captured by FO over strings when extended with a least-fixed point operator (FO+LFP). It seems like a natural candidate for what I'm looking for (if it is not $\exists\text{MSO}$).

## A first answer

As per [@makoto-kanazawa's answer](https://cstheory.stackexchange.com/a/9968/5396), both FO(LFP) and FO(TC) capture more than regular languages, where TC is an operator of transitive closure of binary relations. It remains to be seen whether TC can be replaced by another operator or set of operators in such a way that the extension captures exactly the class of regular languages, and no others.

First-order logic alone, as we know, is not enough, since it captures star-free languages, a proper subclass of the regular languages. As a classical example, the language **Parity**$\;\;=(aa)^\*$ cannot be expressed using a FO sentence.

## Updated question

Here is a new wording of my question, which remains unanswered.

> What is the *minimal* extension of first-order logic such that FO + this extension, when taken over strings, captures **exactly** the class of regular languages?

Here, an extension is minimal if it is the least expressive (when taken over general structures) among all extensions that capture the class of regular languages (when taken over strings).

**Tags:** reference-request, lo.logic, regular-language, finite-model-theory
> **Comments:**
> **username_1**: If I am not mistaken, $\mu$-calculus is indeed equivalent to MSO over strings.  
> **username_0**: @Sylvain, any reference? I don't know anything about $\mu$-calculus.  
> **username_1**: It appears to be proven in http://dx.doi.org/10.1109/LICS.1988.5137 for the infinite tree, and in http://dx.doi.org/10.1007/3-540-61604-7_60 for the equivalence with the bisimulation-invariant fragment of MSO over arbitrary structures.  
> **username_0**: I'm taking a look at the second paper, though I'm afraid many concepts are new to me. In particular, I didn't know about bisimulation-invariant transition systems. It appears to be that DFA are particular cases of a transition system, but I don't know if they are bisimulation-invariant. If they are, that would answer part of my question (there could be yet another less expressive logic for regular languages); if they are not, I think nothing can be said, for there could still be an equivalence when considering strings only.  
> **username_1**: Two _finite words_, seen as transition systems, are bisimilar iff they are isomorphic.  (In the notations of the second paper, a word $a_1\cdots a_n$ in $\Sigma^\ast$ with $\Sigma=2^{\mathit{Prop}}$ can be seen as a transition system $\langle\{1,\dots,n\},1,\{(i,i+1)\mid i<n\},\{i\mid p\in a_i\}_{p\in\mathit{Prop}}\rangle$.)  
> **username_1**: It's not clear to me what would make an extension _minimal_.  For instance, you could imagine that ext1 and ext2 coincide on strings but might capture incomparable classes of general structures.  Also, why should you restrict yourself to full FO+ext?  As the case of the $\mu$-calculus indicates, bisimulation-invariant logics are sufficient for strings, for instance one might venture that PDL (propositional dynamic logic) would be enough.  
> **username_0**: @Sylvain Yep, it could be the case that two extensions coincide over strings but are not comparable over general structures. The reason I want to know about a minimal extension of **FO** is because I'm interested in the "gap" between FO and SO over different structures, make some kind of hierarchy. I don't have it clear myself, it is something I have to talk about with my future advisor if I ever start a PhD in TCS (possible question about career advice there as well).  

---

## 3 answers

### Answer by username_2 on 2012-01-28. Score: 12

FO(LFP) captures PTIME on ordered structures, and strings are ordered structures. So the languages definable by FO(LFP) include all regular languages and much much more.
<http://dx.doi.org/10.1016/S0019-9958(86)80029-8>

Ebbinghaus and Flum's textbook contains an exercise that asks to show FO(TC^1) (first-order logic extended with transitive closures of binary relations) is equivalent to MSO on strings. In the same exercise, $\{ a^n b^n \mid n \geq 1 \}$ is used as an example to show FO(TC^2) is more expressive than MSO on strings. All FO(TC) formulas are clearly equivalent to FO(LFP) formulas.

> **Comments:**
> **username_0**: Excellent. I don't know what you mean by TC^1 and TC^2, is that a typo? As far as I know, in the book you mention the notation used is FO(TC) for the extension of FO with *transitive closure* and FO(DTC) for the extension of FO with *deterministic transitive closure*, which is defined differently. I haven't found the exercise you mention, though. It remains to see whether there is an operator less expressive than TC that still allows to capture regular languages. I will update my question accordingly.  

---

### Answer by username_3 on 2012-04-11. Score: 10

This answer is a bit late, but it is known that one can obtain all and only the regular languages by adjoining a generalized group quantifier for each finite group (or equivalently for each finite simple group). Eg, see "Regular Languages Definable by Lindstrom Quantifiers" by Zoltan Esiky and Kim G. Larsen, at <http://www.brics.dk/RS/03/28/BRICS-RS-03-28.pdf>.

Moreover, this is optimal in the sense that a regular language will only be definable if the quantifiers for every group dividing its syntactic monoid are available.


---

### Answer by username_2 on 2012-01-31. Score: 7

It's Exercise 8.6.3 on page 221 of the second edition of Ebbinghaus and Flum's textbook, *Finite Model Theory*. The notation FO(TC$^r$) is explained there. FO(TC$^r$) can form the transitive closure of a $2r$-ary relation, regarded as a binary relation on $r$-tuples.

I found some more references you might be interested in.

FO(TC$^1$) is called FO(MTC) (first-order logic with monadic transitive closure) in [ten Cate and Segoufin's 2010 paper](http://dl.acm.org/citation.cfm?id=1706598). It proves, among other things, FO(MTC) is strictly less expressive than MSO on finite trees.

[Bargury and Makowsky's 1992 paper](http://www.springerlink.com/content/5l466173q574j788/) shows that *deterministic* monadic transitive closure—FO(DTC$^1$) in Ebbinghaus and Flum's notation—suffices to define regular string languages (see Theorem 5 in this paper).


---

