Bitstring semantics for logical fragments (skeleton)

Per @cite{demey-smessaert-2018} §3.2, Definition 7 and Theorems 1–2.

Given a fragment ℱ with partition Π_S(ℱ) = {α_1, ..., α_n}, the bitstring semantics β_S^ℱ : 𝔹(ℱ) → BitVec n assigns each formula in the Boolean closure of ℱ a bitstring whose i-th position is 1 iff the anchor formula α_i entails it:

[β_S^ℱ(φ)]_i := 1 iff ⊨_S α_i → φ

Theorem 1: β_S^ℱ is a Boolean-algebra isomorphism. Theorem 2: β_S^ℱ is therefore an Aristotelian isomorphism (Lemma 1).

The Aristotelian relations on bitstrings (Definition 2) are bitwise:

Relation	Bitstring condition
Contradictory	b₁ ∧ b₂ = 0 and b₁ ∨ b₂ = 1
Contrary	b₁ ∧ b₂ = 0 and b₁ ∨ b₂ ≠ 1
Subcontrary	b₁ ∧ b₂ ≠ 0 and b₁ ∨ b₂ = 1
Subaltern	b₁ ∧ b₂ = b₁ and b₁ ∨ b₂ ≠ b₁

What's here

• bitstringOf φ ψ — Definition 7 (the bit at index i says whether anchor α_i entails ψ)
• BitContradictory/BitContrary/BitSubcontrary/BitSubaltern — Definition 2 (Aristotelian relations on bitstrings)
• bitstringOf_orderIso : closure (Set.range φ) ≃o (Fin n → Bool) — Theorem 1 (Boolean-algebra isomorphism), §11
• contradictory_iff_bitContradictory and three siblings — Theorem 2 (Aristotelian relations transfer), §10

noncomputable def Core.Opposition.bitstringOf {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (ψ : W → Bool) : Fin (partition ι W φ).card → Bool

The bitstring of a Boolean predicate ψ relative to a fragment φ: bit i is true iff anchor formula i entails ψ.

Equations

• Core.Opposition.bitstringOf φ ψ i = decide (∀ (w : W), Core.Opposition.anchor φ (Core.Opposition.anchorIndex✝ φ i) w = true → ψ w = true)

def Core.Opposition.bitAnd {n : ℕ} (b₁ b₂ : Fin n → Bool) : Fin n → Bool

Bitwise AND.

Equations

• Core.Opposition.bitAnd b₁ b₂ i = (b₁ i && b₂ i)

def Core.Opposition.bitOr {n : ℕ} (b₁ b₂ : Fin n → Bool) : Fin n → Bool

Bitwise OR.

Equations

• Core.Opposition.bitOr b₁ b₂ i = (b₁ i || b₂ i)

def Core.Opposition.zeros (n : ℕ) : Fin n → Bool

All-zeros bitstring.

Equations

• Core.Opposition.zeros n x✝ = false

def Core.Opposition.ones (n : ℕ) : Fin n → Bool

All-ones bitstring.

Equations

• Core.Opposition.ones n x✝ = true

@[simp]

theorem Core.Opposition.bitAnd_apply {n : ℕ} (b₁ b₂ : Fin n → Bool) (i : Fin n) : bitAnd b₁ b₂ i = (b₁ i && b₂ i)

@[simp]

theorem Core.Opposition.bitOr_apply {n : ℕ} (b₁ b₂ : Fin n → Bool) (i : Fin n) : bitOr b₁ b₂ i = (b₁ i || b₂ i)

@[simp]

theorem Core.Opposition.zeros_apply {n : ℕ} (i : Fin n) : zeros n i = false

@[simp]

theorem Core.Opposition.ones_apply {n : ℕ} (i : Fin n) : ones n i = true

def Core.Opposition.BitContradictory {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop

Bitstring contradictoriness: b₁ ∧ b₂ = 0 and b₁ ∨ b₂ = 1.

Equations

• Core.Opposition.BitContradictory b₁ b₂ = (Core.Opposition.bitAnd b₁ b₂ = Core.Opposition.zeros n ∧ Core.Opposition.bitOr b₁ b₂ = Core.Opposition.ones n)

def Core.Opposition.BitContrary {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop

Bitstring contrariety: b₁ ∧ b₂ = 0 and b₁ ∨ b₂ ≠ 1.

Equations

• Core.Opposition.BitContrary b₁ b₂ = (Core.Opposition.bitAnd b₁ b₂ = Core.Opposition.zeros n ∧ Core.Opposition.bitOr b₁ b₂ ≠ Core.Opposition.ones n)

def Core.Opposition.BitSubcontrary {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop

Bitstring subcontrariety: b₁ ∧ b₂ ≠ 0 and b₁ ∨ b₂ = 1.

Equations

• Core.Opposition.BitSubcontrary b₁ b₂ = (Core.Opposition.bitAnd b₁ b₂ ≠ Core.Opposition.zeros n ∧ Core.Opposition.bitOr b₁ b₂ = Core.Opposition.ones n)

def Core.Opposition.BitSubaltern {n : ℕ} (b₁ b₂ : Fin n → Bool) : Prop

Bitstring subalternation: b₁ ⊆ b₂ (bitwise ≤) and not equal.

Equations

• Core.Opposition.BitSubaltern b₁ b₂ = (Core.Opposition.bitAnd b₁ b₂ = b₁ ∧ Core.Opposition.bitOr b₁ b₂ ≠ b₁)

theorem Core.Opposition.bitAnd_bitstringOf_eq_zeros_of_contradictory {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (h : Contradictory ψ₁ ψ₂) : bitAnd (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = zeros (partition ι W φ).card

Forward direction of Theorem 2 (bitAnd half): Boolean contradictoriness of two arbitrary W → Bool predicates implies their bitstrings have empty bitwise-AND. This direction goes through without Boolean-closure infrastructure — only the partition's anchor-consistency matters.

The reverse direction (BitContradictory → Contradictory) and the bitOr-direction (Contradictory → bitOr = ones) require the Boolean-closure precondition (Demey-Smessaert §3, Lemma 6: every φ ∈ 𝔹(ℱ) is anchor-decided), which would in turn need Theorem 1's Boolean-algebra structure on 𝔹(ℱ).

theorem Core.Opposition.anchor_le_or_le_compl_mem_closure {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) {ψ : W → Bool} (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) : anchor φ σ ≤ ψ ∨ anchor φ σ ≤ ψᶜ

Lemma 6 specialized to our indexed-family anchor: every ψ in the Boolean closure of Set.range φ is anchor-decided. Direct induction on closure.

Note: Atoms.lean::anchorBA_le_or_le_compl_mem_closure proves the same statement for the BA-generic anchorBA s σ form (s : Finset α, σ : s → Bool). The two are not directly bridged: the bridge would require Finset.image φ to collapse duplicate generators and a corresponding choice of polarity per duplicate-class — adding case analysis that exceeds the cost of just reproving the specialized form here. The structural proof (induction on closure_bot_sup_induction) is the same in both files; if either changes, so does the other.

theorem Core.Opposition.bitstringOf_eq_apply_at_anchor {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ : W → Bool} (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) (i : Fin (partition ι W φ).card) {w : W} (hw : anchor φ (Core.Opposition.anchorIndex✝ φ i) w = true) : bitstringOf φ ψ i = ψ w

The bridge lemma: for any ψ in the Boolean closure and any world w that satisfies the anchor at index i, the bit bitstringOf φ ψ i equals ψ w. This is the well-definedness of the bitstring representation: Lemma 6 (anchor-decidedness) plus consistency means every anchor-witness world agrees on ψ's truth value, so the bit is unambiguous.

All four Aristotelian-relation theorems below are corollaries of this lemma + partition exhaustion.

noncomputable def Core.Opposition.worldAnchorIndex {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (w : W) : Fin (partition ι W φ).card

For each world, the index of an anchor it satisfies (chosen via Classical on anchor_jointly_exhaustive). Composes with bitstringOf_eq_apply_at_anchor to give bitstringOf φ ψ (worldAnchorIndex φ w) = ψ w.

Equations

• Core.Opposition.worldAnchorIndex φ w = (Core.Opposition.partition ι W φ).equivFin ⟨Classical.choose ⋯, ⋯⟩

theorem Core.Opposition.anchor_worldAnchorIndex {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (w : W) : anchor φ (Core.Opposition.anchorIndex✝ φ (worldAnchorIndex φ w)) w = true

The anchor at worldAnchorIndex φ w is satisfied by w.

theorem Core.Opposition.bitstringOf_apply_at_world {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ : W → Bool} (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) (w : W) : bitstringOf φ ψ (worldAnchorIndex φ w) = ψ w

The world-side bridge: at any world, bitstringOf φ ψ evaluated at that world's anchor index returns ψ at that world. Direct corollary of bitstringOf_eq_apply_at_anchor + anchor_worldAnchorIndex.

theorem Core.Opposition.bitstringOf_injOn_closure {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : Set.InjOn (bitstringOf φ) ↑(BooleanSubalgebra.closure (Set.range φ))

Theorem 1's injectivity half: bitstringOf φ is injective on the Boolean closure. Two formulas in the closure with the same bitstring representation agree at every world.

One-line proof: at each w, ψ_j w = bitstringOf φ ψ_j (worldAnchorIndex φ w) for both j ∈ {1, 2}, and the bitstrings are equal by hypothesis.

theorem Core.Opposition.anchor_mem_closure {W : Type u_1} [Fintype W] {ι : Type} [DecidableEq ι] [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) : anchor φ σ ∈ BooleanSubalgebra.closure (Set.range φ)

Anchor formulas live in the Boolean closure. This is the key Layer-3 bridge: our decide (∀ i : ι, ...) form of anchor (from Partition.lean) matches the Finset-indexed anchor over Finset.univ, which lives in the closure by induction.

noncomputable def Core.Opposition.bitstringInverse {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : W → Bool

The inverse of bitstringOf on the Boolean closure: takes a bitstring b to the Boolean-algebra supremum of those anchor formulas whose bit is true. The result lies in the closure (sup of closure elements via iSup_mem).

Equations

• Core.Opposition.bitstringInverse φ b = ⨆ (i : Fin (Core.Opposition.partition ι W φ).card), if b i = true then Core.Opposition.anchor φ (Core.Opposition.anchorIndex✝ φ i) else ⊥

theorem Core.Opposition.bitstringInverse_mem_closure {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : bitstringInverse φ b ∈ BooleanSubalgebra.closure (Set.range φ)

theorem Core.Opposition.bitstringInverse_apply_at_anchor {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) (j : Fin (partition ι W φ).card) {w : W} (hw : anchor φ (Core.Opposition.anchorIndex✝ φ j) w = true) : bitstringInverse φ b w = b j

The bitstringInverse-evaluation lemma: at a world w satisfying the anchor at index j, the inverse bitstring evaluates to the j-th bit. Heart of both round trips: shows that the iSup collapses to a single summand (the one at j) by uniqueness of the satisfied anchor.

theorem Core.Opposition.bitstringOf_bitstringInverse {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (b : Fin (partition ι W φ).card → Bool) : bitstringOf φ (bitstringInverse φ b) = b

Round trip 1: bitstringOf ∘ bitstringInverse = id on Fin n → Bool. Use bitstringOf_eq_apply_at_anchor (lifting through any anchor witness)

• bitstringInverse_apply_at_anchor (evaluating the inverse).

theorem Core.Opposition.bitstringInverse_bitstringOf {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ : W → Bool} (hψ : ψ ∈ BooleanSubalgebra.closure (Set.range φ)) : bitstringInverse φ (bitstringOf φ ψ) = ψ

Round trip 2: bitstringInverse ∘ bitstringOf = id on closure elements. Symmetric to round trip 1, using bitstringOf_apply_at_world for evaluation of bitstringOf ψ at the worldAnchorIndex.

noncomputable def Core.Opposition.bitstringOf_orderIso {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : ↥(BooleanSubalgebra.closure (Set.range φ)) ≃o (Fin (partition ι W φ).card → Bool)

Theorem 1 (Demey & Smessaert 2018) — the full Boolean-algebra isomorphism. bitstringOf φ restricted to the Boolean closure of Set.range φ is an order isomorphism onto Fin n → Bool where n = |partition|. As an OrderIso between Boolean algebras, it is automatically a Boolean-algebra isomorphism (BA structure is determined by the order).

Construction: toFun := bitstringOf φ, invFun := bitstringInverse φ, round trips established above; monotonicity from bitAnd_eq_left_iff_forall_imp (entailment ↔ bitwise inclusion).

Equations

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

All four Aristotelian-relation theorems below reduce to combinations of three iff lemmas. Each Bit* predicate decomposes into bit-level conditions, and each bit-level condition matches a pointwise predicate via the bridge bitstringOf_eq_apply_at_anchor (forward) and bitstringOf_apply_at_world (reverse).

theorem Core.Opposition.bitAnd_eq_zeros_iff_forall_not_and {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : bitAnd (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = zeros (partition ι W φ).card ↔ ∀ (w : W), ¬(ψ₁ w = true ∧ ψ₂ w = true)

theorem Core.Opposition.bitOr_eq_ones_iff_forall_or {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : bitOr (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = ones (partition ι W φ).card ↔ ∀ (w : W), ψ₁ w = true ∨ ψ₂ w = true

theorem Core.Opposition.bitAnd_eq_left_iff_forall_imp {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : bitAnd (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = bitstringOf φ ψ₁ ↔ ∀ (w : W), ψ₁ w = true → ψ₂ w = true

theorem Core.Opposition.bitOr_eq_left_iff_forall_imp_rev {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : bitOr (bitstringOf φ ψ₁) (bitstringOf φ ψ₂) = bitstringOf φ ψ₁ ↔ ∀ (w : W), ψ₂ w = true → ψ₁ w = true

theorem Core.Opposition.contradictory_iff_bitContradictory {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : Contradictory ψ₁ ψ₂ ↔ BitContradictory (bitstringOf φ ψ₁) (bitstringOf φ ψ₂)

Theorem 2 — Contradictory (Demey & Smessaert 2018).

theorem Core.Opposition.contrary_iff_bitContrary {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : Contrary ψ₁ ψ₂ ↔ BitContrary (bitstringOf φ ψ₁) (bitstringOf φ ψ₂)

Theorem 2 — Contrary (shares bitAnd half with Contradictory).

theorem Core.Opposition.subcontrary_iff_bitSubcontrary {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : Subcontrary ψ₁ ψ₂ ↔ BitSubcontrary (bitstringOf φ ψ₁) (bitstringOf φ ψ₂)

Theorem 2 — Subcontrary (dual of Contrary).

theorem Core.Opposition.subaltern_iff_bitSubaltern {W : Type u_1} [Fintype W] {ι : Type} [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) {ψ₁ ψ₂ : W → Bool} (hψ₁ : ψ₁ ∈ BooleanSubalgebra.closure (Set.range φ)) (hψ₂ : ψ₂ ∈ BooleanSubalgebra.closure (Set.range φ)) : Subaltern ψ₁ ψ₂ ↔ BitSubaltern (bitstringOf φ ψ₁) (bitstringOf φ ψ₂)

Theorem 2 — Subaltern (pointwise inclusion ↔ bitwise).