A Survey of Abstract Algebraic Logic
by Josep Maria Font, Ramon Jansana and Don Pigozzi
Studia Logica (Special Issue on Abstract Algebraic Logic, part II) 74 (2003) 13--97.
See the corrections at the bottom of this page.
Introduction
Algebraic logic was born in the XIXth century with the work of Boole, De Morgan, Peirce, Schröder, etc. on classical logic, see [12, 16]. They took logical equivalence rather than truth as the primitive logical predicate, and, exploiting the similarity between logical equivalence and equality, they developed logical systems in which metalogical investigations take on a distinctly algebraic character. In particular, Boole's work evolved into the modern theory of Boolean algebras, and that of De Morgan, Peirce and Schröder into the theory of relation algebras. Algebraic logic in this sense developed more-or-less independently of the logical systems of Frege and Russell and Whitehead where truth and logical truth were the underlying logical predicates. Reinforced by Hilbert's idea of metamathematics, this trend in logic became focused around the formal notions of assertion (logical validity and theoremhood) and logical inference. Thus we have from the beginning of the contemporary era of logic two approaches to the subject, one centered on the notion of logical equivalence and the other centered on the notions of assertion and inference.
It was not until much later that logicians started to think about connections between these two ways of looking at logic. Tarski ([131]) gave the precise connection between Boolean algebra and the classical propositional calculus. His approach builds on Lindenbaum's idea of viewing the set of formulas as an algebra with operations induced by the logical connectives. Logical equivalence is a congruence relation on the formula algebra, and the associated quotient algebra turns out to be a free Boolean algebra. This is the so-called Lindenbaum-Tarski method. The connection here between the two ways of looking at classical propositional logic is made by interpreting the logical equivalence of formulas A and B as the theoremhood of a suitable formula (A <--> B) in the assertional system. The connection between the predicate calculus and relation algebras is not so straightforward, and in fact, when the Lindenbaum-Tarski method is applied to the predicate calculus, it leads to cylindric and polyadic algebras rather than relation algebras.
Other logics not relaying on the (classical) notion of truth, like intuitionistic logic (centered on the notion of constructive mathematical proof) or multiple-valued logic, can also be approached from the two points of view, the equivalential and the assertional. And the connection between them, like in the predicate-logic case, can be complicated. For instance, when the Lindenbaum- Tarski method is applied to the infinite-valued logistic system of Lukasiewicz one gets not MV-algebras, but the so-called Wajsberg algebras. In contrast to Boolean, cylindric, polyadic, and Wajsberg algebras which were defined before the Lindenbaum-Tarski method was first applied to generate them from the appropriate assertional systems, Heyting algebras seem to be the first algebras of logic that were identified by applying the Lindenbaum-Tarski method to a known assertional system, namely the intuitionistic propositional calculus.
Traditionally algebraic logic has focused on the algebraic investigation of particular classes of algebras of logic, whether or not they could be connected to some known assertional system by means of the Lindenbaum-Tarski method. However, when such a connection could be established, there was interest in investigating the relationhip between various metalogical properties of the logistic system and the algebraic properties of the associated class of algebras (obtaining what are sometimes called bridge theorems). For example, it was discovered that there is a natural relation between the interpolation theorems of classical, intuitionistic, and intermediate propositional calculi, and the amalgamation properties of varieties of Heyting algebras. Similar connections were investigated between interpolation theorems in the predicate calculus and amalgamation results in varieties of cylindric and polyadic algebras.
Although interest in the traditional areas of algebraic logic has not diminished, the field has evolved considerably in other directions. The ad hoc methods by which a class of algebras is associated to a given logic have given way to a systematic investigation of broad classes of logics in an algebraic context. The focus has shifted to the process by which a class of algebras is associated with an arbitrary logic and away from the particular classes of algebras that are obtained when the process is applied to specific logics. The general theory of the algebraization of logical systems that has developed is called Abstract Algebraic Logic (AAL from now on).
One of the goals of AAL is to discover general criteria for a class of algebras (or for a class of mathematical objects closely related to algebras such as, for instance, logical matrices or generalized matrices) to be the algebraic counterpart of a logic, and to develop the methods for obtaining this algebraic counterpart. In this connection an abstraction of the Lindenbaum-Tarski method plays a major role.
Bridge theorems relating metalogical properties of a logic to algebraic properties of its algebraic counterpart take on added interest in the context of AAL. For example, it was known for some time that there is a close connection between the deduction theorem and the property of a class of algebras that its members have uniformly equationally definable principal congruences, but it is only in the more general context of AAL that the connection can be made precise. Indeed, the desire to find the proper context in which this connection could be made precise partly motivated the development of AAL. There are other bridge theorems that relate metalogical properties such as (Beth) definability, the existence of sensible Gentzen calculi, etc. with algebraic properties such as the property that epimorphisms are surjective, congruence extension, etc.
Another important goal of AAL is a classification of logical systems based on the algebraic properties of their algebraic counterpart. Ideally, when it is known that a given logic belongs to a particular group in the classification, one hopes there will be general theorems that provide important information about its properties and behaviour.
In this survey we try to describe the present state of research in AAL after recalling its main building blocks, both historically and conceptually. We think the subject is young enough so that understanding some points in its early history is necessary in order to fully appreciate it. This is not however a work on the details of this history, and we are going to use mainly a unified terminology and notation in order to facilitate the task of reading the paper and as a guide to the current and forthcoming literature. Three papers of a historical or survey nature relating to AAL are [25, 29, 117]. The following five papers [22, 51, 71, 107, 127] deal with various aspects of the prehistory of AAL.
Contents
Introduction1 The First Steps
1.1 Consequence operations and logics2 The Lindenbaum-Tarski Process Fully Generalized
1.2 Logical matrices
1.3 Lindenbaum-Tarski algebras2.1 Frege's principles3 The Core Theory of Abstract Algebraic Logic
2.2 Algebras and matrices canonically associated with a logic3.1 Elements of the general theory of matrices4 Extensions of the Core Theory
3.2 Protoalgebraic logics
3.3 Algebraizable logics
3.4 The Leibniz hierarchy4.1 k-deductive systems and universal algebra5 Generalized Matrix Semantics and Full Models
4.2 Gentzen systems and their generalizations
4.3 Equality-free universal Horn logic
4.4 Algebras of Logic
6 Extensions to More Complex Notions of Logic
6.1 The semantics-based approachReferences
6.2 The categorial approach
Corrections
An update will be published shortly fixing some infelicities in the wording of a definition in page 39, some inaccurate usages of it, and some mixed-up cross-references in page 40. Here you can download the preprint (156 KB).