Sub-Birkhoff

Abstract

A fundamental result in rewriting is:

1. is Birkhoff’s theorem expressing that semantic consequence coincides with syntactic consequence. 2. expresses that equality in equational logic (=) coincides with convertability in rewriting, a property known as logicality.

We show that the result can be extended to hold for several sub-equational logics by restricting the first and third components of the fundamental result in suitable ways. In this way, some hitherto unrelated notions from literature can be related. For instance, Zantema’s notion of quasimodel corresponds to Meseguer’s notion of rewrite logic (equational logic without symmetry) which corresponds to rewriting.