Partitions induced by logical fragments (skeleton)

Per @cite{demey-smessaert-2018} §3.1, Definitions 5–6.

Given a logical system S and a finite fragment ℱ = {φ_1, ..., φ_m}, the partition Π_S(ℱ) is the set of anchor formulas — maximal-information conjunctions of literals over ℱ that are S-consistent:

Π_S(ℱ) := {α | α ≡_S ±φ_1 ∧ ... ∧ ±φ_m, α is S-consistent}

The anchor formulas are mutually exclusive and jointly exhaustive (Lemma 3), forming a partition of the model class. Their cardinality n = |Π_S(ℱ)| determines the bitstring length: |𝔹(ℱ)| = 2^n.

inductive Core.Opposition.Literal (W : Type u_2) : Type u_2

A literal over a Boolean predicate: either the predicate itself or its negation. Used to build anchor formulas.

• pos {W : Type u_2} (φ : W → Bool) : Literal W
• neg {W : Type u_2} (φ : W → Bool) : Literal W

def Core.Opposition.Literal.eval {W : Type u_1} : Literal W → W → Bool

Interpret a literal as a Boolean predicate.

Equations

• (Core.Opposition.Literal.pos φ).eval x✝ = φ x✝
• (Core.Opposition.Literal.neg φ).eval x✝ = !φ x✝

@[reducible, inline]

abbrev Core.Opposition.PolarityAssignment (ι : Type) (W : Type u_2) : Type u_2

A polarity assignment selects one literal per fragment formula.

Equations

• Core.Opposition.PolarityAssignment ι W = (ι → (W → Bool) → Core.Opposition.Literal W)

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

The anchor formula for polarity assignment σ over fragment φ: the conjunction ±φ_1 ∧ ... ∧ ±φ_m with signs given by σ.

Equations

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

def Core.Opposition.anchorConsistent {W : Type u_1} {ι : Type} [Fintype ι] (φ : ι → W → Bool) (σ : ι → Bool) : Prop

An anchor formula is consistent if it is satisfiable in some world.

Equations

• Core.Opposition.anchorConsistent φ σ = ∃ (w : W), Core.Opposition.anchor φ σ w = true

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

The partition of a fragment: all consistent polarity assignments.

Equations

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

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

Two distinct anchor formulas are jointly inconsistent.

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

Every world satisfies exactly one anchor formula (joint exhaustion).

def Core.Opposition.partitionMeet {ι₁ ι₂ : Type} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {W : Type u_2} [Fintype W] (φ₁ : ι₁ → W → Bool) (φ₂ : ι₂ → W → Bool) : Finset ((ι₁ → Bool) × (ι₂ → Bool))

The meet of two partitions: anchor formulas of the union fragment. Per Lemma 4, Π(ℱ₁ ∪ ℱ₂) = Π(ℱ₁) ∧ Π(ℱ₂).

Equations

• Core.Opposition.partitionMeet φ₁ φ₂ = {p ∈ Finset.univ.product Finset.univ | decide (∃ (w : W), Core.Opposition.anchor φ₁ p.1 w = true ∧ Core.Opposition.anchor φ₂ p.2 w = true) = true}