---
layout: default
title : "Legacy.Base.Varieties.EquationalLogic module (The Agda Universal Algebra Library)"
date : "2021-01-14"
author: "agda-algebras development team"
---

### <a id="equational-logic">Equational Logic</a>

This is the [Legacy.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`.


```agda


{-# OPTIONS --cubical-compatible --exact-split --safe #-}

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

module Legacy.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 Legacy.Base.Algebras  {𝑆 = 𝑆}  using ( Algebra ; ov )
open import Legacy.Base.Terms     {𝑆 = 𝑆}  using ( Term ; 𝑻 ; _⟦_⟧ )

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


#### <a id="the-models-relation">The models relation</a>

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 `⊧`.


```agda


_⊧_β‰ˆ_ : 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.


#### <a id="equational-theories-and-models">Equational theories and models</a>

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


```agda


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.


```agda


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 `β„°`.


```agda


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))
```