Frame semantics and completeness for orthologic

[HM24] §4.1 — Goldblatt's compatibility-frame semantics for orthologic and its completeness theorem (Theorem 4.19). A compatibility model is an Orthoframe F with a valuation V : Var → F.Regular assigning each variable a regular proposition. The support relation s ⊩ φ is defined recursively; the set of supporters {s | s ⊩ φ} is exactly the extent of the algebraic value Formula.eval V φ in the ortholattice F.Regular (support_setOf_eq_extent).

Soundness and completeness then reduce to the algebraic versions (Theorem 3.13): the bridge turns frame consequence into the algebraic inequality in every frame algebra, and the representation embedding (Theorem 4.13) places every ortholattice inside a frame algebra via represent, so frame validity entails validity in all ortholattices.

Main results

• Support, support_setOf_eq_extent — the support relation and the bridge.
• frame_sound, frame_complete, derivable_iff_frameConsequence — Theorem 4.19.

Support in a compatibility model

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

The support relation s ⊩ φ of the compatibility model (F, V) ([HM24] Def 4.16): ¬φ is supported at s exactly when s is orthogonal to (incompatible with) every point supporting φ.

Equations

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

theorem Orthologic.support_setOf_eq_extent {Var S : Type u} (F : Orthoframe S) (V : Var → F.Regular) (φ : Formula Var) : {s : S | Support F V s φ} = (Formula.eval V φ).extent

The bridge: the supporters of φ are exactly the extent of its algebraic value Formula.eval V φ in F.Regular.

Frame consequence, soundness, completeness

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

Semantic consequence over compatibility frames ([HM24] Def 4.18): in every model, every point supporting φ supports ψ.

Equations

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

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

Semantic consequence over compatibility frames ([HM24] Def 4.18): in every model, every point supporting φ supports ψ.

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 : Orthoframe S) (V : Var → F.Regular), Formula.eval V φ ≤ Formula.eval V ψ

Frame consequence is the algebraic inequality holding in every frame algebra.

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

Soundness over compatibility frames ([HM24] Thm 4.19).

theorem Orthologic.eval_map {Var L : Type u} [OrthocomplementedLattice L] {V₀ : Set L} (hV : JoinDense V₀) (v : Var → L) (φ : Formula Var) : Formula.eval (fun (p : Var) => Orthoframe.represent V₀ (v p)) φ = Orthoframe.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 φ ψ

Completeness over compatibility frames ([HM24] Thm 4.19): frame consequence implies derivability. Proved from algebraic completeness (Thm 3.13) by embedding every ortholattice into a frame algebra via represent over the join-dense Set.univ (Thm 4.13).

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

Goldblatt's completeness theorem ([HM24] Theorem 4.19): φ ⊢ ψ iff φ ⊨ᶠ ψ — provability equals validity over all compatibility frames.