Epistemic ortholattices

This file defines epistemic ortholattices, Holliday and Mandelkern's algebraic semantics for must and might. A modal ortholattice is an ortholattice with a necessity operator □ preserving ⊓ and ⊤, and its possibility operator ◇a = ¬□¬a preserves ⊔ and ⊥. It is T when □a ≤ a, and epistemic when it is T and satisfies Wittgenstein's Law ¬a ∧ ◇a = 0, which makes "p, but it might be that not p" a contradiction.

The law is what forces ortholattices on the account. In a Boolean algebra it makes ◇¬a entail ¬a, and with T it makes □ the identity. In an ortholattice, where a ⊓ b = ⊥ need not give b ≤ aᶜ, it is compatible with a non-trivial □.

Main definitions

• Orthologic.diamondHom: ◇a = ¬□¬a as a map preserving ⊔ and ⊥.
• Orthologic.WittgensteinLaw: ¬a ∧ ◇a = 0.

Main results

• Orthologic.wittgensteinLaw_iff: the law in the form a ∧ ◇¬a = 0.
• Orthologic.wittgensteinLaw_iff_eq_bot: with T, the law holds iff □a = 0 implies a = 0.
• Orthologic.WittgensteinLaw.disjoint_diamondHom_iterate: with T, a ∧ ◇ⁿ¬a = 0 for every n.
• Orthologic.diamondHom_le_box_diamondHom: 4 and a ≤ □◇a give 5, ◇a ≤ □◇a.
• Orthologic.wittgensteinLaw_iff_diamondHom_compl_le, Orthologic.WittgensteinLaw.eq_id: the collapse when ᶜ is a pseudocomplement, as in a Boolean algebra.

Implementation notes

The paper's modal ortholattice is not a new structure: □ is a bundled InfTopHom L L, since one lattice carries many modalities, and T is the hypothesis ∀ a, box a ≤ a. An epistemic ortholattice is the conjunction of T and WittgensteinLaw. The frame semantics producing epistemic ortholattices is Logic/Orthologic/ModalFrame.lean, and the logic they characterize is Logic/Orthologic/EpistemicOrthologic.lean.

References

• [HM24]

def Orthologic.diamondHom {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (box : InfTopHom L L) : SupBotHom L L

diamondHom box is the possibility operator ◇a = ¬□¬a of box, which preserves joins and ⊥ ([HM24] Definition 3.15 and Lemma 3.16).

Equations

• Orthologic.diamondHom box = { toFun := fun (a : L) => (box aᶜ)ᶜ, map_sup' := ⋯, map_bot' := ⋯ }

@[simp]

theorem Orthologic.diamondHom_apply {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} (a : L) : (diamondHom box) a = (box aᶜ)ᶜ

theorem Orthologic.diamondHom_iterate_compl {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} (n : ℕ) (a : L) : (⇑(diamondHom box))^[n] aᶜ = ((⇑box)^[n] a)ᶜ

Iterated possibility of a complement is the complement of iterated necessity, ◇ⁿ¬a = ¬□ⁿa.

theorem Orthologic.diamondHom_le_box_diamondHom {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} (h4 : ∀ (a : L), box a ≤ box (box a)) (hB : ∀ (a : L), a ≤ box ((diamondHom box) a)) (a : L) : (diamondHom box) a ≤ box ((diamondHom box) a)

With 4, □a ≤ □□a, the principle a ≤ □◇a yields 5, ◇a ≤ □◇a, so that □ makes an S5 modal ortholattice when it is also T ([HM24] Definition 3.19 and the proof of Theorem 5.7.3).

def Orthologic.WittgensteinLaw {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (box : InfTopHom L L) : Prop

Wittgenstein's Law ¬a ∧ ◇a = 0 makes "p is not the case but might be" a contradiction. With T it makes an ortholattice with □ an epistemic ortholattice ([HM24] Definition 3.18).

Equations

• Orthologic.WittgensteinLaw box = ∀ (a : L), Disjoint aᶜ ((Orthologic.diamondHom box) a)

theorem Orthologic.wittgensteinLaw_iff {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} : WittgensteinLaw box ↔ ∀ (a : L), Disjoint a (box a)ᶜ

Wittgenstein's Law is equivalent by involution to its form a ∧ ◇¬a = 0, "p, but it might be that not p" ([HM24] after Definition 3.18).

theorem Orthologic.WittgensteinLaw.disjoint_compl_box {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} (hW : WittgensteinLaw box) (a : L) : Disjoint a (box a)ᶜ

theorem Orthologic.WittgensteinLaw.eq_bot_of_box_eq_bot {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} (hW : WittgensteinLaw box) {a : L} (h : box a = ⊥) : a = ⊥

A proposition whose necessity is contradictory is itself contradictory ([HM24] Lemma 3.25, algebraically).

theorem Orthologic.wittgensteinLaw_iff_eq_bot {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} [IsOrtholattice L] (hT : ∀ (a : L), box a ≤ a) : WittgensteinLaw box ↔ ∀ (a : L), box a = ⊥ → a = ⊥

Over T, Wittgenstein's Law is equivalent to the principle of Lemma 3.25 that a proposition whose necessity is contradictory is itself contradictory ([HM24] after Lemma 3.25).

theorem Orthologic.WittgensteinLaw.disjoint_compl_box_iterate {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} [IsOrtholattice L] (hT : ∀ (a : L), box a ≤ a) (hW : WittgensteinLaw box) (n : ℕ) (a : L) : Disjoint a ((⇑box)^[n] a)ᶜ

Generalized Wittgenstein sentences are contradictions, since with T a ∧ ◇ⁿ¬a = 0 for every n, here in the form a ⊓ ¬□ⁿa = ⊥ ([HM24] Fact 3.28, algebraically).

theorem Orthologic.WittgensteinLaw.disjoint_diamondHom_iterate {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} [IsOrtholattice L] (hT : ∀ (a : L), box a ≤ a) (hW : WittgensteinLaw box) (n : ℕ) (a : L) : Disjoint a ((⇑(diamondHom box))^[n] aᶜ)

This is Fact 3.28 in the paper's form a ∧ ◇ⁿ¬a = 0.

The collapse under pseudocomplementation

The hypothesis hp says that ᶜ is a pseudocomplement, a ⊓ b = ⊥ → b ≤ aᶜ. It holds in every Boolean algebra (Disjoint.le_compl_left), and in an ortholattice it is equivalent to distributivity ([HM24] Proposition 3.7).

theorem Orthologic.wittgensteinLaw_iff_diamondHom_compl_le {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} (hp : ∀ (a b : L), Disjoint a b → b ≤ aᶜ) [IsOrtholattice L] : WittgensteinLaw box ↔ ∀ (a : L), (diamondHom box) aᶜ ≤ aᶜ

When ᶜ is a pseudocomplement, as in a Boolean algebra, Wittgenstein's Law says that ◇¬a entails ¬a, so treating p ∧ ◇¬p as a contradiction collapses might ([HM24] §1).

theorem Orthologic.WittgensteinLaw.eq_id {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] {box : InfTopHom L L} (hp : ∀ (a b : L), Disjoint a b → b ≤ aᶜ) (hW : WittgensteinLaw box) (hT : ∀ (a : L), box a ≤ a) : box = InfTopHom.id L

When ᶜ is a pseudocomplement, with T Wittgenstein's Law makes □ the identity, so a Boolean algebra has no non-trivial epistemic modality.