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)?$$
> 
> 
> 



Ramsey type theorem
Yes, your conjecture is true.


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.


