<p>The key idea here is that for any conjunction of equations $F\equiv u_1=v_1\wedge\ldots\wedge u_k=v_k$, the set $S_F$ is convex in the geometric sense, i.e. for any two points $p,q\in S_F$, all points between $p$ and $q$ are also in $S_F$.</p>

<p>Now suppose that $F\Rightarrow G$, where $G$ is a disjunction of equations $x_1=y_1\vee\ldots\vee x_n=y_n$ (note that the variables $u_i,v_i,x_i,y_i$ are not assumed to be pairwise distinct). Without loss of generality, we may assume that $G$ is minimal in the sense that for each $i$, there is a point $p_i$ in $S_F$ which satisfies $x_i=y_i$, but not $x_j=y_j$ for any $j\neq i$. Any equation for which this is not the case can simply be removed from $G$ to obtain a smaller disjunction $G'$ which still satisfies $F\Rightarrow G'$. We will show that for such a minimal $G$, $n\le 1$. </p>

<p>Suppose not, i.e. $n&gt;1$. Then the line segment $l$ between (say) $p_1$ and $p_2$ is contained in $S_F$ due to (geometric) convexity. Since $p_1$ and $p_2$ cannot be the same due to their definition, $l$ has infinitely many points. Therefore there must be some $i$ such that $l\cap S_{x_i=y_i}$ has infinitely many points, and so $l\subseteq S_{x_i=y_i}$; in particular, $p_1\in S_{x_i=y_i}$, implying $i=1$, and $p_2\in S_{x_i=y_i}$, implying $i=2$ for a contradiction.</p>

CC BY-SA 3.0
2016-08-08T13:57:44.160Z
2016-08-08T14:06:39.807Z
2016-08-08T14:06:39.807Z
Klaus Draeger
<p>In Example 10.12 of the book The calculus of computation by Bradley and Manna, it is said</p>
<blockquote>
<p>The theory of rationals is convex, as it is convex in a geometric sense.</p>
</blockquote>
<p>How does the geometric sense of convex relate to theories being convex?</p>
<p>It further gives a proof by contradiction but I am unclear on what the assumptions are, what is being contradicted and how.</p>
<blockquote>
<p>The theory of rationals TQ is convex, as it is convex in a geometric sense ... Each equality u<sub>i</sub> = v<sub>i</sub> of the disjunction G of is geometrically convex, but G itself is not. Consider, for example, H : x=y ∨ x=z. Let S<sub>H</sub> be the set of points satisfying H. The point (x,y,z) = (0,0,1) is included in S<sub>H</sub> , as is the point (1,0,1). However, the average of the two points, (12, 0,1) (choosing λ = 1/2), is not in S<sub>H</sub>. Indeed, choose any two points (u, u,v1) and (w,v2,w) from S<sub>x=y</sub> and S<sub>x=z</sub>, respectively, such that neither is in their intersection S<sub>x=y=z</sub> (i.e., v1= u and v2= w). Then for any λ ∈ (0,1), the point</p>
<p>(λu +(1−λ)w, λu+(1−λ)v2, λv1 +(1−λ)w)</p>
<p>is neither in Sx=y nor in Sx=z. Suppose, then, that F ⇒ G : ni=1 ui = vi, but for no i ∈ {1,...,n} does F ⇒ui=vi. Then it must be the case that there are two points s1 and s2 of SF in separate subsets Sui=vi, Suj=vj, i= j, of SG. By the argument above, the points on the line segment between s1 and s2 are not in SG and thus not in SF. Then F is not geometrically convex, a contradiction. Thus, TQ is convex.</p>
</blockquote>
<p>UPDATE:</p>
<p>Context from the same book:</p>
<blockquote>
<p>If a conjunctive formula in a convex theory implies a disjunction of equalities between variables, then it actually implies a single equality. Formally, consider a quantifier-free conjunctive Σ-formula F and a disjunction n</p>
<p>G: conjunction_over_i_to_n ( ui = vi ),</p>
<p>for variables ui and vi.</p>
<p>Theory T is convex if for every such F and G, if n</p>
<p>F ⇒ disjunction_over_i_to_n (ui = vi)</p>
<p>then,</p>
<p>F ⇒ ui=vi for some i∈{1,...,n} .</p>
<p>If F implies G, then F actually implies one of the disjuncts of G.</p>
</blockquote>
<p>Cross-posted from SO: <a href="https://stackoverflow.com/q/38814285/1494559">https://stackoverflow.com/q/38814285/1494559</a> (as it lies in the intersection of the fields)</p>

<sat><decidability><program-verification><model-theory><modal-logic>
Proof that the theory of rationals is convex
np20
# Proof that the theory of rationals is convex

(Asked by: username_0 on 2016-08-08)

In Example 10.12 of the book The calculus of computation by Bradley and Manna, it is said

> The theory of rationals is convex, as it is convex in a geometric sense.

How does the geometric sense of convex relate to theories being convex?

It further gives a proof by contradiction but I am unclear on what the assumptions are, what is being contradicted and how.

> The theory of rationals TQ is convex, as it is convex in a geometric sense ... Each equality ui = vi of the disjunction G of is geometrically convex, but G itself is not. Consider, for example, H : x=y ∨ x=z. Let SH be the set of points satisfying H. The point (x,y,z) = (0,0,1) is included in SH , as is the point (1,0,1). However, the average of the two points, (12, 0,1) (choosing λ = 1/2), is not in SH. Indeed, choose any two points (u, u,v1) and (w,v2,w) from Sx=y and Sx=z, respectively, such that neither is in their intersection Sx=y=z (i.e., v1= u and v2= w). Then for any λ ∈ (0,1), the point
>
> (λu +(1−λ)w, λu+(1−λ)v2, λv1 +(1−λ)w)
>
> is neither in Sx=y nor in Sx=z. Suppose, then, that F ⇒ G : ni=1 ui = vi, but for no i ∈ {1,...,n} does F ⇒ui=vi. Then it must be the case that there are two points s1 and s2 of SF in separate subsets Sui=vi, Suj=vj, i= j, of SG. By the argument above, the points on the line segment between s1 and s2 are not in SG and thus not in SF. Then F is not geometrically convex, a contradiction. Thus, TQ is convex.

UPDATE:

Context from the same book:

> If a conjunctive formula in a convex theory implies a disjunction of equalities between variables, then it actually implies a single equality. Formally, consider a quantifier-free conjunctive Σ-formula F and a disjunction n
>
> G: conjunction\_over\_i\_to\_n ( ui = vi ),
>
> for variables ui and vi.
>
> Theory T is convex if for every such F and G, if n
>
> F ⇒ disjunction\_over\_i\_to\_n (ui = vi)
>
> then,
>
> F ⇒ ui=vi for some i∈{1,...,n} .
>
> If F implies G, then F actually implies one of the disjuncts of G.

Cross-posted from SO: <https://stackoverflow.com/q/38814285/1494559> (as it lies in the intersection of the fields)

**Tags:** sat, decidability, program-verification, model-theory, modal-logic

---

## 1 answers

### Answer by username_1 on 2016-08-08. Score: 4 | Accepted answer

The key idea here is that for any conjunction of equations $F\equiv u\_1=v\_1\wedge\ldots\wedge u\_k=v\_k$, the set $S\_F$ is convex in the geometric sense, i.e. for any two points $p,q\in S\_F$, all points between $p$ and $q$ are also in $S\_F$.

Now suppose that $F\Rightarrow G$, where $G$ is a disjunction of equations $x\_1=y\_1\vee\ldots\vee x\_n=y\_n$ (note that the variables $u\_i,v\_i,x\_i,y\_i$ are not assumed to be pairwise distinct). Without loss of generality, we may assume that $G$ is minimal in the sense that for each $i$, there is a point $p\_i$ in $S\_F$ which satisfies $x\_i=y\_i$, but not $x\_j=y\_j$ for any $j\neq i$. Any equation for which this is not the case can simply be removed from $G$ to obtain a smaller disjunction $G'$ which still satisfies $F\Rightarrow G'$. We will show that for such a minimal $G$, $n\le 1$.

Suppose not, i.e. $n>1$. Then the line segment $l$ between (say) $p\_1$ and $p\_2$ is contained in $S\_F$ due to (geometric) convexity. Since $p\_1$ and $p\_2$ cannot be the same due to their definition, $l$ has infinitely many points. Therefore there must be some $i$ such that $l\cap S\_{x\_i=y\_i}$ has infinitely many points, and so $l\subseteq S\_{x\_i=y\_i}$; in particular, $p\_1\in S\_{x\_i=y\_i}$, implying $i=1$, and $p\_2\in S\_{x\_i=y\_i}$, implying $i=2$ for a contradiction.


---

