---
layout: default
title : "Setoid.Varieties.SoundAndComplete module (The Agda Universal Algebra Library)"
date : "2021-01-14"
author: "agda-algebras development team"
---
#### Entailment, derivation rules, soundness and completeness
This is the [Setoid.Varieties.SoundAndComplete][] module of the [Agda Universal Algebra Library][].
This module is based on [Andreas Abel's Agda formalization of Birkhoff's completeness theorem](http://www.cse.chalmers.se/~abela/agda/MultiSortedAlgebra.pdf).
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module Setoid.Varieties.SoundAndComplete where
open import Agda.Primitive using () renaming ( Set to Type )
open import Data.Product using ( _,_ ; Σ-syntax ; _×_ ; proj₁ ; proj₂ )
open import Function using ( _∘_ ; flip ) renaming ( Func to _⟶_ )
open import Level using ( Level ; _⊔_ )
open import Relation.Binary using ( Setoid ; IsEquivalence )
open import Relation.Unary using ( Pred ; _∈_ )
open import Relation.Binary.PropositionalEquality using ( refl )
import Relation.Binary.Reasoning.Setoid as SetoidReasoning
open import Overture using ( OperationSymbolsOf ; 𝓞 ; 𝓥 ; Signature ; 𝑆 )
open import Overture.Terms using ( Term )
open import Setoid.Algebras using ( Algebra ; ov ; 𝔻[_] )
open import Setoid.Signatures using ( ⟨_⟩ )
open import Setoid.Terms using ( module Environment ; Sub ; _[_] )
open Setoid using ( Carrier ; _≈_ ; isEquivalence )
open _⟶_ renaming ( to to _⟨$⟩_ )
open Term
private variable
χ α ρᵃ ι ℓ : Level
X Γ Δ : Type χ
f : OperationSymbolsOf 𝑆
I : Type ι
```
-->
```agda
record Eq {χ : Level} : Type (ov {𝑆 = 𝑆} χ) where
constructor _≈̇_
field
{cxt} : Type χ
lhs : Term {𝑆 = 𝑆} cxt
rhs : Term {𝑆 = 𝑆} cxt
infix 6 _≈̇_
open Eq public
toEq : {χ ι : Level}{Idx : Type ι}{X : Type χ}
→ (Idx → Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) → (Idx → Eq {χ = χ})
toEq ℰ i = proj₁ (ℰ i) ≈̇ proj₂ (ℰ i)
_⊧_ : (𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ)(term-identity : Eq {χ = χ}) → Type _
𝑨 ⊧ (p ≈̇ q) = Equal p q where open Environment 𝑨
record _⊫_ (𝒦 : Pred (Algebra {𝑆 = 𝑆} α ρᵃ) ℓ)(eq : Eq {χ = χ}) : Type (ℓ ⊔ χ ⊔ ov {𝑆 = 𝑆}(α ⊔ ρᵃ)) where
constructor ⊫-intro
field ⊫-proof : ∀ (𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ) → 𝒦 𝑨 → 𝑨 ⊧ eq
open _⊫_ public
infix 5 _⊫_
_⊨_ : (𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ) → (I → Eq {χ = χ}) → Type _
𝑨 ⊨ ℰ = ∀ i → Equal (lhs (ℰ i))(rhs (ℰ i)) where open Environment 𝑨
_∥≈_ : Pred (Algebra {𝑆 = 𝑆} α ρᵃ) ℓ → (I → Eq {χ = χ}) → Type _
𝒦 ∥≈ ℰ = ∀ i → 𝒦 ⊫ ℰ i
ModTuple : (I → Eq {χ = χ}) → Pred(Algebra {𝑆 = 𝑆} α ρᵃ) _
ModTuple ℰ = _⊨ ℰ
module _ {α ρᵃ ℓ χ : Level} {X : Type χ} where
Mod : Pred(Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) ℓ → Pred (Algebra {𝑆 = 𝑆} α ρᵃ) _
Mod ℰ 𝑨 = ∀ {p q} → (p , q) ∈ ℰ → Equal p q
where open Environment 𝑨
Th : Pred (Algebra {𝑆 = 𝑆} α ρᵃ) ℓ → Pred(Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) _
Th 𝒦 = λ (p , q) → 𝒦 ⊫ (p ≈̇ q)
ℑTh : Pred(Term {𝑆 = 𝑆} X × Term {𝑆 = 𝑆} X) (ℓ ⊔ χ ⊔ ov {𝑆 = 𝑆} (α ⊔ ρᵃ)) → Type _
ℑTh P = Σ[ p ∈ (Term _ × Term _) ] p ∈ P
ThTuple : (𝒦 : Pred (Algebra {𝑆 = 𝑆} α ρᵃ) ℓ) → ℑTh (Th 𝒦) → Eq {χ = χ}
ThTuple 𝒦 = λ i → proj₁ (proj₁ i) ≈̇ proj₂ (proj₁ i)
module _ {𝑆 : Signature 𝓞 𝓥}{α}{ρᵃ}{ι}{I : Type ι} where
_⊃_ : (E : I → Eq {𝑆 = 𝑆}{χ = χ}) (eq : Eq {𝑆 = 𝑆}{χ = χ}) → Type _
E ⊃ eq = (M : Algebra {𝑆 = 𝑆} α ρᵃ) → M ⊨ E → M ⊧ eq
```
##### Derivations in a context
`E ⊢ Γ ▹ p ≈ q`{.AgdaDatatype} is the **derivability** relation of equational
logic: the equation `p ≈ q`, between terms over the context `Γ`, is derivable from
the set of equations `E`. Its constructors *are* the rules of the logic, and
there are only six of them: `hyp`{.AgdaInductiveConstructor} invokes an equation
of `E`; `app`{.AgdaInductiveConstructor} is congruence, deriving equality of two
applications of an operation symbol from equality of their arguments;
`sub`{.AgdaInductiveConstructor} substitutes into a derivation; and
`refl`{.AgdaInductiveConstructor}, `sym`{.AgdaInductiveConstructor} and
`trans`{.AgdaInductiveConstructor} are the equivalence-relation rules.
`⊢▹≈IsEquiv`{.AgdaFunction} packages that last group as an
`IsEquivalence`{.AgdaRecord} for derivability in a fixed context, which is what
allows derivations to be chained in equational-reasoning style.
```agda
module _ {𝑆 : Signature 𝓞 𝓥}{χ ι : Level} where
data _⊢_▹_≈_ {I : Type ι}(E : I → Eq) : (X : Type χ)(p q : Term {𝑆 = 𝑆} X) → Type (ι ⊔ ov {𝑆 = 𝑆} χ) where
hyp : ∀ (i : I) → let p ≈̇ q = E i in E ⊢ _ ▹ p ≈ q
app : ∀ {f : OperationSymbolsOf 𝑆}{ps qs} → (∀ i → E ⊢ Γ ▹ ps i ≈ qs i) → E ⊢ Γ ▹ node f ps ≈ node f qs
sub : ∀ {p q : Term {𝑆 = 𝑆} Δ} → E ⊢ Δ ▹ p ≈ q → ∀ (σ : Sub {𝑆 = 𝑆} Γ Δ) → E ⊢ Γ ▹ p [ σ ] ≈ q [ σ ]
refl : ∀ {p : Term {𝑆 = 𝑆} Γ} → E ⊢ Γ ▹ p ≈ p
sym : ∀ {p q : Term {𝑆 = 𝑆} Γ} → E ⊢ Γ ▹ p ≈ q → E ⊢ Γ ▹ q ≈ p
trans : ∀ {p q r : Term {𝑆 = 𝑆} Γ} → E ⊢ Γ ▹ p ≈ q → E ⊢ Γ ▹ q ≈ r → E ⊢ Γ ▹ p ≈ r
infix 4 _⊢_▹_≈_
⊢▹≈IsEquiv : {I : Type ι}{E : I → Eq} → IsEquivalence (E ⊢ Γ ▹_≈_)
⊢▹≈IsEquiv = record { refl = refl ; sym = sym ; trans = trans }
```
##### Soundness of the inference rules
**Soundness** is the half of the correspondence that says whatever is derivable is
true: in any algebra `𝑨` that models every equation of `E`, a derivation of
`p ≈ q` yields a proof that `𝑨` satisfies `p ≈ q`.
`sound`{.AgdaFunction} is the induction over derivations that establishes it, with
one case per rule. A hypothesis is discharged by the assumption `V` that
`𝑨 ⊨ E`; congruence by `cong`{.AgdaField} of the interpretation; substitution by
the `substitution`{.AgdaFunction} lemma of [Setoid.Terms.Basic][], which relates a
substituted term to the same term under a reinterpreted environment; and the last
three rules by the corresponding properties of `𝑨`'s own equality. The converse,
completeness, is proved further down this module.
```agda
module Soundness
{χ α ι : Level}{I : Type ι} (E : I → Eq {χ = χ})
(𝑨 : Algebra {𝑆 = 𝑆} α ρᵃ)
(V : 𝑨 ⊨ E)
where
open Algebra 𝑨 using ( Interp )
open SetoidReasoning 𝔻[ 𝑨 ]
open Environment 𝑨 renaming ( ⟦_⟧s to ⟪_⟫ )
open IsEquivalence renaming ( refl to refl≈ ; sym to sym≈ ; trans to trans≈ )
sound : ∀ {p q} → E ⊢ X ▹ p ≈ q → 𝑨 ⊧ (p ≈̇ q)
sound (hyp i) = V i
sound (app {f = f} es) ρ = Interp .cong (refl , λ i → sound (es i) ρ)
sound (sub {p = p} {q} Epq σ) ρ = begin
⟦ p [ σ ] ⟧ ⟨$⟩ ρ ≈⟨ substitution p σ ρ ⟩
⟦ p ⟧ ⟨$⟩ ⟪ σ ⟫ ρ ≈⟨ sound Epq (⟪ σ ⟫ ρ) ⟩
⟦ q ⟧ ⟨$⟩ ⟪ σ ⟫ ρ ≈˘⟨ substitution q σ ρ ⟩
⟦ q [ σ ] ⟧ ⟨$⟩ ρ ∎
sound (refl {p = p}) = refl≈ isEquiv {x = p}
sound (sym {p = p} {q} Epq) = sym≈ isEquiv {x = p}{q} (sound Epq)
sound (trans{p = p}{q}{r} Epq Eqr) = trans≈ isEquiv {i = p}{q}{r} (sound Epq)(sound Eqr)
```
The deductive closure of a set E is the set of equations modeled by all models of E;
that is, `Th Mod E`.
The soundness proof above shows
∀ X → E ⊢ X ▹ p ≈ q → (p , q) ∈ Th Mod ℰ.
That is, `∀ X → E ⊢ X ▹ p ≈ q → Mod E ⊫ p ≈ q`.
The converse is Birkhoff's completeness theorem:
if `Mod E ⊫ p ≈ q`, then `E ⊢ X ▹ p ≈ q`.
We will prove that result next.
##### Birkhoff's completeness theorem
The proof proceeds by constructing a relatively free algebra consisting of term
quotiented by derivable equality `E ⊢ X ▹ _≈_`. It then suffices to prove that this
model satisfies all equations in `E`.
We denote by `𝔽[ X ]` the *relatively free algebra* over `X` (relative to `E`), which
is defined as `Term X` modulo `E ⊢ X ▹ _≈_`. This algebra `𝔽[ X ]` is "free" or
"initial" in the variety of algebras satisfying the identities in `E` in the sense
that it satisfies the following universal property: for each algebra `𝑨`, if `𝑨 ⊧ E`,
then there is a unique homomorphism from `𝔽[ X ]` to `𝑨`.
```agda
module FreeAlgebra {𝑆 : Signature 𝓞 𝓥}{χ : Level}{ι : Level}{I : Type ι}(E : I → Eq {χ = χ}) where
open Algebra
FreeDomain : Type χ → Setoid _ _
FreeDomain X = record { Carrier = Term X
; _≈_ = E ⊢ X ▹_≈_
; isEquivalence = ⊢▹≈IsEquiv
}
FreeInterp : ∀ {X} → (⟨ 𝑆 ⟩ (FreeDomain X)) ⟶ (FreeDomain X)
FreeInterp ⟨$⟩ (f , ts) = node f ts
FreeInterp .cong (refl , h) = app h
𝔽[_] : Type χ → Algebra {𝑆 = 𝑆} (ov {𝑆 = 𝑆} χ) (ι ⊔ ov {𝑆 = 𝑆} χ)
Domain 𝔽[ X ] = FreeDomain X
Interp 𝔽[ X ] = FreeInterp
σ₀ : {X : Type χ} → Sub {𝑆 = 𝑆} X X
σ₀ x = ℊ x
identity : (t : Term {𝑆 = 𝑆} X) → E ⊢ X ▹ t [ σ₀ ] ≈ t
identity (ℊ x) = refl
identity (node f ts) = app (identity ∘ ts)
```
Evaluation in the term model is substitution `E ⊢ X ▹ ⟦t⟧σ ≈ t[σ]`. (This would
hold "on the nose" if we had function extensionality.)
(We put this and the next two lemmas into their own submodules to emphasize
the fact that these results are independent of the chosen variable symbol
type `X` (or `Δ`, or `Γ`), which is an arbitrary inhabitant of `Type χ`.)
```agda
module _ {X : Type χ} where
open Environment 𝔽[ X ]
evaluation : (t : Term {𝑆 = 𝑆} Δ) (σ : Sub {𝑆 = 𝑆} X Δ) → E ⊢ X ▹ (⟦ t ⟧ ⟨$⟩ σ) ≈ (t [ σ ])
evaluation (ℊ x) σ = refl
evaluation (node f ts) σ = app (flip (evaluation ∘ ts) σ)
module _ {Δ : Type χ} where
satisfies : 𝔽[ Δ ] ⊨ E
satisfies i σ = begin
⟦ p ⟧ ⟨$⟩ σ ≈⟨ evaluation p σ ⟩
p [ σ ] ≈⟨ sub (hyp i) σ ⟩
q [ σ ] ≈˘⟨ evaluation q σ ⟩
⟦ q ⟧ ⟨$⟩ σ ∎
where
open Environment 𝔽[ Δ ]
open SetoidReasoning (Domain 𝔽[ Δ ]) ; p = lhs (E i) ; q = rhs (E i)
```
We are finally ready to formally state and prove Birkhoff's Completeness Theorem,
which asserts that every valid consequence is derivable.
```agda
module _ {Γ : Type χ} where
completeness : ∀ p q → ModTuple E ⊫ (p ≈̇ q) → E ⊢ Γ ▹ p ≈ q
completeness p q V = begin
p ≈˘⟨ identity p ⟩
p [ σ₀ ] ≈˘⟨ evaluation p σ₀ ⟩
⟦ p ⟧ ⟨$⟩ σ₀ ≈⟨ V .⊫-proof 𝔽[ Γ ] satisfies σ₀ ⟩
⟦ q ⟧ ⟨$⟩ σ₀ ≈⟨ evaluation q σ₀ ⟩
q [ σ₀ ] ≈⟨ identity q ⟩
q ∎
where
open Environment 𝔽[ Γ ]
open SetoidReasoning (Domain 𝔽[ Γ ])
```