Modal Compatibility Frames

[HM24]

Modal extension of compatibility frames. Adds an accessibility relation R and the box/diamond operators whose ortholattice instance validates Wittgenstein's Law (¬A ∩ ◇A = ∅) for epistemic compatibility frames.

This file is the substrate — only general substrate-level definitions and theorems live here. Concrete paper instantiations (the Epistemic Scale over Poss5, Wittgenstein-sentence verifications, free-choice / orthomodularity / pseudocomplementation failures, level-wise classicality theorems, lifting from W={0,1}) live in Studies/HollidayMandelkern2024.lean.

What's here

• ModalCompatFrame S: a compatibility frame plus a reflexive accessibility relation R. The paper's full Definition 4.20 also requires R-regularity; Definition 4.26 adds Knowability (epistemic compatibility frame). The current ModalCompatFrame records only the reflexivity condition.
• box, diamond: modal operators on Set S.
• T_axiom_general: factivity of box from accessibility reflexivity.
• IsRRegular, IsKnowable: per-instance conditions completing Definitions 4.20 / 4.26.
• EpistemicCompatFrame: bundles ModalCompatFrame with IsRRegular and IsKnowable (Definition 4.26).
• wittgensteinLaw: Proposition 4.27 — the headline structural theorem. In any modal compatibility frame satisfying Knowability, ¬A ∩ ◇A = ∅ for every set A. The algebraic content of "p and might-not-p is contradictory."

Decidability of access is not bundled — provide a DecidableRel instance separately (mirrors the CompatFrame convention).

structure Orthologic.ModalCompatFrame (S : Type u_1) extends Orthologic.CompatFrame S : Type u_1

A modal compatibility frame: a compatibility frame equipped with an accessibility relation R satisfying reflexivity (Definition 4.24). The paper's full Definition 4.20 also requires R-regularity; the epistemic compatibility frame (Definition 4.26) adds Knowability. Per-instance frames may witness all three conditions.

• compat : S → S → Prop
• compat_refl : Std.Refl self.compat
• compat_symm : Std.Symm self.compat
• access : S → S → Prop
• access_refl : Std.Refl self.access

theorem Orthologic.ModalCompatFrame.accessRefl {S : Type u_1} (F : ModalCompatFrame S) (x : S) : F.access x x

Accessibility is reflexive (accessor for the bundled Std.Refl).

def Orthologic.box {S : Type u_1} (F : ModalCompatFrame S) (A : Set S) : Set S

Box operator: □A = {x | R(x) ⊆ A}. [HM24] eq. (3).

Equations

• Orthologic.box F A = {x : S | ∀ (y : S), F.access x y → y ∈ A}

@[simp]

theorem Orthologic.mem_box {S : Type u_1} (F : ModalCompatFrame S) (A : Set S) (x : S) : x ∈ box F A ↔ ∀ (y : S), F.access x y → y ∈ A

@[implicit_reducible]

instance Orthologic.instDecidableMemSetBoxOfFintypeOfDecidableRelAccessOfDecidablePred {S : Type u_1} [Fintype S] (F : ModalCompatFrame S) [DecidableRel F.access] (A : Set S) [DecidablePred fun (x : S) => x ∈ A] (x : S) : Decidable (x ∈ box F A)

Equations

• Orthologic.instDecidableMemSetBoxOfFintypeOfDecidableRelAccessOfDecidablePred F A x = id inferInstance

@[implicit_reducible]

instance Orthologic.box_apply_decidable {S : Type u_1} [Fintype S] (F : ModalCompatFrame S) [DecidableRel F.access] (A : Set S) [DecidablePred A] (x : S) : Decidable (box F A x)

Equations

• Orthologic.box_apply_decidable F A x = id (have this := Orthologic.box_apply_decidable._aux_1 A; inferInstance)

def Orthologic.diamond {S : Type u_1} (F : ModalCompatFrame S) (A : Set S) : Set S

Diamond operator: ◇A = ¬□¬A (via orthocomplement, NOT Boolean dual). [HM24] eq. (4).

Equations

• Orthologic.diamond F A = Orthologic.orthoNeg F.toCompatFrame (Orthologic.box F (Orthologic.orthoNeg F.toCompatFrame A))

@[implicit_reducible]

instance Orthologic.instDecidableMemSetDiamondOfFintypeOfCompatOfDecidableRelAccessOfDecidablePred {S : Type u_1} [Fintype S] (F : ModalCompatFrame S) [DecidableRel F.compat] [DecidableRel F.access] (A : Set S) [DecidablePred fun (x : S) => x ∈ A] (x : S) : Decidable (x ∈ diamond F A)

Equations

• Orthologic.instDecidableMemSetDiamondOfFintypeOfCompatOfDecidableRelAccessOfDecidablePred F A x = id inferInstance

@[implicit_reducible]

instance Orthologic.diamond_apply_decidable {S : Type u_1} [Fintype S] (F : ModalCompatFrame S) [DecidableRel F.compat] [DecidableRel F.access] (A : Set S) [DecidablePred A] (x : S) : Decidable (diamond F A x)

Equations

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

theorem Orthologic.T_axiom_general {S : Type u_1} (F : ModalCompatFrame S) (A : Set S) (x : S) (h : x ∈ box F A) : x ∈ A

The T axiom for modal compatibility frames: reflexive accessibility means every world accesses itself, so □A at x forces A at x. [HM24] Proposition 4.25.

def Orthologic.IsRRegular {S : Type u_1} (F : ModalCompatFrame S) : Prop

R-regularity: if x R y' and y' ◇ y, then there is some x' with x ◇ x' and some y'' ◇ x' refining y. Loose reading: "if x can epistemically access a possibility compatible with y, then x is compatible with a possibility according to which y might obtain." [HM24] Definition 4.20 / Definition 4.26 (R-regularity clause), page 866 of the published JPL version.

Equations

• Orthologic.IsRRegular F = ∀ (x y' y : S), F.access x y' → F.compat y' y → ∃ (x' : S), F.compat x x' ∧ ∃ (y'' : S), F.compat x' y'' ∧ Orthologic.refines F.toCompatFrame y'' y

@[implicit_reducible]

instance Orthologic.instDecidableIsRRegularOfFintypeOfCompatOfDecidableRelAccess {S : Type u_1} [Fintype S] (F : ModalCompatFrame S) [DecidableRel F.compat] [DecidableRel F.access] : Decidable (IsRRegular F)

Equations

• Orthologic.instDecidableIsRRegularOfFintypeOfCompatOfDecidableRelAccess F = id inferInstance

def Orthologic.IsKnowable {S : Type u_1} (F : ModalCompatFrame S) : Prop

Knowability: for every possibility x there is some y such that every R-successor of y refines x. Loose reading: "there is a possibility where everything settled true by x is known." [HM24] Definition 4.26 (Knowability clause), page 866.

Equations

• Orthologic.IsKnowable F = ∀ (x : S), ∃ (y : S), ∀ (z : S), F.access y z → Orthologic.refines F.toCompatFrame z x

@[implicit_reducible]

instance Orthologic.instDecidableIsKnowableOfFintypeOfCompatOfDecidableRelAccess {S : Type u_1} [Fintype S] (F : ModalCompatFrame S) [DecidableRel F.compat] [DecidableRel F.access] : Decidable (IsKnowable F)

Equations

• Orthologic.instDecidableIsKnowableOfFintypeOfCompatOfDecidableRelAccess F = id inferInstance

structure Orthologic.EpistemicCompatFrame (S : Type u_1) extends Orthologic.ModalCompatFrame S : Type u_1

An epistemic compatibility frame: a modal compatibility frame satisfying R-regularity, T (= reflexivity, already in ModalCompatFrame), and Knowability. This is the substrate over which Wittgenstein's Law (wittgensteinLaw, Proposition 4.27) holds. [HM24] Definition 4.26, page 866.

• compat : S → S → Prop
• compat_refl : Std.Refl self.compat
• compat_symm : Std.Symm self.compat
• access : S → S → Prop
• access_refl : Std.Refl self.access
• rRegular : IsRRegular self.toModalCompatFrame

  R-regularity per Definition 4.20 / 4.26.

• knowable : IsKnowable self.toModalCompatFrame

  Knowability per Definition 4.26.

theorem Orthologic.wittgensteinLaw {S : Type u_1} (F : ModalCompatFrame S) (hK : IsKnowable F) (A : Set S) : orthoNeg F.toCompatFrame A ∩ diamond F A = ∅

Wittgenstein's Law (Proposition 4.27): in any modal compatibility frame satisfying Knowability, the orthonegation ¬A and the modal ◇A are jointly null at every possibility — for every set A, regular or not. The proof needs only Knowability and reflexivity of accessibility (which is bundled in ModalCompatFrame); R-regularity from the full epistemic-frame definition is not used here.

Linguistic punchline: "A is settled false" and "A might be true" cannot both hold at any possibility — the algebraic content of the claim that "p and might-not-p" is contradictory. [HM24] Proposition 4.27, page 867.

theorem Orthologic.EpistemicCompatFrame.wittgensteinLaw {S : Type u_1} (F : EpistemicCompatFrame S) (A : Set S) : orthoNeg F.toCompatFrame A ∩ diamond F.toModalCompatFrame A = ∅

Wittgenstein's Law on epistemic compatibility frames — the canonical paper-defined surface. Direct corollary of the substrate wittgensteinLaw.