Abstract algebraic logic

2020 Mathematics Subject Classification: Primary: 03-XX Secondary: 03G27 [MSN][ZBL]

Abstract algebraic logic is the study of logical equivalence, more precisely, the study of the relationship between logical equivalence and logical truth. Meta-logical investigations take on a different character when the emphasis is placed on logical equivalence, one that is very algebraic in character. But, in contrast to traditional algebraic logic, abstract algebraic logic focuses on the process by which a class of algebras is associated with a logical system rather than the algebras that are obtained in the process. The strength of the connection between logical equivalence and logical truth can vary greatly depending on the particular logical system under consideration. One of the main tasks of abstract algebraic logic is the classification of logical systems based on the strength of this connection. It is very strong in classical logic and this gives classical logic its distinctly algebraic character.

The way in which the algebras arise from logic has traditionally followed two distinct paths. The first is based on semantical considerations. In this approach the algebras are abstracted directly from a primitive intuitive notion of logical equivalence, and the assertional aspect of the logic (the notion of logical truth) is expressed in its terms. The development of classical propositional logic (cf. also Propositional calculus) followed this path with Boolean algebras coming before the classical propositional calculus (cf. also Boolean algebra). Relation algebras and the way they arose from the calculus of relations is the modern paradigm for the semantics-based method. In the logistic approach, or rule-based approach, the process is inverted. The assertional part comes first and logical equivalence and the associated algebras are then defined by means of the so-called Lindenbaum–Tarski process. The paradigm for the logistic method is the intuitionistic propositional calculus, where the class of Heyting algebras is constructed from Heyting's formalization of Brouwer's intuitionism by the Lindenbaum–Tarski process (cf. also Heyting formal system). Cylindric and polyadic algebras were obtained by applying the semantics-based method to first-order predicate logic, but, at least in the case of cylindric algebras, the influence of the logistic approach is strongly evident.

The basis of the abstract form of logical equivalence is Frege's principle that sentences, like proper names, have a denotation and that this denotation is their truth value. Two sentences are logically equivalent if they have the same denotation in every possible situation. Thus, according to Frege's principle, they are logically equivalent if they are true in exactly the same interpretations of the underlying uninterpreted logic. For logistic systems this principle has the following technical ramifications.

By a language type one means a set $\Lambda$ of connectives or operation symbols (cf. also Propositional connective), depending on whether one views them from a logical or algebraic perspective. Each connective has associated with it a natural number, called its rank or arity. The set $\operatorname {Fm}$ of formulas (terms in an algebraic context) is constructed from the connectives and a fixed, denumerable set of (formula) variable symbols in the usual way. The corresponding formula algebra is denoted by $\textbf{Fm}$. This is the "absolutely free" algebra of type $\Lambda$ with an $n$-ary operation $\lambda ^ { \operatorname{Fm} } : \operatorname{Fm} ^ { n } \rightarrow \operatorname{Fm}$ for each $\lambda \in \Lambda$ of arity $n$ such that $\lambda ^ { \mathbf{Fm} } ( \varphi_0 , \dots , \varphi _ { n - 1} )$ is the formula $\lambda \varphi_{0} , \ldots , \varphi _ { n - 1}$, in prefix notation, or $( \varphi _ { 0 } \lambda \varphi _ { 1 } )$ when $n = 2$ and infix notation is used. The operation of simultaneously substituting fixed but arbitrary formulas for variables is identified with the unique endomorphism of $\textbf{Fm}$ it determines. A logistic or deductive system is a pair $\mathcal{D} = \{ \mathbf{Fm} , \vdash _ { \mathcal{D} } )$, where $\vdash _ { \mathcal{D} }$, the consequence relation of $\mathcal{D}$, is a binary relation between sets of formulas and individual formulas satisfying the following well-known conditions: For all $\Gamma , \Delta \subseteq \operatorname{Fm}$ and $\varphi \in \operatorname {Fm}$,

$\Gamma \vdash_{\mathcal{D}} \varphi$ for all $\varphi \in \Gamma$;

$\Gamma \vdash_{\mathcal{D}} \varphi$ and $\Delta \vdash _ {\cal D } \psi$ for every $\psi \in \Gamma$ imply $\Delta \vdash_{\cal D} \varphi$;

$\Gamma \vdash_{\mathcal{D}} \varphi$ implies $\Gamma ^ { \prime } \vdash_{\mathcal{D}} \varphi$ for some finite $\Gamma ^ { \prime } \subseteq \Gamma$ (finiteness);

$\Gamma \vdash_{\mathcal{D}} \varphi$ implies $\sigma ( \Gamma ) \vdash_{\mathcal{D}} \sigma ( \varphi )$ for every substitution $\sigma$ (substitution invariance). Substitution invariance is the technical counterpart of the idea that logical consequence depends on form and not substance. It plays a key role in abstract algebraic logic because it is an essential feature of equational logic.

A formula $\varphi$ is a theorem of $\mathcal{D}$ if $\vdash_{\mathcal{D}} \varphi$ (i.e., it is a consequence of the empty set of formulas). The set of theorems, which may be empty, is denoted by $\operatorname{Thm} \mathcal{D}$. A set $T$ of formulas is a theory of a deductive system $\mathcal{D}$ if it is closed under consequence, i.e., $\varphi \in T$ whenever $\Gamma \subset T$ and $\Gamma \vdash_{\mathcal{D}} \varphi$. $\operatorname{Thm} \mathcal{D}$ is the smallest theory. The set of all theories of $\mathcal{D}$ is denoted by $\operatorname { Th } \cal D$. The theory axiomatized by an arbitrary set $\Gamma$ of formulas is the set of all formulas $\varphi$ such that $\Gamma \vdash_{\mathcal{D}} \varphi$.

Deductive systems in this sense include all the familiar sentential logics (cf. also Propositional calculus) together with their various fragments and refinements — for example, the classical and intuitionistic propositional calculi $\operatorname{CPC}$ and $\text{IPC}$, the intermediate logics (cf. also Intermediate logic), the various modal logics, including $\mathbf{S} 4$ and $\text{S}5$ (cf. also Modal logic), and the multiple-valued logics of J. Łukasiewicz and E. Post (cf. also Many-valued logic). The substructural logics, such as BCK logic, relevance logic and linear logic can also be formulated as deductive systems, although they are often formulated as Gentzen-type systems (cf. also Gentzen formal system). Even first-order predicate logic can be formalized as a deductive system, although in its usual formulation it is not substitution-invariant.

A (logical) matrix is a structure of the form $\mathfrak { A } = \langle \text{A} , F \rangle$, where $\mathbf{A}$ is an algebra (of the same language type as $\mathcal{D}$), the underlying algebra of $\frak A$, and $F \subseteq A$, the designated set of $\frak A$. An interpretation of $\mathcal{D}$ is a matrix $\frak A$ together with a homomorphism $h : \mathbf{Fm} \rightarrow \mathbf{A}$ from the algebra of formulas $\textbf{Fm}$ into the underlying algebra of $\frak A$. $h ( \varphi )$ is to be thought of as the "sense" or "meaning" of the formula $\varphi$ under the interpretation, and $\varphi$ is "true" or "false" depending on whether or not $h ( \varphi ) \in F$. By the Frege principle, this truth value is the denotation of $\varphi$ under the interpretation. Truth must be preserved under consequence in the sense that, if $\Gamma \vdash_{\mathcal{D}} \varphi$ and each $\psi \in \Gamma$ is true under the interpretation, then $\varphi$ must also be true. A set $\Gamma$ of formulas is said to define a class $\mathsf{K}$ of interpretations if $\mathsf{K}$ is the class of all interpretations in which each formula of $\Gamma$ is true. Because truth is preserved under consequence, the theory axiomatized by $\Gamma$ also defines $\mathsf{K}$; it turns out that it is the unique theory with this property.

The formulas $\varphi$ and $\psi$ are equivalent over a given class $\mathsf{K}$ of interpretations (in the Fregean sense) if they have the same truth value, i.e., $h ( \varphi ) \in F$ if and only if $h ( \psi ) \in F$ for each $\{ \mathfrak{A} , h \}$ in $\mathsf{K}$. They are logically equivalent (with respect to $\mathcal{D}$) if they are equivalent over the class of all interpretations.

The semantical and logistic approaches diverge at this point. In the former attention is restricted to a specific class of interpretations whose peculiar structure may play an important role in the meta-theory. In contrast, in the logistic method every interpretation is considered, and consequently only its representation as an abstract set with operations and a designated subset is significant. Deduction systems treated in this way are sometimes referred to as uninterpreted.

The foundations of the logistic method in abstract algebraic logic can be found in [Ło], [Ta2]; for more recent work, see [Wó]. For relation, polyadic and cylindric algebras, see [ChTa], [Ha], [HeMoTa]. For the origin of the notion of a deductive system, see [Ta].

Logistic abstract algebraic logic.

The assumption that the deductive system $\mathcal{D}$ is uninterpreted implies that one need consider only those matrices $\frak A$ with the property that $\{ \mathfrak{A} , h \}$ is an interpretation for every $h : \mathbf{Fm} \rightarrow \mathbf{A}$. Such a matrix is called a (matrix) model of $\mathcal{D}$; the class of all models of $\mathcal{D}$ is denoted by $\operatorname {Mod} \mathcal{D}$. Secondly, the properties of a given class of interpretations are for most purposes completely specified by the theory that defines it. So matters can be simplified by considering equivalence of formulas over theories rather than classes of interpretations.

Two formulas $\varphi$ and $\psi$ are equivalent over a theory $T$, or $T$-equivalent, in the Fregean sense, if, for every theory $S$ that extends $T$, $\varphi \in S$ if and only if $\psi \in S$; the binary relation between formulas defined this way is called the Frege relation of $T$ and denoted by $\Lambda _ { \cal D } T$. $\varphi$ and $\psi$ are logically equivalent (with respect to $\mathcal{D}$) if they are equivalent over every theory, or, equivalently, if they are equivalent over $\operatorname{Thm} \mathcal{D}$, the set of theorems. In terms of the consequence relation, $\varphi$ and $\psi$ are logically equivalent over $T$ if and only if $\varphi$ and $\psi$ are each consequences of the other over $T$; symbolically, $\varphi \equiv \psi ( \operatorname { mod } \Lambda _ { \mathcal{D} } T )$ if $T , \varphi \vdash_{\mathcal{D}} \psi$ and $T , \psi \vdash _ {\cal D } \varphi$.

If, as in the case of the classical and intuitionistic propositional calculi, $\mathcal{D}$ has a binary implication connective $\rightarrow$ for which the deduction theorem holds, then $\varphi \equiv \psi ( \operatorname { mod } \Lambda _ { \mathcal{D} } T )$ if and only if $\varphi \rightarrow \psi \in T$ and $\psi \rightarrow \varphi \in T$, or equivalently if there is a biconditional, $\varphi \leftrightarrow \psi \in T$. So, under these rather weak conditions on $\mathcal{D}$ logical equivalence in the Fregean sense agrees with the familiar definition of the concept.

As a consequence of Frege's principle, the following rule of replacement, or compositionality, holds when $\mathcal{D}$ is the classical propositional calculus $\operatorname{CPC}$ or the intuitionistic propositional calculus $\text{IPC}$. If in any formula $\varphi$ a subformula $\psi$ is replaced by an equivalent formula $\psi '$, the resulting formula $\varphi ^ { \prime }$ is equivalent to $\varphi$. In algebraic terms this says that for every theory $T$ of $\operatorname{CPC}$ or $\text{IPC}$, $\Lambda _ { \cal D } T$ is a congruence relation on the algebra of formulas $\textbf{Fm}$. A deductive system $\mathcal{D}$ for which $T$-equivalence is compositional for every theory $T$ is called Fregean or extensional; non-Fregean systems are called intensional.

If $\mathcal{D}$ is Fregean, it is possible to form the quotient matrices , where $T$ ranges over all theories. These are called the Lindenbaum–Tarski models of $\mathcal{D}$. The construction of the Lindenbaum–Tarski models is more complicated in the case of intensional systems, where the Frege relation is not a congruence relation. For example, for every theory $T$ of the strong form of the modal system $\text{S}5$, with necessitation as a rule of inference (see below), one has $\varphi \equiv \psi ( \operatorname { mod } \Lambda _ { S 5 } T )$ if and only if $T , \varphi \vdash_{\text{S}5} \psi$ and $T , \psi \vdash_{\text{S}5}$ if and only if $\square \varphi \rightarrow \psi \in T$ and $\square \psi \rightarrow \varphi \in T$. But this relation is not, in general, compositional. $\Lambda _ { \operatorname {S5} } T$ includes however a largest compositional equivalence relation, called the Suszko congruence of $T$ over $\text{S}5$ and denoted by $\tilde { \Omega } _ { S 5 } T$. It can be shown that $\varphi \equiv \psi ( \operatorname { mod } \tilde { \Omega } _ { S 5 } T )$ if and only if $\varphi \leftrightarrow \psi \in T$. So $\tilde { \Omega } _ { S 5 } T$ captures the usual notion of $T$-equivalence for $\text{S}5$.

Suszko congruences can be defined for the theories of any deductive system, and consequently one can construct Lindenbaum–Tarski models of any deductive system. But it turns out to be more useful to consider the Lindenbaum–Tarski process in a broader context. A subset $F$ of the underlying set of an algebra $\mathbf{A}$, of the same language type as $\mathcal{D}$, is called a filter of $\mathcal{D}$ if $\langle {\bf A} , F \rangle$ is a model of $\mathcal{D}$; thus $F$ is a filter if and only if it is closed under consequence in the sense that, if $\Gamma \vdash_{\mathcal{D}} \varphi$, one has $h ( \varphi ) \in F$ for every $h : \mathbf{Fm} \rightarrow \mathbf{A}$ such that $h ( \psi ) \in F$ for every $\psi \in \Gamma$. The set of filters of $\mathcal{D}$ on $\mathbf{A}$ is denoted by $\operatorname{Fi} _ {\cal D } \bf A$. It is easy to see that the theories are the filters on the formula algebra. The Frege relation and the Suszko congruence generalize to filters on an arbitrary algebra $\mathbf{A}$ in a natural way. The Frege relation $\Lambda _ { \mathcal{D} } F$ is the set of all pairs $\langle a , b \rangle$ of elements of $\mathbf{A}$ such that, for every filter $G$ on $\mathbf{A}$ that includes $F$, $a \in G$ if and only if $b \in G$. The Suszko congruence $\widetilde { \Omega } _ { \mathcal{D} } F$ is the largest congruence relation on $\mathbf{A}$ that is included in $\Lambda _ { \mathcal{D} } F$; it always exists.

The quotient matrix $\langle \mathbf{A} / \tilde{\Omega}_{\mathcal{D}} F , F / \tilde{\Omega}_{\mathcal{D}} F \rangle$ is called the Suszko-reduction of $\frak A$ and is denoted by $\mathfrak{A} ^ { *S }$. It can be shown that $\mathfrak{A}^{*S*S}$ coincides with (or, more precisely, is isomorphic to) $\mathfrak{A} ^ { *S }$. A model $\frak A$ is Suszko-reduced if $\mathfrak { A } ^ { * S} = \mathfrak { A }$, i.e., $\widetilde { \Omega } _ { \mathcal{D} } F$ is the identity relation. The class of all Suszko-reduced models of $\mathcal{D}$ is denoted by $\operatorname{Mod} ^ { * S} { \mathcal{D} }$. The Suszko-reduced models of $\mathcal{D}$ are those for which two elements are equivalent in the Fregean sense if and only if they are identical.

The class of underlying algebras of the Suszko-reduced models of $\mathcal{D}$ is denoted by $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$. The underlying algebras of $\operatorname{CPC}$ are the Boolean algebras. Each filter of $\operatorname{CPC}$ on a Boolean algebra $\mathbf{A}$ is completely determined by its Suszko congruence $\tilde { \Omega }F$; more precisely, it coincides with the set of all elements of $\mathbf{A}$ equivalent under $\tilde { \Omega }F$ to the unit element $\top$ of $\mathbf{A}$. Moreover, every congruence relation on $\mathbf{A}$ is the Suszko congruence of a filter of $\operatorname{CPC}$. It follows that the consequence relation of $\operatorname{CPC}$ is completely determined by the equational logic of Boolean algebras, and in this way the class of Boolean algebras constitutes a complete algebraic semantics for $\operatorname{CPC}$. In a similar way, the class of Heyting algebras $\text{Alg Mod}^ { *S } \text{ IPC }$ and the class of so-called monadic algebras $\operatorname{Alg} \operatorname{Mod}^ { *S } \operatorname{S} 5$ constitute complete algebraic semantics for $\text{IPC}$ and $\text{S}5$, respectively, and this is the case for almost all the familiar deductive systems. But in general the connection between the consequence relation of a deductive system $\mathcal{D}$ and the equational logic of $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$ is much weaker. A central problem for abstract algebraic logic is the characterization of those deductive systems for which this connection is as strong as for the traditional logics.

Early work on the Suszko and the closely related Leibniz and Tarski congruences discussed below can be found in [Ło], [Sm]. [Su2] contains historical information on the Tarski–Lindenbaum process. The essential idea of Fregean logic as presented here originated with R. Suszko [BlSu], [Su].

Algebraizable logics.

The basis of the abstract algebraic logic definition of an algebraizable deductive system is the notion of bisimulation between the consequence relation of $\mathcal{D}$ and the equational consequence relation of a class of algebras.

Let $\mathcal{D}$ be a deductive system and $\mathsf{K}$ a class of algebras over the same language type. Let

\begin{equation*} E ( x , y ) = \{ \epsilon _ { i } ( x , y ) : i \in I \} \end{equation*}

be a (possibly infinite) non-empty system of formulas in two variables. $E ( x , y )$ is said to be a faithful interpretation of the equational logic of $\mathsf{K}$ in $\mathcal{D}$ if, for every equation $\varphi \approx \psi$ and every set of equations $\Gamma \approx \Delta$,

\begin{equation*} \Gamma \approx \Delta \models _ { \text{K} } \varphi \approx \psi \text { iff } E ( \Gamma , \Delta ) \vdash _ { \mathcal{D} } E ( \varphi , \psi ), \end{equation*}

where $\Gamma \approx \Delta \vDash _ { \mathsf{K} } \varphi \approx \psi$ means that $\wedge \Gamma \approx \Delta \rightarrow \varphi \approx \psi$ is a quasi-identity of $\mathsf{K}$. Also, $E ( \Gamma , \Delta ) = \{ \epsilon _ { i } ( \gamma , \delta ) : \gamma \approx \delta \in \Gamma \approx \Delta , i \in I \}$ and $E ( \varphi , \psi ) = \{ \epsilon _ { i } ( \varphi , \psi ) : i \in I \}$, and $E ( \Gamma , \Delta ) \vdash _ {\cal D } E ( \varphi , \psi )$ is shorthand for the system of entailments $E ( \Gamma , \Delta ) \vdash _ {\cal D } \epsilon _ { i } ( \varphi , \psi )$ for every $i \in I$; "iff" stands for "if and only if" .

Let

\begin{equation*} K ( x ) \approx L ( x ) = \{ \kappa _ { j } ( x ) \approx \lambda _ { j } ( x ) : j \in J \} \end{equation*}

be a non-empty system of equations in one variable. $K ( x ) \approx L ( x )$ is a faithful interpretation of $\mathcal{D}$ in the equational logic of $\mathsf{K}$ if, for all $\Gamma \cup \{ \varphi \} \subseteq \text{Fm}$,

\begin{equation*} \Gamma \vdash _ { \mathcal{D} } \varphi \text { iff } K ( \Gamma ) \approx L ( \Gamma ) \vDash _ { \text{K} } K ( \varphi ) \approx L ( \varphi ), \end{equation*}

where $K ( \Gamma ) \approx L ( \Gamma ) = \{ \kappa _ { j } ( \psi ) \approx \lambda _ { j } ( \psi ) : \psi \in \Gamma , j \in J \}$ and $K ( \varphi ) \approx L ( \varphi ) = \{ \kappa _ { j } ( \varphi ) \approx \lambda _ { j } ( \varphi ) : j \in J \}$. The two interpretations are mutual inverses if

\begin{equation*} x \dashv \vdash_{\mathcal{D}} E ( K ( x ) , L ( x ) ) \end{equation*}

and

A pair of mutually invertible interpretations $E ( x , y )$ and $K ( x ) \approx L ( x )$ such as these is called a bisimulation between $\mathcal{D}$ and the equational logic of $\mathsf{K}$. A deductive system $\mathcal{D}$ is algebraizable if there is a bisimulation between $\mathcal{D}$ and the equational logic of some class $\mathsf{K}$ of algebras; it is finitely algebraizable if the interpretations are finite. If $\mathcal{D}$ is algebraizable, then $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$ is the largest class $\mathsf{K}$ with the above properties; it is called the equivalent algebraic semantics of $\mathcal{D}$. In general, $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$ is not elementary (i.e., definable by a set of sentences of the first-order predicate logic), and in fact it is an elementary class just in case $\mathcal{D}$ is finitely algebraizable. In this case $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$ is a quasi-variety (cf. also Quasi-variety)

The classical and intuitionistic propositional calculi $\operatorname{CPC}$ and $\text{IPC}$ are finitely algebraizable and their equivalent quasi-varieties are, respectively, the varieties $\textsf{BA}$ of Boolean algebras and $\mathbf{\dashv} \mathsf{A}$ of Heyting algebras. In both cases the faithful interpretation of the equational logic of the equivalent quasi-variety in the deductive system is given by $E ( x , y ) = \{ x \leftrightarrow y \}$, where $\leftrightarrow$ is, respectively, the classical and intuitionistic biconditional, and the inverse faithful interpretation is $K ( x ) \approx L ( x ) = \{ x \approx T \}$. Most of the deductive systems of traditional algebraic logic are finitely algebraizable with similar interpretations. However, there are finitely algebraizable logics with non-standard interpretations, for example the entailment logic $E$.

The bisimulation between a finitely algebraizable deductive system $\mathcal{D}$ and the equational logic of its equivalent quasi-variety $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$ induces a correspondence between the meta-logical properties of $\mathcal{D}$ and the algebraic properties of $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$. This correspondence has been the focus of considerable attention in abstract algebraic logic. One of the most important aspects of traditional algebraic logic is the way in which it can be used to reformulate meta-logical properties of a particular logical system in algebraic terms. Abstract algebraic logic provides a framework for studying such correspondences in a general context. Known meta-logical or algebraic results can then be applied to obtain new results in the other domain. Some correspondences of this kind that have been established are between:

meta-logical interpolation and algebraic amalgamation, e.g., the Craig interpolation theorem of $\operatorname{CPC}$ and the amalgamation property of $\textsf{BA}$;

definability (in the sense of the Beth definability theorem of first-order predicate logic) and the property that every epimorphism (in the categorical sense) is surjective;

the deduction theorem and the equational definability of principal congruences. The deduction theorem is the formal expression of one of the most important and useful properties of classical logic: to prove that an implication holds between propositions it suffices to give a proof of the conclusion on the basis of the assumption of the antecedent. It is such a familiar part of ordinary logical argumentation that it is hardly recognizable as being something whose use might be problematic. But in fact it is not part of the usual formalizations of $\operatorname{CPC}$ and must be proved as a meta-theorem. Moreover, while the deduction theorem remains valid for intuitionistic logic, it is known to fail in other important logics, for instance, certain systems of modal logic. It turns out that there is a close connection between the deduction theorem and the universal algebraic notion of definable principal congruence relations. The development of abstract algebraic logic was motivated in part by a desire to provide the proper context in which to formalize this connection precisely. The ultimate goal was to be able to apply the extensive work on the definability of principal congruence relations in universal algebra to answer some important questions about the validity of the deduction theorem in a variety of logical systems.

Let $\mathcal{D}$ be a deductive system. A finite non-empty set $\Delta ( x , y ) = \{ \delta _ { 0 } ( x , y ) , \ldots , \delta _ { m - 1 } ( x , y ) \}$ of binary formulas is called a deduction-detachment system for $\mathcal{D}$ if the following equivalence holds for all $\Gamma \cup \{ \varphi , \psi \} \subseteq \operatorname{Fm}$:

\begin{equation*} \Gamma , \varphi \vdash_{\mathcal{D}} \psi \end{equation*}

\begin{equation*} \text{iff } \Gamma \vdash _ {\cal D } \Delta ( \varphi , \psi ). \end{equation*}

A deductive system has the deduction-detachment theorem if it has a deduction-detachment system. The implication $x \rightarrow y$ forms a singleton deduction-detachment system for $\operatorname{CPC}$ and $\text{IPC}$, while the formula $\square x \rightarrow y$ forms a singleton deduction-detachment system for the modal systems $\mathbf{S} 4$ and $\text{S}5$.

For an algebra $\mathbf{A}$, let $\operatorname{Co}\mathbf{A}$ be the set of all congruences of $\mathbf{A}$. If $\mathsf{Q}$ is a quasi-variety, then a congruence $\Theta$ on an arbitrary algebra $\mathbf{A}$ (not necessarily in $\mathsf{Q}$) is called a $\mathsf{Q}$-congruence if $\mathbf{A} / \Theta \in \mathsf{Q}$. If $\mathsf{Q}$ is a variety (cf. also Algebraic systems, variety of) and $\bf A \in \mathsf{Q}$, then every congruence is a $\mathsf{Q}$-congruence. The principal $\mathsf{Q}$-congruence generated by the pair $a$ and $b$, $\Theta_{ \mathsf{Q} } ( a , b )$, is the smallest $\mathsf{Q}$-congruence that identifies $a$ and $b$. A quasi-variety $\mathsf{Q}$ has equationally definable principal relative congruences (EDPRC) if there is a finite system of equations $\epsilon_{ 0,0} ( x , y , z , w ) \approx \epsilon_{ 0,1} ( x , y , z , w ) , \ldots , \epsilon _ { m - 1,0 } ( x , y , z , w ) \approx \epsilon _ { m - 1 , 1} ( x , y , z , w )$, in four variables, such that, for every $\bf A \in \mathsf{Q}$ and all $a , b , c , d \in A$,

\begin{equation*} c \equiv d ( \Theta _ { \text{Q} } ( a , b ) ) \end{equation*}

\begin{equation*} \text{iff }\epsilon _ { i,0 } ^ { \mathbf{A} } ( a , b , c , d ) = \epsilon _ { i , 1 } ^ { \mathbf{A} } ( a , b , c , d ) \text { for all } i < m, \end{equation*}

$\epsilon _ { i , j } ^ { \mathbf{A} } ( a , b , c , d ) = h ( \epsilon _ { i , j } ( x , y , z , w ) )$, where $h : \mathbf{Fm} \rightarrow \mathbf{A}$ is any homomorphism such that $h ( x ) = a , \ldots , h ( w ) = d$.

$\mathsf{Q}$-congruence generation in the formula algebra can be interpreted as the consequence relation of the equational logic of $\mathsf{Q}$. Thus, if $\mathsf{Q}$ has EDPRC, the defining equations $\epsilon _ { i , 0 } ( x , y , z , w ) \approx \epsilon _ { i , 1 } ( x , y , z , w )$ can be interpreted collectively as an implication connective for the equational logic. This observation is reflected in the following theorem: Let $\mathcal{D}$ be a finitely algebraizable deductive system and let $\mathsf{Q} = \operatorname { Alg } \operatorname { Mod } ^ { * S } \mathcal{D}$ be its equivalent quasi-variety. Then $\mathcal{D}$ has the deduction-detachment theorem if and only if $\mathsf{Q}$ has EDPRC.

A correspondence of this kind makes it possible to infer new metalogical properties from known algebraic ones and vice versa. In this way it can be proved that orthomodular logic does not have the deduction-detachment theorem. Orthomodular logic can be viewed as a finitely algebraizable deductive system whose equivalent quasi-variety is the variety of orthomodular lattices. There are several different deductive systems that fit this description. It can be shown that, if a quasi-variety $\mathsf{Q}$ has EDPRC, then it has the relative congruence extension property. The variety of orthomodular lattices does not have this property. Thus, no orthomodular logic of the kind described above can have the deduction-detachment theorem with respect to any system of binary formulas.

A definition of an abstract class of deductive systems with the algebraic properties of the traditional logics was first proposed in [BlPi2]; earlier definitions, notably that in [Ra], were not truly abstract because they relied on the existence of connectives with special properties. The notion of algebraizability was subsequently extended in several ways ([Cz4], [CzJa], [He2], [He]). For entailment logic and its algebraizability, see [AnBe], [BlPi2]. For the deduction theorem in abstract algebraic logic, see [BlPi], [Cz]. The result on orthomodular logic is found in [BlPi5], [Ma].

The algebraic hierarchy.

Finitely algebraizable deductive systems exhibit the strongest connection between the meta-logical properties of $\mathcal{D}$ and the algebraic properties of $\operatorname {Alg} \operatorname {Mod} ^ { * S} { \cal D }$. But there are deductive systems where the connection is not as strong but which still have a clear algebraic character. One of the goals of abstract algebraic logic is the classification of deductive systems of this kind. This leads to a hierarchy of systems with the finitely algebraizable systems at the top. There are several ways of specifying it. The most natural, in view of the definition of algebraizability, is in terms of progressively weaker notions of bisimulation. The characteristic property of all deductive systems that make up the hierarchy is that equivalence, as expressed by the Suszko congruence, is explicitly definable in some way. The classification of the hierarchy is based on the nature of the definition.

Let $E ( x , y ) = \{ \epsilon _ { i } ( x , y ) : i \in I \}$ be a (possibly infinite) set of formulas in two variables. $E ( x , y )$ is a proto-equivalence system for a deductive system $\mathcal{D}$ if

\begin{equation*} \vdash_{\mathcal{D}} E ( x , x ) \text { and } x ,\, E ( x , y )\vdash_{\mathcal{D}} y \end{equation*}

($E$-detachment).

A non-empty proto-equivalence system $E ( x , y )$ is an equivalence system if

\begin{equation*} E ( x , y ) \vdash _ { \mathcal{D} } E ( y , x ) , \quad E ( x , y ) , E ( y , z ) \vdash _ { \mathcal{D} } E ( x , z ), \end{equation*}

and

\begin{equation*} E ( x _ { 0 } , y _ { 0 } ) , \ldots , E ( x _ { n - 1} , y _ { n - 1} ) \vdash_ { \mathcal{D} } \end{equation*}

\begin{equation*} \vdash_\mathcal{D} E ( \lambda x _ { 0 } , \ldots , x _ { n - 1} , \lambda y 0 , \ldots , y _ { n - 1} ) \end{equation*}

for all $\lambda \in \Lambda$ ($n$ is the rank of $\lambda$). The reflexivity and transitivity axioms are superfluous as they are provable from the remaining conditions.

The connection between equivalence systems and the Suszko congruence is expressed in the following theorem: A non-empty system $E ( x , y )$ of formulas in two variables is an equivalence system for a deductive system $\mathcal{D}$ if and only if it defines Suszko congruences in the sense that, for every algebra $\mathbf{A}$ and $F \in \operatorname{Fi} _ {\cal D } \bf A$,

\begin{equation*} \widetilde { \Omega } _ { \mathcal{D} } F = \end{equation*}

\begin{equation*} = \{ \langle a , b \rangle \in A ^ { 2 } : \epsilon ^ { \mathbf{A} } ( a , b ) \in F \text { for all } \epsilon ( x , y ) \in E ( x , y ) \}. \end{equation*}

A deductive system is protoalgebraic if it has a proto-equivalence system. Every proto-equivalence system includes a finite subset that is also a proto-equivalence system. A deductive system is (finitely) equivalential if it has a (finite) equivalence system.

The formulas that faithfully interpret in a (finitely) algebraizable deductive system the equational logic of its equivalent algebraic semantics form a (finite) equivalence system. This leads to a meta-logical characterization theorem of (finitely) algebraizable deductive systems that is intrinsic in the sense that it does not require a priori knowledge of the equivalent algebraic semantics: A deductive system is (finitely) algebraizable if and only if it has a (finite) equivalence system for which there exists a finite system $K ( x ) \approx L ( x )$ of equations in one variable, called a system of defining equations, such that $x \dashv \vdash_{\mathcal{D}} E ( K ( x ) , L ( x ) )$.

This last condition abstracts an important property of the biconditional $\leftrightarrow$ of both classical and intuitionistic propositional logic, namely, that $x$ and the biconditional $x \leftrightarrow \top $ are interderivable.

The protoalgebraic, (finitely) equivalential and (finitely) algebraizable deductive systems constitute, along with the weakly algebraizable systems discussed shortly, the algebraic hierarchy. Natural deductive systems can be found to separate all levels of the hierarchy. Protoalgebraicity is a very weak condition and almost all known deductive systems have the property. There are some that do not however, for example the conjunction/disjunction fragment of $\operatorname{CPC}$, subintuitionistic logics and Belnap's logic. Almost all the weak modal logics, without necessitation as a rule of inference, are protoalgebraic but not equivalential. There are also examples of algebraizable logics that are not finitely equivalential, and hence also of logics that are equivalential but not finitely equivalential.

In addition to the syntactical characterizations considered above, each level of the hierarchy can be characterized by both algebraic and model-theoretic means. The algebraic characterization makes use of the Leibniz congruence, a more primitive but more manageable variant of the Suszko congruence.

Given any algebra $\mathbf{A}$ and any subset $F$ of $A$, there is a largest congruence relation $\Omega F$ on $\mathbf{A}$ compatible with $F$ in the sense that $F$ is a union of equivalence classes of $\Omega F$. $\Omega F$ is called the Leibniz congruence of $F$. The relationship between the Leibniz and Suszko congruences is straightforward: For every deductive system $\mathcal{D}$ and $F \in \operatorname{Fi} _ {\cal D } \bf A$,

\begin{equation*} \widetilde { \Omega } _ { \mathcal{D} } F = \bigcap \{ \Omega G : F \subseteq G \in \operatorname{Fi} _ { \mathcal{D} } \mathbf{A} \}. \end{equation*}

$\Omega$ and $\tilde { \Omega }$ can both be viewed as operators mapping the lattice of $\mathcal{D}$-filters of $\mathbf{A}$ to the lattice of congruences of $\mathbf{A}$. Note that the Leibniz and Suszko congruences coincide on $\mathcal{D}$-filters just in case the Leibniz operator is order-preserving, i.e., $F \subseteq G$ implies $\Omega F \subseteq \Omega G$ for all $F , G \in \operatorname {Fi} _ { \mathcal{D} } \mathbf{A}$.

Let $\mathcal{D}$ be a deductive system. Then the following characterizations hold:

i) $\mathcal{D}$ is protoalgebraic if and only if the Leibniz operator $\Omega$ is order-preserving, i.e., if and only if the Leibniz and Suszko congruences coincide;

ii) $\mathcal{D}$ is equivalential if and only if it is protoalgebraic and $\Omega$ commutes with inverse homomorphic images; more precisely, $\Omega h ^ { - 1 } ( F ) = h ^ { - 1 } ( \Omega F )$ for every homomorphism $h : \mathbf{A} \rightarrow \mathbf{B}$ and every $F \in \text{Fi} _ { \mathcal{D} }\mathbf{B}$;

iii) $\mathcal{D}$ is finitely equivalential if and only if it is protoalgebraic and $\Omega$ commutes with directed unions; more precisely, $\Omega \cup {\cal F} = \cup _ { F \in {\cal F} } \Omega F$ for every $\mathcal{F} \subseteq \operatorname{Fi} _ { \mathcal{D} } \mathbf{A}$ that is upward-directed by inclusion;

iv) $\mathcal{D}$ is algebraizable if and only if it is equivalential and $\Omega$ is injective;

v) $\mathcal{D}$ is finitely algebraizable if and only if it is finitely equivalential and $\Omega$ is injective.

A deductive system $\mathcal{D}$ is said to be weakly algebraizable if it is protoalgebraic and the Leibniz operator $\Omega$ is injective. A syntactical characterization of weak algebraizability is also known.

Calculation of the Leibniz congruences can be a practical matter for some small algebras. This gives a way of verifying that a deductive system is not finitely algebraizable, or that a quasi-variety is not the equivalent algebraic semantics of any deductive system. This method has been used to show that the relevance logic $R$ and the various formalizations of modal logic without the rule of necessitation are not finitely algebraizable. It has also been used to show that the variety of complemented distributive lattices is not the equivalent algebraic semantics of any deductive system.

There is also a model-theoretic characterization of the algebraic hierarchy similar to the well-known model-theoretic characterizations of equational and quasi-equational classes by G. Birkhoff and A. Mal'cev.

The Leibniz-reduction of a model of a deductive system is defined just like the Suszko-reduction, except that the Leibniz congruence is used in place of the Suszko congruence. $\operatorname { Mod } ^ { * \text{L}} {\cal D }$ denotes the class of all Leibniz-reduced models of $\mathcal{D}$. If $\mathcal{D}$ is protoalgebraic, then $\operatorname { Mod } ^ { * S} \mathcal{D}= \operatorname { Mod } ^ { * \text{L}} \mathcal{ D }$; this equality in fact characterizes protoalgebraic systems. In general, the best one has is that $\operatorname{Mod} ^ { * S} { \mathcal{D} }$ coincides with the class of all matrices isomorphic to a subdirect product of matrices in $\operatorname { Mod } ^ { * \text{L}} {\cal D }$, in symbols $\operatorname{Mod} ^ { * S} \mathcal{D} = \mathbf{P} _ { \text{SD} } \operatorname{Mod} ^ { *\text{L}} \mathcal{D} $.

For any class $\mathsf{K}$ of matrices, $\mathbf{S}\mathsf{K}$, $\textsf{PK}$, ${\bf P} _ { \text{SD} } \mathsf{K}$, and ${\bf P} _ { \text{U} } \mathsf{K}$ denote, respectively, the classes of isomorphic images of submatrices, direct products, subdirect products, and ultraproducts of members of $\mathsf{K}$.

Let $\mathcal{D}$ be a deductive system. Then the following characterizations hold:

a) $\mathcal{D}$ is protoalgebraic if and only if $\operatorname{Mod} ^ { * \text{L}} \mathcal{D} = \mathbf{P} _ { \text{SD} } \operatorname{Mod} ^ { * \text{L}} \mathcal{D}$, i.e., $Mod ^ { * \operatorname{L}} \mathcal{D} = Mod ^ { * S} \mathcal{ D }$;

b) $\mathcal{D}$ is equivalential if and only if $\operatorname{Mod} ^ { * \text{ L}} \mathcal{D} = \mathbf{SP} \operatorname{Mod} ^ { * \text{ L}} \mathcal{D}$;

c) $\mathcal{D}$ is finitely equivalential if and only if $\operatorname{Mod} ^ { * \text{L}} \mathcal{D} = \mathbf{SPP} _ { \text{U} } \operatorname{Mod} ^ { * \text{L}} \mathcal{D} $, i.e., $\operatorname { Mod } ^ { * \text{L}} {\cal D }$ is a quasi-variety in the sense of Mal'cev;

d) $\mathcal{D}$ is algebraizable if and only if it is equivalential and $F$ is the minimal $\mathcal{D}$-filter of $\mathbf{A}$ for each $\langle \mathbf{A} , F \rangle \in \operatorname{Mod} ^ { * \text{L}} \mathcal{D}$;

e) $\mathcal{D}$ is finitely algebraizable if and only if it is finitely equivalential and $F$ is the minimal $\mathcal{D}$-filter of $\mathbf{A}$ for each $\langle \mathbf{A} , F \rangle \in \operatorname{Mod} ^ { * \text{L}} \mathcal{D}$.

For papers on the specific levels of the algebraic hierarchy, see [BlPi3], [BlPi2], [Cz3], [CzJa], [He2], [He]. Two references of a more general nature are [BlPi4], [Cz2].

Protoalgebraic logics.

Within the context of the model theory of first-order logic, a deductive system can be viewed as a strict universal Horn theory with a single unary predicate and without equality. (cf. also Horn clauses, theory of). It is an interesting question as to how much of the model theory of strict universal Horn logic with equality can be recovered by means of the abstract Lindenbaum–Tarski process. In the case of finitely algebraizable deductive systems it can be essentially completely recovered already in the algebraic reducts of the Leibniz-reduced models. The same is true for finitely equivalential systems where the finite equivalence systems give a strong representation of equality, but here the filter part of the Leibniz-reduced model is essential and cannot be discarded. But much can be recovered even in the case of protoalgebraic systems where the proto-equivalence systems give a much weaker representation of equality. Protoalgebraic systems turn out to be the largest class of deductive systems $\mathcal{D}$ whose Leibniz-reduced model class $\operatorname { Mod } ^ { * \text{L}} {\cal D }$ is well behaved in the sense of strict Horn logic with equality, and the key to this is the following correspondence theorem for $\mathcal{D}$-filters that mirrors the correspondence theorem for congruences in universal algebra: Let $\mathcal{D}$ be a protoalgebraic deductive system, and let $\mathbf{A}$ and $\mathbf{B}$ be algebras and $h : \mathbf{A} \twoheadrightarrow \mathbf B$ a surjective homomorphism. Finally, let $F _ { 0 }$ be the smallest $\mathcal{D}$-filter on $\mathbf{B}$. Then the mapping $F \mapsto h ^ { - 1 } ( F )$ is a one-to-one correspondence between the $\mathcal{D}$-filters on $\mathbf{B}$ and the $\mathcal{D}$-filters on $\mathbf{A}$ that include $h ^ { - 1 } ( F _ { 0 } )$.

When $\mathbf{A}$ is taken to be $\textbf{Fm}$, the algebra of formulas, this correspondence establishes a close connection between the meta-logical properties of $\mathcal{D}$ and the algebraic properties of the class $\operatorname { Mod } ^ { * \text{L}} {\cal D }$ of Leibniz-reduced models of $\mathcal{D}$.

Every class $\mathsf{K}$ of matrices over the same language type $\Lambda$ defines a deductive system $\mathcal D(\mathsf K) = \langle \textbf{F m} , \vDash_{\mathcal K} \rangle$ over $\Lambda$ in the following way. $\psi _ { 0 } , \ldots , \psi _ { n - 1 } \vDash _ { \mathsf{K} } \varphi$ if, for every $\langle {\bf A} , F \rangle \in \mathsf{K}$ and every homomorphism $h : \mathbf{Fm} \rightarrow \mathbf{A}$, $h ( \varphi ) \in F$ whenever $h ( \psi _ { 0 } ) , \ldots , h ( \psi _ { n - 1} ) \in F$. The following theorem is a generalization of Mal'cev's well-known characterization of the strict universal Horn class generated by an arbitrary class of matrices: Let $\mathsf{K}$ be a class of Leibniz-reduced matrices over the same language type; then

if ${\cal D} ( \mathsf{K} )$ is protoalgebraic, then $\operatorname { Mod } ^ { *\operatorname{L} } \mathcal{D} ( \mathsf{K} ) = ( \textbf{SPP} _ { \operatorname{U} } \mathsf{K} ) ^ { *\operatorname{L} } $;

if ${\cal D} ( \mathsf{K} )$ is equivalential, then $\operatorname { Mod}^ { *\text{L} } \mathcal{D} ( \mathsf{K} ) = \mathbf{SPP} _ { \text{U} } \mathsf{K}$.

The following theorem is an analogue of the finite basis theorem of K. Baker for congruence-distributive varieties and of the corresponding result for relatively congruence-distributive quasi-varieties. It uses the notion of filter-distributive deductive system. A deductive system $\mathcal{D}$ is filter-distributive if $\operatorname{Fi} _ {\cal D } \bf A$ is a distributive lattice for every algebra $\mathbf{A}$.

Let $\mathsf{K}$ be a finite set of matrices. If ${\cal D} ( \mathsf{K} )$ is protoalgebraic and filter-distributive, then ${\cal D} ( \mathsf{K} )$ has a presentation by a finite set of axioms and inference rules [Pa]. An important related axiomatizability result can be found in [Cz5].

In analogy to the algebraic hierarchy there is a classification of deductive systems in terms of progressively weaker versions of a deductive-detachment system. Again protoalgebraic systems lie at the lowest level, and filter-distributive systems constitute another level of hierarchy. See [Cz], [Cz2].

The generalization of Mal'cev's theorem above is one of many model-theoretic theorems of this kind involving various levels of the algebraic hierarchy, and the scope of the theory has been broadened to include infinitary universal Horn logic without equality [BlPi4], [Cz3], [DeJa], [El2], [El].

Second-order algebraizable logics.

There are deductive systems with clear algebraic counterparts that are not protoalgebraic and hence not amenable to the methods of abstract algebraic logic discussed so far. Many examples of this kind arise as fragments of more expressive deductive systems that are finitely algebraizable. A paradigm for deductive systems of this kind is the conjunction/disjunction fragment $\operatorname{CPC}_{\wedge \vee}$ of classical propositional logic. It has a natural algebraic semantics, the variety $\mathsf{DL}$ of distributive lattices. In order to extend the standard theory of algebraizability to a wider class of deductive systems, recent investigations in abstract algebraic logic have switched focus from $\mathcal{D}$-filters to certain special classes of $\mathcal{D}$-filters and to a natural generalization of the Leibniz congruence that applies to classes of $\mathcal{D}$-filters.

The non-algebraizability of $\operatorname{CPC}_{\wedge \vee}$ is reflected in the fact that, for an arbitrary algebra $\mathbf{A}$, the Leibniz operator does not give a one-one correspondence between ($\operatorname{CPC}_{\wedge \vee}$)-filters and $\mathsf{DL}$-congruences. The correspondence can in a sense be recovered by replacing single ($\operatorname{CPC}_{\wedge \vee}$)-filters by sets of ($\operatorname{CPC}_{\wedge \vee}$)-filters, each of which is of the form $\mathcal{C} _ { \Gamma }$, where $\mathcal{C} _ { \Gamma }$ consists of all ($\operatorname{CPC}_{\wedge \vee}$)-filters that are compatible with each member of a fixed but arbitrary class $\Gamma$ of congruences on $\mathbf{A}$. The set of congruences $\Gamma$ is completely arbitrary, but it turns out that there is always a single congruence $\Phi$ such that $\mathcal{C} _ { \{ \Phi \} } = \mathcal{C} _ { \Gamma }$, and in fact a smallest one with this property, and it is necessarily a $\mathsf{DL}$-congruence. Moreover, all $\mathsf{DL}$-congruences can be obtained this way.

Considerations such as these lead to the following notion. A full second-order filter of $\mathcal{D}$ on an algebra $\mathbf{A}$ is the set of all $\mathcal{D}$-filters $F$ on $\mathbf{A}$ such that $F$ is compatible with a fixed but arbitrary set of congruences. The set of full second-order filters on $\mathbf{A}$ is denoted by $\operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$. It is easy to check that every $\mathcal{C} \in \operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$ is an algebraic closed-set system of the universe $A$ of $\mathbf{A}$. For each $\mathcal{C} \in \operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$ the Frege relation $\Lambda \mathcal{C}$ is the largest binary relation on $A$ (necessarily an equivalence relation) that is compatible with each $F \in \mathcal{C}$, and the second-order Leibniz congruence, also called the Tarski congruence, $\Omega \mathcal{C}$ is the largest congruence of $\mathbf{A}$ included in $\Lambda \mathcal{C}$.

A set $\mathcal{C}$ of $\mathcal{D}$-filters on $\mathbf{A}$ is a full second-order filter of $\mathcal{D}$ if and only if the set of quotient filters $\{ F / \Omega \mathcal{C} : F \in \mathcal{C} \}$ coincides with the set of all $\mathcal{D}$-filters on the quotient algebra $\mathbf{A} / \Omega \mathcal{C}$. A full second-order model of $\mathcal{D}$ is a second-order matrix $\mathfrak { A } = \langle \mathbf{A} , \mathcal{C} \rangle$ where $\mathcal{C} \in \operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$. $\frak A$ is Leibniz reduced if $\Omega \mathcal{C}$ is the identity relation. $\operatorname{FMod} \mathcal{D}$ (respectively, $\operatorname { FMod} ^ { * \text{L}} \mathcal{D}$) is the class of all (Leibniz-reduced) full second-order models of $\mathcal{D}$.

The following assertion generalizes iv) above, the lattice isomorphism characterization of algebraizable deductive systems, and applies to all deductive systems.

For any deductive system $\mathcal{D}$ and any algebra $\mathbf{A}$ the second-order Leibniz operator $\Omega$ is a dual order-isomorphism between $\operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$ and $\operatorname {Co} _ { \text{Alg} \operatorname {FMod} ^ { * \text{L}} \mathcal{ D }} \mathbf{A}$, both partially ordered by set inclusion.

A full second-order model, and more generally, any second-order matrix $\langle \mathbf{A} , \mathcal{C} \rangle$ where $\mathcal{C}$ is an algebraic closed-set system on $\mathbf{A}$, can be naturally thought of as a model of a Gentzen system. In the context of abstract algebraic logic a Gentzen system can be viewed as a finitary and substitution-invariant consequence relation between sequents; a sequent is a syntactical expression of the form $\varphi _ { 0 } , \ldots , \varphi _ { n - 1 } \rhd \varphi _ { n }$, where $\varphi _ { 0 } , \ldots , \varphi _ { n - 1} , \varphi _ { n }$ is any finite, non-empty sequence of formulas. Let $\mathfrak { A } = \langle \mathbf{A} , \mathcal{C} \rangle$ be a second-order matrix, and let $C : \mathcal{P} ( A ) \rightarrow \mathcal{P} ( A )$ be the closure operator on $A$ associated with the algebraic closed-set system $\mathcal{C}$. $\frak A$ is a model of a Gentzen system $\mathcal{G}$ if the following holds. For every entailment

\begin{equation*} \varphi _ { 0 } ^ { 0 } , \ldots , \varphi _ { n _ { 0 } - 1} ^ { 0 } \rhd \psi ^ { 0 } ; \ldots ; \varphi _ { 0 } ^ { m - 1 } , \ldots , \varphi _ { n _ { m - 1 } -1 } ^ { m - 1 } \rhd \psi ^ { m - 1 } \vdash _ { \mathcal{G} } \end{equation*}

\begin{equation*} \vdash _ { \mathcal{G} } \theta _ { 0 } , \ldots , \theta _ { n - 1 } \rhd \xi , \end{equation*}

and every homomorphism $h : \mathbf{Fm} \rightarrow \mathbf{A}$, if $h ( \psi ^ { i } ) \in C ( \{ h ( \varphi _ { 0 } ^ { i } ) , \ldots , h ( \varphi _ { n _ { i } - 1 } ^ { i } ) \} )$ for each $i < m$, then $h ( \xi ) \in C ( \{ h ( \theta _ { 0 } ) , \ldots , h ( \theta _ { n - 1} ) \} )$.

A deductive system $\mathcal{D}$ is said to have a fully adequate Gentzen system if the class of full second-order models of $\mathcal{D}$ is the class of models of a Gentzen system. (Strictly speaking, this is the form the definition takes when $\mathcal{D}$ has at least one theorem. The definition together with the formulation of some of the results stated below must be modified slightly if there are no theorems.)

The notion of finite algebraizability for deductive systems can be extended to Gentzen systems in a straightforward way. Just as in the case of deductive systems, if a Gentzen system $\mathcal{G}$ is finitely algebraizable, there is a unique quasi-variety $\mathsf{Q}$ that is equivalent to $\mathcal{G}$ in the sense that there is a bisimulation between the consequence relation of $\mathcal{G}$ (between sequents) and the equational consequence relation of $\mathsf{Q}$. In view of the above observations it is natural to take a deductive system $\mathcal{D}$ to be second-order finitely algebraizable if it has a fully adequate Gentzen system $\mathcal{G}$ such that $\mathcal{G}$ is finitely algebraizable. In this case, $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ turns out to coincide with the equivalent quasi-variety of $\mathcal{G}$, and the consequence relation of $\mathcal{D}$ is definable (as part of the consequence relation of $\mathcal{G}$) in the equational consequence relation of $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$, but not vice versa unless $\mathcal{D}$ is also finitely algebraizable. In the latter case $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ coincides with the equivalent quasi-variety of $\mathcal{D}$. When $\mathcal{D}$ is second-order finitely algebraizable, $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ is called the second-order equivalent quasi-variety of $\mathcal{D}$.

Strictly speaking, second-order finite algebraizability does not generalize (first-order) finite algebraizability since there are deductive systems that are finitely algebraizable but do not have a fully adequate Gentzen system. However, this new notion of algebraizability goes a long way toward settling some important questions left open by the earlier theory.

One of these deals with the notion of strong finite algebraizability. A finitely algebraizable deductive system is strongly finitely algebraizable if its equivalent quasi-variety is a variety. All the familiar deductive systems of algebraic logic, including both the Fregean and intensional ones, turn out to be strongly finitely algebraizable, but the standard theory is unable to account for this.

Self-extensionality is a much weakened form of the property of being Fregean. A deductive system $\mathcal{D}$ is self-extensional if $\Lambda _ { \mathcal{D}} \operatorname { Thm } \mathcal{D}$ is a congruence relation on the formula algebra.

Let $\mathcal{D}$ be a self-extensional deductive system that has either conjunction or the deduction-detachment theorem with a single deduction-detachment formula. Then $\mathcal{D}$ is second-order finitely algebraizable and its second-order equivalent quasi-variety $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ is actually a variety.

The conjunction/disjunction fragment $\operatorname{CPC}_{\wedge \vee}$ of classical propositional calculus is self-extensional (in fact Fregean) with conjunction. Hence it is finitely algebraizable in the second-order (but not the first-order) sense. Its second-order equivalent quasi-variety $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ is the variety $\mathsf{DL}$ of distributive lattices.

The modal logic $\text{S}5$ can be formulated as a deductive system in two ways, both of which have the same set of theorems. The first and more familiar one, the strong form, is denoted by $\operatorname{S}5 ^ { S }$ and has the necessitation rule

\begin{equation*} \frac { \varphi } { \square \varphi } \end{equation*}

as an inference rule (cf. also Permissible law (inference)) along with modus ponens

\begin{equation*} \frac { \varphi , \varphi \rightarrow \psi } { \psi }. \end{equation*}

The weak form, $\text{S} 5 ^ { \text{W} }$, has modus ponens as its only rule of inference. $\operatorname{S}5 ^ { S }$ is finitely algebraizable but not self-extensional. $\text{S} 5 ^ { \text{W} }$ is not algebraizable, but it is self-extensional and has both conjunction and the deduction-detachment theorem with a single deduction-detachment formula. So $\text{S} 5 ^ { \text{W} }$ is second-order finitely algebraizable. Moreover, its generalized equivalent quasi-variety is a variety; this turns out to be the variety of monadic algebras, which is also the equivalent quasi-variety of $\operatorname{S}5 ^ { S }$.

The main source for this section is [FoJa], where references to other relevant sources can be found. The generalization of algebraizability to Gentzen systems is found in [ReVe].

Semantics-based abstract algebraic logic.

In this important branch of abstract algebraic logic the fine structure of the interpretations of a deductive system is taken into account. It also features a refinement of the notion of language. Let $\Lambda$ be a language type, assumed to be fixed. For an arbitrary set $P$ disjoint from $\Lambda$, let $\operatorname{Fm} _ { P }$ be the set of formulas built up from the elements of $P$, thought of as abstract atomic formulas, using the connectives of $\Lambda$; the associated formula algebra is denoted by $\textbf{Fm} _ { P }$. For each set $P$ of atomic formulas, let $\mathcal{S} _ { P } = \langle P , \operatorname { Mod } _ { \mathcal{S} _ { P } } , \operatorname { mng } _ { \mathcal{S} _ { P } } , \models _{ \mathcal{S} _ { P }} \rangle$ be a four-tuple, where $\operatorname {Mod}_{\mathcal S _ { P }}$ is a class, called the class of models of $\mathcal{S} _ { P }$; $\operatorname {mng}_{\mathcal{S}_P}$ is a function that assigns to each $\mathfrak { M } \in \operatorname { Mod }_{\mathcal{S}_P}$ a function $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$ with domain $\textbf{Fm} _ { P }$, called the meaning function for $\mathfrak{M}$; and $\models _ { \mathcal{S} _ { P } }$ is a binary relation between $\operatorname {Mod}_{\mathcal S _ { P }}$ and $\operatorname{Fm} _ { P }$, called the validity relation.

$\mathcal{S} _ { P }$ is a semantical system if the following conditions hold for every model $\mathfrak{M}$:

the meaning of a formula does not change if a subformula is replaced by one with the same meaning, i.e., $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$ is a homomorphism;

the validity of a formula depends only on its meaning, i.e., if $\operatorname {mng} _ { \mathcal{S} _ { P }, \mathfrak { M } } ( \varphi ) = \operatorname { mng } _ { \mathcal{S} _ { P }, \mathfrak { M } } ( \psi )$, then $\mathfrak { M } \models _ { \mathcal{S} _ { P }} \varphi$ if and only if $\mathfrak { M } \vDash _ { S _ { P } } \psi$. The meaning algebra of $\mathfrak{M}$, in symbols $\mathbf{Me}_{\mathcal{S} _ { P }} \mathfrak { M }$, is the image of $\textbf{Fm} _ { P }$ under the meaning homomorphism $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$. The final defining condition of a semantical system is the following:

every homomorphism from the formula algebra into the meaning algebra of $\mathfrak{M}$ is the meaning function of some model, i.e., if $h : \mathbf{Fm} _ { P } \rightarrow \mathbf{Me} _ { \mathcal{S} _ { P } } \mathfrak { M }$, then there is a $\mathfrak { N } \in \operatorname{Mod}_{\mathcal{S}_P}$ such that $h = \operatorname { mng } _ {{\cal S}_P, \mathfrak { N } } $.

$\mathfrak{M}$ is a model of a set $\Gamma$ of formulas if $\mathfrak { M } \vDash _ { S _ { P } } \psi$ for each $\psi \in \Gamma$. The class of all models of $\Gamma$ is $\operatorname {Mod}_{\mathcal{S} _ { P }} \Gamma$. The consequence relation of $\mathcal{S}$ is the relation $\Gamma \vDash_{ \mathcal{S} _ { P }} \varphi$ that holds between a set of formulas $\Gamma$ and an individual formula if . $\models _ { \mathcal{S} _ { P } }$ satisfies all the conditions of a consequence relation of a deductive system except possibly finiteness; however, most of the familiar semantical systems are finitary. $\langle \mathbf{Fm} _ { P } , \models_{\mathcal{S}_ { P }} \rangle$ is called the underlying deductive system of $\mathcal{S} _ { P }$ and is denoted by ${\cal D S }_ { P }$.

The theory of a model $\mathfrak{M}$ of $\mathcal{S} _ { P }$, in symbols $\operatorname { Th } _ { \mathcal{S} _ { P }} \mathfrak { M }$, is the set of all formulas valid in $\mathfrak{M}$. The truth filter of $\mathbf{Me}_{\mathcal{S} _ { P }} \mathfrak { M }$, $F _ { \mathcal{S} _ { P } } \mathfrak { M }$, is the image of $\operatorname { Th } _ { \mathcal{S} _ { P }} \mathfrak { M }$ under $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$. Because the validity of a formula depends only on its meaning, the meaning matrix $\langle \textbf{Me} _ { \mathcal{S} _ { P } } \mathfrak { M } , F _ { \mathcal{S} _ { P } } \mathfrak { M } \rangle$ together with the meaning function $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$ is an interpretation of the underlying deductive system of $\mathcal{S} _ { P }$. As before, the Leibniz reduction of the meaning matrix by the Leibniz congruence of the truth filter, $\langle {\bf M e} _ { {\cal S} _ { P }} \mathfrak { M } / \Omega F _ { {\cal S}_P } \mathfrak { M } , F _ { {\cal S} _ { P } } \mathfrak { M } / \Omega F _ { {\cal S} _ { P }} \mathfrak { M } \rangle$, is denoted by $\langle {\bf M e} _ { {\cal S} _ { P } } ^ { * \text{L} } \mathfrak { M } , F _ { {\cal S} _ { P } } ^ { * \text{L} } \mathfrak { M } \rangle$. The model-theoretic properties of a large class of different logical systems can be studied algebraically in this context. Consider, for example, the relation of elementary equivalence. Two models $\mathfrak{M}$ and $\mathfrak{N}$ of $\mathcal{S} _ { P }$ are elementarily equivalent if $\operatorname { Th } _ { {\cal S} _ { P } } \mathfrak { M } = \operatorname { Th } _ { {\cal S} _ { P } } \mathfrak { N }$.

Let $\mathcal{S} _ { P }$ be a semantical system. Two models $\mathfrak{M}$ and $\mathfrak{N}$ of $\mathcal{S} _ { P }$ are elementarily equivalent if and only if there is an isomorphism $h$ between the Leibniz-reduced meaning matrices that commutes with the meaning functions, i.e.,

A) $h$ is an isomorphism between $\mathbf{Me} _ { \mathcal{S} _ { P } } ^ { *L } \mathfrak { M }$ and $\mathbf{Me} ^ { * \text{L} _{\mathfrak { N }}}_{\mathcal{S}_P }$ such that $\operatorname { mng }_{{\cal S} _ { P } , \mathfrak { M }} = \operatorname { mng }_{{\cal S} _ { P } , \mathfrak { M }} \circ h$; and

B) $h$ preserves the truth set, i.e., $h ( F _ { \mathcal S _ { P } } \mathfrak { M } ^ { * L} ) = F _ { \mathcal S _ { P } } \mathfrak { N } ^ { * L}$.

Two different classes of algebras are associated with each semantical system $\mathcal{S} _ { P }$:

$\operatorname {Alg} \operatorname {Mod}^{*\text{L}} \mathcal{DS}_{P}$, the algebraic semantics of the underlying deductive system of $\mathcal{S} _ { P }$; and

$\mathsf{Me}\operatorname{Mod}{\cal S}_P= \left\{ {\bf M e} _ { {\cal S} _ { P } } {\frak M:M}\in \operatorname{Mod}_{{\cal S}_P} \right\}$, the class of meaning algebras of $\mathcal{S} _ { P }$. $\mathcal{S} _ { P }$ is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if its underlying deductive system ${\cal D S }_ { P }$ has the property and the meaning matrix of every model of $\mathcal{S} _ { P }$ is Leibniz-reduced, i.e., if . In this case it can be shown that $\operatorname{Alg}\operatorname{Mod}^{*\text{L}} \mathcal{DS}_{P}=\mathfrak{GB}\mathsf{Me}\operatorname{Mod}\mathcal{S}_{P}$.

In general, for a deductive system $\mathcal{D}$ there are many different semantical systems with underlying deductive system $\mathcal{D}$. A natural semantical system for classical propositional logic is obtained by considering only the interpretations of $\operatorname{CPC}$ whose underlying algebra is a Boolean algebra of sets. More precisely, a model is a pair $\langle X , v \rangle$, where $X$ is a set and $v$ assigns a subset of $X$ to each atomic formula in $P$. The meaning function is the unique homomorphism from $\textbf{Fm} _ { P }$ to the Boolean algebra of subsets of $X$ that extends $v$. $\varphi$ is valid in $\langle X , v \rangle$ if its meaning is $X$.

A semantical system for $\text{S}5$ is obtained in a similar way. A model is a three-tuple $\langle X , x , v \rangle $, where $X$ is a set, $x \in X$, and $v$ assigns subsets of $X$ to atomic formulas. The meaning function is the unique homomorphism from $\textbf{Fm} _ { P }$ into the Boolean algebra of subsets of $X$ extending $v$ such that, for every formula $\varphi$, the meaning of $\square \varphi$ is $X$ if the meaning of $\varphi$ is $X$; otherwise the meaning of $\square \varphi$ is the empty set. $\varphi$ is valid in $\langle X , x , v \rangle $ if $x$ is contained in the meaning of $\varphi$. $\langle X , x , v \rangle $ represents a so-called "possible worlds" model for $\text{S}5$; $X$ is the set of possible worlds and a formula is valid in the model if it is true at the distinguished "real world" $x$.

One of the standard semantical systems for the first-order predicate logic has as its models structures of the form $\langle X , v \rangle$, where $X$ is a non-empty set and $v$ assigns a subset of $X ^ { \omega }$ to each atomic formula. It is assumed that the individual variable symbols are arranged in an $\omega$-sequence. The meaning function is the unique homomorphism from $\textbf{Fm}$ into the Boolean algebra of subsets of $X ^ { \omega }$ extending $v$ such that, for each formula $\varphi$, the meaning of $\exists v_i \varphi$ is the "cylinder" that is swept out by moving the meaning of $\varphi$ parallel to the $i$th coordinate. The meaning algebra is the subalgebra of the $\omega$-dimensional cylindric set algebra over $X$ generated by the $\omega$-ary relations that are the meanings of the atomic formulas. Elementary equivalence in first-order logic is essentially captured by the notion of elementary equivalence in the semantical systems of this kind. The characterization of elementary equivalence given by A) and B) provides a way of investigating elementary equivalence algebraically.

The algebraic study of some model-theoretic notions, such as definability, require semantical systems over varying sets of atomic formulas. A system $\mathcal{S} = \langle \mathcal{S} _ { P } : P \ \text {a set } \rangle$ of semantical systems is called a general semantical system if the $\mathcal{S} _ { P }$ are compatible in the sense that, for all $P$ and $P ^ { \prime }$, $\mathcal{S} _ { P }$ and $\mathcal{S} _ { P^{\prime} }$ are isomorphic in the natural sense whenever $P$ and $P ^ { \prime }$ have the same cardinality, and, if $P \subseteq P ^ { \prime }$, then every model of $\mathcal{S} _ { P }$ extends to a model of $\mathcal{S} _ { P^{\prime} }$ and every model of $\mathcal{S} _ { P^{\prime} }$ restricts to a model of $\mathcal{S} _ { P }$. A general semantical system $\mathcal{S}$ is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if each of its component semantical systems $\mathcal{S} _ { P }$ has this property.

For every general semantical system $\mathcal{S}$, $\text { Alg } \text {Mod} ^ { * \text{L}} \mathcal{DS} = \cup \{ \text { Alg } \text {Mod} ^ { * \text{L}} \mathcal{DS} _ { P } : P \ \text { a set } \}$ and $\mathsf{Me} \operatorname{Mod} \mathcal{S}= \cup \{ \mathsf{Me} \operatorname{Mod} \mathcal{S}_p \ : \ P \ \text{a set} \}$.

Let $\mathcal{S}$ be a general semantical system. Let $P$, $R$ and $R ^ { \prime }$ be disjoint sets of atomic formulas, and let $\square '$ be a bijection between $R$ and $R ^ { \prime }$. Let $\Sigma ( P , R ) \subseteq \operatorname{Fm}_{ P \cup R}$ be a set of formulas whose atomic formulas are in $P \cup R$. Then:

$\Sigma ( P , R )$ defines $R$ explicitly over $P$ (in $\mathcal{S}$) if for every $r \in R$ there exists a $\varphi _ { r } \in \operatorname{Fm} _ { P }$ such that, for every $\mathfrak{M} \in \operatorname{Mod} _ { \mathcal{S} _{P \cup R}}( \Sigma ( P , R ) )$, $\operatorname{mng}_{\mathcal{S}_{P \cup R}} , \mathfrak { M } ( r ) = \operatorname { mng } _{\mathcal{S}_ { P \cup R }} , \mathfrak { M } ( \varphi _ { r } )$.

$\Sigma ( P , R )$ defines $R$ implicitly over $P$ (in $\mathcal{S}$) if for every and every $r \in R$,

here $\Sigma ( P , R ^ { \prime } )$ denotes the set of formulas obtained from $\Sigma ( P , R )$ by replacing each $r \in R$ by $r ^ { \prime }$.

$\Sigma ( P , R )$ is a strong implicit definition of $R$ over $P$ (in $\mathcal{S}$) if it defines $R$ implicitly over $P$ and every has an extension $\mathfrak{N} \in \operatorname {Mod}_{\mathcal{S}_{P \cup R}} ( \Sigma ( P , R ) )$.

$\mathcal{S}$ has the (weak) Beth definability property if for all $\Sigma$, $P$ and $R$ as above, $\Sigma$ defines $R$ implicitly over $P$ (in the strong sense), then $\Sigma$ defines $R$ explicitly over $P$. Explicit definability always implies implicit definability. This is the well-known method of A. Padoa formulated in abstract algebraic logic.

The algebraic analogue of the property of Beth is surjectivity of epimorphisms. Let $\mathsf{K}$ be a class of algebras over the same language type. A homomorphism $h : \mathbf{A} \rightarrow \mathbf{B}$, where $\mathbf{A}, \mathbf{B} \in \textsf{K}$, is called an epimorphism over $\mathsf{K}$ if for any pair of homomorphisms $g , g ^ { \prime } : \bf B \rightarrow C$, if $g \circ h = g ^ { \prime } \circ h$, then $g = g ^ { \prime }$.

Let $\mathsf{K} _ { 0 } \subseteq \mathsf{K} $ be classes of algebras over the same language type. A homomorphism $h : \mathbf{A} \rightarrow \mathbf{B}$, where $\mathbf{A}, \mathbf{B} \in \textsf{K}$, is said to be $ \mathsf{K} _ { 0 }$-extensible over $\mathsf{K}$ if for any $\mathbf{C} \in \mathsf{K}_0$ and every surjection $f : \mathbf{A} \twoheadrightarrow \mathbf{C}$ there is a ${\bf D} \in \mathsf{K}_0$ and $g : \mathbf{B} \mapsto \mathbf{D}$ such that $\bf C \subseteq D$ and $g \circ h = f$.

Let $\mathcal{S}$ be a finitely algebraizable generalized semantical system. Then:

I) $\mathcal{S}$ has the Beth definability property if and only if every epimorphism over $\operatorname{Alg} \operatorname{Mod}^{*\text{L}} \cal DS$ is surjective;

II) $\mathcal{S}$ has the weak Beth definability property if and only if every )-extensible epimorphism of $\operatorname{Alg} \operatorname{Mod}^{*\text{L}} \cal DS$ is surjective.

The algebraic characterization of the weak Beth property requires a semantics-based context, but the result on the ordinary Beth property can be reformulated within logistic abstract algebraic logic and extended to equivalence deductive systems.

The main references for semantics-based abstract algebraic logic are [AnNéSa], [AnKuNéSa], [AnNé]. For the results on definability, see [Ho] and [Ho2].

References

[AnBe]	A.R. Anderson, N.D. Belnap, "Entailment. The logic of relevance and necessity", I, Princeton Univ. Press (1975) MR0406756 Zbl 0323.02030
[BlPi2]	W.J. Blok, D. Pigozzi, "Algebraizable logics", Memoirs, 396, Amer. Math. Soc. (1989) MR0973361 Zbl 0664.03042
[BlPi3]	W.J. Blok, D. Pigozzi, "Protoalgebraic logics" Studia Logica, 45 (1986) pp. 337–369 MR0884144 Zbl 0622.03020
[BlSu]	S.L. Bloom, R. Suszko, "Investigations into the sentential logic with identity" Notre Dame J. Formal Logic, 13 (1972) pp. 289–308
[ChTa]	L.H. Chin, A. Tarski, "Distributive and modular laws in relation algebras" Univ. California Publ. Math. New Ser., 1 : 9 (1951) pp. 341–384 Zbl 0045.31701
[Cz]	J. Czelakowski, "Algebraic aspects of deduction theorems" Studia Logica, 44 (1985) pp. 369–387 MR0832395 Zbl 0612.03016
[Cz2]	J. Czelakowski, "Protoalgebraic logics", Trends in Logic—Studia Logica Libr., 10, Kluwer Acad. Publ. (2001) MR1828895 Zbl 0984.03002
[Cz3]	J. Czelakowski, "Equivalential logics I—II" Studia Logica, 40 (1981) pp. 227–236; 355–372
[Cz4]	J. Czelakowski, "Consequence operations: Foundational studies" Techn. Rept. Inst. Philosophy and Sociology Polish Acad. Sci. (1992)
[Cz5]	J. Czelakowski, "Filter-distributive logics" Studia Logica, 43 (1984) pp. 353–377 MR0803314 Zbl 0578.03012
[CzJa]	J. Czelakowski, R. Jansana, "Weakly algebraizable logics" J. Symbolic Logic, 65 (2000) pp. 641–668 MR1771075 Zbl 0960.03055
[DeJa]	P. Dellunde, R. Jansana, "Some characterization theorems for infinitary universal horn logic without equality" J. Symbolic Logic, 61 (1996) pp. 1242–1260 MR1456105 Zbl 0871.03029
[El]	R. Elgueta, "Subdirect representation theory for classes without equality" Algebra Univ., 40 (1998) pp. 201–246 MR1651879 Zbl 0933.03035
[El2]	R. Elgueta, "Characterizing classes defined without equality" Studia Logica, 58 (1997) pp. 357–394 MR1460253
[FoJa]	J.M. Font, R. Jansana, "A general algebraic semantics for sentential logics", Lecture Notes in Logic, 7, Springer (1996) MR1421569 Zbl 0865.03054
[Ha]	P.R. Halmos, "Algebraic logic I: Monadic Boolean algebras" Compositio Math., 12 (1955) pp. 217–249
[He]	B. Herrmann, "Characterizing equivalential and algebraizable logics" Studia Logica, 58 (1997) pp. 305–323 MR1439022 Zbl 0879.03023
[He2]	B. Herrmann, "Equivalential and algebraizable logics" Studia Logica, 57 (1996) pp. 419–436 MR1416744 Zbl 0864.03043
[Ho]	E. Hoogland, "Algebraic characterization of various Beth definability properties" Studia Logica, 65 (2000) pp. 91–112 MR1781785
[Ho2]	E. Hoogland, "Definability and interpolation. Model-theoretic investigations", ILLC Dissert. Ser. DS-2001-05, Inst. Language, Logic and Computation, Amsterdam (2001) MR1838246
[Ło]	J. Łoś, "O matrycach logicznych" Ser. B. Travaux de la Soc. Sci. et des Lettres de Wrocław, 19 (1949)
[Ma]	J. Malinowski, "The deduction theorem for quantum logic—some negative results" J. Symbolic Logic, 55 (1990) pp. 615–625 MR1056375 Zbl 0702.03039
[Pa]	K. Pałasińska, "Deductive systems and finite axiomatizability properties" PhD Thesis Iowa State Univ. (1994)
[Ra]	H. Rasiowa, "An algebraic approach to non-classical logics", North-Holland (1974) MR0446968 Zbl 0299.02069
[ReVe]	J. Rebagliato, V. Verdú, "On the algebraization of some Gentzen systems" Fundam. Inform., 18 (1993) pp. 319–338 (Special Issue on Algebraic Logic and its Applications) MR1270344 Zbl 0788.03006
[Sm]	T. Smiley, "The independence of connectives" J. Symbolic Logic, 27 (1962) pp. 426–436 MR0172784
[Ta]	A. Tarski, "Über einige fundamentale Begriffe der Metamathematik" C.R. Soc. Sci. Lettr. Varsovie Cl. III, 23 (1930) pp. 22–29
[Ta2]	A. Tarski, "Grundzüge der Systemenkalküls. Erster Teil" Fundam. Math., 25 (1935) pp. 503–526
[Wó]	R. Wójcicki, "Theory of logical calculi. Basic theory of consequence operations", Synthese Library, 199, Reidel (1988) MR1009788 Zbl 0682.03001