Logic and Proof MT24, Presburger arithmetic

The theory of the structure $(\mathbb N, 0, 1, +, <)$ under the intended interpretation.

\[\text{Th}(\mathbb N, 0, 1, +, <)\]

is decidable.

It suffices to show that $\text{Th}(\mathbb N, +)$ is decidable, since any formula over $(\mathbb N, 0, 1, +, <)$ can be rewritten as a formula using $+$ and $=$ that defines the same property on $\mathbb N$:

• $x < y$ may be written as $\exists z (x + z + 1 = y)$.
• Occurrences of $1$ in a formula may be replaced by introducing an existential quantifier $\exists w ( w \ne 0 \land (\forall x \forall y (x \ne w \land y \ne w) \to w \ne x + y) \to F’)$ where $F’$ has all occurrences of $1$ substituted by $w$ (i.e. $1$ is the unique element which is not zero and is not the sum of two elements distinct from itself).
• Occurrences of $0$ in a formula $F$ may be replaced by introducing an existential quantifier $\exists z ((\forall x (x + z) = x) \to F’)$ where $F’$ has all occurrences of $0$ substituted by $z$ (i.e. zero is the unique additive identity).

To show $\text{Th}(\mathbb N, 0, 1, +, <)$ is decidable, given an arbitrary formula $F$ for which we wish to determine $F \stackrel?\in \text{Th}(\mathbb N, 0, 1, +, <)$, we do the following:

• Convert it into an equivalent formula $F’$ over the weaker signature $(\mathbb N, +)$
• Construct a DFA $A$ such that $F’$ is satisfiable iff $A$ has a nonempty language
• Output whether $A$ has nonempty language

---

Case $F$ is quantifier free:

Consider a quantifier-free formula $F$ over variables $x _ 1, \ldots, x _ n$ and consider the corresponding alphabet

\[\Sigma _ n = \left\lbrace \begin{bmatrix} 0 \\\\ 0 \\\\ \vdots \\\\ 0 \end{bmatrix}, \dots, \begin{bmatrix} 1 \\\\ 1 \\\\ \vdots \\\\ 1 \end{bmatrix} \right\rbrace\]

which represents a valuation of these variables using little endian, where the value of $x _ i$ corresponds to the $i$-th row of the vector.

Define $A _ =$ as the following DFA, which accepts the subset of $\Sigma _ 2^\ast$ where the elements satisfy $x _ 1 = x _ 2$:

Define $A _ +$ as the following DFA, which accepts the subset of $\Sigma _ 3^\ast$ where the elements satisfy $x _ 1 + x _ 2 = x _ 3$ by:

We now define $A _ F$ by induction on the structure of $F$. Define

\[\pi _ {i _ 1, \ldots, i _ k} : \begin{bmatrix} x _ 1 \\\\ x _ 2 \\\\ \vdots \\\\ x _ n \end{bmatrix} \mapsto \begin{bmatrix} x _ {i _ 1} \\\\ \vdots \\\\ x _ {i _ k} \end{bmatrix}\]

• Base case: $x _ i = x _ j$, take $A _ F$ to be the DFA for the language defined by $\pi _ {i, j}^{-1}(L(A _ =))$, which is valid as regular languages are closed under inverse homomorphisms.
• Base case: $x _ i + x _ j = x _ k$, take $A _ F$ to be the DFA for the language defined by $\pi _ {i,j,k}^{-1}(L(A _ +))$.
• Case: $F = F _ 1 \wedge F _ 2$. Take $A _ F$ to be an automaton whose language is $L(A _ {F _ 1}) \cap L(A _ {F _ 2})$.
• Case: $F = \lnot G$. Take $A _ F$ to be an automaton whose language is $\Sigma^\ast _ n \setminus L(A _ G)$.

This covers all quantifier-free formulas.

---

$F$ contains quantifiers:

Now consider a sentence

\[F = Q _ 1 x _ 1 \cdots Q _ n x _ n F^\ast\]

in prenex form. For $k = 0, \ldots, n$ we write $F _ k := Q _ {k+1} x _ {k+1} Q _ n x _ n F^\ast$.

We aim to define a corresponding automaton $A _ k$ over alphabet $\Sigma _ k$ such that $A _ k$ accepts the set of values of variables $x _ 1, \ldots, x _ k$ that satisfy $F _ k$.

An invariant is that $A _ k$ has non-empty language iff formula $F _ k$ is satisfiable.

As $F^\ast$ is quantifier free, we can take $A _ n$ to be $A _ F$.

Now consider $F _ {k-1} = \exists x _ k F _ k$. By induction, $A _ k$ is an automaton on an alphabet $A _ k$ corresponding to $F _ k$. Define $A _ {k-1}$ to be an automaton whose language is $\pi(L(A _ k))$ where $\pi : \Sigma _ k \to \Sigma _ {k-1}$ is the map that projects out the $k$-th coordinate of each tuple in $\Sigma _ k$.

Handle the universal quantifier $\forall x _ k$ by treating it as shorthand for $\lnot \exists x _ k \lnot$.

We end up with an automaton $A _ 0$ for the sentence $F _ 0$ over the alphabet $\Sigma _ 0$. This automaton has non-empty language iff $(\mathbb N, +, 0, 1)$ satisfies $F _ 0$.

To show $\text{Th}(\mathcal D)$ is decidable, given an arbitrary formula $F$ for which we wish to determine $F \stackrel?\in \text{Th}(\mathcal D)$, we do the following:

• Construct a NFA $A$ such that $F$ is satisfiable iff $A$ has a nonempty language
• Output whether $A$ has nonempty language

---

Case $F$ is quantifier free:

Consider a quantifier-free formula $F$ over variables $x _ 1, \ldots, x _ n$ and consider the corresponding alphabet

\[\Sigma _ n = \left\lbrace \begin{bmatrix} 0 \\\\ 0 \\\\ \vdots \\\\ 0 \end{bmatrix}, \dots, \begin{bmatrix} 1 \\\\ 1 \\\\ \vdots \\\\ 1 \end{bmatrix} \right\rbrace\]

which represents a valuation of these variables using little endian, where the value of $x _ i$ corresponds to the $i$-th row of the vector.

Define $A _ <$ as the following NFA, which accepts the subset of $\Sigma^\ast _ 2$ where the elements satisfy $x _ 1 < x _ 2$:

Define $A _ \oplus$ as the following NFA, which accepts the subset of $\Sigma^\ast _ 3$ where the elements satisfy $x _ 1 \oplus x _ 2 = x _ 3$ by

(the intuition here is that $q _ 1$ represents no carries, $q _ 2$ represents a carry of $1$, and $q _ 3$ represents a carry of $-1$).

• Base case: $x _ i < x _ j$, take $A _ F$ to be the NFA for the language defined by $\pi^{-1} _ {i, j}(L(A _ <))$.
• Base case: $x _ i + x _ j = x _ k$, take $A _ F$ to be the NFA for the language defined by $\pi _ {i, j, k}^{-1}(L(A _ \oplus))$.
• Case: $F = F _ 1 \land F _ 2$, take $A _ F$ to be the automaton whose language is $L(A _ {F _ 1}) \cap L(A(F _ 2))$.
• Case: $F = \lnot G$, take $A _ F$ to be an automaton whose language is $\Sigma^\ast _ n \setminus L(A _ G)$.

---

$F$ contains quantifiers:

Now consider a sentence

\[F = Q _ 1 x _ 1 \cdots Q _ n x _ n F^\ast\]

in prenex form. For $k = 0, \ldots, n$ we write $F _ k := Q _ {k+1} x _ {k+1} Q _ n x _ n F^\ast$.

We aim to define a corresponding automaton $A _ k$ over alphabet $\Sigma _ k$ such that $A _ k$ accepts the set of values of variables $x _ 1, \ldots, x _ k$ that satisfy $F _ k$.

An invariant is that $A _ k$ has non-empty language iff formula $F _ k$ is satisfiable.

As $F^\ast$ is quantifier free, we can take $A _ n$ to be $A _ F$.

Now consider $F _ {k-1} = \exists x _ k F _ k$. By induction, $A _ k$ is an automaton on an alphabet $A _ k$ corresponding to $F _ k$. Define $A _ {k-1}$ to be an automaton whose language is $\pi(L(A _ k))$ where $\pi : \Sigma _ k \to \Sigma _ {k-1}$ is the map that projects out the $k$-th coordinate of each tuple in $\Sigma _ k$.

Handle the universal quantifier $\forall x _ k$ by treating it as shorthand for $\lnot \exists x _ k \lnot$.

We end up with an automaton $A _ 0$ for the sentence $F _ 0$ over the alphabet $\Sigma _ 0$. This automaton has non-empty language iff $\mathcal D = (D, <, \oplus)$ satisfies $F _ 0$.

@sheets~