---
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 #-}

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

module Setoid.Varieties.SoundAndComplete {𝑆 : Signature π“ž π“₯} where

open import Agda.Primitive   using () renaming ( Set to Type )

-- imports from the Agda Standard Library ---------------------------------------
open import Data.Product     using ( _,_ ; Ξ£-syntax ; _Γ—_ )
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

-- Imports from the Agda Universal Algebra Library -------------------------------
open import Overture                  using ( proj₁ ; projβ‚‚ ; OperationSymbolsOf )
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
-- Equations
-- An equation is a pair (s , t) of terms in the same context.
record Eq : Type (ov Ο‡) where
  constructor _β‰ˆΜ‡_
  field
    {cxt}  : Type Ο‡
    lhs    : Term cxt
    rhs    : Term cxt
infix 6 _β‰ˆΜ‡_
open Eq public

-- The "impedance shim" between the library's two theory shapes.  The interpretability
-- machinery (Setoid.Varieties.Interpretation) records a theory as an indexed family of
-- *pairs of terms* (Idx β†’ Term X Γ— Term X); the derivation calculus _⊒_β–Ή_β‰ˆ_ and the
-- free algebra 𝔽[_] below consume an indexed family of *equations* (I β†’ Eq).  toEq
-- converts the former to the latter.  No companion is needed for satisfaction: 𝑨 βŠ¨β‚‘ β„°
-- there and 𝑨 ⊨ toEq β„° below coincide definitionally (both unfold to pointwise
-- equality of the two interpreted terms under all environments).
toEq : {Ο‡ ΞΉ : Level}{Idx : Type ΞΉ}{X : Type Ο‡}
  β†’ (Idx β†’ Term X Γ— Term X) β†’ (Idx β†’ Eq {Ο‡ = Ο‡})
toEq β„° i = proj₁ (β„° i) β‰ˆΜ‡ projβ‚‚ (β„° i)

-- Equation p β‰ˆΜ‡ q holding in algebra M. (type \~~\^. to get β‰ˆΜ‡; type \models to get ⊧)
_⊧_ : (𝑨 : Algebra Ξ± ρᡃ)(term-identity : Eq{Ο‡}) β†’ Type _
𝑨 ⊧ (p β‰ˆΜ‡ q) = Equal p q where open Environment 𝑨

-- 𝒦 ⊫ (p β‰ˆΜ‡ q) asserts that every algebra in the class 𝒦 models the equation
-- p β‰ˆΜ‡ q.  This is a one-field record (a frozen wrapper around the underlying
-- βˆ€ 𝑨 β†’ 𝒦 𝑨 β†’ 𝑨 ⊧ eq) rather than a plain function type, so that the equation
-- stays visible as an Eq during unification.  Inferring the implicit {p}{q} of
-- a preservation lemma such as V-id1 then unifies the two equations
-- structurally at the Eq level β€” the record type former _⊫_ is injective β€”
-- instead of unfolding _⊫_ β†’ _⊧_ β†’ Equal β†’ ⟦_⟧ and getting stuck on the term
-- interpreter.  (See issue #361.  Note _⊧_ and Equal still reduce
-- definitionally, so the proofs that compute with them are unaffected.)
record _⊫_ (𝒦 : Pred (Algebra Ξ± ρᡃ) β„“)(eq : Eq{Ο‡}) : Type (β„“ βŠ” Ο‡ βŠ” ov(Ξ± βŠ” ρᡃ)) where
  constructor ⊫-intro
  field ⊫-proof : βˆ€ (𝑨 : Algebra Ξ± ρᡃ) β†’ 𝒦 𝑨 β†’ 𝑨 ⊧ eq          -- (type \||= to get ⊫)
open _⊫_ public
infix 5 _⊫_

-- An I-indexed set of equations inhabits the type I β†’ Eq.

-- For such `β„° : I β†’ Eq`...

-- ...`𝑨 ⊨ β„°` is the assertion that the algebra 𝑨 models every equation in β„°.
_⊨_ : (𝑨 : Algebra Ξ± ρᡃ) β†’ (I β†’ Eq{Ο‡}) β†’ Type _
𝑨 ⊨ β„° = βˆ€ i β†’ Equal (lhs (β„° i))(rhs (β„° i)) where open Environment 𝑨  --   (type \|= to get ⊨)

-- ...`𝒦 βˆ₯β‰ˆ β„°` is the assertion that every algebra in 𝒦 models every equation in β„°.
_βˆ₯β‰ˆ_ : Pred (Algebra Ξ± ρᡃ) β„“ β†’ (I β†’ Eq{Ο‡}) β†’ Type _
𝒦 βˆ₯β‰ˆ β„° = βˆ€ i β†’ 𝒦 ⊫ β„° i

-- ...`Mod β„°` is the class of algebras that model every equation in β„°.
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 _ {Ξ±}{ρᡃ}{ΞΉ}{I : Type ΞΉ} where
  -- An entailment E βŠƒ eq holds iff it holds in all models of E.
  _βŠƒ_ : (E : I β†’ Eq{Ο‡}) (eq : Eq{Ο‡}) β†’ Type _
  E βŠƒ eq = (M : Algebra Ξ± ρᡃ) β†’ M ⊨ E β†’ M ⊧ eq
```

##### Derivations in a context

```agda
module _ {Ο‡ ΞΉ : 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    : βˆ€ {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

```agda
module Soundness
  {Ο‡ Ξ± ΞΉ : Level}{I : Type ΞΉ} (E : I β†’ Eq{Ο‡})
  (𝑨 : Algebra Ξ± ρᡃ)   -- We assume an algebra 𝑨
  (V : 𝑨 ⊨ E)          -- that models all equations in E.
  where
  open Algebra 𝑨 using ( Interp ) --  renaming (Domain to A)

  -- In any model 𝑨 that satisfies the equations E, derived equality is actual equality.
  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 {Ο‡ : Level}{ΞΉ : Level}{I : Type ΞΉ}(E : I β†’ Eq) where
  open Algebra

  -- Domain of the relatively free algebra.
  FreeDomain : Type Ο‡ β†’ Setoid _ _
  FreeDomain X = record  { Carrier        = Term X
                         ; _β‰ˆ_            = E ⊒ X β–Ή_β‰ˆ_
                         ; isEquivalence  = βŠ’β–Ήβ‰ˆIsEquiv
                         }

  -- The interpretation of an operation is simply the operation itself.
  -- This works since E ⊒ X β–Ή_β‰ˆ_ is a congruence.
  FreeInterp : βˆ€ {X} β†’ (⟨ 𝑆 ⟩ (FreeDomain X)) ⟢ (FreeDomain X)
  FreeInterp ⟨$⟩ (f , ts) = node f ts
  FreeInterp .cong (refl , h) = app h

  -- The relatively free algebra
  𝔽[_] : Type Ο‡ β†’ Algebra (ov Ο‡) (ΞΉ βŠ” ov Ο‡)
  Domain 𝔽[ X ] = FreeDomain X
  Interp 𝔽[ X ] = FreeInterp

  -- The identity substitution Οƒβ‚€ maps variables to themselves.
  Οƒβ‚€ : {X : Type Ο‡} β†’ Sub X X
  Οƒβ‚€ x = β„Š x

  -- Οƒβ‚€ acts indeed as identity.
  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
    -- The term model satisfies all the equations it started out with.
    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 𝔽[ Ξ“ ])
```