On equational completeness theorems

TL;DR

This paper characterizes when certain logical systems admit equational completeness theorems, linking this property to algebraic and syntactic features, and analyzes the decidability of recognizing such logics.

Contribution

It provides a characterization of logics with equational completeness theorems, including conditions for protoalgebraic logics and decidability results.

Findings

Logics with equational completeness are either locally tabular or have tautologies.

A protoalgebraic logic admits an equational completeness theorem iff it has two distinct, logically equivalent formulas.

Decidability of recognizing such logics varies: decidable for finite matrices and locally tabular logics, undecidable for arbitrary finite Hilbert calculi.

Abstract

A logic is said to admit an equational completeness theorem when it can be interpreted into the equational consequence relative to some class of algebras. We characterize logics admitting an equational completeness theorem that are either locally tabular or have some tautology. In particular, it is shown that a protoalgebraic logic admits an equational completeness theorem precisely when its has two distinct logically equivalent formulas. While the problem of determining whether a logic admits an equational completeness theorem is shown to be decidable both for logics presented by a finite set of finite matrices and for locally tabular logics presented by a finite Hilbert calculus, it becomes undecidable for arbitrary logics presented by finite Hilbert calculi.