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

11/15/2021
by   Andreas Abel, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset