Constructing possibilities from worlds

[HM24] §5 — the epistemic extension of a Boolean algebra. From a Boolean algebra B of non-modal propositions we build a compatibility frame Bᵉ whose possibilities are pairs (truth, info) of propositions with 0 ≠ truth ≤ info (Def 5.1): truth says what is the case, info what must be the case. The regular propositions of Bᵉ form an epistemic ortholattice into which B embeds via e_B(a) = {(b,i) | b ≤ a} (Theorem 5.7.2).

This gives possibility-semantics models a concrete construction from familiar possible-worlds models (take B = ℘(W)), showing the framework is "ontologically innocent": anyone comfortable with worlds can build the whole system on them.

Main results

• Possibility, epistemicFrame — the frame Bᵉ (Def 5.1, Thm 5.7.1).
• eBset_regular, eB — the embedding e_B : B → O(Bᵉ) (Thm 5.7.2): e_B(a) is a regular proposition.

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

A possibility of a Boolean algebra B ([HM24] Def 5.1): a pair (truth, info) with 0 ≠ truth ≤ info. The first component says what is the case, the second what must be the case.

• truth : B

  What is the case at this possibility.

• info : B

  What must be the case at this possibility.

• truth_ne_bot : self.truth ≠ ⊥
• truth_le_info : self.truth ≤ self.info

def Orthologic.Possibility.Compat {B : Type u_1} [BooleanAlgebra B] (p q : Possibility B) : Prop

Compatibility ◊ ([HM24] Def 5.1.2): their truths overlap, and each truth is entailed by the other's information.

Equations

• p.Compat q = (p.truth ⊓ q.truth ≠ ⊥ ∧ p.truth ≤ q.info ∧ q.truth ≤ p.info)

def Orthologic.Possibility.Access {B : Type u_1} [BooleanAlgebra B] (p q : Possibility B) : Prop

Epistemic accessibility R ([HM24] Def 5.1.3).

Equations

• p.Access q = (p.truth ≤ q.truth ∧ q.info ≤ p.info)

theorem Orthologic.Possibility.access_refl {B : Type u_1} [BooleanAlgebra B] (p : Possibility B) : p.Access p

theorem Orthologic.Possibility.access_trans {B : Type u_1} [BooleanAlgebra B] {p q r : Possibility B} (h₁ : p.Access q) (h₂ : q.Access r) : p.Access r

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

The epistemic frame Bᵉ of a Boolean algebra ([HM24] Def 5.1, Theorem 5.7.1): possibilities under compatibility ◊, a CompatFrame (◊ is reflexive and symmetric).

Equations

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

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

The embedding's underlying set e_B(a) = {(b,i) | b ≤ a} ([HM24] Theorem 5.7.2).

Equations

• Orthologic.eBset a = {q : Orthologic.Possibility B | q.truth ≤ a}

theorem Orthologic.eBset_regular {B : Type u_1} [BooleanAlgebra B] (a : B) : IsRegular (epistemicFrame B) (eBset a)

e_B(a) is a regular proposition of Bᵉ ([HM24] Thm 5.7.2): if b ≰ a then the possibility (b ⊓ aᶜ, i) is a ◊-witness none of whose compatible possibilities support e_B(a).

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

The embedding e_B : B → O(Bᵉ) ([HM24] Theorem 5.7.2) as a regular proposition.

Equations

• Orthologic.eB a = (Orthologic.epistemicFrame B).regOf (Orthologic.eBset a) ⋯

@[simp]

theorem Orthologic.mem_eB {B : Type u_1} [BooleanAlgebra B] (a : B) (q : Possibility B) : q ∈ ↑(eB a) ↔ q.truth ≤ a

@[simp]

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

e_B is an order-embedding preserving ⊓, ⊤, ⊥ (Theorem 5.7.2)

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

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

e_B reflects order, hence is an embedding: the possibility (a, ⊤) witnesses a ≤ a' whenever e_B a ≤ e_B a'.

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] (a a' : B) : eB (a ⊓ a') = eB a ⊓ eB a'

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

e_B preserves complement ([HM24] Thm 5.7.2): the orthonegation of e_B(a) is e_B(aᶜ). The ← direction reuses the witness (q ⊓ a, q.info).

theorem Orthologic.eB_sup {B : Type u_1} [BooleanAlgebra B] (a a' : B) : eB (a ⊔ a') = eB a ⊔ eB a'

e_B preserves joins (from ⊓- and complement-preservation via De Morgan), completing the Boolean-algebra embedding ([HM24] Thm 5.7.2).