Anchor formulas in a Boolean algebra: Lemma 6 of @cite{demey-smessaert-2018}

For a finite generator set s : Finset α of a Boolean algebra α, an anchor formula is a meet of literals over s — one literal lit φ b per generator, with polarity selected by an assignment σ : s → Bool:

anchorBA s σ := ⨅ x ∈ s, (if σ x then x else xᶜ)

The central technical lemma (Demey-Smessaert §3, Lemma 6) is anchor- decidedness: for every element ψ of the Boolean closure of s, every anchor formula either entails ψ or entails ¬ψ. Equivalently, the anchor formulas partition the closure's "truth space" into mutually-deciding cells.

Lemma 6 is the engine driving the bitstring representation in Bitstring.lean: the i-th bit of bitstringOf φ ψ is well-defined precisely because the i-th anchor decides ψ. Closing Theorems 1 and 2 from Bitstring.lean reduces to this lemma plus mathlib's existing infrastructure.

What this file uses from mathlib

• BooleanSubalgebra (Yaël Dillies, 2024) for closure-based reasoning
• closure_bot_sup_induction for the inductive proof of Lemma 6
• Standard BooleanAlgebra API (compl_sup, compl_compl, le_inf, ...)

Generality

The lemma is stated for an arbitrary [BooleanAlgebra α]. Specializations to α = W → Bool (the syllogistic case) are immediate.

def Core.Opposition.lit {α : Type u_1} [BooleanAlgebra α] (φ : α) (b : Bool) : α

A literal over a generator φ : α: either φ itself (positive polarity) or its complement φᶜ (negative polarity).

Equations

• Core.Opposition.lit φ b = if b = true then φ else φᶜ

@[simp]

theorem Core.Opposition.lit_true {α : Type u_1} [BooleanAlgebra α] (φ : α) : lit φ true = φ

@[simp]

theorem Core.Opposition.lit_false {α : Type u_1} [BooleanAlgebra α] (φ : α) : lit φ false = φᶜ

def Core.Opposition.anchorBA {α : Type u_1} [BooleanAlgebra α] (s : Finset α) (σ : ↥s → Bool) : α

The anchor formula for a polarity assignment σ : s → Bool over a finite generator set s : Finset α: the meet of lit x (σ x) over all x ∈ s. This is a generic Boolean-algebra version of the Demey-Smessaert anchor (Definition 5).

Equations

• Core.Opposition.anchorBA s σ = s.attach.inf fun (x : ↥s) => Core.Opposition.lit (↑x) (σ x)

theorem Core.Opposition.anchorBA_le_lit {α : Type u_1} [BooleanAlgebra α] (s : Finset α) (σ : ↥s → Bool) (x : ↥s) : anchorBA s σ ≤ lit (↑x) (σ x)

The anchor lies below each of its constituent literals.

theorem Core.Opposition.anchorBA_le_of_pos {α : Type u_1} [BooleanAlgebra α] {s : Finset α} {σ : ↥s → Bool} {x : ↥s} (h : σ x = true) : anchorBA s σ ≤ ↑x

A specific positive-polarity case: if σ x = true, then anchorBA s σ ≤ x.

theorem Core.Opposition.anchorBA_le_compl_of_neg {α : Type u_1} [BooleanAlgebra α] {s : Finset α} {σ : ↥s → Bool} {x : ↥s} (h : σ x = false) : anchorBA s σ ≤ (↑x)ᶜ

A specific negative-polarity case: if σ x = false, then anchorBA s σ ≤ xᶜ.

theorem Core.Opposition.anchorBA_le_or_le_compl_mem_closure {α : Type u_1} [BooleanAlgebra α] {s : Finset α} (σ : ↥s → Bool) {ψ : α} (hψ : ψ ∈ BooleanSubalgebra.closure ↑s) : anchorBA s σ ≤ ψ ∨ anchorBA s σ ≤ ψᶜ

Lemma 6 (Demey & Smessaert 2018): every element of the Boolean closure of a finite generator set is anchor-decided — every anchor formula either entails it or entails its complement.

This holds unconditionally (no consistency hypothesis on the anchor): if the anchor is ⊥, both disjuncts hold trivially. The bitstring semantics in Bitstring.lean uses Lemma 6 with the anchor known to be nonzero (i.e., σ in the partition), giving the exclusive decidedness that makes each bit well-defined.

Proof: induction on closure membership via closure_bot_sup_induction.

• mem: anchor includes lit x (σ x) as a meet; sign of σ x decides.
• bot: anchor ≤ ⊥ᶜ = ⊤ trivially.
• sup: case on which side of the disjunction the anchor sits below.
• compl: flip the disjunction (compl_compl).

theorem Core.Opposition.anchorBA_le_or_le_compl_exclusive {α : Type u_1} [BooleanAlgebra α] {s : Finset α} (σ : ↥s → Bool) {ψ : α} (hψ : ψ ∈ BooleanSubalgebra.closure ↑s) (hCons : anchorBA s σ ≠ ⊥) : anchorBA s σ ≤ ψ ∧ ¬anchorBA s σ ≤ ψᶜ ∨ ¬anchorBA s σ ≤ ψ ∧ anchorBA s σ ≤ ψᶜ

The exclusive form: for a consistent anchor, exactly one disjunct of Lemma 6 holds. (If both held, anchor would be below ψ ⊓ ψᶜ = ⊥.)