On the mathematical synthesis of equational logics

TL;DR

This paper develops a mathematical framework for synthesizing equational logics from algebraic metatheories, demonstrated through reconstructing Birkhoff's logic and creating a new logic for name-binding algebraic structures.

Contribution

It introduces a novel methodology for deriving equational logics from algebraic foundations, including applications to classical and new logic systems.

Findings

Reconstructed Birkhoff's Equational Logic mathematically.

Developed a new equational logic for name-binding operators.

Showed the applicability of the methodology to diverse algebraic structures.

Abstract

We provide a mathematical theory and methodology for synthesising equational logics from algebraic metatheories. We illustrate our methodology by means of two applications: a rational reconstruction of Birkhoff's Equational Logic and a new equational logic for reasoning about algebraic structure with name-binding operators.