On the size of irredundant propagation complete CNF formulas

We investigate propagation complete (PC) CNF formulas for a symmetric definite Horn function of $n$ variables and demonstrate that the minimum size of these formulas is closely related to specific covering numbers, namely, to the smallest number of $k$-subsets of an $n$-set covering all $(k-1)$-subsets for a suitable $k$. As a consequence, we demonstrate an irredundant PC formula whose size is larger than the size of a smallest PC formula for the same function by a factor $\Omega(n/\ln n)$. This complements a known polynomial upper bound on this factor.