# MSOL over Strings

## Syntax and Semantics of Weak Monadic Second-Order Logic over Strings

Explanation of the name:

• second-order logic: we can quantify not only over elements but also over sets and relations
• monadic: we cannot quantify over any relations, just unary relations, that is, sets
• over strings: the domain of interpretation are not general graphs, but only strings, so the only built-in relation is a relation that gives us the next position in a string
• weak: we consider only finite strings

Alternative name is “monadic second-order logic of one successor”.

Minimalistic syntax for monadic second-order logic is:

As the domain of interpretation we take the set of natural numbers . We interpret variables as finite subsets of this set, and as the subset relation. The relation is the successor relation on integers lifted to singleton sets.

More precisely, if then we have the following semantics:

## What can we express in MSOL over strings

Set operations. The ideas is that quantification over sets with gives us the full Boolean algebra of sets.

• Two sets are equal:
• Strict subset:
• Set is empty:
• Set is full:
• Set is singleton (has exactly 1 element):
• Set membership, treating elements as singletons:
• Intersection:
• Union:
• Set difference:

(or just use element-wise definitions with singletons)

• If is a fixed constant, properties , ,

Transitive closure of a relation. If is a formula on singletons, we define reflexive transitive closure as follows. Define shorthand

Then is defined by

Using transitive closure and successors:

• Constant zero: