Congruence Filter Pairs, Adjoints and Leibniz Hierarchy

TL;DR

This paper explores filter pairs as a framework for representing and analyzing finitary, substitution-invariant logics, establishing connections with algebraic semantics and properties like the Craig interpolation property.

Contribution

It introduces congruence filter pairs and characterizes logics with algebraic semantics using these structures, linking algebraic and logical properties through Galois connections.

Findings

Characterization of logics with algebraic semantics via congruence filter pairs

Criteria for Leibniz hierarchy classification using Galois connections

Bridge theorem linking amalgamation property to Craig interpolation property

Abstract

We review the notion of (finitary) filter pair as a tool for creating and analyzing logics. A filter pair can be seen as a presentation of a logic, given by presenting its lattice of theories as the image of a lattice homomorphism, with certain properties ensuring that the resulting logic is finitary and substitution invariant. Every finitary, substitution invariant logic arises from a filter pair. Particular classes of logics can be characterized as arising from special classes of filter pairs. We consider so-called congruence filter pairs, i.e. filter pairs for which the domain of the lattice homomorphism is a lattice of congruences for some quasivariety. We show that the class of logics admitting a presentation by such a filter pair is exactly the class of logics having an algebraic semantics. We study the properties of a certain Galois connection coming with such filter pairs. We give criteria for a congruence filter pair to present a logic in some classes of the Leibniz hierarchy by means of this Galois connection, and its interplay with the Leibniz operator. As an application, we show a bridge theorem, stating that the amalgamation property implies the Craig interpolation property, for a certain class of logics including non-protoalgebraic logics.