Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
sav08:weak_monadic_logic_of_one_successor [2008/05/15 09:37] vkuncak |
sav08:weak_monadic_logic_of_one_successor [2008/05/15 09:38] vkuncak |
||
---|---|---|---|
Line 28: | Line 28: | ||
Note in particular that quantification is restricted to finite sets. | Note in particular that quantification is restricted to finite sets. | ||
+ | |||
===== What can we express in MSOL over strings ===== | ===== What can we express in MSOL over strings ===== | ||
Line 35: | Line 36: | ||
* Strict subset: $(S_1 \subset S_2) = (S_1 \subseteq S_2) \land \lnot (S_2 \subseteq S_1)$ | * Strict subset: $(S_1 \subset S_2) = (S_1 \subseteq S_2) \land \lnot (S_2 \subseteq S_1)$ | ||
* Set is empty: $(S=\emptyset) = \forall S_1. S \subseteq S_1$ | * Set is empty: $(S=\emptyset) = \forall S_1. S \subseteq S_1$ | ||
- | * Set is full: $(S=U) = \forall S_1. S_1 \subseteq S$ | ||
* Set $S$ is singleton (has exactly 1 element): $One(S) = (\lnot (S = \emptyset)) \land (\forall S_1. S_1 \subset S \rightarrow S_1=\emptyset)$ | * Set $S$ is singleton (has exactly 1 element): $One(S) = (\lnot (S = \emptyset)) \land (\forall S_1. S_1 \subset S \rightarrow S_1=\emptyset)$ | ||
* Set membership, treating elements as singletons: $(x \in S) = (x \subseteq S)$ | * Set membership, treating elements as singletons: $(x \in S) = (x \subseteq S)$ |