ModalAlgebra.agda

module K.Semantics.Algebra where
open import K.Syntax
open import Common
open import Algebra.Structures using (IsBooleanAlgebra)
open import Relation.Binary using (Preorder; IsEquivalence)


record ModalAlgebra : Set₁ where
  infix 6 _≃_
  infix 7 _∧_
  infix 7 _∨_
  infix 8 [_]_
  infix 9 ¬_

  field
    C     : Set
    _≃_   : C → C → Set
    _∧_   : C → C → C
    _∨_   : C → C → C
    ¬_    : C → C
    ⊤     : C
    ⊥     : C
    [_]_  : Label → C → C

    isEq      : IsEquivalence _≃_
    isBA      : IsBooleanAlgebra _≃_ _∨_ _∧_ ¬_ ⊤ ⊥
    []-id     : ∀ a → [ a ] ⊤ ≃ ⊤
    []-∧-dist : ∀ a x y → [ a ] (x ∧ y) ≃ [ a ] x ∧ [ a ] y

  _⇒_ : C → C → C
  x ⇒ y = ¬ x ∨ y

  open IsBooleanAlgebra isBA public

open ModalAlgebra {{…}} public


-- Semantics defined in a fixed Modal Algebra.
module _ {{M : ModalAlgebra}} where
  -- A valuation of the free variables in a formula.
  Valuation : Set
  Valuation = Atom → C

  -- Embedding of a given formula under a given valuation into the Modal Algebra.
  _⊨ᵛ_ : Valuation → Form → C
  V ⊨ᵛ (α a)     = V a
  V ⊨ᵛ (ϕ ⇒ᵏ ψ)   = (V ⊨ᵛ ϕ) ⇒ (V ⊨ᵛ ψ)
  V ⊨ᵛ ([ a ]ᵏ ϕ) = [ a ] (V ⊨ᵛ ϕ)
  V ⊨ᵛ (¬ᵏ ϕ)     = ¬ (V ⊨ᵛ ϕ)

  -- Equality with ⊤ under all valuations, or entailment.
  ⊨_ : Form → Set
  ⊨ ϕ = ∀ (V : Valuation) → (V ⊨ᵛ ϕ) ≃ ⊤

  -- Entailment of a context.
  ⊨*_ : Cx → Set
  ⊨* ∅       = Unit
  ⊨* (Γ , A) = (⊨* Γ) × (⊨ A)

-- Contextful entailment in all Modal Algebras.
_⊨_ : Cx → Form → Set₁
Γ ⊨ ϕ = ∀ {{_ : ModalAlgebra}} → ⊨* Γ → ⊨ ϕ


-- Some useful identities of a Modal Algebra
module _ {{M : ModalAlgebra}} where
  open import Relation.Binary.PreorderReasoning (record {isPreorder = (ModalAlgebra.isEq M)})

  id : ∀ a → a ⇒ a ≃ ⊤
  id a = begin
    a ⇒ a ≈⟨⟩
    ¬ a ∨ a ≈⟨ ModalAlgebra.∨-comm M (¬ a) a ⟩
    a ∨ ¬ a ≈⟨ ModalAlgebra.∨-complementʳ M a  ⟩
    ⊤ ∎