Bitstring semantics for logical fragments

Per [DS18a] §3.2. For a fragment φ : ι → W → Bool, the bitstring of a formula ψ in the Boolean closure of Set.range φ records, for each consistent anchor cell, whether that cell entails ψ. This map is a Boolean isomorphism onto Fin n → Bool (Theorem 1), hence an Aristotelian isomorphism (Theorem 2).

Main declarations

• bitstringOf — the bitstring map (Definition 7).
• bitstringOrderIso — the isomorphism closure (Set.range φ) ≃o (Fin n → Bool).
• isAtom_anchor — consistent anchor cells are the atoms of the closure.
• isContradictory_bitstring_iff and siblings — the Aristotelian relations transfer.

Implementation notes

The closure-membership lemmas need only [Fintype ι] (literal membership needs no index instances). [DecidableEq ι] enters only with the partition, so the world-enumeration declarations — which also require [Fintype W] — live in section WorldEnumeration below.

isAtom_anchor is the partition-cell case of mathlib's atom representation for finite Boolean algebras (CompleteAtomicBooleanAlgebra.toSetOfIsAtom); the bitstring isomorphism is its explicit Fin n-indexed form.

Anchor-decidedness

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

Lemma 6 for the indexed-family anchor: every closure element is entailed by an anchor or by its complement ([DS18a]).

Anchor formulas lie in the closure

theorem Aristotelian.anchor_eq_iInf {W : Type u_1} {ι : Type u_2} [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) : anchor φ σ = ⨅ (i : ι), if σ i = true then φ i else (φ i)ᶜ

An anchor is the infimum of its literals ±φ i.

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

Anchor formulas lie in the Boolean closure of Set.range φ — an anchor is the infimum of its literals, each of which lies in the closure.

Atoms of the closure

theorem Aristotelian.isAtom_anchor {W : Type u_1} {ι : Type u_2} [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) (hCons : ∃ (w : W), anchor φ σ w = true) : IsAtom ⟨anchor φ σ, ⋯⟩

A consistent anchor cell is an atom of closure (Set.range φ): it is below or disjoint from every closure element (Lemma 6), so once nonzero nothing lies strictly between it and ⊥.

theorem Aristotelian.atom_imp_anchor {W : Type u_1} {ι : Type u_2} [Fintype ι] (φ : ι → W → Bool) {a : ↥(BooleanSubalgebra.closure (Set.range φ))} (ha : IsAtom a) : ∃ (σ : ι → Bool), ↑a = anchor φ σ ∧ ∃ (w : W), anchor φ σ w = true

Converse of isAtom_anchor: every atom of closure (Set.range φ) is a consistent anchor cell.

theorem Aristotelian.isAtom_iff_anchor {W : Type u_1} {ι : Type u_2} [Fintype ι] (φ : ι → W → Bool) {a : ↥(BooleanSubalgebra.closure (Set.range φ))} : IsAtom a ↔ ∃ (σ : ι → Bool), ↑a = anchor φ σ ∧ ∃ (w : W), anchor φ σ w = true

The atoms of closure (Set.range φ) are exactly the consistent anchor cells — the partition-cell ↔ atom correspondence underlying the bitstring representation.

Bitstring representation (Definition 7)

noncomputable def Aristotelian.anchorIndex {W : Type u_1} {ι : Type u_2} [Fintype W] [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : Fin (partition ι W φ).card → ι → Bool

A positional index for the anchor cells, via partition.equivFin.

Equations

• Aristotelian.anchorIndex φ i = ↑((Aristotelian.partition ι W φ).equivFin.symm i)

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

The bitstring of ψ relative to φ: bit i is true iff anchor i entails ψ ([DS18a], Definition 7).

Equations

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

theorem Aristotelian.anchorIndex_consistent {W : Type u_1} {ι : Type u_2} [Fintype W] [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (i : Fin (partition ι W φ).card) : ∃ (w : W), anchor φ (anchorIndex φ i) w = true

Each partition cell is consistent: some world satisfies the anchor at index i.

Bitstring evaluation

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

If w satisfies anchor i and ψ is in the closure, then bitstringOf φ ψ i is ψ w.

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

An anchor index satisfied by w.

Equations

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

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

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

bitstringOf φ ψ at a world's anchor index recovers ψ at that world.

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

bitstringOf φ is injective on the Boolean closure.

The inverse and round trips

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

The supremum of the anchor cells whose bit is true — the inverse of bitstringOf on the closure.

Equations

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

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

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

If w satisfies anchor j, then bitstringInverse φ b w is the j-th bit: the iSup collapses to the summand at j.

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

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

Theorem 1: the Boolean isomorphism

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

Theorem 1 ([DS18a]): bitstringOf φ is an order isomorphism closure (Set.range φ) ≃o (Fin n → Bool), n = |partition|.

Equations

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

Boolean complexity

def Aristotelian.boolComplexity {W : Type u_1} {ι : Type u_2} [Fintype W] [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) : ℕ

The Boolean complexity of a fragment: its bitstring length |partition| = log₂ |𝔹(𝓕)|. By nonempty_orderIso_closure_iff this is the complete invariant of the Boolean closure up to order-isomorphism ([DS24]).

Equations

• Aristotelian.boolComplexity φ = (Aristotelian.partition ι W φ).card

Theorem 2: Aristotelian transfer

Each relation transfers along the Boolean isomorphism bitstringOrderIso ([DS18a], Theorem 2).

theorem Aristotelian.isContradictory_bitstring_iff {W : Type u_1} {ι : Type u_2} [Fintype W] [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (a b : ↥(BooleanSubalgebra.closure (Set.range φ))) : IsContradictory (bitstringOf φ ↑a) (bitstringOf φ ↑b) ↔ IsContradictory a b

theorem Aristotelian.isContrary_bitstring_iff {W : Type u_1} {ι : Type u_2} [Fintype W] [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (a b : ↥(BooleanSubalgebra.closure (Set.range φ))) : IsContrary (bitstringOf φ ↑a) (bitstringOf φ ↑b) ↔ IsContrary a b

theorem Aristotelian.isSubcontrary_bitstring_iff {W : Type u_1} {ι : Type u_2} [Fintype W] [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (a b : ↥(BooleanSubalgebra.closure (Set.range φ))) : IsSubcontrary (bitstringOf φ ↑a) (bitstringOf φ ↑b) ↔ IsSubcontrary a b

theorem Aristotelian.isSubaltern_bitstring_iff {W : Type u_1} {ι : Type u_2} [Fintype W] [Fintype ι] [DecidableEq ι] (φ : ι → W → Bool) (a b : ↥(BooleanSubalgebra.closure (Set.range φ))) : IsSubaltern (bitstringOf φ ↑a) (bitstringOf φ ↑b) ↔ IsSubaltern a b

Classification up to Boolean isomorphism

theorem Aristotelian.nonempty_orderIso_closure_iff {W : Type u_1} {ι : Type u_2} {ι' : Type u_3} {W' : Type u_4} [Fintype W] [Fintype ι] [DecidableEq ι] [Fintype W'] [Fintype ι'] [DecidableEq ι'] (φ : ι → W → Bool) (ψ : ι' → W' → Bool) : Nonempty (↥(BooleanSubalgebra.closure (Set.range φ)) ≃o ↥(BooleanSubalgebra.closure (Set.range ψ))) ↔ boolComplexity φ = boolComplexity ψ

Classification of fragments up to Boolean isomorphism ([DS24]): the Boolean closures of two fragments are order-isomorphic iff the fragments have equal Boolean complexity. The complete invariant is thus a single natural number — and fragments of different complexity are never Boolean-isomorphic (the obstruction behind the Keynes–Johnson 7 vs 6).