Logic and Proof MT24, Ordered divisible abelian groups
Flashcards
@State the family of axioms that make an abelian group “divisible”.
For each $n$, introduce the axiom $\forall x \exists y (ny = x)$ (where $nx$ here is a notational shortcut for $x + \cdots + x$, $n$ times).
Give an @example of a ordered divisible abelian group.
An ordered divisible abelian group is a structure satisfying the following axioms:
\[\begin{aligned}
F_1 &\quad \forall x \lnot (x < x) \\\\
F_2 &\quad \forall x \forall y \forall z (x < y \land y < z \to x < z) \\\\
F_3 &\quad \forall x \forall y (x < y \lor y < x \lor x = y) \\\\
F_4 &\quad \forall x \forall y (x + y = y + x) \\\\
F_5 &\quad \forall x \forall y \forall z ((x + y) + z = x + (y + z))) \\\\
F_6 &\quad \forall x \exists y (x + y = 0) \\\\
F_7 &\quad \forall x \forall y \forall z (x < y \to x + z < y + z) \\\\
F_8 &\quad \exists x \lnot (x = 0)\\\\
G_n &\quad \forall x \exists y (ny = x)
\end{aligned}\]
Axioms $F _ 1$ to $F _ 3$ correspond to the structure being totally ordered, $F _ 4$ to $F _ 6$ correspond to it being an Abelian group, $F _ 7$ implies addition is monotone, $F _ 8$ says that the group is non-trivial, and $G _ n$ says that the group is divisible.
Let $\pmb T _ \text{ODAG}$ be the theory corresponding to these axioms.
@Prove that $\pmb T _ {ODAG}$ has quantifier elimination.
It suffices to be able to eliminate the quantifier $\exists x$ in the case where $F$ is a conjunction of atomic formulas all of which mention $x$ (a justification is given at the end, here it’s possible to just consider conjunctions of atomic formulas rather than literals, since the negation of an atomic formula can be written as disjuncts of other atomic formulas).
Each atomic formula has the form $t _ 1 < t _ 2$ or $t _ 1 = t _ 2$ for terms $t _ 1$ and $t _ 2$ where at least one of $t _ 1$ or $t _ 2$ mentions $x$. We can simplify further to assume that there exists a positive integer $m$ such that each formula in $F$ has one of the following forms:
- $mx < t$
- $t < mx$
- $mx = t$
Suppose $F$ has the form
\[\bigwedge^{n_1}_{i=1} t_i < mx \land \bigwedge^{n_1}_{j=1} mx < s_j \land \bigwedge^{n_3}_{k=1} mx = u_k\]Then, by the divisibility axioms, $\exists x F \equiv \exists y G$ where
\[\bigwedge^{n_1}_{i=1} t_i < y \land \bigwedge^{n_1}_{j=1} y < s_j \land \bigwedge^{n_3}_{k=1} y = u_k\]If $n _ 3 > 0$, then $\exists y G \equiv G[u _ 1 / y]$. If $n _ 3 = 0$, then
\[\exists y G \equiv \bigwedge^{n_1}_{i=1} \bigwedge^{n_2}_{j = 1} t_i < s_j\]And so in all cases we have eliminated a quantifier as required.
Consider a formula $\exists x F$ where $F$ is quantifier free. We aim to construct a quantifier formula $G$ with the same free variables as $\exists x F$ such that for any structure $\mathcal A$ that satisfies all sentences in $\pmb T _ {UDLO}$ and any valuation $\pmb a$ in $\mathcal A$ of the free variables, we have $\mathcal A \models \exists x F(\pmb a)$ if and only if $\mathcal A \models G(\pmb a)$.
Firstly, convert $F$ into a logically equivalent formula in DNF. Furthermore, we can eliminate negative literals by replacing the sub-formula $\lnot (x _ i < x _ j)$ with $x _ i = x _ j \lor x _ j < x _ i$ and replacing $\lnot (x _ i = x _ j)$ with $x _ i < x _ j \lor x _ j < x _ i$.
So we may assume $F$ is in DNF and is negation-free. Then using the equivalence
\[\exists x (F_1 \lor F_2) \equiv \exists x F_1 \lor \exists x F_2\]it suffices to show how to eliminate the quantifier $\exists x$ in the case $F$ is a conjunction of atomic formulas. And using the equivalence $\exists x (F _ 1 \land F _ 2) \equiv \exists x F _ 1 \land F _ 2$ where $x$ is not free in $F _ 2$, so it suffices to be able to eliminate the quantifier $\exists x$ in the case where $F$ is a conjunction of atomic formulas all of which mention $x$.
Suppose:
- $A, C \in \mathbb Q^{m \times n}$
- $\pmb b, \pmb d \in \mathbb Q^n$
How could you go about answering the question of whether
\[\\{\pmb x \in \mathbb R^n : A\pmb x \le \pmb b} \stackrel?\subseteq \\{\pmb x \in \mathbb R^n : C\pmb x \le \pmb d\\}\]
and what is this process called?
You can translate this into a decision problem for the theory of ordered divisible abelian groups, which has quantifier elimination and is decidable.
In this context, quantifier elimination is called Fourier-Motzkin elimination.