The epistemic frame of a Boolean algebra

This file defines Holliday and Mandelkern's lifting of a possible-worlds model to a possibility model for epistemic modals. The possibilities of the epistemic frame of a Boolean algebra B are the pairs (a, i) with ⊥ ≠ a ≤ i, where a records how things are and might be and i what must be the case. Two possibilities are compatible when their first components overlap and each lies within the other's second component, and (a, i) accesses (a', i') when a ≤ a' and i' ≤ i. Access is reflexive, R-regular and knowable, so the regular propositions form an epistemic ortholattice, and B embeds into it.

Main definitions

• Orthologic.Possibility: the possibilities (a, i) of the epistemic frame.
• Orthologic.epistemicFrame: the compatibility frame on possibilities.
• Orthologic.embed, Orthologic.eB: the embedding of B into the regular propositions.

Main results

• Orthologic.refines_iff: refinement is componentwise.
• Orthologic.mem_core_embed, Orthologic.mem_diamond_embed: b must be the case at (a, i) iff i ≤ b, and might be iff a ⊓ b ≠ ⊥.
• Orthologic.eB_le_iff, Orthologic.eB_compl: the embedding is an order embedding preserving ⊤, ⊥, meets and complements.
• Orthologic.diamondHom_necHom_le: the regular propositions form an S5 epistemic ortholattice.
• Orthologic.not_diamond_embed_subset: ◇ does not collapse on non-trivial embedded propositions.

References

• [HM24]

@[reducible, inline]

abbrev Orthologic.Possibility (B : Type u_2) [BooleanAlgebra B] : Type u_2

A possibility of the epistemic frame of B is a pair (a, i) with ⊥ ≠ a ≤ i ([HM24] Definition 5.1).

Equations

• Orthologic.Possibility B = { p : B × B // p.1 ≠ ⊥ ∧ p.1 ≤ p.2 }

@[reducible, inline]

abbrev Orthologic.Possibility.truth {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : B

The first component of (a, i) records how things are and might be.

Equations

• x.truth = (↑x).1

@[reducible, inline]

abbrev Orthologic.Possibility.info {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : B

The second component of (a, i) records what must be the case.

Equations

• x.info = (↑x).2

theorem Orthologic.Possibility.truth_ne_bot {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : x.truth ≠ ⊥

theorem Orthologic.Possibility.truth_le_info {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : x.truth ≤ x.info

theorem Orthologic.Possibility.info_ne_bot {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : x.info ≠ ⊥

def Orthologic.Possibility.compat {B : Type u_1} [BooleanAlgebra B] (x y : Possibility B) : Prop

Two possibilities are compatible when their truths overlap and each lies within the other's information ([HM24] Definition 5.1.2).

Equations

• x.compat y = (x.truth ⊓ y.truth ≠ ⊥ ∧ x.truth ≤ y.info ∧ y.truth ≤ x.info)

def Orthologic.Possibility.access {B : Type u_1} [BooleanAlgebra B] : SetRel (Possibility B) (Possibility B)

A possibility accesses another when both components of the target lie between the components of the source ([HM24] Definition 5.1.3).

Equations

• Orthologic.Possibility.access = {p : Orthologic.Possibility B × Orthologic.Possibility B | p.1.truth ≤ p.2.truth ∧ p.2.info ≤ p.1.info}

@[instance_reducible]

instance Orthologic.Possibility.instDecidableCompatOfDecidableEqOfDecidableLE {B : Type u_1} [BooleanAlgebra B] (x y : Possibility B) [DecidableEq B] [DecidableLE B] : Decidable (x.compat y)

Equations

• x.instDecidableCompatOfDecidableEqOfDecidableLE y = { decide := decide (x.truth ⊓ y.truth ≠ ⊥) && decide (x.truth ≤ y.info ∧ y.truth ≤ x.info), reflects_decide := ⋯ }

@[instance_reducible]

instance Orthologic.Possibility.instDecidableMemProdSetRelAccessMkOfDecidableEqOfDecidableLE {B : Type u_1} [BooleanAlgebra B] (x y : Possibility B) [DecidableEq B] [DecidableLE B] : Decidable ((x, y) ∈ access)

Equations

• x.instDecidableMemProdSetRelAccessMkOfDecidableEqOfDecidableLE y = { decide := decide ((x, y).1.truth ≤ (x, y).2.truth) && decide ((x, y).2.info ≤ (x, y).1.info), reflects_decide := ⋯ }

def Orthologic.Possibility.diag {B : Type u_1} [BooleanAlgebra B] (a : B) (ha : a ≠ ⊥) : Possibility B

diag a is the possibility (a, a), which knows everything it settles.

Equations

• Orthologic.Possibility.diag a ha = ⟨(a, a), ⋯⟩

@[simp]

theorem Orthologic.Possibility.diag_truth {B : Type u_1} [BooleanAlgebra B] (a : B) (ha : a ≠ ⊥) : (diag a ha).truth = a

@[simp]

theorem Orthologic.Possibility.diag_info {B : Type u_1} [BooleanAlgebra B] (a : B) (ha : a ≠ ⊥) : (diag a ha).info = a

theorem Orthologic.Possibility.compat_diag_truth {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : x.compat (diag x.truth ⋯)

theorem Orthologic.Possibility.compat_diag_info {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : x.compat (diag x.info ⋯)

theorem Orthologic.Possibility.access_diag_info {B : Type u_1} [BooleanAlgebra B] (x : Possibility B) : (x, diag x.info ⋯) ∈ access

def Orthologic.epistemicFrame (B : Type u_2) [BooleanAlgebra B] : CompatFrame (Possibility B)

The epistemic frame of B is the compatibility frame on Possibility B ([HM24] Definition 5.1).

Equations

• Orthologic.epistemicFrame B = { compat := Orthologic.Possibility.compat, compat_refl := ⋯, compat_symm := ⋯, ortho_iff := ⋯ }

instance Orthologic.instIsReflPossibilityAccess {B : Type u_1} [BooleanAlgebra B] : Possibility.access.IsRefl

instance Orthologic.instIsRRegularPossibilityEpistemicFrameAccess {B : Type u_1} [BooleanAlgebra B] : IsRRegular (epistemicFrame B) Possibility.access

Epistemic access is R-regular, witnessed by (a ⊔ d, a ⊔ d) ([HM24] Theorem 5.7.1).

instance Orthologic.instIsKnowablePossibilityEpistemicFrameAccess {B : Type u_1} [BooleanAlgebra B] : IsKnowable (epistemicFrame B) Possibility.access

Epistemic access satisfies Knowability, witnessed by (a, a) ([HM24] Theorem 5.7.1).

@[instance_reducible]

instance Orthologic.instDecidableRelPossibilityCompatEpistemicFrame {B : Type u_1} [BooleanAlgebra B] [DecidableEq B] [DecidableLE B] : DecidableRel (epistemicFrame B).compat

Equations

• Orthologic.instDecidableRelPossibilityCompatEpistemicFrame = Orthologic.instDecidableRelPossibilityCompatEpistemicFrame._aux_1

theorem Orthologic.refines_iff {B : Type u_1} [BooleanAlgebra B] (y x : Possibility B) : refines (epistemicFrame B) y x ↔ y.truth = x.truth ∧ y.info ≤ x.info

Refinement in the epistemic frame is componentwise, (a, i) ⊑ (a', i') iff a = a' and i ≤ i' ([HM24] Lemma 5.2).

def Orthologic.embed {B : Type u_1} [BooleanAlgebra B] (b : B) : Set (Possibility B)

embed b is the set of possibilities whose truth entails b, the underlying set of the embedding e_B ([HM24] Theorem 5.7.2).

Equations

• Orthologic.embed b = {x : Orthologic.Possibility B | x.truth ≤ b}

@[simp]

theorem Orthologic.mem_embed {B : Type u_1} [BooleanAlgebra B] {b : B} {x : Possibility B} : x ∈ embed b ↔ x.truth ≤ b

@[instance_reducible]

instance Orthologic.instDecidablePredPossibilityMemSetEmbedOfDecidableLE {B : Type u_1} [BooleanAlgebra B] [DecidableLE B] (b : B) : DecidablePred fun (x : Possibility B) => x ∈ embed b

Equations

• Orthologic.instDecidablePredPossibilityMemSetEmbedOfDecidableLE b x = Orthologic.instDecidablePredPossibilityMemSetEmbedOfDecidableLE._aux_1 b x

@[instance_reducible]

instance Orthologic.instDecidablePredPossibilityEmbedOfDecidableLE {B : Type u_1} [BooleanAlgebra B] [DecidableLE B] (b : B) : DecidablePred (embed b)

Equations

• Orthologic.instDecidablePredPossibilityEmbedOfDecidableLE b x = Orthologic.instDecidablePredPossibilityEmbedOfDecidableLE._aux_1 b x

theorem Orthologic.mem_core_embed {B : Type u_1} [BooleanAlgebra B] {b : B} {x : Possibility B} : x ∈ Possibility.access.core (embed b) ↔ x.info ≤ b

b must be the case at (a, i) iff i ≤ b. [HM24] Lemma 5.8.2.

theorem Orthologic.mem_diamond_embed {B : Type u_1} [BooleanAlgebra B] {b : B} {x : Possibility B} : x ∈ diamond (epistemicFrame B) Possibility.access (embed b) ↔ x.truth ⊓ b ≠ ⊥

b might be the case at (a, i) iff a ⊓ b ≠ ⊥. [HM24] Lemma 5.8.3.

theorem Orthologic.embed_isRegular {B : Type u_1} [BooleanAlgebra B] (b : B) : IsRegular (epistemicFrame B) (embed b)

Embedded propositions are regular, witnessed at (a, i) ∉ e(b) by (a ⊓ bᶜ, i) ([HM24] Theorem 5.7.2).

theorem Orthologic.embed_compl {B : Type u_1} [BooleanAlgebra B] (b : B) : embed bᶜ = orthoNeg (epistemicFrame B) (embed b)

The embedding sends complements to orthocomplements. [HM24] Theorem 5.7.2.

theorem Orthologic.embed_inf {B : Type u_1} [BooleanAlgebra B] (b c : B) : embed (b ⊓ c) = embed b ∩ embed c

The embedding preserves meets. [HM24] Theorem 5.7.2.

theorem Orthologic.embed_inter_diamond_embed_subset {B : Type u_1} [BooleanAlgebra B] (b c : B) : embed b ∩ diamond (epistemicFrame B) Possibility.access (embed c) ⊆ diamond (epistemicFrame B) Possibility.access (embed (b ⊓ c))

For embedded propositions, what is the case and compatible with c is compatible with both, the inheritance principle of [HM24] Proposition 5.12.3.

The embedding into the regular propositions

def Orthologic.eB {B : Type u_1} [BooleanAlgebra B] (b : B) : (epistemicFrame B).Regular

eB b is the regular proposition e_B(b) of the embedding of B into the regular propositions of its epistemic frame ([HM24] Theorem 5.7.2).

Equations

• Orthologic.eB b = (Orthologic.epistemicFrame B).regOf (Orthologic.embed b) ⋯

@[simp]

theorem Orthologic.coe_eB {B : Type u_1} [BooleanAlgebra B] (b : B) : ↑(eB b) = embed b

theorem Orthologic.eB_mono {B : Type u_1} [BooleanAlgebra B] {b c : B} (h : b ≤ c) : eB b ≤ eB c

theorem Orthologic.eB_le_iff {B : Type u_1} [BooleanAlgebra B] {b c : B} : eB b ≤ eB c ↔ b ≤ c

e_B reflects order, as the possibility (b, ⊤) witnesses b ≤ c from e_B b ≤ e_B c.

theorem Orthologic.eB_injective {B : Type u_1} [BooleanAlgebra B] : Function.Injective eB

theorem Orthologic.eB_top {B : Type u_1} [BooleanAlgebra B] : eB ⊤ = ⊤

theorem Orthologic.eB_bot {B : Type u_1} [BooleanAlgebra B] : eB ⊥ = ⊥

theorem Orthologic.eB_inf {B : Type u_1} [BooleanAlgebra B] (b c : B) : eB (b ⊓ c) = eB b ⊓ eB c

theorem Orthologic.eB_compl {B : Type u_1} [BooleanAlgebra B] (b : B) : eB bᶜ = (eB b)ᶜ

theorem Orthologic.not_diamond_embed_subset {B : Type u_1} [BooleanAlgebra B] {b : B} (hb : b ≠ ⊥) (hb' : b ≠ ⊤) : ¬diamond (epistemicFrame B) Possibility.access (embed b) ⊆ embed b

The diamond of an embedded proposition strictly extends it unless the proposition is trivial, since (⊤, ⊤) lies in ◇e(b) but not in e(b) ([HM24] Theorem 5.7.4).

The epistemic extension is S5

instance Orthologic.instIsTransPossibilityAccess {B : Type u_1} [BooleanAlgebra B] : Possibility.access.IsTrans

theorem Orthologic.subset_core_diamond {B : Type u_1} [BooleanAlgebra B] (U : Set (Possibility B)) : U ⊆ Possibility.access.core (diamond (epistemicFrame B) Possibility.access U)

Whatever is the case must be possible, U ⊆ □◇U for every set U, witnessed by (a ⊔ a'', a ⊔ a'') for (a, i) ∈ U (the proof of [HM24] Theorem 5.7.3).

theorem Orthologic.diamondHom_necHom_le {B : Type u_1} [BooleanAlgebra B] (U : (epistemicFrame B).Regular) : (diamondHom ((epistemicFrame B).necHom Possibility.access)) U ≤ ((epistemicFrame B).necHom Possibility.access) ((diamondHom ((epistemicFrame B).necHom Possibility.access)) U)

The 5 principle ◇U ≤ □◇U in the epistemic extension of B, which is therefore an S5 epistemic ortholattice ([HM24] Theorem 5.7.3).