Modal compatibility frames

This file defines Holliday and Mandelkern's modal compatibility frames, the possibility semantics for must and might. A compatibility frame F carries an epistemic accessibility relation R; necessity is the Kripke operator □A = {x | R(x) ⊆ A}, which is SetRel.core R, and ◇A = ¬□¬A negates with the orthocomplement of F rather than the Boolean complement.

Three conditions on R make the regular propositions of F an epistemic ortholattice (Logic/Orthologic/Epistemic.lean). R-regularity is exactly the condition for □ to preserve regularity, which makes the regular propositions with □ a modal ortholattice; reflexivity makes it T; and over these, Knowability is exactly the condition for Wittgenstein's Law.

Main definitions

• Orthologic.diamond F R: ◇A = ¬□¬A on sets.
• Orthologic.IsRRegular F R, Orthologic.IsKnowable F R: R-regularity and Knowability.
• Orthologic.CompatFrame.necHom: □ as a map on F.Regular preserving meets and ⊤.

Main results

• Orthologic.isRRegular_iff_isRegular_core: R-regularity iff □ preserves regularity.
• Orthologic.isKnowable_iff: Knowability iff □ reflects contradiction on regular sets.
• Orthologic.disjoint_orthoNeg_diamond: ¬A and ◇A are disjoint.
• Orthologic.CompatFrame.isKnowable_iff_wittgensteinLaw: over a reflexive R-regular relation, Knowability iff the regular propositions satisfy Wittgenstein's Law.

Implementation notes

The paper's frame classes are conjunctions of conditions on a bare relation, stated as Prop classes like ModalLogic.IsSerial: a modal compatibility frame is R-regular, a T frame is also reflexive (R.IsRefl), and an epistemic frame also satisfies Knowability. Each theorem assumes only the conditions it uses.

References

• [HM24]

def Orthologic.diamond {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) (A : Set S) : Set S

The possibility ◇A = ¬□¬A negates with the orthocomplement, so x makes ◇A true iff every possibility compatible with x accesses one compatible with an A-possibility ([HM24] eq. (4)).

Equations

• Orthologic.diamond F R A = Orthologic.orthoNeg F (R.core (Orthologic.orthoNeg F A))

@[instance_reducible]

instance Orthologic.instDecidablePredMemSetDiamondOfFintypeOfDecidableRelCompatOfDecidableProdSetRelMk {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) [Fintype S] [DecidableRel F.compat] [(x y : S) → Decidable ((x, y) ∈ R)] (A : Set S) [DecidablePred fun (x : S) => x ∈ A] : DecidablePred fun (x : S) => x ∈ diamond F R A

Equations

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

class Orthologic.IsRRegular {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) : Prop

A relation is R-regular when a possibility accessing one compatible with y is compatible with a possibility according to which y might obtain ([HM24] Definition 4.20).

• rRegular (x y' y : S) : (x, y') ∈ R → F.compat y' y → ∃ (x' : S), F.compat x x' ∧ ∀ (x'' : S), F.compat x' x'' → ∃ (y'' : S), (x'', y'') ∈ R ∧ F.compat y'' y

  The condition is stated in the ◇-free form of [HM24] Lemma 4.21.

class Orthologic.IsKnowable {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) : Prop

A relation satisfies Knowability when every possibility x has one at which everything settled true by x is known, since all it accesses refine x ([HM24] Definition 4.26).

• knowable (x : S) : ∃ (y : S), ∀ (z : S), (y, z) ∈ R → refines F z x

theorem Orthologic.isRegular_core {S : Type u_1} {F : CompatFrame S} (R : SetRel S S) [IsRRegular F R] {A : Set S} (hA : IsRegular F A) : IsRegular F (R.core A)

Over an R-regular frame, □ of a regular set is regular ([HM24] Proposition 4.22).

theorem Orthologic.isRRegular_iff_isRegular_core {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) : IsRRegular F R ↔ ∀ (A : Set S), IsRegular F A → IsRegular F (R.core A)

R-regularity is exactly the condition for □ to preserve regularity. The converse of Proposition 4.22, not stated in [HM24], follows by testing R-regularity on the regular set ¬{y}.

theorem Orthologic.isKnowable_iff {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) : IsKnowable F R ↔ ∀ (A : Set S), IsRegular F A → R.core A = ∅ → A = ∅

Knowability is exactly the condition for □ to reflect contradiction on regular sets: the frame counterpart of the principle of [HM24] Lemma 3.25, to which the paper takes Knowability to correspond. The converse, not stated there, follows by testing Knowability on the regular set of refinements of x.

theorem Orthologic.disjoint_orthoNeg_diamond {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) [R.IsRefl] [IsKnowable F R] (A : Set S) : Disjoint (orthoNeg F A) (diamond F R A)

Over a reflexive relation with Knowability, ¬A and ◇A are disjoint for every set A, regular or not, and without R-regularity ([HM24] Proposition 4.27).

The modal ortholattice of regular propositions

def Orthologic.CompatFrame.necHom {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) [IsRRegular F R] : InfTopHom F.Regular F.Regular

F.necHom R is □ on the regular propositions of an R-regular frame, which preserves meets and ⊤ and so makes them the modal ortholattice O(F) of [HM24] Proposition 4.23.

Equations

• F.necHom R = { toFun := fun (A : F.Regular) => F.regOf (R.core ↑A) ⋯, map_inf' := ⋯, map_top' := ⋯ }

@[simp]

theorem Orthologic.CompatFrame.coe_necHom {S : Type u_1} {F : CompatFrame S} (R : SetRel S S) [IsRRegular F R] (A : F.Regular) : ↑((F.necHom R) A) = R.core ↑A

theorem Orthologic.CompatFrame.coe_diamondHom_necHom {S : Type u_1} {F : CompatFrame S} (R : SetRel S S) [IsRRegular F R] (A : F.Regular) : ↑((diamondHom (F.necHom R)) A) = diamond F R ↑A

◇ of the modal ortholattice is diamond.

theorem Orthologic.CompatFrame.necHom_le {S : Type u_1} {F : CompatFrame S} (R : SetRel S S) [IsRRegular F R] [R.IsRefl] (A : F.Regular) : (F.necHom R) A ≤ A

Over a reflexive relation □A ≤ A, so the modal ortholattice is T ([HM24] Proposition 4.25; its footnote 22 weakens reflexivity to every possibility accessing a refinement of itself).

theorem Orthologic.CompatFrame.necHom_le_necHom_necHom {S : Type u_1} {F : CompatFrame S} (R : SetRel S S) [IsRRegular F R] [R.IsTrans] (A : F.Regular) : (F.necHom R) A ≤ (F.necHom R) ((F.necHom R) A)

Over a transitive relation □A ≤ □□A, which is the 4 principle.

theorem Orthologic.CompatFrame.isKnowable_iff_wittgensteinLaw {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) [IsRRegular F R] [R.IsRefl] : IsKnowable F R ↔ WittgensteinLaw (F.necHom R)

Over a reflexive R-regular relation, Knowability is exactly Wittgenstein's Law for the modal ortholattice. The forward direction is [HM24] Proposition 4.27.

theorem Orthologic.CompatFrame.wittgensteinLaw_necHom {S : Type u_1} (F : CompatFrame S) (R : SetRel S S) [IsRRegular F R] [R.IsRefl] [IsKnowable F R] : WittgensteinLaw (F.necHom R)

Over a reflexive relation with Knowability the modal ortholattice satisfies Wittgenstein's Law, so it is an epistemic ortholattice ([HM24] Proposition 4.27).