Partitions induced by logical fragments

Per [DS18a] §3.1. The partition of a finite fragment φ : ι → W → Bool is its set of consistent anchor formulas — complete conjunctions of literals ±φ i. The anchors are mutually exclusive and jointly exhaustive (Lemma 3), and their count is the bitstring length.

Main declarations

• anchor — the anchor formula of a polarity assignment (Definition 5).
• partition — the consistent anchors of a fragment.
• anchor_mutually_exclusive / anchor_jointly_exhaustive — Lemma 3.

Anchor formulas (Definition 5)

def Aristotelian.anchor {W : Type u_1} {ι : Type u_2} [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) (w : W) : Bool

The anchor formula for polarity assignment σ: the conjunction ±φ_1 ∧ ⋯ ∧ ±φ_m.

Equations

• Aristotelian.anchor φ σ w = decide (∀ (i : ι), if σ i = true then φ i w = true else φ i w = false)

def Aristotelian.partition (ι : Type u_2) [Fintype ι] [DecidableEq ι] (W : Type u_3) [Fintype W] (φ : ι → W → Bool) : Finset (ι → Bool)

The partition of a fragment: all consistent polarity assignments.

Equations

• Aristotelian.partition ι W φ = {σ : ι → Bool | ∃ (w : W), Aristotelian.anchor φ σ w = true}

Lemma 3 — mutual exclusivity and joint exhaustion

theorem Aristotelian.anchor_mutually_exclusive {W : Type u_1} {ι : Type u_2} [Fintype ι] (φ : ι → W → Bool) (σ τ : ι → Bool) (h : σ ≠ τ) (w : W) : ¬(anchor φ σ w = true ∧ anchor φ τ w = true)

Two distinct anchor formulas are jointly inconsistent.

theorem Aristotelian.anchor_jointly_exhaustive {W : Type u_1} {ι : Type u_2} [Fintype ι] (φ : ι → W → Bool) (w : W) : ∃ (σ : ι → Bool), anchor φ σ w = true

Every world satisfies some anchor formula.