# Proof that the theory of rationals is convex

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)

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.