View source for Abstract algebraic logic

{{TEX|want}}
{{MSC|03|03G27}}

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|Propositional calculus]]) followed this path with Boolean algebras coming before the classical propositional calculus (cf. also [[Boolean algebra|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|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300401.png" /> of connectives or operation symbols (cf. also [[Propositional connective|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300402.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300403.png" />. This is the  "absolutely free"  algebra of type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300404.png" /> with an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300405.png" />-ary operation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300406.png" /> for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300407.png" /> of arity <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300408.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a1300409.png" /> is the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004010.png" />, in prefix notation, or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004011.png" /> when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004012.png" /> and infix notation is used. The operation of simultaneously substituting fixed but arbitrary formulas for variables is identified with the unique endomorphism of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004013.png" /> it determines. A logistic or deductive system is a pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004014.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004015.png" />, the consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004016.png" />, is a binary relation between sets of formulas and individual formulas satisfying the following well-known conditions: For all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004017.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004018.png" />,

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004019.png" /> for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004020.png" />;

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004021.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004022.png" /> for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004023.png" /> imply <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004024.png" />;

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004025.png" /> implies <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004026.png" /> for some finite <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004027.png" /> (finiteness);

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004028.png" /> implies <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004029.png" /> for every substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004030.png" /> (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|equational logic]].

A formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004031.png" /> is a theorem of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004032.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004033.png" /> (i.e., it is a consequence of the empty set of formulas). The set of theorems, which may be empty, is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004034.png" />. A set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004035.png" /> of formulas is a theory of a deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004036.png" /> if it is closed under consequence, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004037.png" /> whenever <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004038.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004039.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004040.png" /> is the smallest theory. The set of all theories of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004041.png" /> is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004042.png" />. The theory axiomatized by an arbitrary set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004043.png" /> of formulas is the set of all formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004044.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004045.png" />.

Deductive systems in this sense include all the familiar sentential logics (cf. also [[Propositional calculus|Propositional calculus]]) together with their various fragments and refinements — for example, the classical and intuitionistic propositional calculi <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004046.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004047.png" />, the intermediate logics (cf. also [[Intermediate logic|Intermediate logic]]), the various modal logics, including <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004048.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004049.png" /> (cf. also [[Modal logic|Modal logic]]), and the multiple-valued logics of J. Łukasiewicz and E. Post (cf. also [[Many-valued logic|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|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004050.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004051.png" /> is an algebra (of the same language type as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004052.png" />), the underlying algebra of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004053.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004054.png" />, the designated set of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004055.png" />. An interpretation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004056.png" /> is a matrix <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004057.png" /> together with a homomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004058.png" /> from the algebra of formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004059.png" /> into the underlying algebra of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004060.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004061.png" /> is to be thought of as the  "sense"  or  "meaning"  of the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004062.png" /> under the interpretation, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004063.png" /> is  "true"  or  "false"  depending on whether or not <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004064.png" />. By the Frege principle, this truth value is the denotation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004065.png" /> under the interpretation. Truth must be preserved under consequence in the sense that, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004066.png" /> and each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004067.png" /> is true under the interpretation, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004068.png" /> must also be true. A set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004069.png" /> of formulas is said to define a class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004070.png" /> of interpretations if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004071.png" /> is the class of all interpretations in which each formula of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004072.png" /> is true. Because truth is preserved under consequence, the theory axiomatized by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004073.png" /> also defines <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004074.png" />; it turns out that it is the unique theory with this property.

The formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004075.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004076.png" /> are equivalent over a given class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004077.png" /> of interpretations (in the Fregean sense) if they have the same truth value, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004078.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004079.png" /> for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004080.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004081.png" />. They are logically equivalent (with respect to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004082.png" />) 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 {{Cite|Ło}}, {{Cite|Ta2}}; for more recent work, see {{Cite|Wó}}. For relation, polyadic and cylindric algebras, see {{Cite|ChTa}}, {{Cite|Ha}}, {{Cite|HeMoTa}}. For the origin of the notion of a deductive system, see {{Cite|Ta}}.

==Logistic abstract algebraic logic.==
The assumption that the deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004083.png" /> is uninterpreted implies that one need consider only those matrices <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004084.png" /> with the property that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004085.png" /> is an interpretation for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004086.png" />. Such a matrix is called a (matrix) model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004087.png" />; the class of all models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004088.png" /> is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004089.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004090.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004091.png" /> are equivalent over a theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004092.png" />, or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004095.png" />-equivalent, in the Fregean sense, if, for every theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004096.png" /> that extends <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004097.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004098.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a13004099.png" />; the binary relation between formulas defined this way is called the Frege relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040100.png" /> and denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040101.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040102.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040103.png" /> are logically equivalent (with respect to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040104.png" />) if they are equivalent over every theory, or, equivalently, if they are equivalent over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040105.png" />, the set of theorems. In terms of the consequence relation, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040106.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040107.png" /> are logically equivalent over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040108.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040109.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040110.png" /> are each consequences of the other over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040111.png" />; symbolically, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040112.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040113.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040114.png" />.

If, as in the case of the classical and intuitionistic propositional calculi, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040115.png" /> has a binary implication connective <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040116.png" /> for which the deduction theorem holds, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040117.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040118.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040119.png" />, or equivalently if there is a biconditional, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040120.png" />. So, under these rather weak conditions on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040121.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040122.png" /> is the classical propositional calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040123.png" /> or the intuitionistic propositional calculus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040124.png" />. If in any formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040125.png" /> a subformula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040126.png" /> is replaced by an equivalent formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040127.png" />, the resulting formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040128.png" /> is equivalent to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040129.png" />. In algebraic terms this says that for every theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040130.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040131.png" /> or <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040132.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040133.png" /> is a congruence relation on the algebra of formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040134.png" />. A deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040135.png" /> for which <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040136.png" />-equivalence is compositional for every theory <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040137.png" /> is called Fregean or extensional; non-Fregean systems are called intensional.

If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040138.png" /> is Fregean, it is possible to form the quotient matrices <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040139.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040140.png" /> ranges over all theories. These are called the Lindenbaum–Tarski models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040141.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040142.png" /> of the strong form of the modal system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040143.png" />, with necessitation as a rule of inference (see below), one has <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040144.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040145.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040146.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040147.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040148.png" />. But this relation is not, in general, compositional. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040149.png" /> includes however a largest compositional equivalence relation, called the Suszko congruence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040151.png" /> over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040152.png" /> and denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040153.png" />. It can be shown that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040154.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040155.png" />. So <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040156.png" /> captures the usual notion of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040157.png" />-equivalence for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040158.png" />.

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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040159.png" /> of the underlying set of an algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040160.png" />, of the same language type as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040161.png" />, is called a filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040162.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040163.png" /> is a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040164.png" />; thus <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040165.png" /> is a filter if and only if it is closed under consequence in the sense that, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040166.png" />, one has <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040167.png" /> for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040168.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040169.png" /> for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040170.png" />. The set of filters of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040171.png" /> on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040172.png" /> is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040173.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040174.png" /> in a natural way. The Frege relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040175.png" /> is the set of all pairs <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040176.png" /> of elements of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040177.png" /> such that, for every filter <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040178.png" /> on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040179.png" /> that includes <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040180.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040181.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040182.png" />. The Suszko congruence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040183.png" /> is the largest congruence relation on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040184.png" /> that is included in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040185.png" />; it always exists.

The quotient matrix <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040186.png" /> is called the Suszko-reduction of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040187.png" /> and is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040188.png" />. It can be shown that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040189.png" /> coincides with (or, more precisely, is isomorphic to) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040190.png" />. A model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040191.png" /> is Suszko-reduced if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040192.png" />, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040193.png" /> is the identity relation. The class of all Suszko-reduced models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040194.png" /> is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040195.png" />. The Suszko-reduced models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040196.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040197.png" /> is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040198.png" />. The underlying algebras of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040199.png" /> are the Boolean algebras. Each filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040200.png" /> on a Boolean algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040201.png" /> is completely determined by its Suszko congruence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040202.png" />; more precisely, it coincides with the set of all elements of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040203.png" /> equivalent under <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040204.png" /> to the unit element <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040205.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040206.png" />. Moreover, every congruence relation on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040207.png" /> is the Suszko congruence of a filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040208.png" />. It follows that the consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040209.png" /> is completely determined by the equational logic of Boolean algebras, and in this way the class of Boolean algebras <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040210.png" /> constitutes a complete algebraic semantics for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040211.png" />. In a similar way, the class of Heyting algebras <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040212.png" /> and the class of so-called monadic algebras <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040213.png" /> constitute complete algebraic semantics for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040214.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040215.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040216.png" /> and the equational logic of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040217.png" /> 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 {{Cite|Ło}}, {{Cite|Sm}}. {{Cite|Su2}} contains historical information on the Tarski–Lindenbaum process. The essential idea of Fregean logic as presented here originated with R. Suszko {{Cite|BlSu}}, {{Cite|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040218.png" /> and the equational consequence relation of a class of algebras.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040219.png" /> be a deductive system and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040220.png" /> a class of algebras over the same language type. Let

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040221.png" /></td> </tr></table>

be a (possibly infinite) non-empty system of formulas in two variables. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040222.png" /> is said to be a faithful interpretation of the equational logic of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040223.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040224.png" /> if, for every equation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040225.png" /> and every set of equations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040226.png" />,

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040227.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040228.png" /> means that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040229.png" /> is a quasi-identity of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040230.png" />. Also, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040231.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040232.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040233.png" /> is shorthand for the system of entailments <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040234.png" /> for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040235.png" />;  "iff"  stands for  "if and only if" .

Let

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040236.png" /></td> </tr></table>

be a non-empty system of equations in one variable. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040237.png" /> is a faithful interpretation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040238.png" /> in the equational logic of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040239.png" /> if, for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040240.png" />,

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040241.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040242.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040243.png" />. The two interpretations are mutual inverses if

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040244.png" /></td> </tr></table>

and

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040245.png" /></td> </tr></table>

A pair of mutually invertible interpretations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040246.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040247.png" /> such as these is called a bisimulation between <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040248.png" /> and the equational logic of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040249.png" />. A deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040250.png" /> is algebraizable if there is a bisimulation between <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040251.png" /> and the equational logic of some class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040252.png" /> of algebras; it is finitely algebraizable if the interpretations are finite. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040253.png" /> is algebraizable, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040254.png" /> is the largest class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040255.png" /> with the above properties; it is called the equivalent algebraic semantics of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040256.png" />. In general, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040257.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040258.png" /> is finitely algebraizable. In this case <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040259.png" /> is a quasi-variety (cf. also [[Quasi-variety|Quasi-variety]])

The classical and intuitionistic propositional calculi <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040260.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040261.png" /> are finitely algebraizable and their equivalent quasi-varieties are, respectively, the varieties <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040262.png" /> of Boolean algebras and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040263.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040264.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040265.png" /> is, respectively, the classical and intuitionistic biconditional, and the inverse faithful interpretation is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040266.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040267.png" />.

The bisimulation between a finitely algebraizable deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040268.png" /> and the equational logic of its equivalent quasi-variety <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040269.png" /> induces a correspondence between the meta-logical properties of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040270.png" /> and the algebraic properties of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040271.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040272.png" /> and the amalgamation property of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040273.png" />;

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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040274.png" /> 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|universal algebra]] to answer some important questions about the validity of the deduction theorem in a variety of logical systems.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040275.png" /> be a deductive system. A finite non-empty set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040276.png" /> of binary formulas is called a deduction-detachment system for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040277.png" /> if the following equivalence holds for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040278.png" />:

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040279.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040280.png" /></td> </tr></table>

A deductive system has the deduction-detachment theorem if it has a deduction-detachment system. The implication <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040281.png" /> forms a singleton deduction-detachment system for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040282.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040283.png" />, while the formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040284.png" /> forms a singleton deduction-detachment system for the modal systems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040285.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040286.png" />.

For an algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040287.png" />, let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040288.png" /> be the set of all congruences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040289.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040290.png" /> is a quasi-variety, then a congruence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040291.png" /> on an arbitrary algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040292.png" /> (not necessarily in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040293.png" />) is called a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040295.png" />-congruence if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040296.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040297.png" /> is a variety (cf. also [[Algebraic systems, variety of|Algebraic systems, variety of]]) and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040298.png" />, then every congruence is a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040299.png" />-congruence. The principal <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040301.png" />-congruence generated by the pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040302.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040303.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040304.png" />, is the smallest <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040305.png" />-congruence that identifies <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040306.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040307.png" />. A quasi-variety <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040308.png" /> has equationally definable principal relative congruences (EDPRC) if there is a finite system of equations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040309.png" />, in four variables, such that, for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040310.png" /> and all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040311.png" />,

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040312.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040313.png" /></td> </tr></table>

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040314.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040315.png" /> is any homomorphism such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040316.png" />.

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040317.png" />-congruence generation in the formula algebra can be interpreted as the consequence relation of the equational logic of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040318.png" />. Thus, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040319.png" /> has EDPRC, the defining equations <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040320.png" /> can be interpreted collectively as an implication connective for the equational logic. This observation is reflected in the following theorem: Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040321.png" /> be a finitely algebraizable deductive system and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040322.png" /> be its equivalent quasi-variety. Then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040323.png" /> has the deduction-detachment theorem if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040324.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040325.png" /> 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 {{Cite|BlPi2}}; earlier definitions, notably that in {{Cite|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 ({{Cite|Cz4}}, {{Cite|CzJa}}, {{Cite|He2}}, {{Cite|He}}). For entailment logic and its algebraizability, see {{Cite|AnBe}}, {{Cite|BlPi2}}. For the deduction theorem in abstract algebraic logic, see {{Cite|BlPi}}, {{Cite|Cz}}. The result on orthomodular logic is found in {{Cite|BlPi5}}, {{Cite|Ma}}.

===The algebraic hierarchy.===
Finitely algebraizable deductive systems exhibit the strongest connection between the meta-logical properties of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040326.png" /> and the algebraic properties of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040327.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040328.png" /> be a (possibly infinite) set of formulas in two variables. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040329.png" /> is a proto-equivalence system for a deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040330.png" /> if

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040331.png" /></td> </tr></table>

(<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040333.png" />-detachment).

A non-empty proto-equivalence system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040334.png" /> is an equivalence system if

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040335.png" /></td> </tr></table>

and

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040336.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040337.png" /></td> </tr></table>

for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040338.png" /> (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040339.png" /> is the rank of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040340.png" />). 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040341.png" /> of formulas in two variables is an equivalence system for a deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040342.png" /> if and only if it defines Suszko congruences in the sense that, for every algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040343.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040344.png" />,

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040345.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040346.png" /></td> </tr></table>

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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040347.png" /> of equations in one variable, called a system of defining equations, such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040348.png" />.

This last condition abstracts an important property of the biconditional <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040349.png" /> of both classical and intuitionistic propositional logic, namely, that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040350.png" /> and the biconditional <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040351.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040352.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040353.png" /> and any subset <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040354.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040355.png" />, there is a largest congruence relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040356.png" /> on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040357.png" /> compatible with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040358.png" /> in the sense that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040359.png" /> is a union of equivalence classes of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040360.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040361.png" /> is called the Leibniz congruence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040362.png" />. The relationship between the Leibniz and Suszko congruences is straightforward: For every deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040363.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040364.png" />,

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040365.png" /></td> </tr></table>

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040366.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040367.png" /> can both be viewed as operators mapping the lattice of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040368.png" />-filters of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040369.png" /> to the lattice of congruences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040370.png" />. Note that the Leibniz and Suszko congruences coincide on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040371.png" />-filters just in case the Leibniz operator is order-preserving, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040372.png" /> implies <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040373.png" /> for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040374.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040375.png" /> be a deductive system. Then the following characterizations hold:

i) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040376.png" /> is protoalgebraic if and only if the Leibniz operator <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040377.png" /> is order-preserving, i.e., if and only if the Leibniz and Suszko congruences coincide;

ii) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040378.png" /> is equivalential if and only if it is protoalgebraic and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040379.png" /> commutes with inverse homomorphic images; more precisely, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040380.png" /> for every homomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040381.png" /> and every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040382.png" />;

iii) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040383.png" /> is finitely equivalential if and only if it is protoalgebraic and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040384.png" /> commutes with directed unions; more precisely, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040385.png" /> for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040386.png" /> that is upward-directed by inclusion;

iv) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040387.png" /> is algebraizable if and only if it is equivalential and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040388.png" /> is injective;

v) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040389.png" /> is finitely algebraizable if and only if it is finitely equivalential and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040390.png" /> is injective.

A deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040391.png" /> is said to be weakly algebraizable if it is protoalgebraic and the Leibniz operator <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040392.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040393.png" /> 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. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040394.png" /> denotes the class of all Leibniz-reduced models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040395.png" />. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040396.png" /> is protoalgebraic, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040397.png" />; this equality in fact characterizes protoalgebraic systems. In general, the best one has is that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040398.png" /> coincides with the class of all matrices isomorphic to a subdirect product of matrices in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040399.png" />, in symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040400.png" />.

For any class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040401.png" /> of matrices, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040402.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040403.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040404.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040405.png" /> denote, respectively, the classes of isomorphic images of submatrices, direct products, subdirect products, and ultraproducts of members of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040406.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040407.png" /> be a deductive system. Then the following characterizations hold:

a) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040408.png" /> is protoalgebraic if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040409.png" />, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040410.png" />;

b) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040411.png" /> is equivalential if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040412.png" />;

c) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040413.png" /> is finitely equivalential if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040414.png" />, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040415.png" /> is a quasi-variety in the sense of Mal'cev;

d) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040416.png" /> is algebraizable if and only if it is equivalential and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040417.png" /> is the minimal <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040418.png" />-filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040419.png" /> for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040420.png" />;

e) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040421.png" /> is finitely algebraizable if and only if it is finitely equivalential and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040422.png" /> is the minimal <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040423.png" />-filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040424.png" /> for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040425.png" />.

For papers on the specific levels of the algebraic hierarchy, see {{Cite|BlPi3}}, {{Cite|BlPi2}}, {{Cite|Cz3}}, {{Cite|CzJa}}, {{Cite|He2}}, {{Cite|He}}. Two references of a more general nature are {{Cite|BlPi4}}, {{Cite|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|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040426.png" /> whose Leibniz-reduced model class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040427.png" /> is well behaved in the sense of strict Horn logic with equality, and the key to this is the following correspondence theorem for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040429.png" />-filters that mirrors the correspondence theorem for congruences in universal algebra: Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040430.png" /> be a protoalgebraic deductive system, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040431.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040432.png" /> be algebras and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040433.png" /> a surjective homomorphism. Finally, let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040434.png" /> be the smallest <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040435.png" />-filter on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040436.png" />. Then the mapping <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040437.png" /> is a one-to-one correspondence between the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040438.png" />-filters on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040439.png" /> and the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040440.png" />-filters on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040441.png" /> that include <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040442.png" />.

When <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040443.png" /> is taken to be <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040444.png" />, the algebra of formulas, this correspondence establishes a close connection between the meta-logical properties of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040445.png" /> and the algebraic properties of the class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040446.png" /> of Leibniz-reduced models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040447.png" />.

Every class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040448.png" /> of matrices over the same language type <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040449.png" /> defines a deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040450.png" /> over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040451.png" /> in the following way. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040452.png" /> if, for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040453.png" /> and every homomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040454.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040455.png" /> whenever <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040456.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040457.png" /> be a class of Leibniz-reduced matrices over the same language type; then

if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040458.png" /> is protoalgebraic, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040459.png" />;

if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040460.png" /> is equivalential, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040461.png" />.

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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040462.png" /> is filter-distributive if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040463.png" /> is a distributive lattice for every algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040464.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040465.png" /> be a finite set of matrices. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040466.png" /> is protoalgebraic and filter-distributive, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040467.png" /> has a presentation by a finite set of axioms and inference rules {{Cite|Pa}}. An important related axiomatizability result can be found in {{Cite|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 {{Cite|Cz}}, {{Cite|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 {{Cite|BlPi4}}, {{Cite|Cz3}}, {{Cite|DeJa}}, {{Cite|El2}}, {{Cite|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040468.png" /> of classical propositional logic. It has a natural algebraic semantics, the variety <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040469.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040470.png" />-filters to certain special classes of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040471.png" />-filters and to a natural generalization of the Leibniz congruence that applies to classes of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040472.png" />-filters.

The non-algebraizability of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040473.png" /> is reflected in the fact that, for an arbitrary algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040474.png" />, the Leibniz operator does not give a one-one correspondence between (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040475.png" />)-filters and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040476.png" />-congruences. The correspondence can in a sense be recovered by replacing single (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040477.png" />)-filters by sets of (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040478.png" />)-filters, each of which is of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040479.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040480.png" /> consists of all (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040481.png" />)-filters that are compatible with each member of a fixed but arbitrary class <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040482.png" /> of congruences on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040483.png" />. The set of congruences <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040484.png" /> is completely arbitrary, but it turns out that there is always a single congruence <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040485.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040486.png" />, and in fact a smallest one with this property, and it is necessarily a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040487.png" />-congruence. Moreover, all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040488.png" />-congruences can be obtained this way.

Considerations such as these lead to the following notion. A full second-order filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040489.png" /> on an algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040490.png" /> is the set of all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040491.png" />-filters <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040492.png" /> on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040493.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040494.png" /> is compatible with a fixed but arbitrary set of congruences. The set of full second-order filters on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040495.png" /> is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040496.png" />. It is easy to check that every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040497.png" /> is an algebraic closed-set system of the universe <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040498.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040499.png" />. For each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040500.png" /> the Frege relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040501.png" /> is the largest binary relation on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040502.png" /> (necessarily an equivalence relation) that is compatible with each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040503.png" />, and the second-order Leibniz congruence, also called the Tarski congruence, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040504.png" /> is the largest congruence of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040505.png" /> included in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040506.png" />.

A set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040507.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040508.png" />-filters on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040509.png" /> is a full second-order filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040510.png" /> if and only if the set of quotient filters <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040511.png" /> coincides with the set of all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040512.png" />-filters on the quotient algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040513.png" />. A full second-order model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040514.png" /> is a second-order matrix <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040515.png" /> where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040516.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040517.png" /> is Leibniz reduced if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040518.png" /> is the identity relation. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040519.png" /> (respectively, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040520.png" />) is the class of all (Leibniz-reduced) full second-order models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040521.png" />.

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

For any deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040522.png" /> and any algebra <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040523.png" /> the second-order Leibniz operator <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040524.png" /> is a dual order-isomorphism between <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040525.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040526.png" />, both partially ordered by set inclusion.

A full second-order model, and more generally, any second-order matrix <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040527.png" /> where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040528.png" /> is an algebraic closed-set system on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040529.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040530.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040531.png" /> is any finite, non-empty sequence of formulas. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040532.png" /> be a second-order matrix, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040533.png" /> be the closure operator on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040534.png" /> associated with the algebraic closed-set system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040535.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040536.png" /> is a model of a Gentzen system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040537.png" /> if the following holds. For every entailment

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040538.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040539.png" /></td> </tr></table>

and every homomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040540.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040541.png" /> for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040542.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040543.png" />.

A deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040544.png" /> is said to have a fully adequate Gentzen system if the class of full second-order models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040545.png" /> is the class of models of a Gentzen system. (Strictly speaking, this is the form the definition takes when <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040546.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040547.png" /> is finitely algebraizable, there is a unique quasi-variety <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040548.png" /> that is equivalent to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040549.png" /> in the sense that there is a bisimulation between the consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040550.png" /> (between sequents) and the equational consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040551.png" />. In view of the above observations it is natural to take a deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040552.png" /> to be second-order finitely algebraizable if it has a fully adequate Gentzen system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040553.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040554.png" /> is finitely algebraizable. In this case, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040555.png" /> turns out to coincide with the equivalent quasi-variety of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040556.png" />, and the consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040557.png" /> is definable (as part of the consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040558.png" />) in the equational consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040559.png" />, but not vice versa unless <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040560.png" /> is also finitely algebraizable. In the latter case <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040561.png" /> coincides with the equivalent quasi-variety of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040562.png" />. When <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040563.png" /> is second-order finitely algebraizable, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040564.png" /> is called the second-order equivalent quasi-variety of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040565.png" />.

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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040566.png" /> is self-extensional if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040567.png" /> is a congruence relation on the formula algebra.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040568.png" /> be a self-extensional deductive system that has either conjunction or the deduction-detachment theorem with a single deduction-detachment formula. Then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040569.png" /> is second-order finitely algebraizable and its second-order equivalent quasi-variety <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040570.png" /> is actually a variety.

The conjunction/disjunction fragment <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040571.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040572.png" /> is the variety <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040573.png" /> of distributive lattices.

The modal logic <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040574.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040575.png" /> and has the necessitation rule

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040576.png" /></td> </tr></table>

as an inference rule (cf. also [[Permissible law (inference)|Permissible law (inference)]]) along with [[Modus ponens|modus ponens]]

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040577.png" /></td> </tr></table>

The weak form, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040578.png" />, has modus ponens as its only rule of inference. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040579.png" /> is finitely algebraizable but not self-extensional. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040580.png" /> is not algebraizable, but it is self-extensional and has both conjunction and the deduction-detachment theorem with a single deduction-detachment formula. So <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040581.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040582.png" />.

The main source for this section is {{Cite|FoJa}}, where references to other relevant sources can be found. The generalization of algebraizability to Gentzen systems is found in {{Cite|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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040583.png" /> be a language type, assumed to be fixed. For an arbitrary set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040584.png" /> disjoint from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040585.png" />, let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040586.png" /> be the set of formulas built up from the elements of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040587.png" />, thought of as abstract atomic formulas, using the connectives of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040588.png" />; the associated formula algebra is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040589.png" />. For each set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040590.png" /> of atomic formulas, let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040591.png" /> be a four-tuple, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040592.png" /> is a class, called the class of models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040593.png" />; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040594.png" /> is a function that assigns to each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040595.png" /> a function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040596.png" /> with domain <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040597.png" />, called the meaning function for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040598.png" />; and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040599.png" /> is a binary relation between <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040600.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040601.png" />, called the validity relation.

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040602.png" /> is a semantical system if the following conditions hold for every model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040603.png" />:

the meaning of a formula does not change if a subformula is replaced by one with the same meaning, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040604.png" /> is a homomorphism;

the validity of a formula depends only on its meaning, i.e., if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040605.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040606.png" /> if and only if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040607.png" />. The meaning algebra of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040608.png" />, in symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040609.png" />, is the image of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040610.png" /> under the meaning homomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040611.png" />. The final defining condition of a semantical system is the following:

every homomorphism from the formula algebra into the meaning algebra of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040612.png" /> is the meaning function of some model, i.e., if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040613.png" />, then there is a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040614.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040615.png" />.

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040616.png" /> is a model of a set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040617.png" /> of formulas if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040618.png" /> for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040619.png" />. The class of all models of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040620.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040621.png" />. The consequence relation of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040622.png" /> is the relation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040623.png" /> that holds between a set of formulas <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040624.png" /> and an individual formula if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040625.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040626.png" /> satisfies all the conditions of a consequence relation of a deductive system except possibly finiteness; however, most of the familiar semantical systems are finitary. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040627.png" /> is called the underlying deductive system of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040628.png" /> and is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040629.png" />.

The theory of a model <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040630.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040631.png" />, in symbols <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040632.png" />, is the set of all formulas valid in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040633.png" />. The truth filter of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040634.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040635.png" />, is the image of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040636.png" /> under <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040637.png" />. Because the validity of a formula depends only on its meaning, the meaning matrix <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040638.png" /> together with the meaning function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040639.png" /> is an interpretation of the underlying deductive system of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040640.png" />. As before, the Leibniz reduction of the meaning matrix by the Leibniz congruence of the truth filter, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040641.png" />, is denoted by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040642.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040643.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040644.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040645.png" /> are elementarily equivalent if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040646.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040647.png" /> be a semantical system. Two models <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040648.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040649.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040650.png" /> are elementarily equivalent if and only if there is an isomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040651.png" /> between the Leibniz-reduced meaning matrices that commutes with the meaning functions, i.e.,

A) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040652.png" /> is an isomorphism between <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040653.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040654.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040655.png" />; and

B) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040656.png" /> preserves the truth set, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040657.png" />.

Two different classes of algebras are associated with each semantical system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040658.png" />:

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040659.png" />, the algebraic semantics of the underlying deductive system of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040660.png" />; and

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040661.png" />, the class of meaning algebras of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040662.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040663.png" /> is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if its underlying deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040664.png" /> has the property and the meaning matrix of every model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040665.png" /> is Leibniz-reduced, i.e., if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040666.png" />. In this case it can be shown that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040667.png" />.

In general, for a deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040668.png" /> there are many different semantical systems with underlying deductive system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040669.png" />. A natural semantical system for classical propositional logic is obtained by considering only the interpretations of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040670.png" /> whose underlying algebra is a Boolean algebra of sets. More precisely, a model is a pair <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040671.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040672.png" /> is a set and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040673.png" /> assigns a subset of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040674.png" /> to each atomic formula in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040675.png" />. The meaning function is the unique homomorphism from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040676.png" /> to the Boolean algebra of subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040677.png" /> that extends <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040678.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040679.png" /> is valid in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040680.png" /> if its meaning is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040681.png" />.

A semantical system for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040682.png" /> is obtained in a similar way. A model is a three-tuple <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040683.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040684.png" /> is a set, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040685.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040686.png" /> assigns subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040687.png" /> to atomic formulas. The meaning function is the unique homomorphism from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040688.png" /> into the Boolean algebra of subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040689.png" /> extending <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040690.png" /> such that, for every formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040691.png" />, the meaning of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040692.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040693.png" /> if the meaning of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040694.png" /> is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040695.png" />; otherwise the meaning of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040696.png" /> is the empty set. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040697.png" /> is valid in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040698.png" /> if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040699.png" /> is contained in the meaning of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040700.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040701.png" /> represents a so-called  "possible worlds"  model for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040702.png" />; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040703.png" /> is the set of possible worlds and a formula is valid in the model if it is true at the distinguished  "real world"  <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040704.png" />.

One of the standard semantical systems for the first-order predicate logic has as its models structures of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040705.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040706.png" /> is a non-empty set and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040707.png" /> assigns a subset of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040708.png" /> to each atomic formula. It is assumed that the individual variable symbols are arranged in an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040709.png" />-sequence. The meaning function is the unique homomorphism from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040710.png" /> into the Boolean algebra of subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040711.png" /> extending <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040712.png" /> such that, for each formula <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040713.png" />, the meaning of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040714.png" /> is the  "cylinder"  that is swept out by moving the meaning of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040715.png" /> parallel to the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040716.png" />th coordinate. The meaning algebra is the subalgebra of the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040717.png" />-dimensional cylindric set algebra over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040718.png" /> generated by the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040719.png" />-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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040720.png" /> of semantical systems is called a general semantical system if the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040721.png" /> are compatible in the sense that, for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040722.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040723.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040724.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040725.png" /> are isomorphic in the natural sense whenever <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040726.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040727.png" /> have the same cardinality, and, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040728.png" />, then every model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040729.png" /> extends to a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040730.png" /> and every model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040731.png" /> restricts to a model of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040732.png" />. A general semantical system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040733.png" /> is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if each of its component semantical systems <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040734.png" /> has this property.

For every general semantical system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040735.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040736.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040737.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040738.png" /> be a general semantical system. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040739.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040740.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040741.png" /> be disjoint sets of atomic formulas, and let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040742.png" /> be a bijection between <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040743.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040744.png" />. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040745.png" /> be a set of formulas whose atomic formulas are in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040746.png" />. Then:

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040747.png" /> defines <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040748.png" /> explicitly over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040749.png" /> (in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040750.png" />) if for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040751.png" /> there exists a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040752.png" /> such that, for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040753.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040754.png" />.

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040755.png" /> defines <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040756.png" /> implicitly over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040757.png" /> (in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040758.png" />) if for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040759.png" /> and every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040760.png" />,

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040761.png" /></td> </tr></table>

here <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040762.png" /> denotes the set of formulas obtained from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040763.png" /> by replacing each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040764.png" /> by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040765.png" />.

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040766.png" /> is a strong implicit definition of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040767.png" /> over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040768.png" /> (in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040769.png" />) if it defines <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040770.png" /> implicitly over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040771.png" /> and every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040772.png" /> has an extension <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040773.png" />.

<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040774.png" /> has the (weak) Beth definability property if for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040775.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040776.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040777.png" /> as above, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040778.png" /> defines <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040779.png" /> implicitly over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040780.png" /> (in the strong sense), then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040781.png" /> defines <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040782.png" /> explicitly over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040783.png" />. 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040784.png" /> be a class of algebras over the same language type. A homomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040785.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040786.png" />, is called an epimorphism over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040787.png" /> if for any pair of homomorphisms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040788.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040789.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040790.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040791.png" /> be classes of algebras over the same language type. A homomorphism <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040792.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040793.png" />, is said to be <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040795.png" />-extensible over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040796.png" /> if for any <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040797.png" /> and every surjection <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040798.png" /> there is a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040799.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040800.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040801.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040802.png" />.

Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040803.png" /> be a finitely algebraizable generalized semantical system. Then:

I) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040804.png" /> has the Beth definability property if and only if every epimorphism over <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040805.png" /> is surjective;

II) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040806.png" /> has the weak Beth definability property if and only if every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040807.png" />)-extensible epimorphism of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040808.png" /> 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 {{Cite|AnNéSa}}, {{Cite|AnKuNéSa}}, {{Cite|AnNé}}. For the results on definability, see {{Cite|Ho}} and {{Cite|Ho2}}.

====References====
{|
|-
|valign="top"|{{Ref|AnBe}}||valign="top"|  A.R. Anderson,   N.D. Belnap,   "Entailment. The logic of relevance and necessity", '''I''', Princeton Univ. Press  (1975)
|-
|valign="top"|{{Ref|AnKuNéSa}}||valign="top"|  H. Andréka,   A. Kurucz,   I. Németi,   I. Sain,   "Applying algebraic logic: A general methodology", ''Proc. Summer School of Algebraic Logic'', Kluwer Acad. Publ.  (to appear)  (Short version in:  {{Cite|AnNéSa}})
|-
|valign="top"|{{Ref|AnNé}}||valign="top"|  H. Andréka,   I. Németi,   "General algebraic logic: A perspective on ``what is logic''"  D. Gabbay (ed.), ''What is a logical system?'', Clarendon Press  (1994)  pp. 485–569
|-
|valign="top"|{{Ref|AnNéSa}}||valign="top"|  H. Andréka,   I. Németi,   I. Sain,   "Applying algebraic logic to logic"  M. Nivat (ed.)  et al. (ed.), ''Algebraic Methodology and Software Techn. (AMAST'93, Proc. 3rd Internat. Conf. Algebraic Methodology and Software Techn.), Workshops in Computing'', Springer  (1994)  pp. 3–26
|-
|valign="top"|{{Ref|BlPi}}||valign="top"|  W.J. Blok,   D. Pigozzi,   "Abstract algebraic logic and the deduction theorem"  ''Bull. Symbolic Logic''  (to appear)
|-
|valign="top"|{{Ref|BlPi2}}||valign="top"|  W.J. Blok,   D. Pigozzi,   "Algebraizable logics", ''Memoirs'', '''396''', Amer. Math. Soc.  (1989)
|-
|valign="top"|{{Ref|BlPi3}}||valign="top"|  W.J. Blok,   D. Pigozzi,   "Protoalgebraic logics"  ''Studia Logica'', '''45'''  (1986)  pp. 337–369
|-
|valign="top"|{{Ref|BlPi4}}||valign="top"|  W.J. Blok,   D. Pigozzi,   "Algebraic semantics for universal Horn logic without equality"  A. Romanowska (ed.)  J.D.H. Smith (ed.), ''Universal Algebra and Quasigroup Theory'', Heldermann  (1992)  pp. 1–56
|-
|valign="top"|{{Ref|BlPi5}}||valign="top"|  W.J. Blok,   D. Pigozzi,   "Local deduction theorems in algebraic logic"  H. Andréka (ed.)  J.D. Monk (ed.)  I. Németi (ed.), ''Algebraic Logic (Proc. Conf. Budapest 1988)'', ''Colloq. Math. Soc. J. Bolyai'', '''54''', North-Holland  (1991)  pp. 75–109
|-
|valign="top"|{{Ref|BlSu}}||valign="top"|  S.L. Bloom,   R. Suszko,   "Investigations into the sentential logic with identity"  ''Notre Dame J. Formal Logic'', '''13'''  (1972)  pp. 289–308
|-
|valign="top"|{{Ref|ChTa}}||valign="top"|  L.H. Chin,   A. Tarski,   "Distributive and modular laws in relation algebras"  ''Univ. California Publ. Math. New Ser.'', '''1''' :  9  (1951)  pp. 341–384
|-
|valign="top"|{{Ref|Cz}}||valign="top"|  J. Czelakowski,   "Algebraic aspects of deduction theorems"  ''Studia Logica'', '''44'''  (1985)  pp. 369–387
|-
|valign="top"|{{Ref|Cz2}}||valign="top"|  J. Czelakowski,   "Protoalgebraic logics", ''Trends in Logic—Studia Logica Libr.'', '''10''', Kluwer Acad. Publ.  (2001)
|-
|valign="top"|{{Ref|Cz3}}||valign="top"|  J. Czelakowski,   "Equivalential logics I—II"  ''Studia Logica'', '''40'''  (1981)  pp. 227–236; 355–372
|-
|valign="top"|{{Ref|Cz4}}||valign="top"|  J. Czelakowski,   "Consequence operations: Foundational studies"  ''Techn. Rept. Inst. Philosophy and Sociology Polish Acad. Sci.''  (1992)
|-
|valign="top"|{{Ref|Cz5}}||valign="top"|  J. Czelakowski,   "Filter-distributive logics"  ''Studia Logica'', '''43'''  (1984)  pp. 353–377
|-
|valign="top"|{{Ref|CzJa}}||valign="top"|  J. Czelakowski,   R. Jansana,   "Weakly algebraizable logics"  ''J. Symbolic Logic'', '''65'''  (2000)  pp. 641–668
|-
|valign="top"|{{Ref|DeJa}}||valign="top"|  P. Dellunde,   R. Jansana,   "Some characterization theorems for infinitary universal horn logic without equality"  ''J. Symbolic Logic'', '''61'''  (1996)  pp. 1242–1260
|-
|valign="top"|{{Ref|El}}||valign="top"|  R. Elgueta,   "Subdirect representation theory for classes without equality"  ''Algebra Univ.'', '''40'''  (1998)  pp. 201–246
|-
|valign="top"|{{Ref|El2}}||valign="top"|  R. Elgueta,   "Characterizing classes defined without equality"  ''Studia Logica'', '''58'''  (1997)  pp. 357–394
|-
|valign="top"|{{Ref|FoJa}}||valign="top"|  J.M. Font,   R. Jansana,   "A general algebraic semantics for sentential logics", ''Lecture Notes in Logic'', '''7''', Springer  (1996)
|-
|valign="top"|{{Ref|Ha}}||valign="top"|  P.R. Halmos,   "Algebraic logic I: Monadic Boolean algebras"  ''Compositio Math.'', '''12'''  (1955)  pp. 217–249
|-
|valign="top"|{{Ref|He}}||valign="top"|  B. Herrmann,   "Characterizing equivalential and algebraizable logics"  ''Studia Logica'', '''58'''  (1997)  pp. 305–323
|-
|valign="top"|{{Ref|He2}}||valign="top"|  B. Herrmann,   "Equivalential and algebraizable logics"  ''Studia Logica'', '''57'''  (1996)  pp. 419–436
|-
|valign="top"|{{Ref|HeMoTa}}||valign="top"|  L. Henkin,   J.D. Monk,   A. Tarski,   "Cylindric algebras, Parts I—II", North-Holland  (1971/85)
|-
|valign="top"|{{Ref|Ho}}||valign="top"|  E. Hoogland,   "Algebraic characterization of various Beth definability properties"  ''Studia Logica'', '''65'''  (2000)  pp. 91–112
|-
|valign="top"|{{Ref|Ho2}}||valign="top"|  E. Hoogland,   "Definability and interpolation. Model-theoretic investigations", ''ILLC Dissert. Ser. DS-2001-05'', Inst. Language, Logic and Computation, Amsterdam  (2001)
|-
|valign="top"|{{Ref|Ło}}||valign="top"|  J. Łoś,   "O matrycach logicznych"  ''Ser. B. Travaux de la Soc. Sci. et des Lettres de Wrocław'', '''19'''  (1949)
|-
|valign="top"|{{Ref|Ma}}||valign="top"|  J. Malinowski,   "The deduction theorem for quantum logic—some negative results"  ''J. Symbolic Logic'', '''55'''  (1990)  pp. 615–625
|-
|valign="top"|{{Ref|Pa}}||valign="top"|  K. Pałasińska,   "Deductive systems and finite axiomatizability properties"  ''PhD Thesis Iowa State Univ.''  (1994)
|-
|valign="top"|{{Ref|Ra}}||valign="top"|  H. Rasiowa,   "An algebraic approach to non-classical logics", North-Holland  (1974)
|-
|valign="top"|{{Ref|ReVe}}||valign="top"|  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)
|-
|valign="top"|{{Ref|Sm}}||valign="top"|  T. Smiley,   "The independence of connectives"  ''J. Symbolic Logic'', '''27'''  (1962)  pp. 426–436
|-
|valign="top"|{{Ref|Su}}||valign="top"|  R. Suszko,   "Abolition of the Fregean axiom", ''Logic Colloquium (Boston 1972/3)'', ''Lecture Notes in Mathematics'', '''453''', Springer  (1975)  pp. 169–236
|-
|valign="top"|{{Ref|Su2}}||valign="top"|  S.J. Surma,   "On the origin and subsequent applications of the concept of the Lindenbaum algebra", ''Logic, Methodology and Philosophy of Science VI (Hannover 1979)'', North-Holland  (1982)  pp. 719–734
|-
|valign="top"|{{Ref|Ta}}||valign="top"|  A. Tarski,   "Über einige fundamentale Begriffe der Metamathematik"  ''C.R. Soc. Sci. Lettr. Varsovie Cl. III'', '''23'''  (1930)  pp. 22–29
|-
|valign="top"|{{Ref|Ta2}}||valign="top"|  A. Tarski,   "Grundzüge der Systemenkalküls. Erster Teil"  ''Fundam. Math.'', '''25'''  (1935)  pp. 503–526
|-
|valign="top"|{{Ref|Wó}}||valign="top"|  R. Wójcicki,   "Theory of logical calculi. Basic theory of consequence operations", ''Synthese Library'', '''199''', Reidel  (1988)
|-
|}