Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda
Logic in Computer Science
2021-11-16 v1
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.
Keywords
Cite
@article{arxiv.2111.07936,
title = {Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda},
author = {Andreas Abel},
journal= {arXiv preprint arXiv:2111.07936},
year = {2021}
}