Compatibility Frames (Possibility Semantics for Orthologic)

[HM24]

Possibility semantics generalizes possible-worlds semantics by replacing maximal worlds with partial possibilities ordered by refinement: a possibility can verify a disjunction without verifying either disjunct. Propositions are the regular sets, negation is orthocomplement, and the resulting algebra of regular propositions is an ortholattice — not a Boolean algebra (distributivity, pseudocomplementation, and orthomodularity all fail).

Main definitions

• CompatFrame — a set of possibilities with a reflexive, symmetric compatibility relation.
• orthoNeg, conj, disj — orthocomplement negation and the De Morgan connectives.
• IsRegular, refines, IsWorld — regularity, the refinement order, and worlds (maximally informative possibilities).
• regularClosure — the c_◇ closure operator whose fixed points are the regular sets.
• orthoNeg_classical, identityFrame — the classical collapse under identity compatibility.

Implementation notes

This file is substrate. The modal extension (□, ◇, T-axiom) lives in Modal.lean; the bundled ortholattice of regular propositions in RegularProp.lean; the abstract OrthocomplementedLattice class in Core.Order.Ortholattice; and the paper's concrete instantiations (the Poss5 path frame, the Epistemic Scale, the ortholattice failures) in Studies.HollidayMandelkern2024.

Propositions are Set S, with set-membership notation preferred. Decidability of compat is not bundled — use sites take [DecidableRel F.compat] (mathlib's SimpleGraph + [DecidableRel G.Adj] idiom), and [Fintype S] appears only where decidability of universally quantified propositions needs it.

Compatibility frames

structure Orthologic.CompatFrame (S : Type u_2) : Type u_2

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. [HM24] Definition 4.1.

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

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

theorem Orthologic.CompatFrame.refl {S : Type u_1} (F : CompatFrame S) (x : S) : F.compat x x

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

theorem Orthologic.CompatFrame.compat.symm {S : Type u_1} {F : CompatFrame S} {x y : S} (h : F.compat x y) : F.compat y x

Compatibility is symmetric: h.symm : F.compat y x for h : F.compat x y (mirrors SimpleGraph.Adj.symm).

Orthocomplement negation and connectives

def 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. [HM24] Proposition 4.8, eq. (1).

Equations

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

@[simp]

theorem 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 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

• Orthologic.instDecidableMemSetOrthoNegOfFintypeOfDecidableRelCompatOfDecidablePred F A x = id inferInstance

@[implicit_reducible]

instance 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

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

@[reducible, inline]

abbrev 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

• Orthologic.conj A B = A ∩ B

def 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)). [HM24] Proposition 4.8, eq. (2).

Equations

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

@[implicit_reducible]

instance 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

• Orthologic.instDecidableMemSetDisjOfFintypeOfDecidableRelCompatOfDecidablePred F A B x = id inferInstance

@[implicit_reducible]

instance 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

• Orthologic.disj_apply_decidable F A B x = id (have hA := Orthologic.disj_apply_decidable._aux_1 A; have hB := Orthologic.disj_apply_decidable._aux_3 B; inferInstance)

@[implicit_reducible]

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

Equations

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

Regularity

def 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. [HM24] Definition 4.3.

Equations

• 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 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

• Orthologic.instDecidableIsRegularOfFintypeOfDecidableRelCompatOfDecidablePredMemSet F A = id inferInstance

@[implicit_reducible]

instance 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

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

Refinement and worlds

def 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. [HM24] Lemma 4.4, condition 2.

Equations

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

@[implicit_reducible]

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

Equations

• Orthologic.instDecidableRefinesOfFintypeOfDecidableRelCompat F y x = id inferInstance

def 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. [HM24] Definition 4.6.

Equations

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

@[implicit_reducible]

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

Equations

• Orthologic.instDecidableIsWorldOfFintypeOfDecidableRelCompat F w = id inferInstance

Classical collapse

theorem 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. [HM24] Remark 4.9 characterizes Boolean collapse as compatibility-implies-compossibility; the identity frame below is the simplest instance of that condition.

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

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

Equations

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

@[implicit_reducible]

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

Equations

• Orthologic.instDecidableRelCompatIdentityFrame a b = id inferInstance

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

The c_◇ closure operator

def 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}. Its fixed points are precisely the ◇-regular sets (IsRegular F), i.e. the underlying sets of CompatFrame.Regular. [HM24] footnote 19 (page 858 of the published JPL version).

Equations

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

@[simp]

theorem 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 Orthologic.regularClosure_isClosed_iff_isRegular {S : Type u_1} (F : CompatFrame S) (A : Set S) : (regularClosure F).IsClosed A ↔ IsRegular F A