Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda

TL;DR

This paper formalizes Birkhoff's completeness theorem for multi-sorted algebras within Agda, providing a machine-checked proof that equational validity in all models implies derivability from a set of equations.

Contribution

It presents the first formal proof of Birkhoff's completeness theorem for multi-sorted algebras in a proof assistant, enhancing rigor and reproducibility.

Findings

Formal proof of Birkhoff's completeness theorem in Agda

Verification of equational entailment in multi-sorted algebras

Reproduction of commented Agda code for transparency

Abstract

This document provides a formal proof of Birkhoff's completeness theorem for multi-sorted algebras which states that any equational entailment valid in all models is also provable in the equational theory. More precisely, if a certain equation is valid in all models that validate a fixed set of equations, then this equation is derivable from that set using the proof rules for a congruence. The proof has been formalized in Agda version 2.6.2 with the Agda Standard Library version 1.7 and this document reproduces the commented Agda code.