Orthologic

[UPSTREAM] candidate.

This file defines orthologic, the logic of ortholattices, and proves Goldblatt's least orthologic sound and complete for them. An orthologic is a consequence relation on formulas built from ⊤, ¬ and ∧ satisfying Goldblatt's ten rules, and its Lindenbaum–Tarski algebra, formulas modulo interderivability, is an ortholattice. Evaluating in that algebra under the canonical valuation shows that a consequence holding in every ortholattice is derivable, following Holliday and Mandelkern's presentation.

Main definitions

• Orthologic.IsOrthologic F: a consequence preorder on F satisfying Goldblatt's rules.
• Orthologic.LindenbaumTarski F: formulas modulo interderivability, an ortholattice for an orthologic.
• Orthologic.Formula, Orthologic.Derivable: the language of orthologic and its least orthologic.
• Orthologic.Formula.eval: the value of a formula in an ortholattice.

Main results

• Orthologic.derivable_iff: the least orthologic is sound and complete for ortholattices.

Implementation notes

The Lindenbaum–Tarski algebra is Antisymmetrization F (· ≤ ·) for the consequence preorder, mathlib's free functor from preorders to partial orders, so the quotient and its order come for free. It is built once for any orthologic, and the epistemic orthologic of Logic/Orthologic/EpistemicOrthologic.lean reuses it.

References

• [HM24]

Syntax

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

Formulas of orthologic over a variable type Var, with disjunction and falsum defined ([HM24] Definition 3.9).

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

def Orthologic.Formula.or {Var : Type u_1} (φ ψ : Formula Var) : Formula Var

Disjunction is De Morgan's φ ∨ ψ := ¬(¬φ ∧ ¬ψ).

Equations

• φ.or ψ = (φ.neg.and ψ.neg).neg

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

Falsum is ¬⊤.

Equations

• Orthologic.Formula.bot = Orthologic.Formula.top.neg

The proof system

inductive Orthologic.Derivable {Var : Type u_1} : Formula Var → Formula Var → Prop

Consequence φ ⊢ ψ in the least orthologic is generated by Goldblatt's ten rules: ⊤-introduction, reflexivity, the two ∧-projections, double-negation introduction and elimination, non-contradiction φ ∧ ¬φ ⊢ ψ, cut, ∧-introduction, and contraposition ([HM24] Definition 3.12).

• top_intro {Var : Type u_1} (φ : Formula Var) : Derivable φ Formula.top
• refl {Var : Type u_1} (φ : Formula Var) : Derivable φ φ
• and_le_left {Var : Type u_1} (φ ψ : Formula Var) : Derivable (φ.and ψ) φ
• and_le_right {Var : Type u_1} (φ ψ : Formula Var) : Derivable (φ.and ψ) ψ
• le_negNeg {Var : Type u_1} (φ : Formula Var) : Derivable φ φ.neg.neg
• negNeg_le {Var : Type u_1} (φ : Formula Var) : Derivable φ.neg.neg φ
• contradiction {Var : Type u_1} (φ ψ : Formula Var) : Derivable (φ.and φ.neg) ψ
• trans {Var : Type u_1} {φ ψ χ : Formula Var} : Derivable φ ψ → Derivable ψ χ → Derivable φ χ
• le_and {Var : Type u_1} {φ ψ χ : Formula Var} : Derivable φ ψ → Derivable φ χ → Derivable φ (ψ.and χ)
• neg_le_neg {Var : Type u_1} {φ ψ : Formula Var} : Derivable φ ψ → Derivable ψ.neg φ.neg

def Orthologic.«term_⊢_» : Lean.TrailingParserDescr

Consequence φ ⊢ ψ in the least orthologic is generated by Goldblatt's ten rules: ⊤-introduction, reflexivity, the two ∧-projections, double-negation introduction and elimination, non-contradiction φ ∧ ¬φ ⊢ ψ, cut, ∧-introduction, and contraposition ([HM24] Definition 3.12).

Equations

• Orthologic.«term_⊢_» = Lean.ParserDescr.trailingNode `Orthologic.«term_⊢_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢ ") (Lean.ParserDescr.cat `term 51))

Orthologics and their Lindenbaum–Tarski algebras

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

A consequence preorder on formulas with ⊤, ⊓ and ᶜ is an orthologic when it satisfies Goldblatt's rules, reflexivity and cut being the preorder axioms. On Formula Var this is the notion of an orthologic of [HM24] Definition 3.12.

• le_top (φ : F) : φ ≤ ⊤
• inf_le_left (φ ψ : F) : φ ⊓ ψ ≤ φ
• inf_le_right (φ ψ : F) : φ ⊓ ψ ≤ ψ
• le_compl_compl (φ : F) : φ ≤ φᶜᶜ
• compl_compl_le (φ : F) : φᶜᶜ ≤ φ
• inf_compl_le (φ ψ : F) : φ ⊓ φᶜ ≤ ψ
• le_inf {φ ψ χ : F} : φ ≤ ψ → φ ≤ χ → φ ≤ ψ ⊓ χ
• compl_le_compl {φ ψ : F} : φ ≤ ψ → ψᶜ ≤ φᶜ

@[reducible, inline]

abbrev Orthologic.LindenbaumTarski (F : Type u_1) [Preorder F] : Type u_1

The Lindenbaum–Tarski algebra of a consequence preorder is the type of formulas modulo interderivability, the Antisymmetrization of the preorder. It is an ortholattice when the preorder is an orthologic.

Equations

• Orthologic.LindenbaumTarski F = Antisymmetrization F fun (x1 x2 : F) => x1 ≤ x2

def Orthologic.IsOrthologic.sup {F : Type u_1} [Min F] [Compl F] (φ ψ : F) : F

Disjunction is De Morgan's φ ∨ ψ := ¬(¬φ ∧ ¬ψ).

Equations

• Orthologic.IsOrthologic.sup φ ψ = (φᶜ ⊓ ψᶜ)ᶜ

theorem Orthologic.IsOrthologic.inf_mono {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] {φ φ' ψ ψ' : F} (h₁ : φ ≤ φ') (h₂ : ψ ≤ ψ') : φ ⊓ ψ ≤ φ' ⊓ ψ'

theorem Orthologic.IsOrthologic.le_sup_left {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (φ ψ : F) : φ ≤ sup φ ψ

theorem Orthologic.IsOrthologic.le_sup_right {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (φ ψ : F) : ψ ≤ sup φ ψ

theorem Orthologic.IsOrthologic.sup_le {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] {φ ψ χ : F} (h₁ : φ ≤ χ) (h₂ : ψ ≤ χ) : sup φ ψ ≤ χ

theorem Orthologic.IsOrthologic.sup_mono {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] {φ φ' ψ ψ' : F} (h₁ : φ ≤ φ') (h₂ : ψ ≤ ψ') : sup φ ψ ≤ sup φ' ψ'

theorem Orthologic.LindenbaumTarski.mk_le_mk {F : Type u_1} [Preorder F] {φ ψ : F} : toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) φ ≤ toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) ψ ↔ φ ≤ ψ

⟦φ⟧ ≤ ⟦ψ⟧ in the Lindenbaum–Tarski algebra iff φ ≤ ψ.

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instMin {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] : Min (LindenbaumTarski F)

Equations

• Orthologic.LindenbaumTarski.instMin = { min := Quotient.map₂ (fun (x1 x2 : F) => x1 ⊓ x2) ⋯ }

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instMax {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] : Max (LindenbaumTarski F)

Equations

• Orthologic.LindenbaumTarski.instMax = { max := Quotient.map₂ Orthologic.IsOrthologic.sup ⋯ }

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instCompl {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] : Compl (LindenbaumTarski F)

Equations

• Orthologic.LindenbaumTarski.instCompl = { compl := Quotient.map (fun (x : F) => xᶜ) ⋯ }

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instTop {F : Type u_1} [Preorder F] [Top F] : Top (LindenbaumTarski F)

Equations

• Orthologic.LindenbaumTarski.instTop = { top := toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) ⊤ }

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instBot {F : Type u_1} [Preorder F] [Top F] [Compl F] : Bot (LindenbaumTarski F)

Equations

• Orthologic.LindenbaumTarski.instBot = { bot := toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) ⊤ᶜ }

@[simp]

theorem Orthologic.LindenbaumTarski.mk_inf {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (φ ψ : F) : toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) (φ ⊓ ψ) = toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) φ ⊓ toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) ψ

@[simp]

theorem Orthologic.LindenbaumTarski.mk_compl {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] (φ : F) : toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) φᶜ = (toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) φ)ᶜ

@[simp]

theorem Orthologic.LindenbaumTarski.mk_top {F : Type u_1} [Preorder F] [Top F] : toAntisymmetrization (fun (x1 x2 : F) => x1 ≤ x2) ⊤ = ⊤

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instLattice {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] : Lattice (LindenbaumTarski F)

Equations

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

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instBoundedOrder {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] : BoundedOrder (LindenbaumTarski F)

Equations

• Orthologic.LindenbaumTarski.instBoundedOrder = { toTop := Orthologic.LindenbaumTarski.instTop, le_top := ⋯, toBot := Orthologic.LindenbaumTarski.instBot, bot_le := ⋯ }

@[instance_reducible]

instance Orthologic.LindenbaumTarski.instInvolutiveCompl {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] : InvolutiveCompl (LindenbaumTarski F)

Equations

• Orthologic.LindenbaumTarski.instInvolutiveCompl = { toCompl := Orthologic.LindenbaumTarski.instCompl, compl_compl := ⋯, compl_le_compl := ⋯ }

instance Orthologic.LindenbaumTarski.instIsOrtholattice {F : Type u_1} [Preorder F] [Top F] [Min F] [Compl F] [IsOrthologic F] : IsOrtholattice (LindenbaumTarski F)

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

The least orthologic

@[instance_reducible]

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

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Consequence in the least orthologic is a preorder, reflexivity and cut.

Equations

• Orthologic.Formula.instPreorder = { le := Orthologic.Derivable, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

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

Evaluation, soundness and completeness

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

The value of a formula in an ortholattice under a valuation v : Var → L ([HM24] Definition 3.10).

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Orthologic.sound {Var : Type u_1} {L : Type u_2} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] [IsOrtholattice L] {φ ψ : Formula Var} (h : Derivable φ ψ) (v : Var → L) : Formula.eval v φ ≤ Formula.eval v ψ

Derivable consequences hold in every ortholattice under every valuation ([HM24] Theorem 3.13, soundness).

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

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

Equations

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

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

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

theorem Orthologic.complete {Var : Type u} {φ ψ : Formula Var} (h : ∀ {L : Type u} [inst : Lattice L] [inst_1 : BoundedOrder L] [inst_2 : InvolutiveCompl L] [IsOrtholattice L] (v : Var → L), Formula.eval v φ ≤ Formula.eval v ψ) : Derivable φ ψ

A consequence holding in every ortholattice under every valuation is derivable, by evaluating in the Lindenbaum–Tarski algebra under the canonical valuation ([HM24] Theorem 3.13, completeness). Ortholattices in Var's universe suffice.

theorem Orthologic.derivable_iff {Var : Type u} {φ ψ : Formula Var} : Derivable φ ψ ↔ ∀ {L : Type u} [inst : Lattice L] [inst_1 : BoundedOrder L] [inst_2 : InvolutiveCompl L] [IsOrtholattice L] (v : Var → L), Formula.eval v φ ≤ Formula.eval v ψ

Derivability is consequence in every ortholattice ([HM24] Theorem 3.13).