Modal Compatibility Frames

@cite{holliday-mandelkern-2024}

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 Phenomena/Modality/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 Semantics.Modality.Orthologic.ModalCompatFrame (S : Type u_1) extends Semantics.Modality.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 (x : S) : self.compat x x
• compat_symm (x y : S) : self.compat x y ↔ self.compat y x
• access : S → S → Prop
• access_refl (x : S) : self.access x x

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

Box operator: □A = {x | R(x) ⊆ A}. @cite{holliday-mandelkern-2024} eq. (3).

Equations

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

@[simp]

theorem Semantics.Modality.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 Semantics.Modality.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

• Semantics.Modality.Orthologic.instDecidableMemSetBoxOfFintypeOfDecidableRelAccessOfDecidablePred F A x = id inferInstance

@[implicit_reducible]

instance Semantics.Modality.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

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

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

Diamond operator: ◇A = ¬□¬A (via orthocomplement, NOT Boolean dual). @cite{holliday-mandelkern-2024} eq. (4).

Equations

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

@[implicit_reducible]

instance Semantics.Modality.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

• Semantics.Modality.Orthologic.instDecidableMemSetDiamondOfFintypeOfCompatOfDecidableRelAccessOfDecidablePred F A x = id inferInstance

@[implicit_reducible]

instance Semantics.Modality.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 Semantics.Modality.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. @cite{holliday-mandelkern-2024} Proposition 4.25.

def Semantics.Modality.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." @cite{holliday-mandelkern-2024} Definition 4.20 / Definition 4.26 (R-regularity clause), page 866 of the published JPL version.

Equations

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

@[implicit_reducible]

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

Equations

• Semantics.Modality.Orthologic.instDecidableIsRRegularOfFintypeOfCompatOfDecidableRelAccess F = id inferInstance

def Semantics.Modality.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." @cite{holliday-mandelkern-2024} Definition 4.26 (Knowability clause), page 866.

Equations

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

@[implicit_reducible]

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

Equations

• Semantics.Modality.Orthologic.instDecidableIsKnowableOfFintypeOfCompatOfDecidableRelAccess F = id inferInstance

structure Semantics.Modality.Orthologic.EpistemicCompatFrame (S : Type u_1) extends Semantics.Modality.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. @cite{holliday-mandelkern-2024} Definition 4.26, page 866.

• compat : S → S → Prop
• compat_refl (x : S) : self.compat x x
• compat_symm (x y : S) : self.compat x y ↔ self.compat y x
• access : S → S → Prop
• access_refl (x : S) : self.access x x
• rRegular : IsRRegular self.toModalCompatFrame

  R-regularity per Definition 4.20 / 4.26.

• knowable : IsKnowable self.toModalCompatFrame

  Knowability per Definition 4.26.

theorem Semantics.Modality.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. @cite{holliday-mandelkern-2024} Proposition 4.27, page 867.

theorem Semantics.Modality.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.