Documentation

Linglib.Studies.HollidayMandelkern2024

[HM24]: Possibility-Semantics Case Studies #

Concrete instantiations and paper-specific theorems from H&M 2024 "The Orthologic of Epistemic Modals" (JPL 2024). The general substrate (compatibility frames, ortholattice of regular sets, modal compat frames, T/epistemic frames) lives in Linglib/Semantics/Modality/Orthologic/{Frames,Modal}.lean (plus Linglib/Core/Order/Ortholattice.lean for the abstract typeclass); this file collects the paper's worked examples and the decide-checked predictions that depend on them.

What's formalized #

The five-possibility path frame Poss5 (Example 4.11, Figure 7).
The Epistemic Scale epistemicScale over Poss5 (Example 4.30, Figure 12; Example 4.33, Figure 13).
Ortholattice properties of the path-frame regular subsets: De Morgan-style negations, double negation, excluded middle, non-contradiction, the canonical distributivity failure at x₃.
Epistemic-scale predictions for p, □p, ◇p and their negations.
Wittgenstein's Law instantiated on the Epistemic Scale (Proposition 4.27).
Disjunctive-syllogism failure, orthomodularity failure, pseudocomplementation failure (paper §2 desiderata, §3.2 algebraic counterexamples — Example 3.20 in particular — re-derived in possibility semantics).
Within-level Boolean classicality vs. cross-level failure (§3.2.4).
Lifting from the two-world Boolean model W = {0, 1}, V(p) = {0} (Example 5.3, Lemma 5.4): worldlyA0/worldlyA1/worldlyI0/worldlyI1
- agreement of derived compat/access with pathFrame/epistemicScale
- truth of p/□p/◇p from world membership in A/I.

Out of scope (deferred) #

General lifting from arbitrary Boolean algebra B (Definition 5.1). The current file specializes B = ℘({0, 1}); the construction B^e = ⟨S, ◇, R⟩ for arbitrary B is unformalized and would belong in Semantics/Modality/Orthologic/Lifting.lean once added.
Theorem 5.7 (the embedding e_B : B → O(B^e) is a Boolean-algebra homomorphism into an epistemic ortholattice).
Lemma 5.8 (algebraic counterpart of Lemma 5.4 for arbitrary B).
Proposition 5.12 (the five inheritance principles for the image of e_B, including the Inheritance principle relevant to free choice).
Modal ortho-Boolean lattice typeclasses (Definitions 3.15-3.32) that would let within_level_distrib derive from the algebraic structure rather than decide on Poss5.
The Epistemic Grid for two propositional variables (Example 4.34, Figure 14) — natural sequel for engaging Hawke & Steinert-Threlkeld 2021 and Aloni-Incurvati-Schlöder 2023 on Inheritance.
Comparison theorems against the free-choice studies (the orthogonal phenomenon HM 2024 also addresses; HM's account predicts free-choice failure at x₁ — free_choice_fails_at_x1 — but the cross-paper agreement bridge is unwritten).

inductive HollidayMandelkern2024.Poss5 :

Five possibilities arranged in a path: x₁—x₂—x₃—x₄—x₅. The canonical 5-possibility example used by H&M for epistemic-modal applications. Note: Example 4.12 (Figure 9) shows two distinct 4-element frames realizing the smaller non-Boolean ortholattices O₆ and MO₂ from Figure 1 — the path frame is the canonical illustrative example, not the smallest non-Boolean instance. [HM24] Example 4.11, Figure 7.

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

Instances For

@[implicit_reducible]

instance HollidayMandelkern2024.instDecidableEqPoss5 :

DecidableEq Poss5

Equations

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

@[implicit_reducible]

instance HollidayMandelkern2024.instReprPoss5 :

Repr Poss5

Equations

HollidayMandelkern2024.instReprPoss5 = { reprPrec := HollidayMandelkern2024.instReprPoss5.repr }

def HollidayMandelkern2024.instReprPoss5.repr :

Poss5 → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance HollidayMandelkern2024.instInhabitedPoss5 :

Inhabited Poss5

Equations

HollidayMandelkern2024.instInhabitedPoss5 = { default := HollidayMandelkern2024.instInhabitedPoss5.default }

@[implicit_reducible]

instance HollidayMandelkern2024.instFintypePoss5 :

Fintype Poss5

Equations

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

def HollidayMandelkern2024.Poss5.compat :

Poss5 → Poss5 → Prop

Compatibility on the path frame: a possibility is compatible with itself and with each of its two neighbors.

Equations

Instances For

@[implicit_reducible]

instance HollidayMandelkern2024.instDecidableRelPoss5Compat :

DecidableRel Poss5.compat

Equations

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

def HollidayMandelkern2024.pathFrame :

Orthologic.CompatFrame Poss5

The path compatibility frame: adjacent possibilities are compatible.

Equations

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

Instances For

@[implicit_reducible]

instance HollidayMandelkern2024.instDecidableRelPoss5CompatPathFrame :

DecidableRel pathFrame.compat

Equations

HollidayMandelkern2024.instDecidableRelPoss5CompatPathFrame = HollidayMandelkern2024.instDecidableRelPoss5CompatPathFrame._aux_1

theorem HollidayMandelkern2024.neg_left (x : Poss5) :

Orthologic.orthoNeg pathFrame HollidayMandelkern2024.pLeft✝ x ↔ HollidayMandelkern2024.pRight✝ x

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

theorem HollidayMandelkern2024.neg_right (x : Poss5) :

Orthologic.orthoNeg pathFrame HollidayMandelkern2024.pRight✝ x ↔ HollidayMandelkern2024.pLeft✝ x

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

theorem HollidayMandelkern2024.neg_mid (x : Poss5) :

Orthologic.orthoNeg pathFrame HollidayMandelkern2024.pMid✝ x ↔ HollidayMandelkern2024.pEndpoints✝ x

theorem HollidayMandelkern2024.doubleNeg_left (x : Poss5) :

Orthologic.orthoNeg pathFrame (Orthologic.orthoNeg pathFrame HollidayMandelkern2024.pLeft✝) x ↔ HollidayMandelkern2024.pLeft✝ x

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

theorem HollidayMandelkern2024.excludedMiddle_left (x : Poss5) :

Orthologic.disj pathFrame HollidayMandelkern2024.pLeft✝ (Orthologic.orthoNeg pathFrame HollidayMandelkern2024.pLeft✝) x

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

theorem HollidayMandelkern2024.nonContradiction_left (x : Poss5) :

¬Orthologic.conj HollidayMandelkern2024.pLeft✝ (Orthologic.orthoNeg pathFrame HollidayMandelkern2024.pLeft✝) x

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

theorem HollidayMandelkern2024.distributivity_failure :

Orthologic.conj HollidayMandelkern2024.pMid✝ (Orthologic.disj pathFrame HollidayMandelkern2024.pLeft✝ HollidayMandelkern2024.pRight✝) Poss5.x3 ∧ ¬Orthologic.disj pathFrame (Orthologic.conj HollidayMandelkern2024.pMid✝ HollidayMandelkern2024.pLeft✝) (Orthologic.conj HollidayMandelkern2024.pMid✝ HollidayMandelkern2024.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. [HM24] Example 4.33 (the path-frame instantiation; the algebraic version is Example 3.20, Figure 3). Figure 8 enumerates the ten ◇-regular subsets of pathFrame; the distributivity discussion appears in the prose following Proposition 4.27.

theorem HollidayMandelkern2024.distrib_lhs_at_x3 :

Orthologic.conj HollidayMandelkern2024.pMid✝ (Orthologic.disj pathFrame HollidayMandelkern2024.pLeft✝ HollidayMandelkern2024.pRight✝) Poss5.x3

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

theorem HollidayMandelkern2024.distrib_rhs_at_x3 :

¬Orthologic.disj pathFrame (Orthologic.conj HollidayMandelkern2024.pMid✝ HollidayMandelkern2024.pLeft✝) (Orthologic.conj HollidayMandelkern2024.pMid✝ HollidayMandelkern2024.pRight✝) Poss5.x3

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

theorem HollidayMandelkern2024.x1_is_world :

Orthologic.IsWorld pathFrame Poss5.x1

x₁ is a world (maximal possibility).

theorem HollidayMandelkern2024.x5_is_world :

Orthologic.IsWorld pathFrame Poss5.x5

x₅ is a world.

theorem HollidayMandelkern2024.x3_not_world :

¬Orthologic.IsWorld pathFrame Poss5.x3

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

theorem HollidayMandelkern2024.regular_left :

Orthologic.IsRegular pathFrame HollidayMandelkern2024.pLeft✝

All propositions in the ortholattice are regular.

theorem HollidayMandelkern2024.regular_right :

Orthologic.IsRegular pathFrame HollidayMandelkern2024.pRight✝

theorem HollidayMandelkern2024.regular_mid :

Orthologic.IsRegular pathFrame HollidayMandelkern2024.pMid✝

theorem HollidayMandelkern2024.regular_empty :

Orthologic.IsRegular pathFrame ∅

theorem HollidayMandelkern2024.regular_full :

Orthologic.IsRegular pathFrame Set.univ

Lifting to regular propositions (typeclass-level reasoning) #

Pack the path-frame regular sets as pathFrame.Regular elements and demonstrate that the abstract OrthocomplementedLattice instance immediately delivers the De Morgan / excluded-middle / non-contradiction laws that are otherwise proved pointwise via decide. The set-membership theorems above remain available as the user-facing API; the …Reg versions below are the same propositions phrased in lattice notation.

def HollidayMandelkern2024.pLeftReg :

pathFrame.Regular

{x₁, x₂} packaged as a regular proposition.

Equations

HollidayMandelkern2024.pLeftReg = HollidayMandelkern2024.pathFrame.regOf HollidayMandelkern2024.pLeft✝ HollidayMandelkern2024.regular_left

Instances For

def HollidayMandelkern2024.pRightReg :

pathFrame.Regular

{x₄, x₅} packaged as a regular proposition.

Equations

HollidayMandelkern2024.pRightReg = HollidayMandelkern2024.pathFrame.regOf HollidayMandelkern2024.pRight✝ HollidayMandelkern2024.regular_right

Instances For

def HollidayMandelkern2024.pMidReg :

pathFrame.Regular

{x₃} packaged as a regular proposition.

Equations

HollidayMandelkern2024.pMidReg = HollidayMandelkern2024.pathFrame.regOf HollidayMandelkern2024.pMid✝ HollidayMandelkern2024.regular_mid

Instances For

theorem HollidayMandelkern2024.pLeftReg_compl_compl :

pLeftReg ᶜ ᶜ = pLeftReg

Double negation on pLeftReg from the typeclass: (pLeftReg)ᶜᶜ = pLeftReg. Replaces the pointwise doubleNeg_left proof — abstract typeclass result, no decide on Poss5.

theorem HollidayMandelkern2024.pLeftReg_sup_compl :

pLeftReg ⊔ pLeftReg ᶜ = ⊤

Excluded middle on pLeftReg from the typeclass: pLeftReg ⊔ pLeftRegᶜ = ⊤. Replaces the pointwise excludedMiddle_left proof.

theorem HollidayMandelkern2024.pLeftReg_inf_compl :

pLeftReg ⊓ pLeftReg ᶜ = ⊥

Non-contradiction on pLeftReg from the typeclass: pLeftReg ⊓ pLeftRegᶜ = ⊥. Replaces the pointwise nonContradiction_left proof.

theorem HollidayMandelkern2024.pLeftReg_compl_eq :

pLeftReg ᶜ = pRightReg

The orthocomplement of pLeftReg is pRightReg: (pLeftReg)ᶜ = pRightReg. Lattice-level statement of the pointwise neg_left theorem.

The Epistemic Scale is constructed from a 2-world model W = {0, 1} with V(p) = {0}. The possibilities are pairs (A, I) where ∅ ≠ A ⊆ I ⊆ W: - x₁ = ({0}, {0}) — settled that p, knows p - x₂ = ({0}, {0,1}) — settled that p, doesn't know - x₃ = ({0,1}, {0,1}) — nothing settled (full uncertainty) - x₄ = ({1}, {0,1}) — settled that ¬p, doesn't know - x₅ = ({1}, {1}) — settled that ¬p, knows ¬p

Compatibility: (a,i) ◇ (a',i') iff a ∩ a' ≠ ∅ ∧ a ⊆ i' ∧ a' ⊆ i.
Accessibility: (a,i) R (a',i') iff a ⊆ a' ∧ i' ⊆ i.
[holliday-mandelkern-2024] Definition 5.1, Example 5.3.

def HollidayMandelkern2024.Poss5.epistAccess :

Poss5 → Poss5 → Prop

Epistemic accessibility for the Epistemic Scale. R(x₁) = {x₁}, R(x₂) = {x₁,x₂,x₃}, R(x₃) = {x₃}, R(x₄) = {x₃,x₄,x₅}, R(x₅) = {x₅}. Note: Figure 12 shows dotted arrows that look symmetric on adjacents, but R as encoded here is the unique relation satisfying R-regularity, Reflexivity, and Knowability on the path compatibility frame — verified operationally by every Figure-13 truth-value matching decide.

Equations

Instances For

@[implicit_reducible]

instance HollidayMandelkern2024.instDecidableRelPoss5EpistAccess :

DecidableRel Poss5.epistAccess

Equations

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

def HollidayMandelkern2024.epistemicScale :

Orthologic.ModalCompatFrame Poss5

The epistemic scale frame. Compatibility is the path graph; accessibility captures epistemic access (refining information). [HM24] Example 4.30, Example 4.33.

Equations

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

Instances For

@[implicit_reducible]

instance HollidayMandelkern2024.instDecidableRelPoss5AccessEpistemicScale :

DecidableRel epistemicScale.access

Equations

HollidayMandelkern2024.instDecidableRelPoss5AccessEpistemicScale = HollidayMandelkern2024.instDecidableRelPoss5AccessEpistemicScale._aux_1

@[implicit_reducible]

instance HollidayMandelkern2024.instDecidableRelPoss5CompatEpistemicScale :

DecidableRel epistemicScale.compat

Equations

HollidayMandelkern2024.instDecidableRelPoss5CompatEpistemicScale = HollidayMandelkern2024.instDecidableRelPoss5CompatEpistemicScale._aux_1

Witnessing the epistemic-frame conditions #

epistemicScale satisfies all three conditions of HM 2024 Definition 4.26 (Reflexivity is in the structure; R-regularity and Knowability are decide-checked here). Bundled as epistemicCompatFrame, so HollidayMandelkern2024.wittgenstein_p and wittgenstein_neg_p collapse to one-line corollaries of the substrate Semantics.Modality.Orthologic.wittgensteinLaw (Proposition 4.27).

theorem HollidayMandelkern2024.epistemicScale_rRegular :

Orthologic.IsRRegular epistemicScale

epistemicScale is R-regular (Definition 4.20 / 4.26 clause).

theorem HollidayMandelkern2024.epistemicScale_knowable :

Orthologic.IsKnowable epistemicScale

epistemicScale is knowable (Definition 4.26 clause).

def HollidayMandelkern2024.epistemicCompatFrame :

Orthologic.EpistemicCompatFrame Poss5

The Epistemic Scale as an EpistemicCompatFrame — all three Definition 4.26 conditions assembled.

Equations

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

Instances For

def HollidayMandelkern2024.propP :

Equations

HollidayMandelkern2024.propP HollidayMandelkern2024.Poss5.x1 = True
HollidayMandelkern2024.propP HollidayMandelkern2024.Poss5.x2 = True
HollidayMandelkern2024.propP x = False

Instances For

@[implicit_reducible]

instance HollidayMandelkern2024.propP_dec :

DecidablePred propP

Equations

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

Verification of the truth values listed in Example 4.33 / Figure 13.

@[simp]

theorem HollidayMandelkern2024.box_p (x : Poss5) :

Orthologic.box epistemicScale propP x ↔ HollidayMandelkern2024.boxP✝ x

□p = {x₁}: only x₁ knows p (R(x₁) = {x₁} ⊆ V(p)).

@[simp]

theorem HollidayMandelkern2024.neg_p (x : Poss5) :

Orthologic.orthoNeg pathFrame propP x ↔ HollidayMandelkern2024.negP✝ x

¬p = {x₄, x₅}: the orthocomplement of V(p).

@[simp]

theorem HollidayMandelkern2024.box_neg_p (x : Poss5) :

Orthologic.box epistemicScale (Orthologic.orthoNeg pathFrame propP) x ↔ HollidayMandelkern2024.boxNegP✝ x

□¬p = {x₅}: only x₅ knows ¬p.

@[simp]

theorem HollidayMandelkern2024.diamond_p (x : Poss5) :

Orthologic.diamond epistemicScale propP x ↔ HollidayMandelkern2024.diamP✝ x

◇p = {x₁, x₂, x₃}: p might be true at x₁, x₂, and x₃.

@[simp]

theorem HollidayMandelkern2024.diamond_neg_p (x : Poss5) :

Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP) x ↔ HollidayMandelkern2024.diamNegP✝ x

◇¬p = {x₃, x₄, x₅}: ¬p might be true at x₃, x₄, and x₅.

theorem HollidayMandelkern2024.uncertainty_at_x3 :

Orthologic.conj (Orthologic.diamond epistemicScale propP) (Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP)) Poss5.x3

◇p ∧ ◇¬p = {x₃}: only the point of full uncertainty.

The motivating examples from §1–2 of the paper: epistemic possibility does not collapse to classical negation, and truth does not collapse to knowledge.

theorem HollidayMandelkern2024.diamond_neg_not_entail_neg :

Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP) Poss5.x3 ∧ ¬Orthologic.orthoNeg pathFrame propP Poss5.x3

◇¬p does NOT entail ¬p: x₃ makes "it might not be raining" true but does not settle "it's not raining." This is the core motivation for the entire paper — in classical logic, ◇¬p → ¬p, but this fails in possibility semantics. [HM24] §1.

theorem HollidayMandelkern2024.p_not_entail_box_p :

propP Poss5.x2 ∧ ¬Orthologic.box epistemicScale propP Poss5.x2

p does NOT entail □p: x₂ makes p true without knowing p. "It's raining" does not mean "It must be raining." Failure of necessitation for non-logical truths. [HM24] §2.

Wittgenstein's Law: ¬A ∩ ◇A = ∅. "It's raining and it might not be raining" is contradictory. In possibility semantics, if x settles ¬A (all compatible possibilities fail A), then x cannot also make ◇A true (which requires a compatible possibility in □¬A's complement). [HM24] Proposition 4.27.

Both theorems below are **structural corollaries** of the substrate
`wittgensteinLaw` on epistemic compatibility frames — no per-frame
`decide` is needed. The Poss5-specific content was reduced (above) to
`epistemicCompatFrame`'s `decide`-checked R-regularity + Knowability;
the algebraic identity itself comes from substrate.

theorem HollidayMandelkern2024.wittgenstein_p (x : Poss5) :

¬Orthologic.conj (Orthologic.orthoNeg pathFrame propP) (Orthologic.diamond epistemicScale propP) x

¬p ∧ ◇p = ∅: "p is false and p might be true" is contradictory. One-line corollary of EpistemicCompatFrame.wittgensteinLaw applied to propP.

theorem HollidayMandelkern2024.wittgenstein_neg_p (x : Poss5) :

¬Orthologic.conj (Orthologic.orthoNeg pathFrame (Orthologic.orthoNeg pathFrame propP)) (Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP)) x

p ∧ ◇¬p = ∅: "p is true and ¬p might be true" is contradictory. One-line corollary: take A := orthoNeg pathFrame propP in EpistemicCompatFrame.wittgensteinLaw.

theorem HollidayMandelkern2024.epistemic_distrib_failure :

have pDisj := Orthologic.disj pathFrame propP (Orthologic.orthoNeg pathFrame propP); have uncertainty := Orthologic.conj (Orthologic.diamond epistemicScale propP) (Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP)); have lhs := Orthologic.conj pDisj uncertainty; have rhs := Orthologic.disj pathFrame (Orthologic.conj propP uncertainty) (Orthologic.conj (Orthologic.orthoNeg pathFrame propP) uncertainty); lhs Poss5.x3 ∧ ¬rhs Poss5.x3

Distributivity fails across epistemic levels: (p ∨ ¬p) ∧ (◇p ∧ ◇¬p) is true at x₃, but (p ∧ ◇p ∧ ◇¬p) ∨ (¬p ∧ ◇p ∧ ◇¬p) is not. The partial possibility x₃ verifies the disjunction without committing to either disjunct — both disjuncts are empty by Wittgenstein's Law (p ∧ ◇¬p = ∅ and ¬p ∧ ◇p = ∅). [HM24] Example 3.20 (algebraic), Example 4.33 (possibility-semantic instantiation).

Free choice disjunction: ◇(A ∨ B) entails ◇A ∧ ◇B.

HM 2024 do not aim to predict free choice — see footnote 33 (page 890):
"We will not try to adjudicate that complicated topic here." The closest
paper-anchored result is the **Inheritance principle**
(Proposition 5.12.3, page 885): `(U ∨ ◇V) ∧ □V ⊆ ◇(U ∨ V)`.

On the Epistemic Scale, full free choice fails because the path frame
is non-Boolean. The pattern derivable here is partial: it holds at x₃
(full uncertainty, where both p and ¬p remain epistemically possible)
but fails at x₁ (knows p, where ◇(p ∨ ¬p) is trivially true but
◇¬p is false).

For a deontic-modal account where free choice DOES emerge — via
pragmatic enrichment in BSML — see `Studies/Aloni2022.lean`.
The contrast is *modal-flavor-dependent* rather than directly contradictory:
Aloni 2022 derives FC for permission-flavored ◇, HM 2024 predicts FC failure
for epistemic-flavored ◇.

Free choice holds at x₃: ◇(p ∨ ¬p) → ◇p ∧ ◇¬p.

Free choice FAILS at x₁: ◇(p ∨ ¬p) is true but ◇¬p is false. x₁ knows p, so while the disjunction is trivially possible, the individual disjunct ¬p is not epistemically accessible.

theorem HollidayMandelkern2024.T_axiom_p (x : Poss5) :

Orthologic.box epistemicScale propP x → propP x

T axiom: □A entails A (knowledge is factive). [HM24] Proposition 4.25.

theorem HollidayMandelkern2024.box_implies_diamond (x : Poss5) :

Orthologic.box epistemicScale propP x → Orthologic.diamond epistemicScale propP x

□p entails ◇p (knowledge implies epistemic possibility).

Disjunctive syllogism ({p ∨ q, ¬q} ⊨ p) fails for epistemic modals: "Either the dog is inside or it must be outside; it's not the case that it must be outside; therefore it is inside." The tautological first premise carries no information. [HM24] §2.3.

theorem HollidayMandelkern2024.disjSyllogism_fails :

have mustNotP := Orthologic.box epistemicScale (Orthologic.orthoNeg pathFrame propP); have pOrMustNotP := Orthologic.disj pathFrame propP mustNotP; have notMustNotP := Orthologic.orthoNeg pathFrame mustNotP; pOrMustNotP Poss5.x3 ∧ notMustNotP Poss5.x3 ∧ ¬propP Poss5.x3

Disjunctive syllogism fails: p ∨ □¬p and ¬□¬p both hold at x₃ (full uncertainty) but p does not.

Orthomodularity (if φ ⊨ ψ then ψ ⊨ φ ∨ (¬φ ∧ ψ)) fails. Since p ⊨ ◇p, orthomodularity would give ◇p ⊨ p ∨ (¬p ∧ ◇p). But ¬p ∧ ◇p = ⊥ by Wittgenstein's Law, so this collapses to ◇p ⊨ p — absurd. [HM24] §2.4.

theorem HollidayMandelkern2024.p_entails_diamond (x : Poss5) (h : propP x) :

Orthologic.diamond epistemicScale propP x

p entails ◇p: truth implies epistemic possibility. Follows from T (T_axiom_general) + duality (per HM 2024 §2.4 p. 839, derivable in their full system).

theorem HollidayMandelkern2024.orthomodularity_fails :

have diamP := Orthologic.diamond epistemicScale propP; have rhs := Orthologic.disj pathFrame propP (Orthologic.conj (Orthologic.orthoNeg pathFrame propP) diamP); diamP Poss5.x3 ∧ ¬rhs Poss5.x3

Orthomodularity fails: ◇p holds at x₃ but p ∨ (¬p ∧ ◇p) does not (since ¬p ∧ ◇p = ⊥ by Wittgenstein, this reduces to p).

Pseudocomplementation (a ∧ b = 0 → b ≤ ¬a) fails. In a Boolean algebra, ¬a is the greatest element disjoint from a. In an ortholattice this need not hold: p ∧ ◇¬p = ⊥ (Wittgenstein) but ◇¬p ≰ ¬p. This is the algebraic root of why ◇¬p ≠ ¬p. [HM24] Lemma 3.6 (algebraic statement), Example 3.20 (concrete failure).

theorem HollidayMandelkern2024.pseudocomplementation_fails :

have negP := Orthologic.orthoNeg pathFrame propP; have diamNegP := Orthologic.diamond epistemicScale negP; (∀ (x : Poss5), ¬Orthologic.conj propP diamNegP x) ∧ diamNegP Poss5.x3 ∧ ¬negP Poss5.x3

Pseudocomplementation fails: p ∧ ◇¬p = ⊥ but ◇¬p ≰ ¬p. x₃ witnesses ◇¬p (might not be raining) without witnessing ¬p.

Level-wise classicality: classical reasoning is safe within an epistemic level but dangerous across levels. The subortholattice B₀ = {⊥, p, ¬p, ⊤} is a four-element Boolean algebra; B₁ (generated by applying □ and ◇ to B₀) is an eight-element Boolean algebra. Distributivity only fails when mixing levels. [HM24] §3.2.4.

theorem HollidayMandelkern2024.within_level_distrib (x : Poss5) :

have dp := Orthologic.diamond epistemicScale propP; have dnp := Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP); Orthologic.conj dp (Orthologic.disj pathFrame dnp dp) x ↔ Orthologic.disj pathFrame (Orthologic.conj dp dnp) (Orthologic.conj dp dp) x

Within-level distributivity (B₁): ◇p ∧ (◇¬p ∨ ◇p) = (◇p ∧ ◇¬p) ∨ (◇p ∧ ◇p). All operands from the same epistemic level → distributivity holds.

theorem HollidayMandelkern2024.cross_level_distrib_fails :

have dp := Orthologic.diamond epistemicScale propP; have negP := Orthologic.orthoNeg pathFrame propP; have lhs := Orthologic.conj dp (Orthologic.disj pathFrame propP negP); have rhs := Orthologic.disj pathFrame (Orthologic.conj dp propP) (Orthologic.conj dp negP); lhs Poss5.x3 ∧ ¬rhs Poss5.x3

Cross-level failure: ◇p ∧ (p ∨ ¬p) ≠ (◇p ∧ p) ∨ (◇p ∧ ¬p). ◇p is from B₁ but p, ¬p are from B₀. At x₃ the LHS is true (◇p and excluded middle both hold) but the RHS is false (both disjuncts are empty by Wittgenstein's Law).

Lifting construction specialized to the two-world Boolean algebra B = ℘({0, 1}) with valuation V(p) = {0}. The five possibilities are pairs (A, I) with ∅ ≠ A ⊆ I ⊆ W:

- 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

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

The general lifting from an arbitrary Boolean algebra `B` (Def 5.1)
is unformalized; this section verifies the agreement of the derived
`liftedCompat`/`liftedAccess` with the stipulated `pathFrame`/
`epistemicScale` for the W={0,1} case.

def HollidayMandelkern2024.worldlyA0 :

Poss5 → Bool

World 0 (the p-world) is in the actuality set A(x).

Equations

Instances For

def HollidayMandelkern2024.worldlyA1 :

Poss5 → Bool

World 1 (the ¬p-world) is in the actuality set A(x).

Equations

Instances For

def HollidayMandelkern2024.worldlyI0 :

Poss5 → Bool

World 0 is in the information set I(x).

Equations

Instances For

def HollidayMandelkern2024.worldlyI1 :

Poss5 → Bool

World 1 is in the information set I(x).

Equations

Instances For

def HollidayMandelkern2024.liftedCompat (x y : Poss5) :

Bool

Compatibility derived from lifting: (A,I) ◇ (A',I') iff A ∩ A' ≠ ∅ ∧ A ⊆ I' ∧ A' ⊆ I. [HM24] Definition 5.1.2.

Equations

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

Instances For

def HollidayMandelkern2024.liftedAccess (x y : Poss5) :

Bool

Accessibility derived from lifting: (A,I) R (A',I') iff A ⊆ A' ∧ I' ⊆ I (refining = expanding actuality, shrinking information). [HM24] Definition 5.1.3.

Equations

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

Instances For

theorem HollidayMandelkern2024.compat_from_lifting (x y : Poss5) :

epistemicScale.compat x y ↔ liftedCompat x y = true

The epistemic scale's compatibility matches the lifting construction.

theorem HollidayMandelkern2024.access_from_lifting (x y : Poss5) :

epistemicScale.access x y ↔ liftedAccess x y = true

The epistemic scale's accessibility matches the lifting construction.

[HM24] 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)

@[simp]

theorem HollidayMandelkern2024.boolean_truth_from_worlds (x : Poss5) :

propP x ↔ worldlyA1 x = false

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

@[simp]

theorem HollidayMandelkern2024.box_truth_from_worlds (x : Poss5) :

Orthologic.box epistemicScale propP x ↔ worldlyI1 x = false

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

@[simp]

theorem HollidayMandelkern2024.diamond_truth_from_worlds (x : Poss5) :

Orthologic.diamond epistemicScale propP x ↔ worldlyA0 x = true

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

HM 2024's formal predictions agree with the empirical patterns recorded in the prior literature. These bridges close the loop between Yalcin's embedding diagnostic, Mandelkern's distributivity-failure intuition, Klinedinst & Rothschild's disjunctive-syllogism failure, and HM's formal theorems on the Epistemic Scale.

Each agreement bundles **two** components: (i) the proof-bearing
structural witness from this file, exhibiting the prediction as a
Lean theorem, and (ii) the literal `:= rfl` over the sibling's Bool
table, serving as a drift sentry — if either side later changes, the
`rfl` will fail loudly.

HM 2024 predicts that Wittgenstein sentences are infelicitous — matching Yalcin (2007). Witnesses: wittgenstein_p (¬p ∧ ◇p = ∅) and wittgenstein_neg_p (p ∧ ◇¬p = ∅), both reducing to substrate wittgensteinLaw (Proposition 4.27).

theorem HollidayMandelkern2024.hm_predicts_classical_infelicitous :

(∀ (x : Poss5), ¬Orthologic.conj propP (Orthologic.orthoNeg pathFrame propP) x) ∧ Yalcin2007.felicitousUnderEmbedding Yalcin2007.SentenceType.classical = false

HM 2024 predicts that classical contradictions are infelicitous — matching Yalcin (2007). Witness: p ∧ ¬p = ∅ on the Epistemic Scale, structurally guaranteed by the inf_compl_eq_bot ortholattice axiom on pathFrame.Regular.

theorem HollidayMandelkern2024.hm_predicts_distrib_failure :

(have pDisj := Orthologic.disj pathFrame propP (Orthologic.orthoNeg pathFrame propP); have uncertainty := Orthologic.conj (Orthologic.diamond epistemicScale propP) (Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP)); have lhs := Orthologic.conj pDisj uncertainty; have rhs := Orthologic.disj pathFrame (Orthologic.conj propP uncertainty) (Orthologic.conj (Orthologic.orthoNeg pathFrame propP) uncertainty); lhs Poss5.x3 ∧ ¬rhs Poss5.x3) ∧ Mandelkern2019.distribFailure.lhsFelicitous = true ∧ Mandelkern2019.distribFailure.rhsFelicitous = false

HM 2024 predicts Mandelkern (2019)'s distributivity-failure pattern: LHS felicitous, RHS infelicitous. Witness: epistemic_distrib_failure (§8) — proves (p ∨ ¬p) ∧ (◇p ∧ ◇¬p) true at x₃ but (p ∧ ◇p ∧ ◇¬p) ∨ (¬p ∧ ◇p ∧ ◇¬p) false at x₃.

theorem HollidayMandelkern2024.hm_predicts_disjSyll_failure :

(have mustNotP := Orthologic.box epistemicScale (Orthologic.orthoNeg pathFrame propP); have pOrMustNotP := Orthologic.disj pathFrame propP mustNotP; have notMustNotP := Orthologic.orthoNeg pathFrame mustNotP; pOrMustNotP Poss5.x3 ∧ notMustNotP Poss5.x3 ∧ ¬propP Poss5.x3) ∧ KlinedinstRothschild2012.disjSyllFailure.valid = false

HM 2024 predicts Klinedinst & Rothschild (2012)'s disjunctive-syllogism failure: from p ∨ □¬p and ¬□¬p, the conclusion p does not follow. Witness: disjSyllogism_fails (§11) exhibits x₃ as the joint witness where both premises hold but the conclusion fails.

HM 2024's wittgenstein_p and wittgenstein_neg_p (§7) jointly say that BOTH ¬p ∧ ◇p and p ∧ ◇¬p are infelicitous on every state of the Epistemic Scale — Wittgenstein's Law is symmetric in possibility semantics.

Veltman 1996's update semantics predicts the opposite: order MATTERS.
`Semantics.Dynamic.UpdateSemantics.Basic.might_order_matters`
proves that `p ∧ might ¬p` collapses to ∅ but `might ¬p ∧ p` does not,
on any state with `Nontrivial W`.

Both files acknowledge this divergence in prose; the theorem below
makes the structural contradiction Lean-checkable — a
cross-framework contradiction stated at theorem level.
Per linglib's mission: theoretical incompatibilities should be visible
at theorem level, not docstring level.

HM 2024 predicts Wittgenstein collapse SYMMETRICALLY: both orderings are infelicitous at every Poss5 state. Bundles wittgenstein_p and wittgenstein_neg_p from §7.

theorem HollidayMandelkern2024.hm_veltman_disagree_on_wittgenstein_symmetry :

(∀ (x : Poss5), ¬Orthologic.conj (Orthologic.orthoNeg pathFrame propP) (Orthologic.diamond epistemicScale propP) x ∧ ¬Orthologic.conj (Orthologic.orthoNeg pathFrame (Orthologic.orthoNeg pathFrame propP)) (Orthologic.diamond epistemicScale (Orthologic.orthoNeg pathFrame propP)) x) ∧ ∃ (p : Bool → Prop) (x : DecidablePred p) (s : Semantics.Dynamic.UpdateSemantics.State Bool), (Semantics.Dynamic.UpdateSemantics.Update.prop p).conj (Semantics.Dynamic.UpdateSemantics.Update.prop fun (w : Bool) => ¬p w).might s = ∅ ∧ Set.Nonempty ((Semantics.Dynamic.UpdateSemantics.Update.prop fun (w : Bool) => ¬p w).might.conj (Semantics.Dynamic.UpdateSemantics.Update.prop p) s)

Cross-framework contradiction (HM 2024 vs Veltman 1996): HM predicts that both Wittgenstein orderings collapse to ∅ on every Poss5 state (hm_wittgenstein_symmetric), while Veltman predicts that on any Nontrivial W there is a state where p ∧ might ¬p collapses but might ¬p ∧ p survives (might_order_matters). The two frameworks disagree at the theorem level on whether Wittgenstein's Law is symmetric — instantiated at W := Bool.