Frame semantics and completeness for orthologic

This file proves Goldblatt's completeness theorem for orthologic over compatibility frames, in the form Holliday and Mandelkern give it. A compatibility model is a frame F with a valuation V : Var → F.Regular assigning each variable a regular proposition, and support s ⊩ φ is defined recursively. The supporters of a formula are exactly its algebraic value in the ortholattice of regular propositions, so frame consequence is the algebraic inequality in every frame algebra. The representation of ortholattices places every ortholattice inside a frame algebra, so frame validity entails validity in all ortholattices, and completeness follows from algebraic completeness.

Main definitions

• Orthologic.Support: support of a formula at a possibility of a compatibility model.
• Orthologic.FrameConsequence: consequence over all compatibility models.
• Orthologic.CompatFrame.ofOrtholattice: the canonical frame of an ortholattice.

Main results

• Orthologic.support_setOf_eq_coe_eval: the supporters of φ are its algebraic value.
• Orthologic.derivable_iff_frameConsequence: derivability is frame consequence.

References

• [HM24]

Support in a compatibility model

def Orthologic.Support {Var S : Type u} (F : CompatFrame S) (V : Var → F.Regular) (s : S) : Formula Var → Prop

Support in the compatibility model (F, V): s supports ¬φ when no possibility compatible with s supports φ ([HM24] Definition 4.15).

Equations

• Orthologic.Support F V s Orthologic.Formula.top = True
• Orthologic.Support F V s (Orthologic.Formula.var p) = (s ∈ V p)
• Orthologic.Support F V s φ.neg = ∀ (t : S), F.compat s t → ¬Orthologic.Support F V t φ
• Orthologic.Support F V s (φ.and ψ) = (Orthologic.Support F V s φ ∧ Orthologic.Support F V s ψ)

theorem Orthologic.support_setOf_eq_coe_eval {Var S : Type u} (F : CompatFrame S) (V : Var → F.Regular) (φ : Formula Var) : {s : S | Support F V s φ} = ↑(Formula.eval V φ)

The supporters of φ are its algebraic value in the regular propositions, so in particular they form a regular set ([HM24] Lemma 4.16).

Frame consequence, soundness, completeness

def Orthologic.FrameConsequence {Var : Type u} (φ ψ : Formula Var) : Prop

ψ is a semantic consequence of φ over compatibility frames when in every model every possibility supporting φ supports ψ ([HM24] Definition 4.18).

Equations

• Orthologic.FrameConsequence φ ψ = ∀ {S : Type ?u.1} (F : Orthologic.CompatFrame S) (V : Var → F.Regular) (s : S), Orthologic.Support F V s φ → Orthologic.Support F V s ψ

def Orthologic.«term_⊨ᶠ_» : Lean.TrailingParserDescr

ψ is a semantic consequence of φ over compatibility frames when in every model every possibility supporting φ supports ψ ([HM24] Definition 4.18).

Equations

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

theorem Orthologic.frameConsequence_iff_eval {Var : Type u} {φ ψ : Formula Var} : FrameConsequence φ ψ ↔ ∀ {S : Type u} (F : CompatFrame S) (V : Var → F.Regular), Formula.eval V φ ≤ Formula.eval V ψ

Frame consequence is the algebraic inequality in every frame algebra.

theorem Orthologic.frame_sound {Var : Type u} {φ ψ : Formula Var} (h : Derivable φ ψ) : FrameConsequence φ ψ

Derivability is sound for frame consequence ([HM24] Theorem 4.19).

def Orthologic.CompatFrame.ofOrtholattice {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] [IsOrtholattice L] (V : Set L) : CompatFrame (InvolutiveCompl.Point V)

The canonical frame of an ortholattice over V: two nonzero elements of V are compatible when neither lies below the complement of the other ([HM24] Theorem 4.13).

Equations

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

@[simp]

theorem Orthologic.CompatFrame.ofOrtholattice_compat {L : Type u_1} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] [IsOrtholattice L] {V : Set L} {a b : InvolutiveCompl.Point V} : (ofOrtholattice V).compat a b ↔ ¬↑a ≤ (↑b)ᶜ

theorem Orthologic.eval_map {Var L : Type u} [Lattice L] [BoundedOrder L] [InvolutiveCompl L] [IsOrtholattice L] {V₀ : Set L} (hV : JoinDense V₀) (v : Var → L) (φ : Formula Var) : Formula.eval (fun (p : Var) => InvolutiveCompl.represent V₀ (v p)) φ = InvolutiveCompl.represent V₀ (Formula.eval v φ)

Formula.eval commutes with the representation embedding represent V₀.

theorem Orthologic.frame_complete {Var : Type u} {φ ψ : Formula Var} (h : FrameConsequence φ ψ) : Derivable φ ψ

Frame consequence implies derivability ([HM24] Theorem 4.19): the canonical frame of any ortholattice over Set.univ embeds it into a frame algebra, so frame validity gives validity in every ortholattice.

theorem Orthologic.derivable_iff_frameConsequence {Var : Type u} {φ ψ : Formula Var} : Derivable φ ψ ↔ FrameConsequence φ ψ

Derivability is consequence over all compatibility frames, Goldblatt's completeness theorem ([HM24] Theorem 4.19).