Question
Consider the set $V$ of all unordered 3-clauses $(l_1, l_2, l_3)$, where $l_i$ is a literal (i.e. a variable $x$ or its negation $\neg x$), and no clause contains two literals having the same variable. Clauses are given the usual interpretation from boolean satisfiability: $l_1 \lor l_2 \lor l_3$. Sets of clauses are interpreted as their conjunction.
Let $A$ a finite subset of $V$. Define $A^*$ as the set of all clauses that are not in $A$ and are tautologically implied by $A$.
Is there an $A$ such that
- for every proper subset $B \subset A$, we have $B^*=\varnothing$ and
- $|A^*|$ is other than $0$, $1$ or $\infty$
?
Examples
- $A = \{ (x_1,x_2,x_3) \}, A^* = \varnothing$
- $A = \{ (x_1,x_2,x_4), (x_3,\neg x_4,x_5), (x_1,x_2,\neg x_5) \}, A^* = \{ (x_1,x_2,x_3) \}$
- $A = \{ (x_1,x_2,x_3), (x_1,x_2,\neg x_3) \}, A^* = \{ (x_1, x_2, l) : l \text{ is any literal whose variable is not } x_1, x_2 \text{ or } x_3 \}$
Motivation
I was wondering about the nature of "difficult" tautologies in the context of proof theory and the structure of the progress an efficient proof system would need to follow. I found many examples of such $A$ such that $|A^*|=1$ with a computer program and it's straightforward to construct a trivial such set of arbitrary size. Any set of the form of the third example obviously implies infinitely many clauses and thus can't be further enlarged. But I wasn't able to find examples for other finite cardinalities.
P.S. I'm not a mathematician. I'm sorry if the question is not suitable or the answer is trivial. I did my best to find the answer for some time and on the internet.
