Agda UALib ↑

### Model Theory and Equational Logic

This section presents the 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.

Agda supports the definition of infix operations and relations, and we use this to define ⊧ so that we may write, e.g., `𝑨 ⊧ p ≈ q` or `𝒦 ⊧ p ≋ q`.

We also prove some closure and invariance properties of ⊧. In particular, we prove the following facts (which are needed, for example, in the proof the Birkhoff HSP Theorem).

• Algebraic invariance. The ⊧ relation is an algebraic invariant (stable under isomorphism).

• Subalgebraic invariance. Identities modeled by a class of algebras are also modeled by all subalgebras of algebras in the class.

• Product invariance. Identities modeled by a class of algebras are also modeled by all products of algebras in the class.

Notation. In the Agda UALib, 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 𝑨 ⊧ 𝑝 ≈ 𝑞.

Unicode Hints. To produce the symbols ≈, ⊧, and ≋ in agda2-mode, type `\~~`, `\models`, and `\~~~`, respectively.

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

open import Algebras.Signatures using (Signature; 𝓞; 𝓥)
open import Universes using (Universe; _̇)

module Varieties.EquationalLogic {𝑆 : Signature 𝓞 𝓥}{𝓧 : Universe}{X : 𝓧 ̇} where

open import Subalgebras.Subalgebras{𝑆 = 𝑆} hiding (Universe; _̇) public
open import MGS-Embeddings using (embeddings-are-lc) public

```

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

```
module _ {𝓤 : Universe} where
_⊧_≈_ : Algebra 𝓤 𝑆 → Term X → Term X → 𝓤 ⊔ 𝓧 ̇
𝑨 ⊧ p ≈ q = 𝑨 ⟦ p ⟧ ≡ 𝑨 ⟦ q ⟧

_⊧_≋_ : Pred(Algebra 𝓤 𝑆)(ov 𝓤) → Term X → Term X → 𝓧 ⊔ ov 𝓤 ̇
𝒦 ⊧ p ≋ q = {𝑨 : Algebra _ 𝑆} → 𝒦 𝑨 → 𝑨 ⊧ p ≈ q

```
##### Syntax and semantics of ⊧

The expression `𝑨 ⊧ 𝑝 ≈ 𝑞` represents the assertion that the identity `p ≈ q` holds when interpreted in the algebra 𝑨; syntactically, `𝑝 ̇ 𝑨 ≡ 𝑞 ̇ 𝑨`. It should be emphasized that the expression `𝑝 ̇ 𝑨 ≡ 𝑞 ̇ 𝑨` is interpreted computationally as an extensional equality, by which we mean that for each assignment function `𝒂 : X → ∣ 𝑨 ∣`, assigning values in the domain of `𝑨` to the variable symbols in `X`, we have `(𝑝 ̇ 𝑨) 𝒂 ≡ (𝑞 ̇ 𝑨) 𝒂`.

#### Equational theories and models

Here we define a type `Th` so that, if 𝒦 denotes a class of algebras, then `Th 𝒦` represents the set of identities modeled by all members of 𝒦.

```
Th : Pred (Algebra 𝓤 𝑆)(ov 𝓤) → Pred(Term X × Term X)(𝓧 ⊔ ov 𝓤)
Th 𝒦 = λ (p , q) → 𝒦 ⊧ p ≋ q

```

If ℰ denotes a set of identities, then the class of algebras satisfying all identities in ℰ is represented by `Mod ℰ`, which we define in the following natural way.

```
Mod : Pred(Term X × Term X)(𝓧 ⊔ ov 𝓤) → Pred(Algebra 𝓤 𝑆)(ov (𝓧 ⊔ 𝓤))
Mod ℰ = λ 𝑨 → ∀ p q → (p , q) ∈ ℰ → 𝑨 ⊧ p ≈ q

```

#### Algebraic invariance of ⊧

The binary relation ⊧ would be practically useless if it were not an algebraic invariant (i.e., invariant under isomorphism).

```

DFunExt : 𝓤ω
DFunExt = (𝓤 𝓥 : Universe) → dfunext 𝓤 𝓥

module _ {𝓤 𝓦 : Universe}{𝑨 : Algebra 𝓤 𝑆} where

⊧-I-invar : DFunExt → (𝑩 : Algebra 𝓦 𝑆)(p q : Term X)
→          𝑨 ⊧ p ≈ q  →  𝑨 ≅ 𝑩  →  𝑩 ⊧ p ≈ q

⊧-I-invar fe 𝑩 p q Apq (f , g , f∼g , g∼f) = (fe (𝓧 ⊔ 𝓦) 𝓦) λ x →
(𝑩 ⟦ p ⟧) x                      ≡⟨ refl ⟩
(𝑩 ⟦ p ⟧) (∣ 𝒾𝒹 𝑩 ∣ ∘ x)         ≡⟨ ap (𝑩 ⟦ p ⟧) ((fe 𝓧 𝓦) λ i → ((f∼g)(x i))⁻¹)⟩
(𝑩 ⟦ p ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘ x)  ≡⟨ (comm-hom-term (fe 𝓥 𝓦) 𝑩 f p (∣ g ∣ ∘ x))⁻¹ ⟩
∣ f ∣ ((𝑨 ⟦ p ⟧) (∣ g ∣ ∘ x))    ≡⟨ ap (λ - → ∣ f ∣ (- (∣ g ∣ ∘ x))) Apq ⟩
∣ f ∣ ((𝑨 ⟦ q ⟧) (∣ g ∣ ∘ x))    ≡⟨ comm-hom-term (fe 𝓥 𝓦) 𝑩 f q (∣ g ∣ ∘ x) ⟩
(𝑩 ⟦ q ⟧) ((∣ f ∣ ∘ ∣ g ∣) ∘  x) ≡⟨ ap (𝑩 ⟦ q ⟧) ((fe 𝓧 𝓦) λ i → (f∼g) (x i)) ⟩
(𝑩 ⟦ q ⟧) x                      ∎

```

As the proof makes clear, we show 𝑩 ⊧ p ≈ q by showing that p ̇ 𝑩 ≡ q ̇ 𝑩 holds extensionally, that is, `∀ x, (𝑩 ⟦ p ⟧) x ≡ (q ̇ 𝑩) x`.

#### Lift-invariance of ⊧

The ⊧ relation is also invariant under the algebraic lift and lower operations.

```
module _ {𝓤 𝓦 : Universe}{𝑨 : Algebra 𝓤 𝑆} where

⊧-Lift-invar : DFunExt → (p q : Term X) → 𝑨 ⊧ p ≈ q → Lift-alg 𝑨 𝓦 ⊧ p ≈ q
⊧-Lift-invar fe p q Apq = ⊧-I-invar fe (Lift-alg 𝑨 _) p q Apq Lift-≅

⊧-lower-invar : DFunExt → (p q : Term X) → Lift-alg 𝑨 𝓦 ⊧ p ≈ q  →  𝑨 ⊧ p ≈ q
⊧-lower-invar fe p q lApq = ⊧-I-invar fe 𝑨 p q lApq (≅-sym Lift-≅)

```

#### Subalgebraic invariance of ⊧

Identities modeled by an algebra 𝑨 are also modeled by every subalgebra of 𝑨, which fact can be formalized as follows.

```
module _ {𝓤 𝓦 : Universe}
-- (fwxw : dfunext (𝓦 ⊔ 𝓧) 𝓦)(fvu : dfunext 𝓥 𝓤)
where

⊧-S-invar : DFunExt → {𝑨 : Algebra 𝓤 𝑆}(𝑩 : Algebra 𝓦 𝑆){p q : Term X}
→          𝑨 ⊧ p ≈ q  →  𝑩 ≤ 𝑨  →  𝑩 ⊧ p ≈ q
⊧-S-invar fe {𝑨} 𝑩 {p}{q} Apq B≤A = (fe (𝓧 ⊔ 𝓦) 𝓦) λ b → (embeddings-are-lc ∣ h ∣ ∥ B≤A ∥) (ξ b)
where
h : hom 𝑩 𝑨
h = ∣ B≤A ∣

ξ : ∀ b → ∣ h ∣ ((𝑩 ⟦ p ⟧) b) ≡ ∣ h ∣ ((𝑩 ⟦ q ⟧) b)
ξ b = ∣ h ∣((𝑩 ⟦ p ⟧) b)   ≡⟨ comm-hom-term (fe 𝓥 𝓤) 𝑨 h p b ⟩
(𝑨 ⟦ p ⟧)(∣ h ∣ ∘ b) ≡⟨ happly Apq (∣ h ∣ ∘ b) ⟩
(𝑨 ⟦ q ⟧)(∣ h ∣ ∘ b) ≡⟨ (comm-hom-term (fe 𝓥 𝓤) 𝑨 h q b)⁻¹ ⟩
∣ h ∣((𝑩 ⟦ q ⟧) b)   ∎

```

Next, identities modeled by a class of algebras is also modeled by all subalgebras of the class. In other terms, every term equation `p ≈ q` that is satisfied by all `𝑨 ∈ 𝒦` is also satisfied by every subalgebra of a member of 𝒦.

```
⊧-S-class-invar : DFunExt → {𝒦 : Pred (Algebra 𝓤 𝑆)(ov 𝓤)}(p q : Term X)
→                𝒦 ⊧ p ≋ q → (𝑩 : SubalgebraOfClass{𝓦} 𝒦) → ∣ 𝑩 ∣ ⊧ p ≈ q
⊧-S-class-invar fe p q Kpq (𝑩 , 𝑨 , SA , (ka , BisSA)) = ⊧-S-invar fe 𝑩 {p}{q}((Kpq ka)) (h , hem)
where
h : hom 𝑩 𝑨
h = ∘-hom 𝑩 𝑨 (∣ BisSA ∣) ∣ snd SA ∣
hem : is-embedding ∣ h ∣
hem = ∘-embedding (∥ snd SA ∥) (iso→embedding BisSA)
```

#### Product invariance of ⊧

An identity satisfied by all algebras in an indexed collection is also satisfied by the product of algebras in that collection.

```
module _ {𝓤 𝓦 : Universe}(I : 𝓦 ̇)(𝒜 : I → Algebra 𝓤 𝑆) where

⊧-P-invar : DFunExt → {p q : Term X} → (∀ i → 𝒜 i ⊧ p ≈ q) → ⨅ 𝒜 ⊧ p ≈ q
⊧-P-invar fe {p}{q} 𝒜pq = γ
where
γ : ⨅ 𝒜 ⟦ p ⟧  ≡  ⨅ 𝒜 ⟦ q ⟧
γ = (fe (𝓧 ⊔ 𝓤 ⊔ 𝓦) (𝓤 ⊔ 𝓦)) λ a → (⨅ 𝒜 ⟦ p ⟧) a      ≡⟨ interp-prod (fe 𝓥 (𝓤 ⊔ 𝓦)) p 𝒜 a ⟩
(λ i → (𝒜 i ⟦ p ⟧)(λ x → (a x)i)) ≡⟨ (fe 𝓦 𝓤) (λ i → cong-app (𝒜pq i) (λ x → (a x) i)) ⟩
(λ i → (𝒜 i ⟦ q ⟧)(λ x → (a x)i)) ≡⟨ (interp-prod (fe 𝓥 (𝓤 ⊔ 𝓦)) q 𝒜 a)⁻¹ ⟩
(⨅ 𝒜 ⟦ q ⟧) a                     ∎

```

An identity satisfied by all algebras in a class is also satisfied by the product of algebras in the class.

```
⊧-P-class-invar : DFunExt → {𝒦 : Pred (Algebra 𝓤 𝑆)(ov 𝓤)}{p q : Term X}
→                𝒦 ⊧ p ≋ q → (∀ i → 𝒜 i ∈ 𝒦) → ⨅ 𝒜 ⊧ p ≈ q

⊧-P-class-invar fe {𝒦}{p}{q}α K𝒜 = ⊧-P-invar fe {p}{q}λ i → α (K𝒜 i)

```

Another fact that will turn out to be useful is that a product of a collection of algebras models p ≈ q if the lift of each algebra in the collection models p ≈ q.

```
⊧-P-lift-invar : DFunExt → {p q : Term X}
→               (∀ i → (Lift-alg (𝒜 i) 𝓦) ⊧ p ≈ q)  →  ⨅ 𝒜 ⊧ p ≈ q

⊧-P-lift-invar fe {p}{q} α = ⊧-P-invar fe {p}{q}Aipq
where
Aipq : ∀ i → (𝒜 i) ⊧ p ≈ q
Aipq i = ⊧-lower-invar fe p q (α i) --  (≅-sym Lift-≅)

```

#### Homomorphic invariance of ⊧

If an algebra 𝑨 models an identity p ≈ q, then the pair (p , q) belongs to the kernel of every homomorphism φ : hom (𝑻 X) 𝑨 from the term algebra to 𝑨; that is, every homomorphism from 𝑻 X to 𝑨 maps p and q to the same element of 𝑨.

```
module _ {𝓤 𝓦 : Universe}{𝑨 : Algebra 𝓤 𝑆} where

⊧-H-invar : DFunExt → {p q : Term X}(φ : hom (𝑻 X) 𝑨) → 𝑨 ⊧ p ≈ q  →  ∣ φ ∣ p ≡ ∣ φ ∣ q

⊧-H-invar fe {p}{q} φ β = ∣ φ ∣ p      ≡⟨ ap ∣ φ ∣ (term-agreement {fe = (fe 𝓥 (ov 𝓧))} p) ⟩
∣ φ ∣((𝑻 X ⟦ p ⟧) ℊ)   ≡⟨ (comm-hom-term (fe 𝓥 𝓤) 𝑨 φ p ℊ ) ⟩
(𝑨 ⟦ p ⟧) (∣ φ ∣ ∘ ℊ)  ≡⟨ happly β (∣ φ ∣ ∘ ℊ ) ⟩
(𝑨 ⟦ q ⟧) (∣ φ ∣ ∘ ℊ)  ≡⟨ (comm-hom-term (fe 𝓥 𝓤) 𝑨 φ q ℊ )⁻¹ ⟩
∣ φ ∣ ((𝑻 X ⟦ q ⟧) ℊ)  ≡⟨(ap ∣ φ ∣ (term-agreement {fe = (fe 𝓥 (ov 𝓧))} q))⁻¹ ⟩
∣ φ ∣ q                ∎

```

More generally, an identity is satisfied by all algebras in a class if and only if that identity is invariant under all homomorphisms from the term algebra `𝑻 X` into algebras of the class. More precisely, if `𝒦` is a class of `𝑆`-algebras and `𝑝`, `𝑞` terms in the language of `𝑆`, then,

`𝒦 ⊧ p ≈ q ⇔ ∀ 𝑨 ∈ 𝒦, ∀ φ : hom (𝑻 X) 𝑨, φ ∘ (𝑝 ̇ (𝑻 X)) = φ ∘ (𝑞 ̇ (𝑻 X))`.

```
module _ {𝒦 : Pred (Algebra 𝓤 𝑆)(ov 𝓤)}  where

-- ⇒ (the "only if" direction)
⊧-H-class-invar : DFunExt → {p q : Term X}
→                𝒦 ⊧ p ≋ q → ∀ 𝑨 φ → 𝑨 ∈ 𝒦 → ∣ φ ∣ ∘ (𝑻 X ⟦ p ⟧) ≡ ∣ φ ∣ ∘ (𝑻 X ⟦ q ⟧)
⊧-H-class-invar fe {p}{q} α 𝑨 φ ka = (fe (ov 𝓧) 𝓤) ξ
where
ξ : ∀(𝒂 : X → ∣ 𝑻 X ∣ ) → ∣ φ ∣ ((𝑻 X ⟦ p ⟧) 𝒂) ≡ ∣ φ ∣ ((𝑻 X ⟦ q ⟧) 𝒂)
ξ 𝒂 = ∣ φ ∣ ((𝑻 X ⟦ p ⟧) 𝒂)  ≡⟨ comm-hom-term (fe 𝓥 𝓤) 𝑨 φ p 𝒂 ⟩
(𝑨 ⟦ p ⟧)(∣ φ ∣ ∘ 𝒂)   ≡⟨ happly (α ka) (∣ φ ∣ ∘ 𝒂) ⟩
(𝑨 ⟦ q ⟧)(∣ φ ∣ ∘ 𝒂)   ≡⟨ (comm-hom-term (fe 𝓥 𝓤) 𝑨 φ q 𝒂)⁻¹ ⟩
∣ φ ∣ ((𝑻 X ⟦ q ⟧) 𝒂)  ∎

-- ⇐ (the "if" direction)
⊧-H-class-coinvar : DFunExt → {p q : Term X}
→  (∀ 𝑨 φ → 𝑨 ∈ 𝒦 → ∣ φ ∣ ∘ (𝑻 X ⟦ p ⟧) ≡ ∣ φ ∣ ∘ (𝑻 X ⟦ q ⟧)) → 𝒦 ⊧ p ≋ q

⊧-H-class-coinvar fe {p}{q} β {𝑨} ka = γ
where
φ : (𝒂 : X → ∣ 𝑨 ∣) → hom (𝑻 X) 𝑨
φ 𝒂 = lift-hom 𝑨 𝒂

γ : 𝑨 ⊧ p ≈ q
γ = (fe (𝓧 ⊔ 𝓤) 𝓤) λ 𝒂 → (𝑨 ⟦ p ⟧)(∣ φ 𝒂 ∣ ∘ ℊ)     ≡⟨(comm-hom-term (fe 𝓥 𝓤) 𝑨 (φ 𝒂) p ℊ)⁻¹ ⟩
(∣ φ 𝒂 ∣ ∘ (𝑻 X ⟦ p ⟧)) ℊ  ≡⟨ cong-app (β 𝑨 (φ 𝒂) ka) ℊ ⟩
(∣ φ 𝒂 ∣ ∘ (𝑻 X ⟦ q ⟧)) ℊ  ≡⟨ (comm-hom-term (fe 𝓥 𝓤) 𝑨 (φ 𝒂) q ℊ) ⟩
(𝑨 ⟦ q ⟧)(∣ φ 𝒂 ∣ ∘ ℊ)     ∎

⊧-H : DFunExt → {p q : Term X} → 𝒦 ⊧ p ≋ q ⇔ (∀ 𝑨 φ → 𝑨 ∈ 𝒦 → ∣ φ ∣ ∘ (𝑻 X ⟦ p ⟧) ≡ ∣ φ ∣ ∘(𝑻 X ⟦ q ⟧))
⊧-H fe {p}{q} = ⊧-H-class-invar fe {p}{q} , ⊧-H-class-coinvar fe {p}{q}

```