---
layout: default
title : "Setoid.Varieties.EquationalLogic module (The Agda Universal Algebra Library)"
date : "2021-09-24"
author: "agda-algebras development team"
---

### Equational Logic and varieties of setoid algebras

This is the [Setoid.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 𝑝 β‰ˆ π‘ž, from the term algebra 𝑻 X. If 𝑨 is an 𝑆-algebra we say that 𝑨 *satisfies* 𝑝 β‰ˆ π‘ž provided 𝑝 Μ‡ 𝑨 ≑ π‘ž Μ‡ 𝑨 holds. In this situation, we write 𝑨 ⊧ 𝑝 β‰ˆ π‘ž and say that 𝑨 *models* the identity 𝑝 β‰ˆ q. If 𝒦 is a class of algebras, all of the same signature, we write 𝒦 ⊧ p β‰ˆ q if, for every 𝑨 ∈ 𝒦, 𝑨 ⊧ 𝑝 β‰ˆ π‘ž.

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 𝒦 ⊧ 𝑝 β‰ˆ π‘ž, we have settled on 𝒦 ⊫ p β‰ˆ q to denote this relation.  To reiterate, if 𝒦 is a class of 𝑆-algebras, we write 𝒦 ⊫ 𝑝 β‰ˆ π‘ž if every 𝑨 ∈ 𝒦 satisfies 𝑨 ⊧ 𝑝 β‰ˆ π‘ž.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

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

module Setoid.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 ; proj₁ ; projβ‚‚ )
open import Function         using () renaming ( Func to _⟢_ )
open import Level            using ( _βŠ”_ ; Level )
open import Relation.Binary  using ( Setoid )
open import Relation.Unary   using ( Pred ; _∈_ )

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Setoid.Algebras  {𝑆 = 𝑆} using ( Algebra ; ov )
open import Overture.Terms   {𝑆 = 𝑆} using ( Term )
open import Setoid.Terms     {𝑆 = 𝑆} using ( module Environment )

private variable Ο‡ Ξ± ρᡃ β„“ ΞΉ : Level
```
-->


#### 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 ⊧.  More will be proved about ⊧ in the next module,
Varieties.EquationalLogic.

```agda
open _⟢_ using () renaming ( to to _⟨$⟩_ )

module _  {X : Type Ο‡} where

  open Setoid   using ( Carrier )
  open Algebra  using ( Domain )

  _⊧_β‰ˆ_ : Algebra Ξ± ρᡃ β†’ Term X β†’ Term X β†’ Type _
  𝑨 ⊧ p β‰ˆ q = βˆ€ (ρ : Carrier (Env X)) β†’ ⟦ p ⟧ ⟨$⟩ ρ β‰ˆ ⟦ q ⟧ ⟨$⟩ ρ
    where
    open Setoid ( Domain 𝑨 )  using ( _β‰ˆ_ )
    open Environment 𝑨        using ( Env ; ⟦_⟧ )
  infix 10 _⊧_β‰ˆ_

  _⊫_β‰ˆ_ : Pred(Algebra Ξ± ρᡃ) β„“ β†’ Term X β†’ Term X β†’ Type (Ο‡ βŠ” β„“ βŠ” ov(Ξ± βŠ” ρᡃ))
  𝒦 ⊫ 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 `𝑨` for any environment ρ; syntactically, we write
this interpretation as `⟦ p ⟧ ρ β‰ˆ ⟦ q ⟧ ρ`. (Recall, and environment is simply an
assignment of values in the domain to variable symbols).


#### Equational theories and models over setoids

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

```agda
  Th' : Pred (Algebra Ξ± ρᡃ) β„“ β†’ Pred(Term X Γ— Term X) (Ο‡ βŠ” β„“ βŠ” ov(Ξ± βŠ” ρᡃ))
  Th' 𝒦 = Ξ» (p , q) β†’ 𝒦 ⊫ p β‰ˆ q

Th'' :  {Ο‡ Ξ± : Level}{X : Type Ο‡} β†’ Pred (Algebra Ξ± Ξ±) (ov Ξ±)
  β†’      Pred(Term X Γ— Term X) (Ο‡ βŠ” ov Ξ±)
Th'' 𝒦 = Ξ» (p , q) β†’ 𝒦 ⊫ p β‰ˆ q
```

Perhaps we want to represent Th 𝒦 as an indexed collection.  We do so
essentially by taking `Th 𝒦` itself to be the index set, as shown below.

```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 Ξ± ρᡃ) (ρᡃ βŠ” ov(Ξ± βŠ” Ο‡))
  Mod' β„° = Ξ» 𝑨 β†’ βˆ€ p q β†’ (p , q) ∈ β„° β†’ 𝑨 ⊧ p β‰ˆ q
```

It is sometimes more convenient to have a "tupled" version of the previous definition, which we denote by `Modα΅—` and define as follows.

```agda
  Modα΅— : {I : Type ΞΉ} β†’ (I β†’ Term X Γ— Term X) β†’ {Ξ± : Level} β†’ Pred(Algebra Ξ± ρᡃ) (Ο‡ βŠ” ρᡃ βŠ” ΞΉ βŠ” Ξ±)
  Modα΅— β„° = Ξ» 𝑨 β†’ βˆ€ i β†’ 𝑨 ⊧ proj₁ (β„° i) β‰ˆ projβ‚‚ (β„° i)
```