The four-generator Boolean clone classification

Every positive-arity Boolean clone consists of essentially unary operations or contains AND, OR, majority or minority: [Che06], Theorem 5.1, arXiv v1, printed pp. 17–18. The arbitrary-arity proof is original: ternary partition minors detect a singleton coordinate. This shared algebraic theorem supports both Schaefer's dichotomy and Post's criterion.

Main definitions

• Cslib.Logic.EssentiallyUnary: dependence on at most one coordinate.

Main results

• Cslib.Logic.BooleanClone.classification: the four-generator classification at all arities.
• Cslib.Logic.BooleanClone.exists_projection_of_ternaryMinors: ternary minors detect projections.

References

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

def Cslib.Logic.EssentiallyUnary {n : ℕ} (f : (Fin n → Bool) → Bool) : Prop

An operation depends on at most one coordinate, including constant operations. Positive arity is essential: the witnessing coordinate cannot exist at arity zero.

theorem Cslib.Logic.EssentiallyUnary.exists_projection {n : ℕ} {f : (Fin n → Bool) → Bool} (hf : EssentiallyUnary f) (hid : ∀ (b : Bool), (f fun (x : Fin n) => b) = b) : ∃ (i : Fin n), ∀ (a : Fin n → Bool), f a = a i

For an idempotent operation, essential unarity means being a projection.

theorem Cslib.Logic.BooleanClone.binary_essentiallyUnary (C : BooleanClone) (hand : andOp ∉ C.operations 2) (hor : orOp ∉ C.operations 2) (hminority : parity 3 ∉ C.operations 3) {f : (Fin 2 → Bool) → Bool} (hf : f ∈ C.operations 2) : EssentiallyUnary f

Without AND, OR and minority, every binary operation is essentially unary. The ten non-unary binary truth tables generate AND, OR or minority by the displayed superpositions; the remaining six tables depend on at most one input.

theorem Cslib.Logic.BooleanClone.ternary_idempotent_projection (C : BooleanClone) (hand : andOp ∉ C.operations 2) (hor : orOp ∉ C.operations 2) (hmajority : majority 3 ∉ C.operations 3) (hminority : parity 3 ∉ C.operations 3) {f : (Fin 3 → Bool) → Bool} (hf : f ∈ C.operations 3) (hid : ∀ (b : Bool), (f fun (x : Fin 3) => b) = b) : ∃ (i : Fin 3), ∀ (a : Fin 3 → Bool), f a = a i

An idempotent ternary operation in a clone missing the four generators is a projection. The eight self-dual idempotent tables are the three projections, majority, minority, and three skew majorities; each skew majority generates majority by self-composition.

theorem Cslib.Logic.BooleanClone.exists_projection_of_ternaryMinors {n : ℕ} {f : (Fin n → Bool) → Bool} (hid : ∀ (b : Bool), (f fun (x : Fin n) => b) = b) (h : ∀ (p : Fin n → Fin 3), ∃ (k : Fin 3), ∀ (a : Fin 3 → Bool), f (a ∘ p) = a k) : ∃ (i : Fin n), ∀ (a : Fin n → Bool), f a = a i

Ternary identification minors detect every finite Boolean operation that is not a projection. This statement covers arbitrary finite arity, including arity zero: its hypotheses are then inconsistent, since a nullary operation cannot be idempotent.

theorem Cslib.Logic.BooleanClone.idempotent_projection (C : BooleanClone) (hand : andOp ∉ C.operations 2) (hor : orOp ∉ C.operations 2) (hmajority : majority 3 ∉ C.operations 3) (hminority : parity 3 ∉ C.operations 3) {n : ℕ} (hn : 0 < n) {f : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) (hid : ∀ (b : Bool), (f fun (x : Fin n) => b) = b) : ∃ (i : Fin n), ∀ (a : Fin n → Bool), f a = a i

An arbitrary positive-arity idempotent operation in a clone missing the four generators is a projection. There is no upper bound on its arity.

theorem Cslib.Logic.BooleanClone.essentiallyUnary_of_missing_generators (C : BooleanClone) (hand : andOp ∉ C.operations 2) (hor : orOp ∉ C.operations 2) (hmajority : majority 3 ∉ C.operations 3) (hminority : parity 3 ∉ C.operations 3) {n : ℕ} (hn : 0 < n) {f : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) : EssentiallyUnary f

Chen's Boolean clone classification, Theorem 5.1 (arXiv v1, printed pp. 17–18), in contrapositive form. All positive arities are quantified, and constants count as essentially unary operations.

theorem Cslib.Logic.BooleanClone.classification (C : BooleanClone) : (∀ (n : ℕ), 0 < n → ∀ f ∈ C.operations n, EssentiallyUnary f) ∨ andOp ∈ C.operations 2 ∨ orOp ∈ C.operations 2 ∨ majority 3 ∈ C.operations 3 ∨ parity 3 ∈ C.operations 3

A positive-arity Boolean clone either has only essentially unary operations or contains AND, OR, majority or minority. This does not assume Post's or a minimal-clone classification.