# Ramsey type theorem

Let $\mathcal{P}(\{0,\dotsc,7\})$ denote the power set of $\{0,\dotsc,7\}$.

Is the following true?

For any function $f: \mathcal{P}(\{0,\dotsc,7\})\rightarrow\{0,1\}$ there exists $0\leq k\leq 3$ and three mutually disjoint sets $A,B,C\subseteq \{0,\dotsc,7\}$ such that $\min A = 2k, \min B = 2k+1,$ and $$f(C) = f(A\cup C) = f(B\cup C) = f(A\cup B\cup C)?$$

• It's revised now. – Jiayi Liu Feb 18 '18 at 8:41
• In my opinion one should give the OP the benefit of the doubt that this is a question that they need to know in their mathematical research. It is a sensible question, which can come up in research. It could be equivalently rephrased more catchily as 'Is it true that for every hypergraph $\mathcal{H}$ on the finite ordinal $8$, there exist three disjoint subsets $A$, $B$, $C$ of $8$ such that (0) the sets $C$, $A\cup C$, $B\cup C$, $A\cup B\cup C$ either all are in $\mathcal{H}$ or all are out, and (2) the minimum element of $B$ is one larger than the minimum of $A$, and is at most $7$.' – Peter Heinig Feb 18 '18 at 10:58
• If you negate this question to place it in the existential form 'does there exist $f$ such that for all $A, B, C$ satisfying these properties, at least one of $\{f(C), f(A \cup C), f(B \cup C), f(A \cup B \cup C) \}$ is true and at least one is false?', then it can be written as a conjunction of many 4-variable clauses over $2^8$ variables (the function values). This could be given to a SAT solver and (I suspect) solved almost instantaneously. – Adam P. Goucher Feb 18 '18 at 22:51
• I wasn't seeking for an algorithm to determine answers for such kind of problems. I only wonder this particular problem. – Jiayi Liu Feb 19 '18 at 7:21
• Maybe worth noting, just to motivate the question, that we cannot take the parity of the minimum element, since that can be the same for all four sets, and we cannot take the parity of the size of the set, since $A$ and $B$ can both have even size. They can also have the same size mod 3 or 4. So a lot of the usual methods for finding counterexamples to Ramsey questions don't work here. – gowers Feb 19 '18 at 15:44

Suppose otherwise. Then there exists a counterexample $f : \mathcal{P}(8) \rightarrow \{0, 1\}$. For each set $X \in \mathcal{P}(8)$, let the proposition $P_X$ denote $f(X) = 1$.

There are $5440$ different choices of the tuple $(A, B, C) \in \mathcal{P}(8)^3$ satisfying your constraints. For each such tuple, we obtain two clauses which must be true of the counterexample $f$:

$$(\neg P_C \lor \neg P_{A \cup C} \lor \neg P_{B \cup C} \lor \neg P_{A \cup B \cup C})$$

$$(P_C \lor P_{A \cup C} \lor P_{B \cup C} \lor P_{A \cup B \cup C})$$

This gives a succinct list of $10880$ clauses which must be true of the $256$ primitive propositions $\{ P_X : X \in \mathcal{P}(8) \}$.

Inputting this list of clauses into the SAT solver Glucose gives the response 'UNSAT' (meaning 'unsatisfiable'), so no such counterexample exists. It also exports a verifiable certificate of unsatisfiability which can be checked in polynomial time.

The proof is somewhat unilluminating, because it doesn't give any indication as to why your conjecture is true, just that it is.

• Since Glucose measures the "quality" of learned clauses as it runs, it is perhaps possible that some of these might be useful steps in a "human" proof. – François G. Dorais Feb 19 '18 at 20:56
• The certificate is only 1489 lines long, and presumably could be optimised by symmetry considerations, so that's conceivable. But I imagine that, even after simplifying the proof, we would still be left with an inelegant case-bash. – Adam P. Goucher Feb 19 '18 at 21:02