Holliday and Mandelkern (2024): The orthologic of epistemic modals

This file formalizes Holliday and Mandelkern's possibility semantics for epistemic modals on their running example, the Epistemic Scale. The Scale is the epistemic frame of the two-world Boolean algebra of a coin flip, whose five possibilities run from knowing p through full uncertainty to knowing ¬p. The frame comes from the general construction Orthologic.epistemicFrame, so its compatibility and accessibility relations are derived rather than stipulated, and the paper's truth-value table follows by decision. On this model Wittgenstein sentences are contradictions while ◇¬p does not entail ¬p, and the classical laws the paper gives up fail at the point of full uncertainty.

Main results

• compat_iff, access_iff: the compatibility and accessibility relations of the Scale.
• wittgenstein, diamond_neg_not_entail_neg, not_entail_box: Wittgenstein sentences are contradictions, yet ◇¬p does not entail ¬p and p does not entail □p.
• not_derivable_dia_neg_neg, not_derivable_box: so neither entailment is derivable in the epistemic orthologic EO.
• distributivity_fails, disjunctive_syllogism_fails: the classical inferences of (10) and (13) fail at the point of full uncertainty.
• orthomodularity_fails, not_isModularLattice, pseudocomplementation_fails: the regular propositions form an ortholattice that is not orthomodular, not modular, and whose orthonegation is not a pseudocomplement.
• deMorgan, not_known_either: the contrasts with state-based semantics.
• stratified_level1, not_stratified_across_levels: classicality within each level of modal iteration, but not across levels.

Implementation notes

The Boolean algebra is Finset (Fin 2), so every claim about the Scale is decidable; the general truth conditions of embedded propositions are Orthologic.mem_core_embed and Orthologic.mem_diamond_embed. The paper contrasts its symmetric Wittgenstein's Law with the order asymmetry of dynamic semantics, whose side is Veltman1996.consistent_might_neg beside Veltman1996.not_consistent_up_might_neg; no theorem here conjoins the two.

TODO

The Epistemic Grid (Example 4.34), the logic EO+ with its completeness theorem, and the remaining principles of Proposition 5.12 are not formalized.

References

• [HM24]

@[reducible, inline]

abbrev HollidayMandelkern2024.Coin : Type

Coin is the two-world Boolean algebra of the coin flip (Example 5.3).

Equations

• HollidayMandelkern2024.Coin = Finset (Fin 2)

@[reducible, inline]

abbrev HollidayMandelkern2024.Poss : Type

Poss is the type of possibilities of the epistemic frame of Coin.

Equations

• HollidayMandelkern2024.Poss = Orthologic.Possibility HollidayMandelkern2024.Coin

@[reducible, inline]

abbrev HollidayMandelkern2024.frame : Orthologic.CompatFrame Poss

frame is the Epistemic Scale's compatibility frame, with accessibility access.

Equations

• HollidayMandelkern2024.frame = Orthologic.epistemicFrame HollidayMandelkern2024.Coin

@[instance_reducible]

instance HollidayMandelkern2024.instDecidableRelPossCompatFrame : DecidableRel frame.compat

Equations

• HollidayMandelkern2024.instDecidableRelPossCompatFrame = HollidayMandelkern2024.instDecidableRelPossCompatFrame._aux_1

def HollidayMandelkern2024.x1 : Poss

The possibility x1 = ({0}, {0}) knows p.

Equations

• HollidayMandelkern2024.x1 = ⟨({0}, {0}), HollidayMandelkern2024.x1._proof_1⟩

def HollidayMandelkern2024.x2 : Poss

The possibility x2 = ({0}, {0, 1}) settles p without knowing it.

Equations

• HollidayMandelkern2024.x2 = ⟨({0}, {0, 1}), HollidayMandelkern2024.x2._proof_1⟩

def HollidayMandelkern2024.x3 : Poss

The possibility x3 = ({0, 1}, {0, 1}) is fully uncertain.

Equations

• HollidayMandelkern2024.x3 = ⟨({0, 1}, {0, 1}), HollidayMandelkern2024.x3._proof_1⟩

def HollidayMandelkern2024.x4 : Poss

The possibility x4 = ({1}, {0, 1}) settles ¬p without knowing it.

Equations

• HollidayMandelkern2024.x4 = ⟨({1}, {0, 1}), HollidayMandelkern2024.x4._proof_1⟩

def HollidayMandelkern2024.x5 : Poss

The possibility x5 = ({1}, {1}) knows ¬p.

Equations

• HollidayMandelkern2024.x5 = ⟨({1}, {1}), HollidayMandelkern2024.x5._proof_1⟩

theorem HollidayMandelkern2024.card_poss : Fintype.card Poss = 5

Two worlds give five possibilities, the first row of Table 1.

theorem HollidayMandelkern2024.compat_iff (x y : Poss) : frame.compat x y ↔ x = y ∨ (x, y) ∈ [(x1, x2), (x2, x1), (x2, x3), (x3, x2), (x3, x4), (x4, x3), (x4, x5), (x5, x4)]

Compatibility is the path x1 — x2 — x3 — x4 — x5 (Figure 7 and Example 5.3).

theorem HollidayMandelkern2024.access_iff (x y : Poss) : (x, y) ∈ Orthologic.Possibility.access ↔ x = y ∨ (x, y) ∈ [(x2, x1), (x2, x3), (x4, x3), (x4, x5)]

x2 accesses x1 and x3, x4 accesses x3 and x5, and every possibility accesses itself (Figure 12 and Example 5.3).

@[reducible, inline]

abbrev HollidayMandelkern2024.P : Set Poss

P is the proposition that the coin lands 0, the embedding of {0}.

Equations

• HollidayMandelkern2024.P = Orthologic.embed {0}

@[reducible, inline]

abbrev HollidayMandelkern2024.nP : Set Poss

nP is ¬p.

Equations

• HollidayMandelkern2024.nP = Orthologic.orthoNeg HollidayMandelkern2024.frame HollidayMandelkern2024.P

@[reducible, inline]

abbrev HollidayMandelkern2024.bP : Set Poss

bP is □p.

Equations

• HollidayMandelkern2024.bP = Orthologic.Possibility.access.core HollidayMandelkern2024.P

@[reducible, inline]

abbrev HollidayMandelkern2024.bnP : Set Poss

bnP is □¬p.

Equations

• HollidayMandelkern2024.bnP = Orthologic.Possibility.access.core HollidayMandelkern2024.nP

@[reducible, inline]

abbrev HollidayMandelkern2024.dP : Set Poss

dP is ◇p.

Equations

• HollidayMandelkern2024.dP = Orthologic.diamond HollidayMandelkern2024.frame Orthologic.Possibility.access HollidayMandelkern2024.P

@[reducible, inline]

abbrev HollidayMandelkern2024.dnP : Set Poss

dnP is ◇¬p.

Equations

• HollidayMandelkern2024.dnP = Orthologic.diamond HollidayMandelkern2024.frame Orthologic.Possibility.access HollidayMandelkern2024.nP

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetP : DecidablePred fun (x : Poss) => x ∈ P

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetP = inferInstance

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetNP : DecidablePred fun (x : Poss) => x ∈ nP

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetNP = inferInstance

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetBP : DecidablePred fun (x : Poss) => x ∈ bP

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetBP = inferInstance

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetBnP : DecidablePred fun (x : Poss) => x ∈ bnP

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetBnP = inferInstance

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetDP : DecidablePred fun (x : Poss) => x ∈ dP

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetDP = inferInstance

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetDnP : DecidablePred fun (x : Poss) => x ∈ dnP

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetDnP = inferInstance

Example 4.33: the truth values of Figure 13

theorem HollidayMandelkern2024.mem_P (x : Poss) : x ∈ P ↔ x = x1 ∨ x = x2

theorem HollidayMandelkern2024.mem_nP (x : Poss) : x ∈ nP ↔ x = x4 ∨ x = x5

theorem HollidayMandelkern2024.mem_bP (x : Poss) : x ∈ bP ↔ x = x1

theorem HollidayMandelkern2024.mem_bnP (x : Poss) : x ∈ bnP ↔ x = x5

theorem HollidayMandelkern2024.mem_dP (x : Poss) : x ∈ dP ↔ x = x1 ∨ x = x2 ∨ x = x3

theorem HollidayMandelkern2024.mem_dnP (x : Poss) : x ∈ dnP ↔ x = x3 ∨ x = x4 ∨ x = x5

theorem HollidayMandelkern2024.mem_dP_inter_dnP (x : Poss) : x ∈ dP ∩ dnP ↔ x = x3

◇p ∧ ◇¬p holds only at the point of full uncertainty.

theorem HollidayMandelkern2024.mem_bP_disj_bnP (x : Poss) : x ∈ Orthologic.disj frame bP bnP ↔ x = x1 ∨ x = x5

□p ∨ □¬p holds exactly where something is known.

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetCoeFinset (s : Finset Poss) : DecidablePred fun (x : Poss) => x ∈ ↑s

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetCoeFinset s x = Finset.decidableMem x s

theorem HollidayMandelkern2024.card_regular : {s : Finset Poss | Orthologic.IsRegular frame ↑s}.card = 10

The compatibility frame has ten regular subsets (Example 4.11).

The desiderata of §2 on the Scale

theorem HollidayMandelkern2024.wittgenstein : nP ∩ dP = ∅ ∧ P ∩ dnP = ∅

Wittgenstein sentences of both orders are contradictions ((2) and (3)), by Proposition 4.27 applied to p and to ¬p, using that ¬¬p = p for the regular p.

theorem HollidayMandelkern2024.diamond_neg_not_entail_neg : x3 ∈ dnP ∧ x3 ∉ nP

At the coin whose outcome is unknown, ◇¬p does not entail ¬p (§1) and p does not entail □p (§2). In a Boolean algebra wittgenstein would force both entailments (Orthologic.wittgensteinLaw_iff_diamondHom_compl_le).

theorem HollidayMandelkern2024.not_entail_box : x2 ∈ P ∧ x2 ∉ bP

theorem HollidayMandelkern2024.not_derivable_dia_neg_neg : ¬Orthologic.EDerivable (Orthologic.ModalFormula.var ()).neg.dia (Orthologic.ModalFormula.var ()).neg

EO does not derive ◇¬p ⊢ ¬p: the Scale's regular propositions form an epistemic ortholattice (Proposition 4.27), so by soundness (Theorem 3.26) the derivation would make x3, which settles ◇¬p, settle ¬p (§1).

theorem HollidayMandelkern2024.not_derivable_box : ¬Orthologic.EDerivable (Orthologic.ModalFormula.var ()) (Orthologic.ModalFormula.var ()).box

EO does not derive p ⊢ □p: at x2, which settles p without knowing it (§2).

theorem HollidayMandelkern2024.distributivity_fails : x3 ∈ Orthologic.disj frame P nP ∩ (dP ∩ dnP) ∧ x3 ∉ Orthologic.disj frame (P ∩ dnP) (nP ∩ dP)

At x3 the conjunction (p ∨ ¬p) ∧ (◇p ∧ ◇¬p) holds but its distribution (p ∧ ◇¬p) ∨ (¬p ∧ ◇p) does not ((10) and Example 4.33).

theorem HollidayMandelkern2024.disjunctive_syllogism_fails : (∀ (x : Poss), x ∈ Orthologic.disj frame P bnP) ∧ x3 ∈ Orthologic.orthoNeg frame bnP ∧ x3 ∉ P

Disjunctive syllogism fails (13), since p ∨ □¬p is a logical truth and ¬□¬p holds at x3 while p does not.

theorem HollidayMandelkern2024.orthomodularity_fails : ¬IsOrthomodularLattice frame.Regular

The regular propositions of the Scale are not orthomodular ((21) and Example 3.20), since p entails ◇p but ◇p does not entail p ∨ (¬p ∧ ◇p), which fails at x3.

theorem HollidayMandelkern2024.not_isModularLattice : ¬IsModularLattice frame.Regular

Nor are they modular, since a modular ortholattice is orthomodular ([HM24] footnote 4), and so they are not distributive.

theorem HollidayMandelkern2024.pseudocomplementation_fails : ¬∀ (a b : frame.Regular), Disjoint a b → b ≤ aᶜ

Orthonegation is not pseudocomplementation (Example 3.20), since p ∧ ◇¬p = ⊥ although ◇¬p ≰ ¬p.

theorem HollidayMandelkern2024.deMorgan (x : Poss) : x ∈ dP ∩ dnP ↔ x ∈ Orthologic.orthoNeg frame (Orthologic.disj frame bnP bP)

De Morgan's law makes ◇p ∧ ◇¬p equivalent to ¬(□¬p ∨ □p) (29).

theorem HollidayMandelkern2024.not_known_either : x3 ∉ Orthologic.disj frame bnP bP

The disjunction □¬p ∨ □p is not a logical truth (30).

theorem HollidayMandelkern2024.diamond_P_not_subset : ¬dP ⊆ P

The diamond of p does not collapse to p (Theorem 5.7.4).

Example 4.42: levelwise classicality

inductive HollidayMandelkern2024.Level0 : Type

Level0 indexes the Boolean level B0 = {∅, p, ¬p, ⊤}.

• bot : Level0
• p : Level0
• np : Level0
• top : Level0

@[instance_reducible]

instance HollidayMandelkern2024.instDecidableEqLevel0 : DecidableEq Level0

Equations

• HollidayMandelkern2024.instDecidableEqLevel0 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HollidayMandelkern2024.instFintypeLevel0 : Fintype Level0

Equations

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

def HollidayMandelkern2024.Level0.set : Level0 → Set Poss

Level0.set sends each index to its proposition in B0.

Equations

• HollidayMandelkern2024.Level0.bot.set = ∅
• HollidayMandelkern2024.Level0.p.set = HollidayMandelkern2024.P
• HollidayMandelkern2024.Level0.np.set = HollidayMandelkern2024.nP
• HollidayMandelkern2024.Level0.top.set = Set.univ

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetSet (l : Level0) : DecidablePred fun (x : Poss) => x ∈ l.set

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetSet HollidayMandelkern2024.Level0.bot = HollidayMandelkern2024.instDecidablePredPossMemSetSet._aux_1
• HollidayMandelkern2024.instDecidablePredPossMemSetSet HollidayMandelkern2024.Level0.p = HollidayMandelkern2024.instDecidablePredPossMemSetSet._aux_3
• HollidayMandelkern2024.instDecidablePredPossMemSetSet HollidayMandelkern2024.Level0.np = HollidayMandelkern2024.instDecidablePredPossMemSetSet._aux_5
• HollidayMandelkern2024.instDecidablePredPossMemSetSet HollidayMandelkern2024.Level0.top = HollidayMandelkern2024.instDecidablePredPossMemSetSet._aux_7

inductive HollidayMandelkern2024.Level1 : Type

Level1 indexes the modal level B1, the eight propositions of Example 3.33.

• bot : Level1
• bp : Level1
• dnp : Level1
• dp : Level1
• bnp : Level1
• knownEither : Level1
• uncertain : Level1
• top : Level1

@[instance_reducible]

instance HollidayMandelkern2024.instDecidableEqLevel1 : DecidableEq Level1

Equations

• HollidayMandelkern2024.instDecidableEqLevel1 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HollidayMandelkern2024.instFintypeLevel1 : Fintype Level1

Equations

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

def HollidayMandelkern2024.Level1.set : Level1 → Set Poss

Level1.set sends each index to its proposition in B1.

Equations

• HollidayMandelkern2024.Level1.bot.set = ∅
• HollidayMandelkern2024.Level1.bp.set = HollidayMandelkern2024.bP
• HollidayMandelkern2024.Level1.dnp.set = HollidayMandelkern2024.dnP
• HollidayMandelkern2024.Level1.dp.set = HollidayMandelkern2024.dP
• HollidayMandelkern2024.Level1.bnp.set = HollidayMandelkern2024.bnP
• HollidayMandelkern2024.Level1.knownEither.set = Orthologic.disj HollidayMandelkern2024.frame HollidayMandelkern2024.bP HollidayMandelkern2024.bnP
• HollidayMandelkern2024.Level1.uncertain.set = HollidayMandelkern2024.dP ∩ HollidayMandelkern2024.dnP
• HollidayMandelkern2024.Level1.top.set = Set.univ

@[instance_reducible]

instance HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 (l : Level1) : DecidablePred fun (x : Poss) => x ∈ l.set

Equations

• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.bot = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_1
• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.bp = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_3
• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.dnp = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_5
• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.dp = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_7
• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.bnp = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_9
• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.knownEither = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_11
• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.uncertain = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_13
• HollidayMandelkern2024.instDecidablePredPossMemSetSet_1 HollidayMandelkern2024.Level1.top = HollidayMandelkern2024.instDecidablePredPossMemSetSet_1._aux_15

theorem HollidayMandelkern2024.level1_closed : (∀ (l : Level1), Orthologic.IsRegular frame l.set) ∧ (∀ (l : Level1), ∃ (m : Level1), ∀ (x : Poss), x ∈ Orthologic.orthoNeg frame l.set ↔ x ∈ m.set) ∧ ∀ (l m : Level1), ∃ (n : Level1), ∀ (x : Poss), x ∈ l.set ∩ m.set ↔ x ∈ n.set

B1 is closed under orthonegation and meet, and its members are regular.

theorem HollidayMandelkern2024.stratified_level0 (l m : Level0) : (∃ x ∈ l.set, ∃ y ∈ m.set, frame.compat x y) → ∃ z ∈ l.set, z ∈ m.set

Within B0, compatible witnesses of two propositions yield a common witness, so B0 is Boolean by the criterion of Proposition 4.39.

theorem HollidayMandelkern2024.stratified_level1 (l m : Level1) : (∃ x ∈ l.set, ∃ y ∈ m.set, frame.compat x y) → ∃ z ∈ l.set, z ∈ m.set

Within B1 the criterion of Proposition 4.39 holds too, so B1 is an eight-element Boolean algebra.

theorem HollidayMandelkern2024.not_stratified_across_levels : x2 ∈ P ∧ x3 ∈ dnP ∧ frame.compat x2 x3 ∧ ∀ (z : Poss), z ∉ P ∩ dnP

Across levels the criterion fails, since x2 settles p, x3 settles ◇¬p, the two are compatible, and nothing settles both.