Majority preservation and 2CNF definability

A Boolean relation on finitely many coordinates is preserved by majority exactly when it is definable by a CNF formula with clauses of width at most two. This is the bijunctive branch of the Boolean preservation classification, [Bod26], Lemma 6.32 (September 14, 2026 version, Section 6.6, p. 76). Finite coordinate types replace the source's numbered variables; empty relations and nullary relations are included explicitly. The finite-projection proof here is original, rather than the source's proof through reduced CNF. This is not Schaefer's complexity dichotomy; [Che06], Section 4, treats the corresponding tractability results.

Relations are Set (V → Bool), and defining formulas use precisely the existing CNF V semantics, with no auxiliary variables. Empty relations and empty coordinate types are allowed; an empty clause defines falsity, and the empty CNF defines truth. No complexity certificate for constructing the defining CNF is claimed.

Main results

• Cslib.Logic.PL.isPolymorphism_majority_iff: majority preservation expressed using the existing coordinatewise median.
• Cslib.Logic.PL.mem_of_pairwise_of_majority: a nonempty majority-closed finite relation is determined by its projections onto at most two coordinates.
• Cslib.Logic.PL.isPolymorphism_majority_iff_exists_twoCNF: the characterization.

theorem Cslib.Logic.PL.isPolymorphism_majority_iff {V : Type u_1} (R : Set (V → Bool)) : IsPolymorphism (majority 3) R ↔ ∀ x ∈ R, ∀ y ∈ R, ∀ z ∈ R, BitString.median x y z ∈ R

Majority preservation can equivalently be expressed by closure under coordinatewise median.

theorem Cslib.Logic.PL.mem_of_pairwise_of_majority {V : Type u_1} [Finite V] {R : Set (V → Bool)} (hR : IsPolymorphism (majority 3) R) (hne : R.Nonempty) (a : V → Bool) (hp : ∀ (i j : V), ∃ b ∈ R, b i = a i ∧ b j = a j) : a ∈ R

A nonempty majority-closed relation on finitely many coordinates contains a tuple whenever each of its pairs of coordinates extends to a tuple in the relation. Pairing a coordinate with itself includes singleton projections; nonemptiness handles the empty coordinate type.

theorem Cslib.Logic.PL.Clause.eval_median_of_length_le_two {V : Type u_1} {c : Clause V} (hc : List.length c ≤ 2) {x y z : V → Bool} (hx : eval x c = true) (hy : eval y c = true) (hz : eval z c = true) : eval (BitString.median x y z) c = true

A clause of width at most two is preserved by coordinatewise majority, including arbitrary literal signs, repeated variables, the empty clause and unit clauses.

theorem Cslib.Logic.PL.CNF.isPolymorphism_majority {V : Type u_1} {φ : CNF V} (hφ : ∀ c ∈ φ, List.length c ≤ 2) : IsPolymorphism (majority 3) {a : V → Bool | eval a φ = true}

Models of a width-two CNF form a majority-preserved relation.

theorem Cslib.Logic.PL.exists_separating_clause_of_majority {V : Type u_1} [Finite V] {R : Set (V → Bool)} (hR : IsPolymorphism (majority 3) R) {a : V → Bool} (ha : a ∉ R) : ∃ (c : Clause V), List.length c ≤ 2 ∧ (∀ b ∈ R, Clause.eval b c = true) ∧ Clause.eval a c = false

A tuple outside a majority-closed finite Boolean relation is separated from every tuple in the relation by a clause with at most two literals.

theorem Cslib.Logic.PL.isPolymorphism_majority_iff_exists_twoCNF {V : Type u_1} [Finite V] (R : Set (V → Bool)) : IsPolymorphism (majority 3) R ↔ ∃ (φ : CNF V), (∀ c ∈ φ, List.length c ≤ 2) ∧ ∀ (a : V → Bool), a ∈ R ↔ CNF.eval a φ = true

Majority preservation iff 2CNF definability. Relations on finitely many Boolean coordinates, including empty and nullary relations, are majority-preserved exactly when they are the models of a CNF with clauses of width at most two, without auxiliary variables.