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...

anycorrect Horn clouses of your type about at most $m-1$ sets each? I mean, neither of them will allow you to draw any non-trivial conclusion here. $\endgroup$ – fedja Jan 7 '11 at 6:32