Positive-arity Boolean clones

A clone contains every coordinate projection and is closed under superposition. Nullary operations are excluded; constant functions of positive arity are allowed. This is the common algebraic interface for the Boolean Schaefer classification and Post's completeness criterion.

Main definitions

• Cslib.Logic.BooleanClone: positive-arity Boolean clones.

Main results

• Cslib.Logic.BooleanClone.minor: variable identification, permutation and dummy variables.
• Cslib.Logic.BooleanClone.diagonal: identifying every argument gives a unary operation.

structure Cslib.Logic.BooleanClone : Type

A clone of positive-arity Boolean operations. Nullary operations are excluded.

• operations (n : ℕ) : Set ((Fin n → Bool) → Bool)

  Operations of each arity.

• nullary : self.operations 0 = ∅

  There are no nullary operations.

• projection {n : ℕ} (i : Fin n) : (fun (a : Fin n → Bool) => a i) ∈ self.operations n

  Every coordinate projection belongs to the clone.

• comp {m n : ℕ} (hm : 0 < m) (hn : 0 < n) {f : (Fin m → Bool) → Bool} {g : Fin m → (Fin n → Bool) → Bool} (hf : f ∈ self.operations m) (hg : ∀ (i : Fin m), g i ∈ self.operations n) : (fun (a : Fin n → Bool) => f fun (i : Fin m) => g i a) ∈ self.operations n

  Superposition of positive-arity operations belongs to the clone.

def Cslib.Logic.BooleanClone.andOp (a : Fin 2 → Bool) : Bool

AND as a binary operation.

def Cslib.Logic.BooleanClone.orOp (a : Fin 2 → Bool) : Bool

OR as a binary operation.

theorem Cslib.Logic.BooleanClone.minor (C : BooleanClone) {m n : ℕ} (hm : 0 < m) (hn : 0 < n) {f : (Fin m → Bool) → Bool} (hf : f ∈ C.operations m) (p : Fin m → Fin n) : (fun (a : Fin n → Bool) => f (a ∘ p)) ∈ C.operations n

Identifying, permuting or adding dummy variables preserves clone membership.

theorem Cslib.Logic.BooleanClone.diagonal (C : BooleanClone) {n : ℕ} (hn : 0 < n) {f : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) : (fun (a : Fin 1 → Bool) => f fun (x : Fin n) => a 0) ∈ C.operations 1

Applying an operation to a constant tuple gives a unary operation in the clone.

theorem Cslib.Logic.BooleanClone.arity_pos (C : BooleanClone) {n : ℕ} {f : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) : 0 < n

Every operation in a positive-arity clone has positive arity.

def Cslib.Logic.BooleanClone.binaryTable (b00 b01 b10 b11 : Bool) (a : Fin 2 → Bool) : Bool

A binary Boolean operation specified by its four truth-table entries.

theorem Cslib.Logic.BooleanClone.binaryTable_eq (f : (Fin 2 → Bool) → Bool) : f = binaryTable (f ![false, false]) (f ![false, true]) (f ![true, false]) (f ![true, true])

A binary operation is determined by its four truth-table entries.