Dedekind Numbers

A Dedekind number M(n) counts the number of monotone Boolean functions on n variables, or equivalently, the number of antichains (Sperner families) in the Boolean lattice 2^[n].

For example, $$M ( 0 ) = 2 , M ( 1 ) = 3 , M ( 2 ) = 6 , and M ( 3 ) = 20 .$$ The first few values grew slowly: $$M ( 4 ) = 168 , M ( 5 ) = 7581$$, but then rapidly: $$M ( 6 ) = 7828354 , M ( 7 ) = 2414682040998 , M ( 8 ) = 56130437228687557907788$$, and $$M ( 9 ) = 286386577668298411128469151667598498812366$$ (computed in 2023).

We formalize two definitions:

• M n: the number of monotone Boolean functions (Fin n → Bool) → Bool
• M' n: the number of antichains (Sperner families) of Finset (Fin n)

We prove their values for small n and show that the two definitions agree for all n.

The problem is to determine the exact values of $M(n)$ for $n ≥ 10$. In particular, the value of $M(10)$ is currently unknown.

References:

• Wikipedia
• Oeis/A372

instance DedekindNumber.piFinBoolDecidableLE {n : ℕ} : DecidableRel fun (a b : Fin n → Bool) => a ≤ b

Equations

• DedekindNumber.piFinBoolDecidableLE a b = ⋯.mpr Fintype.decidableForallFintype

def DedekindNumber.M (n : ℕ) : ℕ

$M(n)$ is the number of monotone Boolean functions on $n$ variables.

Equations

• DedekindNumber.M n = Fintype.card { f : (Fin n → Bool) → Bool // Monotone f }

def DedekindNumber.IsSperner {n : ℕ} (A : Finset (Finset (Fin n))) : Prop

A Sperner family (antichain) of subsets of Fin n: a family of sets such that no member is a subset of another.

Equations

• DedekindNumber.IsSperner A = IsAntichain (fun (s t : Finset (Fin n)) => s ⊆ t) ↑A

instance DedekindNumber.isSpernerDecidable {n : ℕ} : DecidablePred fun (A : Finset (Finset (Fin n))) => IsSperner A

Equations

• DedekindNumber.isSpernerDecidable A = id (id (id (⋯.mpr inferInstance)))

def DedekindNumber.M' (n : ℕ) : ℕ

$M'(n)$ is the number of antichains (Sperner families) of subsets of Fin n.

Equations

• DedekindNumber.M' n = Fintype.card { A : Finset (Finset (Fin n)) // DedekindNumber.IsSperner A }

theorem DedekindNumber.M_zero : M 0 = 2

Values for small n

theorem DedekindNumber.M_one : M 1 = 3

theorem DedekindNumber.M_two : M 2 = 6

theorem DedekindNumber.M_three : M 3 = 20

theorem DedekindNumber.M'_zero : M' 0 = 2

theorem DedekindNumber.M'_one : M' 1 = 3

theorem DedekindNumber.M'_two : M' 2 = 6

theorem DedekindNumber.M'_three : M' 3 = 20

def DedekindNumber.χ {n : ℕ} (s : Finset (Fin n)) : Fin n → Bool

The indicator function of a finset: χ s i = true ↔ i ∈ s.

Equations

• DedekindNumber.χ s i = decide (i ∈ s)

def DedekindNumber.supp {n : ℕ} (v : Fin n → Bool) : Finset (Fin n)

The support of a Boolean-valued function: supp v = {i | v i = true}.

Equations

• DedekindNumber.supp v = {i : Fin n | v i = true}

def DedekindNumber.toSperner {n : ℕ} (f : (Fin n → Bool) → Bool) : Finset (Finset (Fin n))

Forward map: monotone function → Sperner family (the minimal true sets).

Equations

• DedekindNumber.toSperner f = {s : Finset (Fin n) | f (DedekindNumber.χ s) = true ∧ ∀ t ⊆ s, f (DedekindNumber.χ t) = true → s ⊆ t}

def DedekindNumber.fromSperner {n : ℕ} (A : Finset (Finset (Fin n))) (v : Fin n → Bool) : Bool

Backward map: Sperner family → monotone Boolean function.

Equations

• DedekindNumber.fromSperner A v = decide (∃ s ∈ A, ∀ i ∈ s, v i = true)

theorem DedekindNumber.χ_supp {n : ℕ} (v : Fin n → Bool) : χ (supp v) = v

theorem DedekindNumber.supp_χ {n : ℕ} (s : Finset (Fin n)) : supp (χ s) = s

theorem DedekindNumber.χ_le_iff {n : ℕ} (s t : Finset (Fin n)) : χ s ≤ χ t ↔ s ⊆ t

theorem DedekindNumber.mem_supp_iff {n : ℕ} (v : Fin n → Bool) (i : Fin n) : i ∈ supp v ↔ v i = true

theorem DedekindNumber.toSperner_isSperner {n : ℕ} (f : (Fin n → Bool) → Bool) : Monotone f → IsSperner (toSperner f)

theorem DedekindNumber.fromSperner_monotone {n : ℕ} (A : Finset (Finset (Fin n))) : IsSperner A → Monotone (fromSperner A)

theorem DedekindNumber.exists_minimal_true_subset {n : ℕ} {f : (Fin n → Bool) → Bool} : Monotone f → ∀ {s : Finset (Fin n)} (hs : f (χ s) = true), ∃ t ⊆ s, f (χ t) = true ∧ ∀ u ⊆ t, f (χ u) = true → t ⊆ u

Every true set of a monotone Boolean function contains a minimal true set.

theorem DedekindNumber.fromSperner_toSperner {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : Monotone f) : fromSperner (toSperner f) = f

Converting a monotone function to a Sperner family and back yields the same function.

theorem DedekindNumber.toSperner_fromSperner {n : ℕ} (A : Finset (Finset (Fin n))) (hA : IsSperner A) : toSperner (fromSperner A) = A

Converting a Sperner family to a monotone function and back yields the same family.

def DedekindNumber.equivMonotoneSperner (n : ℕ) : { f : (Fin n → Bool) → Bool // Monotone f } ≃ { A : Finset (Finset (Fin n)) // IsSperner A }

The set of monotone Boolean functions on n variables is in bijection with the set of Sperner families of subsets of Fin n.

Equations

• One or more equations did not get rendered due to their size.

theorem DedekindNumber.M_eq_M' : M = M'

def DedekindNumber.kisielewiczFormula (n : ℕ) : ℕ

A closed formula for the Dedekind numbers as found by Kisielewicz (1998): $$ M(n) = \sum_{k=0}^{2^{2^n}}\prod_{j = 1}^{2 ^ n - 1}\prod_{i = 0}^{j - 1} \left( 1 - b_i^kb_j^k \prod_{m = 0}^{\log_2 i} (1 - b_m^i + b_m^ib_m^j)\right), $$, where $b_i^k$ is the $i$-th bit of $k$.

Equations

• One or more equations did not get rendered due to their size.

theorem DedekindNumber.kisielewiczFormula_zero : kisielewiczFormula 0 = 2

theorem DedekindNumber.kisielewiczFormula_one : kisielewiczFormula 1 = 3

theorem DedekindNumber.kisielewiczFormula_two : kisielewiczFormula 2 = 6

theorem DedekindNumber.kisielewiczFormula_three : kisielewiczFormula 3 = 20

theorem DedekindNumber.M_eq_kisielewiczFormula : M = kisielewiczFormula

Kisielewicz (1988) proved the following arithmetic formula for the Dedekind numbers: $$ M(n) = \sum_{k=0}^{2^{2^n}}\prod_{j = 1}^{2 ^ n - 1}\prod_{i = 0}^{j - 1} \left( 1 - b_i^kb_j^k \prod_{m = 0}^{\log_2 i} (1 - b_m^i + b_m^ib_m^j)\right), $$ where $b_i^k$ is the $i$-th bit of $k$. However, this formula is not computationally efficient for large $n$.

theorem DedekindNumber.M_eq : M = sorry

No closed-form expression that allows efficient computation of Dedekind numbers is currently known.

theorem DedekindNumber.Dedekind_10 : M 10 = sorry

In particular, the Dedekind number for n = 10 is currently unknown.