Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:weak_monadic_logic_of_one_successor [2008/05/15 10:02]
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$).
 +
  
  
Line 72: 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 91: 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$.
  
  
 
sav08/weak_monadic_logic_of_one_successor.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice