Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:weak_monadic_logic_of_one_successor [2008/05/15 09:50] vkuncak |
sav08:weak_monadic_logic_of_one_successor [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 18: | Line 18: | ||
| Let $\mathbb{N} = \{0,1,2,\ldots\}$ denote non-negative integers. Let $D$ be the set of all //finite subsets// of $\mathbb{N}$. We consider the set of interpretations $(D,\alpha)$ where for each variable $v$ we have $\alpha(v) \in D$, where $\subseteq$ is the subset relation | Let $\mathbb{N} = \{0,1,2,\ldots\}$ denote non-negative integers. Let $D$ be the set of all //finite subsets// of $\mathbb{N}$. We consider the set of interpretations $(D,\alpha)$ where for each variable $v$ we have $\alpha(v) \in D$, where $\subseteq$ is the subset relation | ||
| - | \[ | + | \begin{equation*} |
| \alpha({\subseteq}) = \{ (S_1,S_2) \mid S_1 \subseteq S_2 \} | \alpha({\subseteq}) = \{ (S_1,S_2) \mid S_1 \subseteq S_2 \} | ||
| - | \] | + | \end{equation*} |
| and the relation $succ(v_1,v_2)$ is the successor relation on integers lifted to singleton sets: | and the relation $succ(v_1,v_2)$ is the successor relation on integers lifted to singleton sets: | ||
| - | \[ | + | \begin{equation*} |
| \alpha(succ) = \{ (\{k\},\{k+1\}) \mid k \in \mathbb{N} \} | \alpha(succ) = \{ (\{k\},\{k+1\}) \mid k \in \mathbb{N} \} | ||
| - | \] | + | \end{equation*} |
| The meaning of formulas is given by standard [[First-order logic semantics]]. | The meaning of formulas is given by standard [[First-order logic semantics]]. | ||
| Note in particular that quantification is restricted to finite sets (elements of $D$). | Note in particular that quantification is restricted to finite sets (elements of $D$). | ||
| + | |||
| + | |||
| ===== Expressive Power ===== | ===== Expressive Power ===== | ||
| Line 57: | Line 59: | ||
| **Using transitive closure and successors:** | **Using transitive closure and successors:** | ||
| - | * Constant zero: $(x=0) = One(x) \land \lnot (\exists y. One(y) \land s(y,x))$ | + | * Constant zero: $(x=0) = One(x) \land \lnot (\exists y. One(y) \land succ(y,x))$ |
| - | * Addition by constant: $(x = y + c) = (\exists y_1,\ldots,y_{c-1}. s(y,y_1) \land s(y_1,y_2) \land \ldots \land s(y_{c-1},x))$ | + | * Addition by constant: $(x = y + c) = (\exists y_1,\ldots,y_{c-1}. succ(y,y_1) \land succ(y_1,y_2) \land \ldots \land succ(y_{c-1},x))$ |
| - | * Ordering on positions in the string: $(u \leq v) = ((u,v) \in \{(x,y)|s(x,y))\}^*$ | + | * Ordering on positions in the string: $(u \leq v) = ((u,v) \in \{(x,y)|succ(x,y))\}^*$ |
| * Reachability in $k$-increments, that is, $\exists k \geq 0. y=x + c\cdot k$: $\mbox{Reach}_c(u,v) = ((u,v) \in \{(x,y)\mid y=x+c\}^*)$ | * Reachability in $k$-increments, that is, $\exists k \geq 0. y=x + c\cdot k$: $\mbox{Reach}_c(u,v) = ((u,v) \in \{(x,y)\mid y=x+c\}^*)$ | ||
| * Congruence modulo $c$: $(x \equiv y)(\mbox{mod}\ c) = \mbox{Reach}_c(x,y) \lor \mbox{Reach}_c(y,x)$ | * Congruence modulo $c$: $(x \equiv y)(\mbox{mod}\ c) = \mbox{Reach}_c(x,y) \lor \mbox{Reach}_c(y,x)$ | ||
| Line 71: | Line 73: | ||
| Then we can define addition $N(Z) = N(X) + N(Y)$ by saying that there exists a set of carry bits $C$ such that the rules for binary addition hold: | Then we can define addition $N(Z) = N(X) + N(Y)$ by saying that there exists a set of carry bits $C$ such that the rules for binary addition hold: | ||
| \begin{equation*} | \begin{equation*} | ||
| - | \exists C.\ 0 \notin i\ \land \forall i.\ | + | \exists C.\ 0 \notin C\ \land \forall i.\ |
| \big(\begin{array}[t]{rcl} | \big(\begin{array}[t]{rcl} | ||
| ((i \in Z) &\leftrightarrow& ((i \in X) \oplus (i \in Y) \oplus (i \in C))\ \land\\ | ((i \in Z) &\leftrightarrow& ((i \in X) \oplus (i \in Y) \oplus (i \in C))\ \land\\ | ||
| Line 90: | Line 92: | ||
| Relations on singleton sets: | Relations on singleton sets: | ||
| - | \[ | + | \begin{equation*} |
| r^s_F = \{(p,q) \mid F(\{p\},\{q\}) \} | r^s_F = \{(p,q) \mid F(\{p\},\{q\}) \} | ||
| - | \] | + | \end{equation*} |
| Relations on binary representations: | Relations on binary representations: | ||
| - | \[ | + | \begin{equation*} |
| r^b_F = \{(p,q) \mid F(N(p),N(q)) \} | r^b_F = \{(p,q) \mid F(N(p),N(q)) \} | ||
| - | \] | + | \end{equation*} |
| Addition is not definable as some $r^s_F$, but it is definable as $r^b_F$. | Addition is not definable as some $r^s_F$, but it is definable as $r^b_F$. | ||