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)