Lifting Construction: From Boolean Algebras to Epistemic Ortholattices #

@cite{holliday-mandelkern-2024} Definition 5.1, Lemma 5.4

The lifting construction connects Kripke possible-world semantics to possibility semantics. Given a Boolean algebra B (propositions over worlds), the epistemic extension lifts it to an ortholattice whose elements are pairs (A, I) with ∅ ≠ A ⊆ I ⊆ W:

A (actuality set): worlds compatible with what has been settled
I (information set): worlds compatible with what is known

Compatibility: (A,I) ◇ (A',I') iff A ∩ A' ≠ ∅ ∧ A ⊆ I' ∧ A' ⊆ I Accessibility: (A,I) R (A',I') iff A ⊆ A' ∧ I' ⊆ I

For the 2-world model W = {0, 1} with V(p) = {0}, the five possibilities are:

x₁ = ({0}, {0}) — knows p
x₂ = ({0}, {0,1}) — settled p, doesn't know
x₃ = ({0,1}, {0,1}) — full uncertainty
x₄ = ({1}, {0,1}) — settled ¬p, doesn't know
x₅ = ({1}, {1}) — knows ¬p

This file verifies that the epistemic scale's compatibility and accessibility relations match the lifting construction, and derives truth conditions for p, □p, ◇p in terms of world membership in A and I.

source

def Semantics.PossibilitySemantics.liftedCompat (x y : Poss5) :

Bool

Compatibility derived from lifting: (A,I) ◇ (A',I') iff A ∩ A' ≠ ∅ ∧ A ⊆ I' ∧ A' ⊆ I. @cite{holliday-mandelkern-2024} Definition 5.1.

Equations

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

Instances For

source

def Semantics.PossibilitySemantics.liftedAccess (x y : Poss5) :

Bool

Accessibility derived from lifting: (A,I) R (A',I') iff A ⊆ A' ∧ I' ⊆ I (refining = expanding actuality, shrinking information). @cite{holliday-mandelkern-2024} Definition 5.1.

Equations

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

Instances For

source

theorem Semantics.PossibilitySemantics.compat_from_lifting (x y : Poss5) :

epistemicScale.compat x y = liftedCompat x y

The epistemic scale's compatibility matches the lifting construction.

source

theorem Semantics.PossibilitySemantics.access_from_lifting (x y : Poss5) :

epistemicScale.access x y = liftedAccess x y

The epistemic scale's accessibility matches the lifting construction.

@cite{holliday-mandelkern-2024} Lemma 5.4: truth at a possibility reduces to truth at worlds via the A and I sets.

- propP x = true  iff  world 1 ∉ A(x)  (all actual worlds satisfy p)
- □p x = true     iff  world 1 ∉ I(x)  (all information-accessible worlds satisfy p)
- ◇p x = true     iff  world 0 ∈ A(x)  (some actual world satisfies p)

source

theorem Semantics.PossibilitySemantics.boolean_truth_from_worlds (x : Poss5) :

propP x = !worldlyA1 x

Boolean truth from worlds: p holds at x iff the ¬p-world is not actual.

source

theorem Semantics.PossibilitySemantics.box_truth_from_worlds (x : Poss5) :

box epistemicScale propP x = !worldlyI1 x

Box truth from worlds: □p holds at x iff the ¬p-world is not information-accessible.

source

theorem Semantics.PossibilitySemantics.diamond_truth_from_worlds (x : Poss5) :

diamond epistemicScale propP x = worldlyA0 x

Diamond truth from worlds: ◇p holds at x iff the p-world is actual.

Documentation

Linglib.Theories.Semantics.PossibilitySemantics.Lifting

Lifting Construction: From Boolean Algebras to Epistemic Ortholattices #