The epistemic orthologic

This file defines Holliday and Mandelkern's epistemic orthologics and proves the least one, EO, sound and complete for epistemic ortholattices. The modal language adds a necessity modal □ to the language of orthologic, with ◇φ := ¬□¬φ. An epistemic orthologic is an orthologic under which □ is monotone, preserves ∧ and ⊤, and is factive, and which satisfies Wittgenstein's Law ¬φ ∧ ◇φ ⊢ ⊥. Its Lindenbaum–Tarski algebra is an epistemic ortholattice, so the algebraic consequences of the law hold in every epistemic orthologic, and a consequence holding in every epistemic ortholattice is derivable in EO.

Main definitions

• Orthologic.IsEpistemicOrthologic F box: the rules for □ on an orthologic.
• Orthologic.LindenbaumTarski.boxHom: □ on the Lindenbaum–Tarski algebra.
• Orthologic.ModalFormula, Orthologic.EDerivable: the modal language and the least epistemic orthologic EO.
• Orthologic.ModalFormula.eval: the value of a formula in an ortholattice with a necessity operator.

Main results

• Orthologic.IsEpistemicOrthologic.le_bot_of_box_le_bot: if □φ ⊢ ⊥ then φ ⊢ ⊥.
• Orthologic.IsEpistemicOrthologic.inf_dia_iterate_compl_le: φ ∧ ◇ⁿ¬φ ⊢ ⊥ for every n.
• Orthologic.ModalFormula.derivable_iff: EO is sound and complete for epistemic ortholattices.

References

• [HM24]

Epistemic orthologics

class Orthologic.IsEpistemicOrthologic (F : Type u_1) [Preorder F] [Top F] [Min F] [Compl F] (box : F → F) : Prop

An orthologic with a necessity operator box is an epistemic orthologic when box is monotone, preserves ∧ and ⊤, and is factive, and ¬φ ∧ ◇φ ⊢ ⊥ holds with ◇φ = ¬□¬φ and ⊥ = ¬⊤ ([HM24] Definition 3.24).

• box_mono {φ ψ : F} : φ ≤ ψ → box φ ≤ box ψ
• box_inf_le (φ ψ : F) : box φ ⊓ box ψ ≤ box (φ ⊓ ψ)
• le_box_top (φ : F) : φ ≤ box ⊤
• box_le (φ : F) : box φ ≤ φ
• wittgenstein (φ : F) : φᶜ ⊓ (box φᶜ)ᶜ ≤ ⊤ᶜ

def Orthologic.LindenbaumTarski.boxHom {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (box : F → F) [IsEpistemicOrthologic F box] : InfTopHom (LindenbaumTarski F) (LindenbaumTarski F)

□ on the Lindenbaum–Tarski algebra of an epistemic orthologic, which preserves ⊓ and ⊤.

Equations

• Orthologic.LindenbaumTarski.boxHom box = { toFun := Quotient.map box ⋯, map_inf' := ⋯, map_top' := ⋯ }

theorem Orthologic.LindenbaumTarski.boxHom_mk {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (box : F → F) [IsEpistemicOrthologic F box] (φ : F) : (boxHom box) (toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) φ) = toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) (box φ)

theorem Orthologic.LindenbaumTarski.boxHom_le {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (box : F → F) [IsEpistemicOrthologic F box] (a : LindenbaumTarski F) : (boxHom box) a ≤ a

theorem Orthologic.LindenbaumTarski.wittgensteinLaw_boxHom {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (box : F → F) [IsEpistemicOrthologic F box] : WittgensteinLaw (boxHom box)

The Lindenbaum–Tarski algebra of an epistemic orthologic is an epistemic ortholattice.

theorem Orthologic.LindenbaumTarski.mk_dia_iterate {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (box : F → F) [IsEpistemicOrthologic F box] (n : ℕ) (φ : F) : toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) ((fun (ψ : F) => (box ψᶜ)ᶜ)^[n] φ) = (⇑(diamondHom (boxHom box)))^[n] (toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) φ)

theorem Orthologic.IsEpistemicOrthologic.le_bot_of_box_le_bot {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] {box : F → F} [IsEpistemicOrthologic F box] {φ : F} (h : box φ ≤ ⊤ᶜ) : φ ≤ ⊤ᶜ

In an epistemic orthologic a proposition whose necessity is contradictory is itself contradictory ([HM24] Lemma 3.25).

theorem Orthologic.IsEpistemicOrthologic.inf_dia_iterate_compl_le {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] {box : F → F} [IsEpistemicOrthologic F box] (n : ℕ) (φ : F) : φ ⊓ (fun (ψ : F) => (box ψᶜ)ᶜ)^[n] φᶜ ≤ ⊤ᶜ

In an epistemic orthologic generalized Wittgenstein sentences are contradictions, φ ∧ ◇ⁿ¬φ ⊢ ⊥ for every n ([HM24] Fact 3.28).

The least epistemic orthologic

inductive Orthologic.ModalFormula (Var : Type u_1) : Type u_1

Formulas of the modal language over a variable type Var, with ⊥ and ◇ defined ([HM24] Definition 3.21).

• top {Var : Type u_1} : ModalFormula Var
• var {Var : Type u_1} (p : Var) : ModalFormula Var
• neg {Var : Type u_1} (φ : ModalFormula Var) : ModalFormula Var
• and {Var : Type u_1} (φ ψ : ModalFormula Var) : ModalFormula Var
• box {Var : Type u_1} (φ : ModalFormula Var) : ModalFormula Var

def Orthologic.ModalFormula.bot {Var : Type u_1} : ModalFormula Var

Falsum is ¬⊤.

Equations

• Orthologic.ModalFormula.bot = Orthologic.ModalFormula.top.neg

def Orthologic.ModalFormula.dia {Var : Type u_1} (φ : ModalFormula Var) : ModalFormula Var

Possibility is ◇φ := ¬□¬φ.

Equations

• φ.dia = φ.neg.box.neg

inductive Orthologic.EDerivable {Var : Type u_1} : ModalFormula Var → ModalFormula Var → Prop

Consequence in the least epistemic orthologic EO is generated by Goldblatt's ten rules for orthologic, rules making □ monotone, preserve ∧ and ⊤, and factive, and Wittgenstein's Law ([HM24] Definition 3.24).

• top_intro {Var : Type u_1} (φ : ModalFormula Var) : EDerivable φ ModalFormula.top
• refl {Var : Type u_1} (φ : ModalFormula Var) : EDerivable φ φ
• and_le_left {Var : Type u_1} (φ ψ : ModalFormula Var) : EDerivable (φ.and ψ) φ
• and_le_right {Var : Type u_1} (φ ψ : ModalFormula Var) : EDerivable (φ.and ψ) ψ
• le_negNeg {Var : Type u_1} (φ : ModalFormula Var) : EDerivable φ φ.neg.neg
• negNeg_le {Var : Type u_1} (φ : ModalFormula Var) : EDerivable φ.neg.neg φ
• contradiction {Var : Type u_1} (φ ψ : ModalFormula Var) : EDerivable (φ.and φ.neg) ψ
• trans {Var : Type u_1} {φ ψ χ : ModalFormula Var} : EDerivable φ ψ → EDerivable ψ χ → EDerivable φ χ
• le_and {Var : Type u_1} {φ ψ χ : ModalFormula Var} : EDerivable φ ψ → EDerivable φ χ → EDerivable φ (ψ.and χ)
• neg_le_neg {Var : Type u_1} {φ ψ : ModalFormula Var} : EDerivable φ ψ → EDerivable ψ.neg φ.neg
• box_mono {Var : Type u_1} {φ ψ : ModalFormula Var} : EDerivable φ ψ → EDerivable φ.box ψ.box
• box_and {Var : Type u_1} (φ ψ : ModalFormula Var) : EDerivable (φ.box.and ψ.box) (φ.and ψ).box
• le_box_top {Var : Type u_1} (φ : ModalFormula Var) : EDerivable φ ModalFormula.top.box
• box_le {Var : Type u_1} (φ : ModalFormula Var) : EDerivable φ.box φ
• wittgenstein {Var : Type u_1} (φ : ModalFormula Var) : EDerivable (φ.neg.and φ.dia) ModalFormula.bot

@[instance_reducible]

instance Orthologic.ModalFormula.instTop {Var : Type u_1} : Top (ModalFormula Var)

The connectives of the modal language share the symbols of the lattice operations, as in [HM24].

Equations

• Orthologic.ModalFormula.instTop = { top := Orthologic.ModalFormula.top }

@[instance_reducible]

instance Orthologic.ModalFormula.instMin {Var : Type u_1} : Min (ModalFormula Var)

Equations

• Orthologic.ModalFormula.instMin = { min := Orthologic.ModalFormula.and }

@[instance_reducible]

instance Orthologic.ModalFormula.instCompl {Var : Type u_1} : Compl (ModalFormula Var)

Equations

• Orthologic.ModalFormula.instCompl = { compl := Orthologic.ModalFormula.neg }

@[instance_reducible]

instance Orthologic.ModalFormula.instPreorder {Var : Type u_1} : Preorder (ModalFormula Var)

Consequence in EO is a preorder, reflexivity and cut.

Equations

• Orthologic.ModalFormula.instPreorder = { le := Orthologic.EDerivable, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

instance Orthologic.ModalFormula.instIsOrthologic {Var : Type u_1} : IsOrthologic (ModalFormula Var)

instance Orthologic.ModalFormula.instIsEpistemicOrthologicBox {Var : Type u_1} : IsEpistemicOrthologic (ModalFormula Var) box

Evaluation, soundness and completeness

def Orthologic.ModalFormula.eval {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (bx : InfTopHom L L) (v : Var → L) : ModalFormula Var → L

The value of a formula in an ortholattice with a necessity operator under a valuation ([HM24] Definition 3.22).

Equations

• Orthologic.ModalFormula.eval bx v Orthologic.ModalFormula.top = ⊤
• Orthologic.ModalFormula.eval bx v (Orthologic.ModalFormula.var p) = v p
• Orthologic.ModalFormula.eval bx v φ.neg = (Orthologic.ModalFormula.eval bx v φ)ᶜ
• Orthologic.ModalFormula.eval bx v (φ.and ψ) = Orthologic.ModalFormula.eval bx v φ ⊓ Orthologic.ModalFormula.eval bx v ψ
• Orthologic.ModalFormula.eval bx v φ.box = bx (Orthologic.ModalFormula.eval bx v φ)

@[simp]

theorem Orthologic.ModalFormula.eval_top {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (bx : InfTopHom L L) (v : Var → L) : eval bx v ⊤ = ⊤

@[simp]

theorem Orthologic.ModalFormula.eval_var {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (bx : InfTopHom L L) (v : Var → L) (p : Var) : eval bx v (var p) = v p

@[simp]

theorem Orthologic.ModalFormula.eval_compl {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (bx : InfTopHom L L) (v : Var → L) (φ : ModalFormula Var) : eval bx v φᶜ = (eval bx v φ)ᶜ

@[simp]

theorem Orthologic.ModalFormula.eval_inf {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (bx : InfTopHom L L) (v : Var → L) (φ ψ : ModalFormula Var) : eval bx v (φ ⊓ ψ) = eval bx v φ ⊓ eval bx v ψ

@[simp]

theorem Orthologic.ModalFormula.eval_box {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (bx : InfTopHom L L) (v : Var → L) (φ : ModalFormula Var) : eval bx v φ.box = bx (eval bx v φ)

@[simp]

theorem Orthologic.ModalFormula.eval_dia {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] (bx : InfTopHom L L) (v : Var → L) (φ : ModalFormula Var) : eval bx v φ.dia = (diamondHom bx) (eval bx v φ)

theorem Orthologic.ModalFormula.sound {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] [IsOrtholattice L] {bx : InfTopHom L L} (hT : ∀ (a : L), bx a ≤ a) (hW : WittgensteinLaw bx) {φ ψ : ModalFormula Var} (h : EDerivable φ ψ) (v : Var → L) : eval bx v φ ≤ eval bx v ψ

EO-consequences hold in every epistemic ortholattice under every valuation ([HM24] Theorem 3.26, soundness).

def Orthologic.ModalFormula.canonicalVal {Var : Type u_1} : Var → LindenbaumTarski (ModalFormula Var)

The canonical valuation into the Lindenbaum–Tarski algebra sends p to its class.

Equations

• Orthologic.ModalFormula.canonicalVal p = toAntisymmetrization (fun (x1 x2 : Orthologic.ModalFormula Var) => x1 ≤ x2) (Orthologic.ModalFormula.var p)

theorem Orthologic.ModalFormula.eval_canonicalVal {Var : Type u_1} (φ : ModalFormula Var) : eval (LindenbaumTarski.boxHom box) canonicalVal φ = toAntisymmetrization (fun (x1 x2 : ModalFormula Var) => x1 ≤ x2) φ

Under the canonical valuation every formula evaluates to its own class.

theorem Orthologic.ModalFormula.derivable_iff {Var : Type u} {φ ψ : ModalFormula Var} : EDerivable φ ψ ↔ ∀ {L : Type u} [inst : Lattice L] [inst_1 : BoundedOrder L] [inst_2 : InvolutiveCompl L] [IsOrtholattice L] (bx : InfTopHom L L), (∀ (a : L), bx a ≤ a) → WittgensteinLaw bx → ∀ (v : Var → L), eval bx v φ ≤ eval bx v ψ

EO is sound and complete for epistemic ortholattices: φ ⊢ ψ iff the inequality holds in every epistemic ortholattice under every valuation ([HM24] Theorem 3.26). Epistemic ortholattices in Var's universe suffice.