# Notes - Logic and Proof MT24, Presburger arithmetic

> Source: https://ollybritton.com/notes/uni/part-b/mt24/logic-and-proof/notes/presburger-arithmetic/ · Updated: 2025-06-11 · Tags: uni, notes

- [Course - Logic and Proof MT24](https://ollybritton.com/notes/uni/part-b/mt24/logic-and-proof/)
	- [Notes - Logic and Proof MT24, Decidable theories](https://ollybritton.com/notes/uni/part-b/mt24/logic-and-proof/notes/decidable-theories/)
	- [Notes - Logic and Proof MT24, Regular languages](https://ollybritton.com/notes/uni/part-b/mt24/logic-and-proof/notes/regular-languages/)
	- See also:
	- [Notes - Models of Computation MT23, DFAs](https://ollybritton.com/notes/uni/part-a/mt23/models-of-computation/notes/dfas/)
	- ["Presburger Arithmetic"](https://en.wikipedia.org/wiki/Presburger_arithmetic) on Wikipedia
	- ["Quantifier elimination"](https://jdh.hamkins.org/quantifer-elimination/) by Joel David Hamkins

### Flashcards
#### Presburger arithmetic
@Define Presburger arithmetic.::

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

@State a decidability result about Presburger arithmetic.::

$$
\mathrm{Th}(\mathbb N, 0, 1, +, <)
$$
is decidable.

@Prove that Presburger arithmetic is decidable (∆presburger-decidable).::

It suffices to show that $\mathrm{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) \land 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)) \land F')$ where $F'$ has all occurrences of $0$ substituted by $z$ (i.e. zero is the unique additive identity).

To show $\mathrm{Th}(\mathbb N, 0, 1, +, <)$ is decidable, given an arbitrary formula $F$ for which we wish to determine $F \stackrel?\in \mathrm{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$:

![Screenshot 2024-10-31 at 20.43.01.png](https://ollybritton.com/assets/attachments/img/Screenshot 2024-10-31 at 20.43.01.png)

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:

![Screenshot 2024-10-31 at 20.43.48.png](https://ollybritton.com/assets/attachments/img/Screenshot 2024-10-31 at 20.43.48.png)

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} \cdots 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 the alphabet $\Sigma _ 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$.

Describe a DFA $A^=$ over the alphabet
$$
\Sigma _ 2 = \left\lbrace
\begin{bmatrix}
0 \\ 0
\end{bmatrix},
\dots,
\begin{bmatrix}
1 \\ 1
\end{bmatrix}
\right\rbrace
$$
such that $A^=$ accepts the subset of $\Sigma^\ast _ 2$ such that $x _ 1 = x _ 2$ where the value of $x _ i$ corresponds to the $i$th row of the vector in little endian.::

![Screenshot 2024-10-31 at 20.43.01.png](https://ollybritton.com/assets/attachments/img/Screenshot 2024-10-31 at 20.43.01.png)

Describe a DFA $A^+$ over the alphabet
$$
\Sigma _ 3 = \left\lbrace
\begin{bmatrix}
0 \\ 0 \\ 0
\end{bmatrix},
\dots,
\begin{bmatrix}
1 \\ 1 \\ 1 
\end{bmatrix}
\right\rbrace
$$
such that $A^+$ accepts the subset of $\Sigma^\ast _ 3$ such that $x _ 1 + x _ 2 = x _ 3$ where the value of $x _ i$ corresponds to the $i$th row of the vector in little endian.::

![Screenshot 2024-10-31 at 20.43.48.png](https://ollybritton.com/assets/attachments/img/Screenshot 2024-10-31 at 20.43.48.png)

#### Dyadic rationals with an averaging operation
Suppose:

- $\mathcal D = (D, \oplus, <)$
- $D = \lbrace m / 2^n \mid m, n \in \mathbb N, 0 \le m < 2^n \rbrace$ is the set of dyadic rationals
- $a \oplus b = (a + b) /2$

@Prove that $\mathrm{Th}(\mathcal D)$ is decidable.::

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

- Construct an 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$:

![Screenshot 2025-05-27 at 19.13.58.png](https://ollybritton.com/assets/attachments/img/Screenshot 2025-05-27 at 19.13.58.png)

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

![Screenshot 2025-05-27 at 19.13.46.png](https://ollybritton.com/assets/attachments/img/Screenshot 2025-05-27 at 19.13.46.png)

(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 \oplus 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} \cdots 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 the alphabet $\Sigma _ 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~

---
Olly Britton — https://ollybritton.com. Machine-readable index: https://ollybritton.com/llms.txt