↑ Top

Equational Logic

This is the Base.Varieties.EquationalLogic module of the Agda Universal Algebra Library where the binary β€œmodels” relation ⊧, relating algebras (or classes of algebras) to the identities that they satisfy, is defined.

Let 𝑆 be a signature. By an identity or equation in 𝑆 we mean an ordered pair of terms, written p β‰ˆ q, from the term algebra 𝑻 X. If 𝑨 is an 𝑆-algebra we say that 𝑨 satisfies p β‰ˆ q provided p Μ‡ 𝑨 ≑ q Μ‡ 𝑨 holds. In this situation, we write 𝑨 ⊧ p β‰ˆ q and say that 𝑨 models the identity p β‰ˆ q. If 𝒦 is a class of 𝑆-algebras, then we write 𝒦 ⊧ p β‰ˆ q iff, for every 𝑨 ∈ 𝒦, 𝑨 ⊧ p β‰ˆ q.

Because a class of structures has a different type than a single structure, we must use a slightly different syntax to avoid overloading the relations ⊧ and β‰ˆ. As a reasonable alternative to what we would normally express informally as 𝒦 ⊧ p β‰ˆ q, we have settled on 𝒦 ⊫ p β‰ˆ q to denote this relation. To reiterate, if 𝒦 is a class of 𝑆-algebras, we write 𝒦 ⊫ p β‰ˆ q iff every 𝑨 ∈ 𝒦 satisfies 𝑨 ⊧ p β‰ˆ q.


{-# OPTIONS --without-K --exact-split --safe #-}

open import Overture using ( π“ž ; π“₯ ; Signature )

module Base.Varieties.EquationalLogic {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library ----------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Data.Product    using ( _Γ—_ ; _,_ ; Ξ£-syntax)
                            renaming ( proj₁ to fst ; projβ‚‚ to snd )
open import Level           using ( Level ;  _βŠ”_ )
open import Relation.Unary  using ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library ----------------
open import Overture                using ( _β‰ˆ_ )
open import Base.Algebras  {𝑆 = 𝑆}  using ( Algebra ; ov )
open import Base.Terms     {𝑆 = 𝑆}  using ( Term ; 𝑻 ; _⟦_⟧ )

private variable
 Ο‡ Ξ± ρ ΞΉ : Level
 X : Type Ο‡

The models relation

We define the binary β€œmodels” relation ⊧ using infix syntax so that we may write, e.g., 𝑨 ⊧ p β‰ˆ q or 𝒦 ⊫ p β‰ˆ q, relating algebras (or classes of algebras) to the identities that they satisfy. We also prove a couple of useful facts about ⊧.


_⊧_β‰ˆ_ : Algebra Ξ± β†’ Term X β†’ Term X β†’ Type _
𝑨 ⊧ p β‰ˆ q = 𝑨 ⟦ p ⟧ β‰ˆ 𝑨 ⟦ q ⟧

_⊫_β‰ˆ_ : Pred(Algebra Ξ±) ρ β†’ Term X β†’ Term X β†’ Type _
𝒦 ⊫ p β‰ˆ q = {𝑨 : Algebra _} β†’ 𝒦 𝑨 β†’ 𝑨 ⊧ p β‰ˆ q

Unicode tip. Type \models to get ⊧ ; type \||= to get ⊫.

The expression 𝑨 ⊧ p β‰ˆ q represents the assertion that the identity p β‰ˆ q holds when interpreted in the algebra 𝑨; syntactically, 𝑨 ⟦ p ⟧ β‰ˆ 𝑨 ⟦ q ⟧.

The expression 𝑨 ⟦ p ⟧ β‰ˆ 𝑨 ⟦ q ⟧ denotes extensional equality; that is, for each β€œenvironment” Ξ· : X β†’ ∣ 𝑨 ∣ (assigning values in the domain of 𝑨 to the variable symbols in X) the (intensional) equality 𝑨 ⟦ p ⟧ Ξ· ≑ 𝑨 ⟦ q ⟧ Ξ· holds.

Equational theories and models

If 𝒦 denotes a class of structures, then Th 𝒦 represents the set of identities modeled by the members of 𝒦.


Th : Pred (Algebra Ξ±) (ov Ξ±) β†’ Pred(Term X Γ— Term X) _
Th 𝒦 = Ξ» (p , q) β†’ 𝒦 ⊫ p β‰ˆ q

We represent Th 𝒦 as an indexed collection of algebras by taking Th 𝒦, itself, to be the index set.


module _ {X : Type Ο‡}{𝒦 : Pred (Algebra Ξ±) (ov Ξ±)} where

 ℐ : Type (ov(Ξ± βŠ” Ο‡))
 ℐ = Ξ£[ (p , q) ∈ (Term X Γ— Term X) ] 𝒦 ⊫ p β‰ˆ q

 β„° : ℐ β†’ Term X Γ— Term X
 β„° ((p , q) , _) = (p , q)

If β„° denotes a set of identities, then Mod β„° is the class of structures satisfying the identities in β„°.


Mod : Pred(Term X Γ— Term X) (ov Ξ±) β†’ Pred(Algebra Ξ±) _
Mod β„° = Ξ» 𝑨 β†’ βˆ€ p q β†’ (p , q) ∈ β„° β†’ 𝑨 ⊧ p β‰ˆ q
-- (tupled version)
Modα΅— : {I : Type ΞΉ} β†’ (I β†’ Term X Γ— Term X) β†’ {Ξ± : Level} β†’ Pred(Algebra Ξ±) _
Modα΅— β„° = Ξ» 𝑨 β†’ βˆ€ i β†’ 𝑨 ⊧ (fst (β„° i)) β‰ˆ (snd (β„° i))

↑ Base.Varieties Base.Varieties.Closure β†’