Weak Monadic Logic of One Successor
Closely related to “weak monadic second-order logic over strings” (there are some very minor differences).
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 relations of arity two or more, just over unary relations (sets)
- weak: the sets we quantify over are finite
- of one successor: the domain is an infinite chain, where each element has one successor (we only have successor and equality)
Syntax and Semantics
Let denote non-negative integers. Let be the set of all finite subsets of . We consider the set of interpretations where for each variable we have , where is the subset relation
and the relation is the successor relation on integers lifted to singleton sets:
The meaning of formulas is given by standard First-order logic semantics.
Note in particular that quantification is restricted to finite sets (elements of ).
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 singleton (has exactly 1 element):
- Set membership, treating elements as singletons:
- 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
Thus, we can express
in WS1S. (To express structures with multiple acyclic lists and 'null', we introduce the set 'Nulls' denoting natural numbers that are considered null.)
Using transitive closure and successors:
- Constant zero:
- Addition by constant:
- Ordering on positions in the string:
- Reachability in -increments, that is, :
- Congruence modulo :
Note that although we interpret elements as sets of integers, we cannot even talk about addition of two arbitrary integers , only addition with a constant. Also, although we can say we cannot say in how many steps we reach from . However, if we view sets of integers digits of a binary representation of another integer, then we can express much more. If is a finite set, let represent the number whose digits are , that is:
Then we can define addition by saying that there exists a set of carry bits such that the rules for binary addition hold:
This way we can represent entire Presburger arithmetic in MSOL over strings. Moreover, we have more expressive power because means that the one bits of are included in the bits of , that is, the bitwise or of and is equal to . In fact, if we add the relation of bit inclusion into Presburger arithmetic, we obtain precisely the expressive power of MSOL when sets are treated as binary representations of integers (Indeed, taking the minimal syntax of MSOL from the beginning, the bit inclusion gives us the subset, whereas the successor relation is expressible using .)
We can define relations on in two different ways.
Relations on singleton sets:
Relations on binary representations:
Addition is not definable as some , but it is definable as .