Possibility Semantics

@cite{holliday-mandelkern-2024}

Possibility semantics generalizes possible world semantics by replacing maximal possible worlds with partial possibilities ordered by refinement. A possibility can verify a disjunction without verifying either disjunct.

Key differences from possible world semantics

• Propositions are not arbitrary sets of possibilities but only regular sets — those satisfying a closure condition.
• Negation is orthocomplement: ¬A = {x | ∀y ◇ x, y ∉ A}.
• Disjunction is weaker than union: A ∨ B = ¬(¬A ∧ ¬B).
• The resulting algebra of propositions is an ortholattice, not a Boolean algebra.

What validates and what fails

Validated: excluded middle, non-contradiction, double negation, De Morgan, contraposition. Failed: distributivity — a possibility can verify A ∧ (B ∨ C) without verifying either A ∧ B or A ∧ C. This is the key departure from classical logic and the source of linguistic applications (epistemic contradictions, free choice disjunction).

Architecture

• Basic.lean (this file): compatibility frames, orthocomplement, regularity
• Epistemic.lean: epistemic modals, Wittgenstein sentences, free choice

structure Semantics.PossibilitySemantics.CompatFrame (S : Type u_1) : Type u_1

A compatibility frame: a set of possibilities with a reflexive, symmetric compatibility relation. Two possibilities are compatible if neither settles as true anything the other settles as false. @cite{holliday-mandelkern-2024} Definition 4.1.

• compat : S → S → Bool
• compat_refl (x : S) : self.compat x x = true
• compat_symm (x y : S) : self.compat x y = self.compat y x

def Semantics.PossibilitySemantics.orthoNeg {S : Type u_1} [Core.Proposition.FiniteWorlds S] (F : CompatFrame S) (A : BProp S) : BProp S

Orthocomplement negation. ¬A = {x | ∀y compatible with x, y ∉ A}. A possibility x makes ¬A true iff no compatible possibility makes A true — i.e., x's information settles ¬A. @cite{holliday-mandelkern-2024} Proposition 4.8, eq. (I).

Equations

• Semantics.PossibilitySemantics.orthoNeg F A x = (List.filter (F.compat x) Core.Proposition.FiniteWorlds.worlds).all fun (y : S) => !A y

def Semantics.PossibilitySemantics.conj {S : Type u_1} (A B : BProp S) : BProp S

Conjunction is intersection (same as classical).

Equations

• Semantics.PossibilitySemantics.conj A B x = (A x && B x)

def Semantics.PossibilitySemantics.disj {S : Type u_1} [Core.Proposition.FiniteWorlds S] (F : CompatFrame S) (A B : BProp S) : BProp S

Disjunction via De Morgan: A ∨ B = ¬(¬A ∧ ¬B). Weaker than set-theoretic union. A possibility x makes A ∨ B true iff every y compatible with x is itself compatible with some z that makes A or B true. @cite{holliday-mandelkern-2024} eq. (II).

Equations

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

def Semantics.PossibilitySemantics.isRegular {S : Type u_1} [Core.Proposition.FiniteWorlds S] (F : CompatFrame S) (A : BProp S) : Bool

A set A is ◇-regular iff: whenever x ∉ A, there exists y compatible with x such that all z compatible with y are also not in A. Regularity = "indeterminacy implies compatibility with falsity." Only regular sets count as propositions. @cite{holliday-mandelkern-2024} Definition 4.3.

Equations

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

def Semantics.PossibilitySemantics.refines {S : Type u_1} [Core.Proposition.FiniteWorlds S] (F : CompatFrame S) (y x : S) : Bool

Refinement: y ⊑ x iff every possibility compatible with y is also compatible with x. A refinement carries at least as much information. @cite{holliday-mandelkern-2024} Lemma 4.4, condition 2.

Equations

• Semantics.PossibilitySemantics.refines F y x = Core.Proposition.FiniteWorlds.worlds.all fun (z : S) => !F.compat y z || F.compat x z

def Semantics.PossibilitySemantics.isWorld {S : Type u_1} [Core.Proposition.FiniteWorlds S] (F : CompatFrame S) (w : S) : Bool

A world is a possibility that refines everything it is compatible with — the most informative kind of possibility. @cite{holliday-mandelkern-2024} Definition 4.6.

Equations

• Semantics.PossibilitySemantics.isWorld F w = Core.Proposition.FiniteWorlds.worlds.all fun (x : S) => !F.compat w x || Semantics.PossibilitySemantics.refines F w x

inductive Semantics.PossibilitySemantics.Poss5 : Type

Five possibilities arranged in a path: x₁—x₂—x₃—x₄—x₅. The simplest frame whose ortholattice is non-Boolean. @cite{holliday-mandelkern-2024} Example 4.11, Figure 7.

• x1 : Poss5
• x2 : Poss5
• x3 : Poss5
• x4 : Poss5
• x5 : Poss5

instance Semantics.PossibilitySemantics.instDecidableEqPoss5 : DecidableEq Poss5

Equations

• Semantics.PossibilitySemantics.instDecidableEqPoss5 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.PossibilitySemantics.instBEqPoss5 : BEq Poss5

Equations

• Semantics.PossibilitySemantics.instBEqPoss5 = { beq := Semantics.PossibilitySemantics.instBEqPoss5.beq }

def Semantics.PossibilitySemantics.instBEqPoss5.beq : Poss5 → Poss5 → Bool

Equations

• Semantics.PossibilitySemantics.instBEqPoss5.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.PossibilitySemantics.instReprPoss5.repr : Poss5 → ℕ → Std.Format

Equations

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

instance Semantics.PossibilitySemantics.instReprPoss5 : Repr Poss5

Equations

• Semantics.PossibilitySemantics.instReprPoss5 = { reprPrec := Semantics.PossibilitySemantics.instReprPoss5.repr }

instance Semantics.PossibilitySemantics.instInhabitedPoss5 : Inhabited Poss5

Equations

• Semantics.PossibilitySemantics.instInhabitedPoss5 = { default := Semantics.PossibilitySemantics.instInhabitedPoss5.default }

def Semantics.PossibilitySemantics.instInhabitedPoss5.default : Poss5

Equations

• Semantics.PossibilitySemantics.instInhabitedPoss5.default = Semantics.PossibilitySemantics.Poss5.x1

instance Semantics.PossibilitySemantics.instFiniteWorldsPoss5 : Core.Proposition.FiniteWorlds Poss5

Equations

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

instance Semantics.PossibilitySemantics.instFintypePoss5 : Fintype Poss5

Equations

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

def Semantics.PossibilitySemantics.pathFrame : CompatFrame Poss5

The path compatibility frame: adjacent possibilities are compatible.

Equations

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

theorem Semantics.PossibilitySemantics.neg_left : orthoNeg pathFrame Semantics.PossibilitySemantics.pLeft✝ = Semantics.PossibilitySemantics.pRight✝

Negation: ¬{x₁,x₂} = {x₄,x₅}.

theorem Semantics.PossibilitySemantics.neg_right : orthoNeg pathFrame Semantics.PossibilitySemantics.pRight✝ = Semantics.PossibilitySemantics.pLeft✝

Negation: ¬{x₄,x₅} = {x₁,x₂}.

theorem Semantics.PossibilitySemantics.neg_mid : orthoNeg pathFrame Semantics.PossibilitySemantics.pMid✝ = Semantics.PossibilitySemantics.pEndpoints✝

theorem Semantics.PossibilitySemantics.doubleNeg_left : orthoNeg pathFrame (orthoNeg pathFrame Semantics.PossibilitySemantics.pLeft✝) = Semantics.PossibilitySemantics.pLeft✝¹

Double negation: ¬¬A = A (involutive on regular sets).

theorem Semantics.PossibilitySemantics.excludedMiddle_left (x : Poss5) : disj pathFrame Semantics.PossibilitySemantics.pLeft✝ (orthoNeg pathFrame Semantics.PossibilitySemantics.pLeft✝¹) x = true

Excluded middle: A ∨ ¬A = S (every possibility verifies it).

theorem Semantics.PossibilitySemantics.nonContradiction_left (x : Poss5) : conj Semantics.PossibilitySemantics.pLeft✝ (orthoNeg pathFrame Semantics.PossibilitySemantics.pLeft✝¹) x = false

Non-contradiction: A ∧ ¬A = ∅ (no possibility verifies it).

theorem Semantics.PossibilitySemantics.distributivity_failure : conj Semantics.PossibilitySemantics.pMid✝ (disj pathFrame Semantics.PossibilitySemantics.pLeft✝ Semantics.PossibilitySemantics.pRight✝) Poss5.x3 ≠ disj pathFrame (conj Semantics.PossibilitySemantics.pMid✝¹ Semantics.PossibilitySemantics.pLeft✝¹) (conj Semantics.PossibilitySemantics.pMid✝² Semantics.PossibilitySemantics.pRight✝¹) Poss5.x3

Distributivity failure. The key result of possibility semantics. C ∧ (A ∨ B) ≠ (C ∧ A) ∨ (C ∧ B), where C = {x₃}, A = {x₁,x₂}, B = {x₄,x₅}. Possibility x₃ is compatible with both A and B worlds, so it makes A ∨ B true; but it doesn't commit to either disjunct, so neither C ∧ A nor C ∧ B is non-empty. @cite{holliday-mandelkern-2024} Example 4.11, Figure 8.

theorem Semantics.PossibilitySemantics.distrib_lhs_at_x3 : conj Semantics.PossibilitySemantics.pMid✝ (disj pathFrame Semantics.PossibilitySemantics.pLeft✝ Semantics.PossibilitySemantics.pRight✝) Poss5.x3 = true

The LHS of distributivity at x₃: true (x₃ makes C ∧ (A ∨ B) true).

theorem Semantics.PossibilitySemantics.distrib_rhs_at_x3 : disj pathFrame (conj Semantics.PossibilitySemantics.pMid✝ Semantics.PossibilitySemantics.pLeft✝) (conj Semantics.PossibilitySemantics.pMid✝¹ Semantics.PossibilitySemantics.pRight✝) Poss5.x3 = false

The RHS of distributivity at x₃: false (x₃ fails (C∧A) ∨ (C∧B)).

theorem Semantics.PossibilitySemantics.x1_is_world : isWorld pathFrame Poss5.x1 = true

x₁ is a world (maximal possibility).

theorem Semantics.PossibilitySemantics.x5_is_world : isWorld pathFrame Poss5.x5 = true

x₅ is a world.

theorem Semantics.PossibilitySemantics.x3_not_world : isWorld pathFrame Poss5.x3 = false

x₃ is NOT a world — it's a partial possibility, compatible with possibilities on both sides without being a refinement of either.

theorem Semantics.PossibilitySemantics.regular_left : isRegular pathFrame Semantics.PossibilitySemantics.pLeft✝ = true

All propositions in the ortholattice are regular.

theorem Semantics.PossibilitySemantics.regular_right : isRegular pathFrame Semantics.PossibilitySemantics.pRight✝ = true

theorem Semantics.PossibilitySemantics.regular_mid : isRegular pathFrame Semantics.PossibilitySemantics.pMid✝ = true

theorem Semantics.PossibilitySemantics.regular_empty : isRegular pathFrame Semantics.PossibilitySemantics.pEmpty✝ = true

theorem Semantics.PossibilitySemantics.regular_full : isRegular pathFrame Semantics.PossibilitySemantics.pFull✝ = true

theorem Semantics.PossibilitySemantics.orthoNeg_classical {S : Type u_1} [Core.Proposition.FiniteWorlds S] [DecidableEq S] (F : CompatFrame S) (hClassical : ∀ (x y : S), F.compat x y = true → x = y) (A : BProp S) (x : S) : orthoNeg F A x = !A x

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. @cite{holliday-mandelkern-2024} Remark 4.9.

def Semantics.PossibilitySemantics.identityFrame {S : Type u_1} [DecidableEq S] : CompatFrame S

The identity compatibility frame: compat x y ↔ x = y.

Equations

• Semantics.PossibilitySemantics.identityFrame = { compat := fun (x y : S) => decide (x = y), compat_refl := ⋯, compat_symm := ⋯ }

theorem Semantics.PossibilitySemantics.identityFrame_classical {S : Type u_1} [Core.Proposition.FiniteWorlds S] [DecidableEq S] (A : BProp S) (x : S) : orthoNeg identityFrame A x = !A x

In the identity frame, orthoNeg is pointwise Boolean negation.