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)$ | ||