Compatibility frames

This file defines compatibility frames, the possibility semantics for orthologic on which Holliday and Mandelkern build their account of epistemic modals, and the ortholattice of regular propositions of a frame. A compatibility frame is a set of partial possibilities with a reflexive, symmetric compatibility relation, and a possibility can settle a disjunction without settling either disjunct. The propositions are the regular sets, negation is the orthocomplement orthoNeg, and the regular sets form an ortholattice that need not be Boolean.

Main definitions

• CompatFrame: a set of possibilities with a reflexive, symmetric compatibility relation.
• orthoNeg, disj: orthocomplement negation and De Morgan disjunction.
• IsRegular, refines, IsWorld: regularity, refinement, and worlds.
• regularClosure: the closure operator whose fixed points are the regular sets.
• CompatFrame.Regular: the ortholattice of regular propositions.
• identityFrame: the frame whose compatibility is identity.

Main results

• IsRegular.mem_of_refines: regular sets are closed under refinement.
• refines_iff_mem_orthoNeg_orthoNeg: the refinements of x form the regular set ¬¬{x}.
• isRegular_iff_isExtent: the regular sets are the concept extents of orthogonality.
• orthoNeg_classical: negation is Boolean when compatibility is identity.

Implementation notes

A frame also carries its orthogonality relation ortho, the complement of compatibility, which defaults to ¬ compat and is stored as data in the way Preorder stores <. The regular propositions are the concepts of ortho (Core/Order/Concept.lean), and a frame built from an orthogonality relation, such as the canonical frame of an ortholattice, keeps that relation definitionally. Decidability of compat is not bundled: use sites take [DecidableRel F.compat], as for SimpleGraph.Adj. The paper's frames are nonempty; no result here needs it, so the structure does not require it.

References

• [HM24]

Compatibility frames

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

A compatibility frame is a set of possibilities with a reflexive, symmetric compatibility relation; two possibilities are compatible when neither settles as true anything the other settles as false ([HM24] Definition 4.1).

• compat : S → S → Prop

  Compatibility of possibilities.

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

  Orthogonality, the complement of compatibility.

• ortho_iff (x y : S) : self.ortho x y ↔ ¬self.compat x y

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

Compatibility is reflexive.

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, as SimpleGraph.Adj.symm is for adjacency.

instance Orthologic.CompatFrame.instSymmOrtho {S : Type u_1} (F : CompatFrame S) : Std.Symm F.ortho

instance Orthologic.CompatFrame.instIrreflOrtho {S : Type u_1} (F : CompatFrame S) : Std.Irrefl F.ortho

@[instance_reducible]

instance Orthologic.CompatFrame.instDecidableRelOrthoOfCompat {S : Type u_1} (F : CompatFrame S) [DecidableRel F.compat] : DecidableRel F.ortho

Equations

• F.instDecidableRelOrthoOfCompat x y = decidable_of_iff (¬F.compat x y) ⋯

Orthocomplement negation and connectives

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

The orthocomplement ¬A holds at the possibilities compatible with no A-possibility, those whose 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

@[instance_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

@[instance_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)

This instance decides orthoNeg F A x in application form from [DecidablePred A], for goals that reduce membership.

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, named beside disj.

Equations

• Orthologic.conj A B = A ∩ B

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

The De Morgan disjunction A ∨ B = ¬(¬A ∩ ¬B) holds at x iff every possibility compatible with x is compatible with one making A or B true, so it is weaker than union ([HM24] Proposition 4.8, eq. (2)).

Equations

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

@[instance_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

@[instance_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)

@[instance_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 = { decide := decide (A x) && decide (B x), reflects_decide := ⋯ }

Regularity

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

A set A is regular when every possibility outside A is compatible with one all of whose compatible possibilities lie outside A; 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

@[instance_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

@[instance_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)

This instance decides IsRegular F A from [DecidablePred A].

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

A possibility y refines x, written y ⊑ x, when every possibility compatible with y is compatible with x, so that y 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

@[instance_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

theorem Orthologic.IsRegular.mem_of_refines {S : Type u_1} {F : CompatFrame S} {A : Set S} (hA : IsRegular F A) {z x : S} (h : refines F z x) (hx : x ∈ A) : z ∈ A

Regular sets are closed under refinement, since a refinement settles every proposition its coarsening settles. This is the direction of [HM24] Lemma 4.4 from compatibility to regular sets.

theorem Orthologic.refines_iff_mem_orthoNeg_orthoNeg {S : Type u_1} (F : CompatFrame S) {z x : S} : refines F z x ↔ z ∈ orthoNeg F (orthoNeg F {x})

The refinements of x are the possibilities settling ¬¬{x}, so they form a regular set ([HM24] Lemma 4.5).

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

@[instance_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

In the identity frame each possibility is compatible only with itself.

Equations

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

@[instance_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 closure operator c_◇ sends A to the possibilities all of whose compatible possibilities are compatible with an A-possibility; its fixed points are the regular sets ([HM24] footnote 19).

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

Closure properties of regular sets

theorem Orthologic.orthoNeg_isRegular {S : Type u_1} (F : CompatFrame S) (A : Set S) : IsRegular F (orthoNeg F A)

The orthocomplement of any set is regular, whether or not the set is.

theorem Orthologic.inter_isRegular {S : Type u_1} {F : CompatFrame S} {A B : Set S} (hA : IsRegular F A) (hB : IsRegular F B) : IsRegular F (A ∩ B)

Regular sets are closed under intersection.

theorem Orthologic.disj_isRegular {S : Type u_1} (F : CompatFrame S) (A B : Set S) : IsRegular F (disj F A B)

A disjunction is regular, being an orthocomplement.

theorem Orthologic.empty_isRegular {S : Type u_1} (F : CompatFrame S) : IsRegular F ∅

The empty set is regular.

theorem Orthologic.univ_isRegular {S : Type u_1} (F : CompatFrame S) : IsRegular F Set.univ

The full set is regular.

theorem Orthologic.orthoNeg_orthoNeg_of_isRegular {S : Type u_1} (F : CompatFrame S) {A : Set S} (hA : IsRegular F A) : orthoNeg F (orthoNeg F A) = A

Orthocomplementation is involutive on regular sets, ¬¬A = A ([HM24] Proposition 4.8).

Regular sets as concept extents

theorem Orthologic.orthoNeg_eq_upperPolar {S : Type u_1} (F : CompatFrame S) (A : Set S) : orthoNeg F A = upperPolar F.ortho A

orthoNeg is the upperPolar of the orthogonality relation.

theorem Orthologic.isRegular_iff_orthoNeg_orthoNeg {S : Type u_1} (F : CompatFrame S) (A : Set S) : IsRegular F A ↔ orthoNeg F (orthoNeg F A) = A

IsRegular is the double-orthonegation fixed-point condition.

theorem Orthologic.isRegular_iff_isExtent {S : Type u_1} (F : CompatFrame S) (A : Set S) : IsRegular F A ↔ Order.IsExtent F.ortho A

The regular sets of F are exactly the concept extents of its orthogonality relation. [HM24]'s Proposition 4.8 is then mathlib's upperPolar_lowerPolar_upperPolar.

The ortholattice of regular propositions

@[reducible, inline]

abbrev Orthologic.CompatFrame.Regular {S : Type u_1} (F : CompatFrame S) : Type u_1

The regular propositions of F form the ortholattice of concepts of its orthogonality relation.

Equations

• F.Regular = Concept S S F.ortho

def Orthologic.CompatFrame.regOf {S : Type u_1} (F : CompatFrame S) (A : Set S) (h : IsRegular F A) : F.Regular

F.regOf A h is the regular proposition with underlying set A.

Equations

• F.regOf A h = Concept.ofIsExtent F.ortho A ⋯

theorem Orthologic.CompatFrame.Regular.isRegular {S : Type u_1} {F : CompatFrame S} (A : F.Regular) : IsRegular F ↑A

The underlying set of a regular proposition is regular.

@[simp]

theorem Orthologic.CompatFrame.coe_regOf {S : Type u_1} {F : CompatFrame S} (A : Set S) (h : IsRegular F A) : ↑(F.regOf A h) = A

@[simp]

theorem Orthologic.CompatFrame.mem_regOf {S : Type u_1} {F : CompatFrame S} (A : Set S) (h : IsRegular F A) (x : S) : x ∈ F.regOf A h ↔ x ∈ A

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_inf {S : Type u_1} {F : CompatFrame S} (A B : F.Regular) : ↑(A ⊓ B) = ↑A ∩ ↑B

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_top {S : Type u_1} {F : CompatFrame S} : ↑⊤ = Set.univ

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_bot {S : Type u_1} {F : CompatFrame S} : ↑⊥ = ∅

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_eq_empty {S : Type u_1} {F : CompatFrame S} {A : F.Regular} : ↑A = ∅ ↔ A = ⊥

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_compl {S : Type u_1} {F : CompatFrame S} (A : F.Regular) : ↑Aᶜ = orthoNeg F ↑A

@[simp]

theorem Orthologic.CompatFrame.Regular.coe_sup {S : Type u_1} {F : CompatFrame S} (A B : F.Regular) : ↑(A ⊔ B) = disj F ↑A ↑B

The join of regular propositions is their De Morgan disjunction disj.