Clones of positive-arity Boolean operations

A clone contains the coordinate projections and is closed under superposition. Only positive arities participate; the set of nullary operations is explicitly empty. This convention permits empty relations and agrees with the unary constants in the Boolean CSP criterion.

The classification is [Che06], Theorem 5.1 (arXiv version 1, printed pp. 17–18): a Boolean clone consists of essentially unary operations or contains AND, OR, majority or minority. The arbitrary-arity proof in the shared classification is original: ternary partition minors detect a singleton coordinate, avoiding a minimum-essential-arity argument. There is no bound on operation arity. This is an algebraic classification, not a complexity dichotomy.

Main definitions

• Cslib.Logic.BooleanClone: positive-arity Boolean clones.
• Cslib.Logic.EssentiallyUnary: dependence on at most one coordinate.
• Cslib.Logic.PL.CSP.polymorphismClone: the clone of a fixed Boolean language.

Main results

• Cslib.Logic.BooleanClone.classification: the four-generator classification at all arities.
• Cslib.Logic.PL.CSP.projection_or_negation_of_not_hasSchaeferPolymorphism: the six-case corollary.
• Cslib.Logic.PL.CSP.isPolymorphism_selfDual_of_not_hasSchaeferPolymorphism: preservation of every self-dual relation in the negative six-case branch.

References

• H. Chen, A Rendezvous of Logic, Complexity, and Algebra, Theorem 5.1, arXiv version 1, printed pp. 17–18.

def Cslib.Logic.BooleanClone.ofRelations {Rel : Type u_1} (arity : Rel → ℕ) (R : (r : Rel) → Set (Fin (arity r) → Bool)) : BooleanClone

The common positive-arity polymorphisms of any fixed family of finite Boolean relations form a clone. No finiteness or nonemptiness of the family, or of its relations, is required.

def Cslib.Logic.PL.CSP.polymorphismClone {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) : BooleanClone

The positive-arity polymorphism clone of a fixed Boolean CSP language.

theorem Cslib.Logic.PL.CSP.mem_polymorphismClone_iff {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) {n : ℕ} (f : (Fin n → Bool) → Bool) : f ∈ (polymorphismClone arity sem).operations n ↔ 0 < n ∧ HasPolymorphism arity sem f

Membership includes the positive-arity convention explicitly.

theorem Cslib.Logic.PL.CSP.projection_or_negation_of_not_hasSchaeferPolymorphism {Rel : Type u_1} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : ¬HasSchaeferPolymorphism arity sem) {n : ℕ} (hn : 0 < n) {f : (Fin n → Bool) → Bool} (hf : HasPolymorphism arity sem f) : ∃ (i : Fin n), (f = fun (a : Fin n → Bool) => a i) ∨ f = fun (a : Fin n → Bool) => !a i

If all six Schaefer polymorphisms are absent, each positive-arity polymorphism is a coordinate projection or its Boolean negation. Constants here are unary, so empty relations are handled by precisely the shared Schaefer criterion.

theorem Cslib.Logic.PL.CSP.isPolymorphism_selfDual_of_not_hasSchaeferPolymorphism {Rel : Type u_1} {I : Type u_2} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (h : ¬HasSchaeferPolymorphism arity sem) {n : ℕ} (hn : 0 < n) {f : (Fin n → Bool) → Bool} (hf : HasPolymorphism arity sem f) (R : Set (I → Bool)) (hR : ∀ a ∈ R, (fun (i : I) => !a i) ∈ R) : IsPolymorphism f R

Every polymorphism of a language missing the six operations preserves every relation closed under simultaneous Boolean negation. This includes empty and nullary relations.