Let me start with Helly's theorem: Let $A_1$, $A_2$, …, $A_{n+2}$ be $n+2$ convex subsets of $\mathbb R^n$. If any $n+1$ of these subsets intersect (this means: have nonempty intersection), the so do all $n+2$.
This assertion is, logically speaking, a definite clause: All conditions are of the form "some subsets intersect", and so is the assertion. Generally, a definite clause about intersection of convex sets looks like this: Given some sets $S_1$, $S_2$, …, $S_k$ and $T$ and a family $\left(F_a\right)_{a\in S_1\cup S_2\cup …\cup S_k\cup T}$ of convex subsets of $\mathbb R^n$ indexed by the elements of $S_1\cup S_2\cup …\cup S_k\cup T$, we claim that if every $i\in\left\lbrace 1,2,…,k\right\rbrace$ satisfies $\bigcap\limits_{a\in S_i}F_a\neq\emptyset$, then $\bigcap\limits_{a\in T}F_a\neq\emptyset$.
Now it is an easy exercise to see that every tautological (= true for every choice of convex subsets) definite clause about intersection of convex sets is derivable using trivial properties of intersection (such as $A\cap A=A$, $A\cap B=B\cap A$ and $A\cap \left(B\cap C\right)=\left(A\cap B\right)\cap C$) and Helly's theorem only. (Note that we consider $n$ as given a priori and fixed during our proof, so we can't project on a subspace and use Helly for a smaller $n$, for example. We really only can manipulate intersections and use Helly for various intersection of convex subsets. I could write up what we can do as a natural deduction system, but it is pretty obvious.)
Now, what if we allow indefinite clauses? These are statements of the form: Given some sets $S_1$, $S_2$, …, $S_k$ and $T_1$, $T_2$, …, $T_l$ and a family $\left(F_a\right)_{a\in S_1\cup S_2\cup …\cup S_k\cup T_1\cup T_2\cup …\cup T_l}$ of convex subsets of $\mathbb R^n$ indexed by the elements of $S_1\cup S_2\cup …\cup S_k\cup T_1\cup T_2\cup …\cup T_l$, we claim that if every $i\in\left\lbrace 1,2,…,k\right\rbrace$ satisfies $\bigcap\limits_{a\in S_i}F_a\neq\emptyset$, then at least SOME $j\in\left\lbrace 1,2,…,l\right\rbrace$ satisfies $\bigcap\limits_{a\in T_j}F_a\neq\emptyset$.
What set of "axioms" (such as Helly's theorem) do we need in order to prove such indefinite clauses, if they are tautological? By "prove" I mean prove without using the convexity of the sets or that the sets are set at all (a pointfree approach, so to speak) – only using formal properties of $\cap$, logic (let's say constructive) and these axioms. Obviously Helly alone is not enough anymore; for example, for $n=1$ we have this here: If $A$, $B$, $C$, $D$ are four convex subsets of $\mathbb R^n$ such that $A\cap B$, $B\cap C$, $C\cap D$ and $D\cap A$ are nonempty, then at least one of the sets $A\cap C$ and $B\cap D$ are nonempty.
A connection to temporal logic is possible, but to be honest I have no idea about temporal logic; if somebody could point me to a reference that is of help here this might change…
Best Answer
This is an interesting question. (Even if there is no finite list of "axioms".)
For example the following is true: Suppose you have a (d+1)-dimensional polytope P. Associate a convex set in $R^d$ to every facet of P, and suppose that every non empty intersection among the facets implies a non empty intersection for the corresponding sets. Then there are some set of facets of the polytope with empty intersection so that the corresponding convex sets have non empty intersection. This is a large collection of statements of the kind you asked that already includes Helly's theorem.
Note that the nerve theorem gives you a lot of information on intersection patterns that cannot be realized. (Including the statement made above.)
A stronger statement for the case described above goes as follows: Suppose that 0 is in the interior of P. Then you can find two faces of F and G of P so that 0 is in their convex hull and the intersection of all sets corresponding to facets containing F and all sets corresponding to facets containing G is nonempty. This can be derived from the Borsuk-Ulam theorem.
Another well known result of the kind you ask about is the colorful Helly theorem (proved by Lovasz and a dual Caratheodory version was proved independently by Barany). It sais that if you have d+1 collections of convex sets in R^d, and if for every choice of one set from each collection there is a point common to all chosen sets then there is a collection all whose members have a point in common.
For n=1 there is a theorem by Lekkerkerker and Boland characterizing interval graphs. The characterization is based on two requirements: (1) there are no induced cycles of length >3. (This leaves us with chordal graphs.) (2) for every 3 vertices, one of the vertices is a neighbor of a vertex in every path between the other two. This gives an infinite set of "axioms" in the sense asked in the question. I suppose there is no finite list.
So overall there are many interesting theorems of the kind you described, and this is a rich area. But a complete description for dimension > 1 does not look realistic.
A more general question is to study the situation where you allow both operation: (1) taking the intersection (2) taking convex hull. This makes the problem even much more complicated and not much is known. An example of a recent result in this more general setting is the following theorem by Novick: Given 7.2k pairwise disjoint convex sets in the plane there is a set in the family that is disjoint to the convex hull of k other sets in the family.