Orthologic: syntax, proof system, and algebraic completeness

[UPSTREAM] candidate.

Orthologic ([HM24] §3.1, after Goldblatt) is the logic of ortholattices: φ ⊢ ψ is the consequence relation holding in every OrthocomplementedLattice. This file gives the syntax, Goldblatt's proof system (Definition 3.12), and — via mathlib's Antisymmetrization (documented as the free Preorder → PartialOrder functor) — the Lindenbaum–Tarski algebra witnessing algebraic completeness (Theorem 3.13): the least orthologic is sound and complete with respect to the class of all ortholattices.

Main definitions

• Formula — orthologic formulas (⊤, variables, ¬, ∧; ∨ De Morgan-defined).
• Derivable (⊢) — the least orthologic (Goldblatt's ten rules).
• LindenbaumTarski — formulas modulo interderivability (an OrthocomplementedLattice).
• eval, soundness, completeness.

Implementation notes

The Lindenbaum–Tarski algebra is Antisymmetrization (Formula Var) (· ≤ ·) for the provability preorder; mathlib documents Antisymmetrization as the free functor Preord → PartOrd, so the quotient and its PartialOrder come for free. This file adds the OrthocomplementedLattice structure and completeness.

Syntax

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

Orthologic formulas over a variable type Var. Disjunction is De Morgan-defined (Formula.or), matching the ortholattice signature.

• 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

De Morgan disjunction φ ∨ ψ := ¬(¬φ ∧ ¬ψ).

Equations

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

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

Falsum ⊥ := ¬⊤.

Equations

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

The proof system

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

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

• 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

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

Equations

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

The provability preorder and the Lindenbaum–Tarski algebra

@[implicit_reducible]

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

Provability is a preorder (reflexivity + cut).

Equations

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

@[reducible, inline]

abbrev Orthologic.LindenbaumTarski (Var : Type u_1) : Type u_1

The Lindenbaum–Tarski algebra: formulas modulo interderivability. As the Antisymmetrization of the provability preorder it is automatically a PartialOrder; the OrthocomplementedLattice structure is added below.

Equations

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

Evaluation and soundness

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

Evaluate a formula in an ortholattice under a valuation v : Var → L.

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 ψ

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

Soundness: a derivable consequence holds in every ortholattice under every valuation ([HM24] Theorem 3.13, soundness half).

Provability lemmas for the lattice structure

These are the ortholattice axioms at the level of formulas; the quotient instance below lifts them through Antisymmetrization.

theorem Orthologic.Formula.bot_le {Var : Type u_3} (φ : Formula Var) : Derivable bot φ

⊥ ⊢ φ (ex falso, with ⊥ = ¬⊤).

theorem Orthologic.Formula.and_mono {Var : Type u_3} {φ φ' ψ ψ' : Formula Var} (h₁ : Derivable φ φ') (h₂ : Derivable ψ ψ') : Derivable (φ.and ψ) (φ'.and ψ')

Conjunction is monotone.

theorem Orthologic.Formula.le_or_left {Var : Type u_3} (φ ψ : Formula Var) : Derivable φ (φ.or ψ)

φ ⊢ φ ∨ ψ.

theorem Orthologic.Formula.le_or_right {Var : Type u_3} (φ ψ : Formula Var) : Derivable ψ (φ.or ψ)

ψ ⊢ φ ∨ ψ.

theorem Orthologic.Formula.or_le {Var : Type u_3} {φ ψ χ : Formula Var} (h₁ : Derivable φ χ) (h₂ : Derivable ψ χ) : Derivable (φ.or ψ) χ

φ ∨ ψ ⊢ χ from φ ⊢ χ and ψ ⊢ χ.

theorem Orthologic.Formula.or_mono {Var : Type u_3} {φ φ' ψ ψ' : Formula Var} (h₁ : Derivable φ φ') (h₂ : Derivable ψ ψ') : Derivable (φ.or ψ) (φ'.or ψ')

Disjunction is monotone.

theorem Orthologic.Formula.and_compl_le_bot {Var : Type u_3} (φ : Formula Var) : Derivable (φ.and φ.neg) bot

Non-contradiction: φ ∧ ¬φ ⊢ ⊥.

theorem Orthologic.Formula.top_le_or_compl {Var : Type u_3} (φ : Formula Var) : Derivable top (φ.or φ.neg)

Excluded middle: ⊤ ⊢ φ ∨ ¬φ.

The Lindenbaum–Tarski algebra is an ortholattice

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instMin {Var : Type u_3} : Min (LindenbaumTarski Var)

Equations

• Orthologic.LindenbaumTarski.instMin = { min := Quotient.map₂ Orthologic.Formula.and ⋯ }

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instMax {Var : Type u_3} : Max (LindenbaumTarski Var)

Equations

• Orthologic.LindenbaumTarski.instMax = { max := Quotient.map₂ Orthologic.Formula.or ⋯ }

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instCompl {Var : Type u_3} : Compl (LindenbaumTarski Var)

Equations

• Orthologic.LindenbaumTarski.instCompl = { compl := Quotient.map Orthologic.Formula.neg ⋯ }

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instTop {Var : Type u_3} : Top (LindenbaumTarski Var)

Equations

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

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instBot {Var : Type u_3} : Bot (LindenbaumTarski Var)

Equations

• Orthologic.LindenbaumTarski.instBot = { bot := toAntisymmetrization (fun (x1 x2 : Orthologic.Formula Var) => x1 ≤ x2) Orthologic.Formula.bot }

theorem Orthologic.LindenbaumTarski.mk_le_mk {Var : Type u_3} {x y : Formula Var} : toAntisymmetrization (fun (x1 x2 : Formula Var) => x1 ≤ x2) x ≤ toAntisymmetrization (fun (x1 x2 : Formula Var) => x1 ≤ x2) y ↔ Derivable x y

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

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instLattice {Var : Type u_3} : Lattice (LindenbaumTarski Var)

Equations

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

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instBoundedOrder {Var : Type u_3} : BoundedOrder (LindenbaumTarski Var)

Equations

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

@[implicit_reducible]

instance Orthologic.LindenbaumTarski.instOrthocomplementedLattice {Var : Type u_3} : OrthocomplementedLattice (LindenbaumTarski Var)

The Lindenbaum–Tarski algebra of orthologic is an orthocomplemented lattice.

Equations

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

Completeness

def Orthologic.Formula.canonicalVal {Var : Type u_3} : Var → LindenbaumTarski Var

The canonical valuation into the Lindenbaum–Tarski algebra: p ↦ ⟦p⟧.

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_3} (φ : Formula Var) : eval canonicalVal φ = toAntisymmetrization (fun (x1 x2 : Formula Var) => x1 ≤ x2) φ

Evaluating under the canonical valuation returns the formula's own class.

theorem Orthologic.complete {Var : Type u} {φ ψ : Formula Var} (h : ∀ {L : Type u} [inst : OrthocomplementedLattice L] (v : Var → L), Formula.eval v φ ≤ Formula.eval v ψ) : Derivable φ ψ

Completeness ([HM24] Theorem 3.13): if φ ⊨ ψ holds in every ortholattice under every valuation, then φ ⊢ ψ. Proved by evaluating in the Lindenbaum–Tarski algebra under the canonical valuation. (Testing ortholattices at Var's universe suffices — the L–T algebra is the worst case.)

theorem Orthologic.derivable_iff {Var : Type u} {φ ψ : Formula Var} : Derivable φ ψ ↔ ∀ {L : Type u} [inst : OrthocomplementedLattice L] (v : Var → L), Formula.eval v φ ≤ Formula.eval v ψ

Algebraic completeness of orthologic ([HM24] Theorem 3.13): φ ⊢ ψ iff the inequality holds in every ortholattice.