Post's functional completeness criterion

A family of positive-arity Boolean operations generates every positive-arity Boolean function exactly when it is contained in none of the five classes: preserving false, preserving true, monotone, self-dual, and affine. This is [PM90], the theorem on printed p. 466. Families may be infinite and operation arities are unbounded. Constants are unary constant functions, as in the shared Schaefer clone API; no nullary gate is synthesized.

The affine class uses Cslib.BitString.IsAffine, preservation of sums of three points over 𝔽₂, equivalently a constant plus a parity of selected inputs. The source's "counting" functions have exactly this meaning. NOT and constants follow the source's Lemmas 1–2, pp. 466–467. The remainder is an original combination of the shared four-generator Boolean clone classification with a binary affine-witness construction, followed by truth-table normalization and disjunctive normal form. The full lattice of Boolean clones is not asserted.

Main definitions

• Cslib.Logic.BooleanClone.PostCriterion: a witness outside each of the five closed classes.

Main results

• Cslib.Logic.BooleanClone.isComplete_iff_postCriterion: the criterion for a Boolean clone.
• Cslib.Logic.BooleanClone.functionallyComplete_iff: Post's criterion for a generating family.

References

• F. J. Pelletier and N. M. Martin, Post's Functional Completeness Theorem, printed pp. 466–469.

def Cslib.Logic.BooleanClone.notOp (a : Fin 1 → Bool) : Bool

Unary negation.

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

A positive-arity witness outside each of Post's five composition-closed classes. Witnesses may have different arities and the same operation may serve several clauses.

theorem Cslib.Logic.BooleanClone.PostCriterion.mono {G H : (n : ℕ) → Set ((Fin n → Bool) → Bool)} (hG : PostCriterion G) (h : ∀ (n : ℕ), 0 < n → G n ⊆ H n) : PostCriterion H

Enlarging the positive-arity generators preserves the five witnesses.

theorem Cslib.Logic.BooleanClone.comp_not (C : BooleanClone) {n : ℕ} (hnot : notOp ∈ C.operations 1) {f : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) : (fun (a : Fin n → Bool) => !f a) ∈ C.operations n

Substitute an available operation into unary negation.

theorem Cslib.Logic.BooleanClone.comp_and (C : BooleanClone) {n : ℕ} (hand : andOp ∈ C.operations 2) {f g : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) (hg : g ∈ C.operations n) : (fun (a : Fin n → Bool) => f a && g a) ∈ C.operations n

Apply an available binary conjunction to two available operations.

theorem Cslib.Logic.BooleanClone.comp_or (C : BooleanClone) {n : ℕ} (hor : orOp ∈ C.operations 2) {f g : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) (hg : g ∈ C.operations n) : (fun (a : Fin n → Bool) => f a || g a) ∈ C.operations n

Apply an available binary disjunction to two available operations.

theorem Cslib.Logic.BooleanClone.const_mem (C : BooleanClone) {n : ℕ} (hn : 0 < n) {b : Bool} (hb : (fun (x : Fin 1 → Bool) => b) ∈ C.operations 1) : (fun (x : Fin n → Bool) => b) ∈ C.operations n

A unary constant supplies the same constant at every positive arity.

theorem Cslib.Logic.BooleanClone.not_mem_of_witnesses (C : BooleanClone) (hzero : ∃ (n : ℕ), 0 < n ∧ ∃ f ∈ C.operations n, (f fun (x : Fin n) => false) ≠ false) (hone : ∃ (n : ℕ), 0 < n ∧ ∃ f ∈ C.operations n, (f fun (x : Fin n) => true) ≠ true) (hmono : ∃ (n : ℕ), 0 < n ∧ ∃ f ∈ C.operations n, ¬Monotone f) : notOp ∈ C.operations 1

Failure of preservation of both constants and of monotonicity generates NOT. This is Lemma 1 of [PM90], printed pp. 466–467.

theorem Cslib.Logic.BooleanClone.constants_mem_of_not_selfDual (C : BooleanClone) (hnot : notOp ∈ C.operations 1) (hself : ∃ (n : ℕ), 0 < n ∧ ∃ f ∈ C.operations n, ¬∀ (a : Fin n → Bool), (f fun (i : Fin n) => !a i) = !f a) (b : Bool) : (fun (x : Fin 1 → Bool) => b) ∈ C.operations 1

NOT and failure of self-duality supply both unary constant functions. This is Lemma 2 of [PM90], printed p. 467.

theorem Cslib.Logic.BooleanClone.comp_xor (C : BooleanClone) {n : ℕ} (hxor : parity 2 ∈ C.operations 2) {f g : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) (hg : g ∈ C.operations n) : (fun (a : Fin n → Bool) => f a ^^ g a) ∈ C.operations n

Compose two operations with available XOR.

theorem Cslib.Logic.BooleanClone.and_mem_of_odd_binary (C : BooleanClone) (hnot : notOp ∈ C.operations 1) {f : (Fin 2 → Bool) → Bool} (hf : f ∈ C.operations 2) (hodd : (f ![false, false] ^^ f ![false, true] ^^ f ![true, false] ^^ f ![true, true]) = true) : andOp ∈ C.operations 2

Any binary truth table of odd parity generates AND in the presence of NOT.

theorem Cslib.Logic.BooleanClone.and_mem_of_xor_of_not_affine (C : BooleanClone) (hnot : notOp ∈ C.operations 1) (hconst : ∀ (b : Bool), (fun (x : Fin 1 → Bool) => b) ∈ C.operations 1) (hxor : parity 2 ∈ C.operations 2) {n : ℕ} {f : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) (haff : ¬BitString.IsAffine f) : andOp ∈ C.operations 2

With XOR, NOT and constants, a failure of affinity gives an odd binary truth table, hence AND. This reduces an arbitrary-arity affine witness directly to its four square values.

theorem Cslib.Logic.BooleanClone.and_mem_of_not_affine (C : BooleanClone) (hnot : notOp ∈ C.operations 1) (hconst : ∀ (b : Bool), (fun (x : Fin 1 → Bool) => b) ∈ C.operations 1) {n : ℕ} {f : (Fin n → Bool) → Bool} (hf : f ∈ C.operations n) (haff : ¬BitString.IsAffine f) : andOp ∈ C.operations 2

The shared Schaefer classification supplies AND, using a non-affine witness to handle its minority branch.

theorem Cslib.Logic.BooleanClone.isComplete_of_not_and (C : BooleanClone) (hnot : notOp ∈ C.operations 1) (hand : andOp ∈ C.operations 2) (hconst : ∀ (b : Bool), (fun (x : Fin 1 → Bool) => b) ∈ C.operations 1) : C.IsComplete

NOT, AND and the unary constants generate every positive-arity Boolean operation. The construction is disjunctive normal form, with one conjunction per accepted assignment.

theorem Cslib.Logic.BooleanClone.isComplete_iff_postCriterion (C : BooleanClone) : C.IsComplete ↔ PostCriterion C.operations

Post's five-class criterion for a positive-arity Boolean clone.

theorem Cslib.Logic.BooleanClone.functionallyComplete_iff (G : (n : ℕ) → Set ((Fin n → Bool) → Bool)) : FunctionallyComplete G ↔ PostCriterion G

Post's functional completeness theorem. An arbitrary family of positive-arity Boolean operations is complete iff it has a witness outside each of the five closed classes. There is no finiteness or common-arity assumption on the family.