Generated Boolean clones and functional completeness

BooleanClone.generated G contains exactly the operations obtained from positive-arity members of G and coordinate projections by finitely many superpositions. Members of G 0 are ignored: constant functions here have positive arity, rather than being nullary gates.

Main definitions

• Cslib.Logic.BooleanClone.Generated: finite superposition derivations.
• Cslib.Logic.BooleanClone.generated: the clone generated by a family of operations.
• Cslib.Logic.BooleanClone.IsComplete: containing every positive-arity Boolean operation.
• Cslib.Logic.BooleanClone.FunctionallyComplete: generation of all positive-arity operations.

Main results

• Cslib.Logic.BooleanClone.generated_le_iff: the universal property of the generated clone.

inductive Cslib.Logic.BooleanClone.Generated (G : (n : ℕ) → Set ((Fin n → Bool) → Bool)) {n : ℕ} : ((Fin n → Bool) → Bool) → Prop

A finite derivation from positive-arity generators, projections and superposition.

• of_mem {G : (n : ℕ) → Set ((Fin n → Bool) → Bool)} {n : ℕ} {f : (Fin n → Bool) → Bool} : 0 < n → f ∈ G n → Generated G f
• projection {G : (n : ℕ) → Set ((Fin n → Bool) → Bool)} {n : ℕ} (i : Fin n) : Generated G fun (a : Fin n → Bool) => a i
• comp {G : (n : ℕ) → Set ((Fin n → Bool) → Bool)} {m n : ℕ} (hm : 0 < m) (hn : 0 < n) {f : (Fin m → Bool) → Bool} {g : Fin m → (Fin n → Bool) → Bool} : Generated G f → (∀ (i : Fin m), Generated G (g i)) → Generated G fun (a : Fin n → Bool) => f fun (i : Fin m) => g i a

theorem Cslib.Logic.BooleanClone.Generated.arity_pos {G : (n : ℕ) → Set ((Fin n → Bool) → Bool)} {n : ℕ} {f : (Fin n → Bool) → Bool} (h : Generated G f) : 0 < n

Derivations only construct positive-arity operations.

def Cslib.Logic.BooleanClone.generated (G : (n : ℕ) → Set ((Fin n → Bool) → Bool)) : BooleanClone

The clone of operations with a finite superposition derivation from G.

theorem Cslib.Logic.BooleanClone.generated_le_iff (G : (n : ℕ) → Set ((Fin n → Bool) → Bool)) (C : BooleanClone) : (∀ (n : ℕ), (generated G).operations n ⊆ C.operations n) ↔ ∀ (n : ℕ), 0 < n → G n ⊆ C.operations n

A clone contains the generated clone exactly when it contains every positive-arity original generator. No condition on G 0 is imposed.

def Cslib.Logic.BooleanClone.IsComplete (C : BooleanClone) : Prop

A clone is complete when it contains every Boolean operation of every positive arity.

def Cslib.Logic.BooleanClone.FunctionallyComplete (G : (n : ℕ) → Set ((Fin n → Bool) → Bool)) : Prop

Functional completeness for positive arities, allowing unary constant functions. This does not require synthesizing nullary gates.