Compatibility Frames (Possibility Semantics for Orthologic)

@cite{holliday-mandelkern-2024}

Possibility semantics generalizes possible-worlds semantics by replacing maximal possible worlds with partial possibilities ordered by refinement. A possibility can verify a disjunction without verifying either disjunct.

Key differences from possible-world semantics

• Propositions are not arbitrary sets of possibilities but only regular sets — those satisfying a closure condition.
• Negation is orthocomplement: ¬A = {x | ∀y ◇ x, y ∉ A}.
• Disjunction is De Morgan from orthonegation, weaker than union.
• The resulting algebra of regular propositions is an ortholattice, not a Boolean algebra. Distributivity, pseudocomplementation, and orthomodularity all fail.

Architecture

This file (Frames.lean) is the substrate: compatibility frames, orthonegation, regularity, refinement, worlds, and the classical-collapse theorem under identity compatibility. The modal extension (□, ◇, T-axiom) lives in Modal.lean; the abstract OrthocomplementedLattice typeclass is upstream substrate at Linglib.Core.Order.Ortholattice; the OrthocomplementedLattice instance for the regular subsets of a frame lives in RegularProp.lean.

Paper-specific instantiations of the substrate (the five-possibility path frame Poss5, the Epistemic Scale, ortholattice failures of distributivity / orthomodularity / pseudocomplementation, and the two-world lifting) live in Phenomena/Modality/Studies/HollidayMandelkern2024.lean.

Conventions

• Carrier: propositions are Set S. Set-membership notation (x ∈ A, A ⊆ B, A ∩ B, Aᶜ) is preferred over functional-application notation. Set α is definitionally α → Prop.
• Decidability: CompatFrame does not bundle DecidableRel compat; use sites take [DecidableRel F.compat] (mathlib idiom — cf. SimpleGraph + [DecidableRel G.Adj]).
• Finiteness: [Fintype S] only appears on instances/theorems that need it (decidability of universally-quantified propositions); raw definitions stay Fintype-free.

structure Semantics.Modality.Orthologic.CompatFrame (S : Type u_1) : Type u_1

A compatibility frame: a set of possibilities with a reflexive, symmetric compatibility relation. Two possibilities are compatible if neither settles as true anything the other settles as false. @cite{holliday-mandelkern-2024} Definition 4.1.

Decidability of compat is not bundled — provide a DecidableRel instance separately for each concrete frame.

• 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

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

Orthocomplement negation. ¬A = {x | ∀y compatible with x, y ∉ A}. A possibility x makes ¬A true iff no compatible possibility makes A true — i.e., x's information settles ¬A. @cite{holliday-mandelkern-2024} Proposition 4.8, eq. (1).

Equations

• Semantics.Modality.Orthologic.orthoNeg F A = {x : S | ∀ (y : S), F.compat x y → y ∉ A}

@[simp]

theorem Semantics.Modality.Orthologic.mem_orthoNeg {S : Type u_1} (F : CompatFrame S) (A : Set S) (x : S) : x ∈ orthoNeg F A ↔ ∀ (y : S), F.compat x y → y ∉ A

@[implicit_reducible]

instance Semantics.Modality.Orthologic.instDecidableMemSetOrthoNegOfFintypeOfDecidableRelCompatOfDecidablePred {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (A : Set S) [DecidablePred fun (x : S) => x ∈ A] (x : S) : Decidable (x ∈ orthoNeg F A)

Equations

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

@[implicit_reducible]

instance Semantics.Modality.Orthologic.orthoNeg_apply_decidable {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (A : Set S) [DecidablePred A] (x : S) : Decidable (orthoNeg F A x)

Application-form alias of the membership-form Decidable instance, for goals that reduce orthoNeg F A x instead of x ∈ orthoNeg F A. Uses DecidablePred A (not DecidablePred (· ∈ A)) so it synthesises from the standard instance : DecidablePred A users define.

Equations

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

@[reducible, inline]

abbrev Semantics.Modality.Orthologic.conj {S : Type u_1} (A B : Set S) : Set S

Conjunction is intersection (transparent alias for Set.inter). Kept as a named operation for symmetry with disj in study-file theorems; conj A B = A ∩ B definitionally.

Equations

• Semantics.Modality.Orthologic.conj A B = A ∩ B

def Semantics.Modality.Orthologic.disj {S : Type u_1} (F : CompatFrame S) (A B : Set S) : Set S

Disjunction via De Morgan: A ∨ B = ¬(¬A ∩ ¬B). Strictly weaker than set-theoretic union: a possibility x makes A ∨ B true iff every y compatible with x is itself compatible with some z that makes A or B true (the unpacked form, paper eq. (2)). @cite{holliday-mandelkern-2024} Proposition 4.8, eq. (2).

Equations

• Semantics.Modality.Orthologic.disj F A B = Semantics.Modality.Orthologic.orthoNeg F (Semantics.Modality.Orthologic.orthoNeg F A ∩ Semantics.Modality.Orthologic.orthoNeg F B)

@[implicit_reducible]

instance Semantics.Modality.Orthologic.instDecidableMemSetDisjOfFintypeOfDecidableRelCompatOfDecidablePred {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (A B : Set S) [DecidablePred fun (x : S) => x ∈ A] [DecidablePred fun (x : S) => x ∈ B] (x : S) : Decidable (x ∈ disj F A B)

Equations

• Semantics.Modality.Orthologic.instDecidableMemSetDisjOfFintypeOfDecidableRelCompatOfDecidablePred F A B x = id inferInstance

@[implicit_reducible]

instance Semantics.Modality.Orthologic.disj_apply_decidable {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (A B : Set S) [DecidablePred A] [DecidablePred B] (x : S) : Decidable (disj F A B x)

Equations

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

@[implicit_reducible]

instance Semantics.Modality.Orthologic.conj_apply_decidable {S : Type u_1} (A B : Set S) [DecidablePred A] [DecidablePred B] (x : S) : Decidable (conj A B x)

Equations

• Semantics.Modality.Orthologic.conj_apply_decidable A B x = Semantics.Modality.Orthologic.conj_apply_decidable._aux_1 A B x

def Semantics.Modality.Orthologic.isRegular {S : Type u_1} (F : CompatFrame S) (A : Set S) : Prop

A set A is ◇-regular iff: whenever x ∉ A, there exists y compatible with x such that all z compatible with y are also not in A. Regularity = "indeterminacy implies compatibility with falsity." Only regular sets count as propositions. @cite{holliday-mandelkern-2024} Definition 4.3.

Equations

• Semantics.Modality.Orthologic.isRegular F A = ∀ (x : S), x ∈ A ∨ ∃ (y : S), F.compat x y ∧ ∀ (z : S), F.compat y z → z ∉ A

@[implicit_reducible]

instance Semantics.Modality.Orthologic.instDecidableIsRegularOfFintypeOfDecidableRelCompatOfDecidablePredMemSet {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (A : Set S) [DecidablePred fun (x : S) => x ∈ A] : Decidable (isRegular F A)

Equations

• Semantics.Modality.Orthologic.instDecidableIsRegularOfFintypeOfDecidableRelCompatOfDecidablePredMemSet F A = id inferInstance

@[implicit_reducible]

instance Semantics.Modality.Orthologic.isRegular_apply_decidable {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (A : Set S) [DecidablePred A] : Decidable (isRegular F A)

Application-form alias for isRegular so decide finds it from [DecidablePred A] instances directly.

Equations

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

def Semantics.Modality.Orthologic.refines {S : Type u_1} (F : CompatFrame S) (y x : S) : Prop

Refinement: y ⊑ x iff every possibility compatible with y is also compatible with x. A refinement carries at least as much information. @cite{holliday-mandelkern-2024} Lemma 4.4, condition 2.

Equations

• Semantics.Modality.Orthologic.refines F y x = ∀ (z : S), F.compat y z → F.compat x z

@[implicit_reducible]

instance Semantics.Modality.Orthologic.instDecidableRefinesOfFintypeOfDecidableRelCompat {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (y x : S) : Decidable (refines F y x)

Equations

• Semantics.Modality.Orthologic.instDecidableRefinesOfFintypeOfDecidableRelCompat F y x = id inferInstance

def Semantics.Modality.Orthologic.isWorld {S : Type u_1} (F : CompatFrame S) (w : S) : Prop

A world is a possibility that refines everything it is compatible with — the most informative kind of possibility. @cite{holliday-mandelkern-2024} Definition 4.6.

Equations

• Semantics.Modality.Orthologic.isWorld F w = ∀ (x : S), F.compat w x → Semantics.Modality.Orthologic.refines F w x

@[implicit_reducible]

instance Semantics.Modality.Orthologic.instDecidableIsWorldOfFintypeOfDecidableRelCompat {S : Type u_1} [Fintype S] (F : CompatFrame S) [DecidableRel F.compat] (w : S) : Decidable (isWorld F w)

Equations

• Semantics.Modality.Orthologic.instDecidableIsWorldOfFintypeOfDecidableRelCompat F w = id inferInstance

theorem Semantics.Modality.Orthologic.orthoNeg_classical {S : Type u_1} (F : CompatFrame S) (hClassical : ∀ (x y : S), F.compat x y → x = y) (A : Set S) (x : S) : x ∈ orthoNeg F A ↔ x ∉ A

When compatibility is identity (every possibility is a world), orthocomplement reduces to Boolean negation and the ortholattice is Boolean. This is the sense in which possible-world semantics is a special case of possibility semantics. @cite{holliday-mandelkern-2024} Remark 4.9 characterizes Boolean collapse as compatibility-implies-compossibility; the identity frame below is the simplest instance of that condition.

def Semantics.Modality.Orthologic.identityFrame {S : Type u_1} [DecidableEq S] : CompatFrame S

The identity compatibility frame: compat x y ↔ x = y.

Equations

• Semantics.Modality.Orthologic.identityFrame = { compat := fun (x y : S) => x = y, compat_refl := ⋯, compat_symm := ⋯ }

@[implicit_reducible]

instance Semantics.Modality.Orthologic.instDecidableRelCompatIdentityFrame {S : Type u_1} [DecidableEq S] : DecidableRel identityFrame.compat

Equations

• Semantics.Modality.Orthologic.instDecidableRelCompatIdentityFrame a b = id inferInstance

theorem Semantics.Modality.Orthologic.identityFrame_classical {S : Type u_1} [DecidableEq S] (A : Set S) (x : S) : x ∈ orthoNeg identityFrame A ↔ x ∉ A

In the identity frame, orthoNeg is pointwise negation.

def Semantics.Modality.Orthologic.regularClosure {S : Type u_1} (F : CompatFrame S) : ClosureOperator (Set S)

The c_◇ closure operator on Set S for a compatibility frame F, mapping A ↦ {x | ∀ y ◇ x, ∃ z ◇ y, z ∈ A}. The fixed points of regularClosure F are precisely the ◇-regular sets — making RegularProp F = (regularClosure F).fixedPoints a mathlib-typed closure-operator-based construction. @cite{holliday-mandelkern-2024} footnote 19 (page 858 of the published JPL version).

Equations

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

@[simp]

theorem Semantics.Modality.Orthologic.mem_regularClosure {S : Type u_1} (F : CompatFrame S) (A : Set S) (x : S) : x ∈ (regularClosure F) A ↔ ∀ (y : S), F.compat x y → ∃ (z : S), F.compat y z ∧ z ∈ A

theorem Semantics.Modality.Orthologic.regularClosure_isClosed_iff_isRegular {S : Type u_1} (F : CompatFrame S) (A : Set S) : (regularClosure F).IsClosed A ↔ isRegular F A