Namespaces
Variants
Actions

Difference between revisions of "Abstract algebraic logic"

From Encyclopedia of Mathematics
Jump to: navigation, search
m (link)
m (AUTOMATIC EDIT (latexlist): Replaced 791 formulas out of 802 by TEX code with an average confidence of 2.0 and a minimal confidence of 2.0.)
Line 1: Line 1:
 +
<!--This article has been texified automatically. Since there was no Nroff source code for this article,
 +
the semi-automatic procedure described at https://encyclopediaofmath.org/wiki/User:Maximilian_Janisch/latexlist
 +
was used.
 +
If the TeX and formula formatting is correct, please remove this message and the {{TEX|semi-auto}} category.
 +
 +
Out of 802 formulas, 791 were replaced by TEX code.-->
 +
 +
{{TEX|semi-auto}}{{TEX|partial}}
 
{{TEX|want}}
 
{{TEX|want}}
 
{{MSC|03|03G27}}
 
{{MSC|03|03G27}}
Line 8: Line 16:
 
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.
 
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" />,
+
By a language type one means a set $\Lambda$ 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 $\operatorname {Fm}$ of formulas (terms in an algebraic context) is constructed from the connectives and a fixed, denumerable set of (formula) variable symbols in the usual way. The corresponding formula algebra is denoted by $\textbf{Fm}$. This is the  "absolutely free"  algebra of type $\Lambda$ with an $n$-ary operation $\lambda ^ { \operatorname{Fm} } : \operatorname{Fm} ^ { n } \rightarrow \operatorname{Fm}$ for each $\lambda \in \Lambda$ of arity $n$ such that $\lambda ^ { \mathbf{Fm} } ( \varphi_0 , \dots , \varphi _ { n  - 1} )$ is the formula $\lambda \varphi_{0} , \ldots , \varphi _ { n  - 1}$, in prefix notation, or $( \varphi _ { 0 } \lambda \varphi _ { 1 } )$ when $n = 2$ and infix notation is used. The operation of simultaneously substituting fixed but arbitrary formulas for variables is identified with the unique endomorphism of $\textbf{Fm}$ it determines. A logistic or deductive system is a pair $\mathcal{D} = \{ \mathbf{Fm} , \vdash _ { \mathcal{D} } )$, where $\vdash _ { \mathcal{D} }$, the consequence relation of $\mathcal{D}$, is a binary relation between sets of formulas and individual formulas satisfying the following well-known conditions: For all $\Gamma , \Delta \subseteq \operatorname{Fm}$ and $\varphi \in \operatorname {Fm}$,
  
<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" />;
+
$\Gamma \vdash_{\mathcal{D}} \varphi$ for all $\varphi \in \Gamma$;
  
<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" />;
+
$\Gamma \vdash_{\mathcal{D}} \varphi$ and $\Delta \vdash _ {\cal D } \psi$ for every $\psi \in \Gamma$ imply $\Delta \vdash_{\cal D} \varphi$;
  
<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);
+
$\Gamma \vdash_{\mathcal{D}} \varphi$ implies $\Gamma ^ { \prime } \vdash_{\mathcal{D}} \varphi$ for some finite $\Gamma ^ { \prime } \subseteq \Gamma$ (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]].
+
$\Gamma \vdash_{\mathcal{D}} \varphi$ implies $\sigma ( \Gamma ) \vdash_{\mathcal{D}} \sigma ( \varphi )$ for every substitution $\sigma$ (substitution invariance). Substitution invariance is the technical counterpart of the idea that logical consequence depends on form and not substance. It plays a key role in abstract algebraic logic because it is an essential feature of [[Equational logic|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" />.
+
A formula $\varphi$ is a theorem of $\mathcal{D}$ if $\vdash_{\mathcal{D}} \varphi$ (i.e., it is a consequence of the empty set of formulas). The set of theorems, which may be empty, is denoted by $\operatorname{Thm} \mathcal{D}$. A set $T$ of formulas is a theory of a deductive system $\mathcal{D}$ if it is closed under consequence, i.e., $\varphi \in T$ whenever $\Gamma \subset T$ and $\Gamma \vdash_{\mathcal{D}} \varphi$. $\operatorname{Thm} \mathcal{D}$ is the smallest theory. The set of all theories of $\mathcal{D}$ is denoted by $\operatorname { Th } \cal D$. The theory axiomatized by an arbitrary set $\Gamma$ of formulas is the set of all formulas $\varphi$ such that $\Gamma \vdash_{\mathcal{D}} \varphi$.
  
Deductive systems in this sense include all the familiar sentential logics (cf. also [[Propositional calculus|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.
+
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 $\operatorname{CPC}$ and $\text{IPC}$, the intermediate logics (cf. also [[Intermediate logic|Intermediate logic]]), the various modal logics, including $\mathbf{S} 4$ and $\text{S}5$ (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.
+
A (logical) matrix is a structure of the form $\mathfrak { A } = \langle \text{A} , F \rangle$, where $\mathbf{A}$ is an algebra (of the same language type as $\mathcal{D}$), the underlying algebra of $\frak A$, and $F \subseteq A$, the designated set of $\frak A$. An interpretation of $\mathcal{D}$ is a matrix $\frak A$ together with a homomorphism $h : \mathbf{Fm} \rightarrow \mathbf{A}$ from the algebra of formulas $\textbf{Fm}$ into the underlying algebra of $\frak A$. $h ( \varphi )$ is to be thought of as the  "sense"  or  "meaning"  of the formula $\varphi$ under the interpretation, and $\varphi$ is  "true"  or  "false"  depending on whether or not $h ( \varphi ) \in F$. By the Frege principle, this truth value is the denotation of $\varphi$ under the interpretation. Truth must be preserved under consequence in the sense that, if $\Gamma \vdash_{\mathcal{D}} \varphi$ and each $\psi \in \Gamma$ is true under the interpretation, then $\varphi$ must also be true. A set $\Gamma$ of formulas is said to define a class $\mathsf{K}$ of interpretations if $\mathsf{K}$ is the class of all interpretations in which each formula of $\Gamma$ is true. Because truth is preserved under consequence, the theory axiomatized by $\Gamma$ also defines $\mathsf{K}$; it turns out that it is the unique theory with this property.
  
The formulas <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 formulas $\varphi$ and $\psi$ are equivalent over a given class $\mathsf{K}$ of interpretations (in the Fregean sense) if they have the same truth value, i.e., $h ( \varphi ) \in F$ if and only if $h ( \psi ) \in F$ for each $\{ \mathfrak{A} , h \}$ in $\mathsf{K}$. They are logically equivalent (with respect to $\mathcal{D}$) if they are equivalent over the class of all interpretations.
  
 
The semantical and logistic approaches diverge at this point. In the former attention is restricted to a specific class of interpretations whose peculiar structure may play an important role in the meta-theory. In contrast, in the logistic method every interpretation is considered, and consequently only its representation as an abstract set with operations and a designated subset is significant. Deduction systems treated in this way are sometimes referred to as uninterpreted.
 
The 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.
Line 31: Line 39:
  
 
==Logistic abstract algebraic logic.==
 
==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.
+
The assumption that the deductive system $\mathcal{D}$ is uninterpreted implies that one need consider only those matrices $\frak A$ with the property that $\{ \mathfrak{A} , h \}$ is an interpretation for every $h : \mathbf{Fm} \rightarrow \mathbf{A}$. Such a matrix is called a (matrix) model of $\mathcal{D}$; the class of all models of $\mathcal{D}$ is denoted by $\operatorname {Mod} \mathcal{D}$. Secondly, the properties of a given class of interpretations are for most purposes completely specified by the theory that defines it. So matters can be simplified by considering equivalence of formulas over theories rather than classes of interpretations.
  
Two formulas <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" />.
+
Two formulas $\varphi$ and $\psi$ are equivalent over a theory $T$, or $T$-equivalent, in the Fregean sense, if, for every theory $S$ that extends $T$, $\varphi \in S$ if and only if $\psi \in S$; the binary relation between formulas defined this way is called the Frege relation of $T$ and denoted by $\Lambda _ { \cal D } T$. $\varphi$ and $\psi$ are logically equivalent (with respect to $\mathcal{D}$) if they are equivalent over every theory, or, equivalently, if they are equivalent over $\operatorname{Thm} \mathcal{D}$, the set of theorems. In terms of the consequence relation, $\varphi$ and $\psi$ are logically equivalent over $T$ if and only if $\varphi$ and $\psi$ are each consequences of the other over $T$; symbolically, $\varphi \equiv \psi ( \operatorname { mod } \Lambda _ { \mathcal{D} } T )$ if $T , \varphi \vdash_{\mathcal{D}} \psi$ and $T , \psi \vdash _ {\cal D } \varphi$.
  
If, as in the case of the classical and intuitionistic propositional calculi, <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.
+
If, as in the case of the classical and intuitionistic propositional calculi, $\mathcal{D}$ has a binary implication connective $\rightarrow$ for which the deduction theorem holds, then $\varphi \equiv \psi ( \operatorname { mod } \Lambda _ { \mathcal{D} } T )$ if and only if $\varphi \rightarrow \psi \in T$ and $\psi \rightarrow \varphi \in T$, or equivalently if there is a biconditional, $\varphi \leftrightarrow \psi \in T$. So, under these rather weak conditions on $\mathcal{D}$ logical equivalence in the Fregean sense agrees with the familiar definition of the concept.
  
As a consequence of Frege's principle, the following rule of replacement, or compositionality, holds when <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.
+
As a consequence of Frege's principle, the following rule of replacement, or compositionality, holds when $\mathcal{D}$ is the classical propositional calculus $\operatorname{CPC}$ or the intuitionistic propositional calculus $\text{IPC}$. If in any formula $\varphi$ a subformula $\psi$ is replaced by an equivalent formula $\psi '$, the resulting formula $\varphi ^ { \prime }$ is equivalent to $\varphi$. In algebraic terms this says that for every theory $T$ of $\operatorname{CPC}$ or $\text{IPC}$, $\Lambda _ { \cal D } T$ is a congruence relation on the algebra of formulas $\textbf{Fm}$. A deductive system $\mathcal{D}$ for which $T$-equivalence is compositional for every theory $T$ is called Fregean or extensional; non-Fregean systems are called intensional.
  
If <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" />.
+
If $\mathcal{D}$ 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 $T$ ranges over all theories. These are called the Lindenbaum–Tarski models of $\mathcal{D}$. The construction of the Lindenbaum–Tarski models is more complicated in the case of intensional systems, where the Frege relation is not a congruence relation. For example, for every theory $T$ of the strong form of the modal system $\text{S}5$, with necessitation as a rule of inference (see below), one has $\varphi \equiv \psi ( \operatorname { mod } \Lambda _ { S 5 } T )$ if and only if $T , \varphi \vdash_{\text{S}5} \psi$ and $T , \psi \vdash_{\text{S}5}$ if and only if $\square \varphi \rightarrow \psi \in T$ and $\square \psi \rightarrow \varphi \in T$. But this relation is not, in general, compositional. $\Lambda _ { \operatorname {S5} } T$ includes however a largest compositional equivalence relation, called the Suszko congruence of $T$ over $\text{S}5$ and denoted by $\tilde { \Omega } _ { S 5 } T$. It can be shown that $\varphi \equiv \psi ( \operatorname { mod } \tilde { \Omega } _ { S 5 } T )$ if and only if $\varphi \leftrightarrow \psi \in T$. So $\tilde { \Omega } _ { S 5 } T$ captures the usual notion of $T$-equivalence for $\text{S}5$.
  
Suszko congruences can be defined for the theories of any deductive system, and consequently one can construct Lindenbaum–Tarski models of any deductive system. But it turns out to be more useful to consider the Lindenbaum–Tarski process in a broader context. A subset <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.
+
Suszko congruences can be defined for the theories of any deductive system, and consequently one can construct Lindenbaum–Tarski models of any deductive system. But it turns out to be more useful to consider the Lindenbaum–Tarski process in a broader context. A subset $F$ of the underlying set of an algebra $\mathbf{A}$, of the same language type as $\mathcal{D}$, is called a filter of $\mathcal{D}$ if $\langle {\bf A} , F \rangle$ is a model of $\mathcal{D}$; thus $F$ is a filter if and only if it is closed under consequence in the sense that, if $\Gamma \vdash_{\mathcal{D}} \varphi$, one has $h ( \varphi ) \in F$ for every $h : \mathbf{Fm} \rightarrow \mathbf{A}$ such that $h ( \psi ) \in F$ for every $\psi \in \Gamma$. The set of filters of $\mathcal{D}$ on $\mathbf{A}$ is denoted by $\operatorname{Fi} _ {\cal  D } \bf A$. It is easy to see that the theories are the filters on the formula algebra. The Frege relation and the Suszko congruence generalize to filters on an arbitrary algebra $\mathbf{A}$ in a natural way. The Frege relation $\Lambda _ { \mathcal{D} } F$ is the set of all pairs $\langle a , b \rangle$ of elements of $\mathbf{A}$ such that, for every filter $G$ on $\mathbf{A}$ that includes $F$, $a \in G$ if and only if $b \in G$. The Suszko congruence $\widetilde { \Omega } _ { \mathcal{D} } F$ is the largest congruence relation on $\mathbf{A}$ that is included in $\Lambda _ { \mathcal{D} } F$; it always exists.
  
The quotient matrix <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 quotient matrix $\langle \mathbf{A} / \tilde{\Omega}_{\mathcal{D}} F , F / \tilde{\Omega}_{\mathcal{D}} F \rangle$ is called the Suszko-reduction of $\frak A$ and is denoted by $\mathfrak{A} ^ { *S }$. It can be shown that $\mathfrak{A}^{*S*S}$ coincides with (or, more precisely, is isomorphic to) $\mathfrak{A} ^ { *S }$. A model $\frak A$ is Suszko-reduced if $\mathfrak { A } ^ { *  S} = \mathfrak { A }$, i.e., $\widetilde { \Omega } _ { \mathcal{D} } F$ is the identity relation. The class of all Suszko-reduced models of $\mathcal{D}$ is denoted by $\operatorname{Mod} ^ { * S}  { \mathcal{D} }$. The Suszko-reduced models of $\mathcal{D}$ are those for which two elements are equivalent in the Fregean sense if and only if they are identical.
  
The class of underlying algebras of the Suszko-reduced models of <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.
+
The class of underlying algebras of the Suszko-reduced models of $\mathcal{D}$ is denoted by $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$. The underlying algebras of $\operatorname{CPC}$ are the Boolean algebras. Each filter of $\operatorname{CPC}$ on a Boolean algebra $\mathbf{A}$ is completely determined by its Suszko congruence $\tilde { \Omega  }F$; more precisely, it coincides with the set of all elements of $\mathbf{A}$ equivalent under $\tilde { \Omega  }F$ to the unit element $\top$ of $\mathbf{A}$. Moreover, every congruence relation on $\mathbf{A}$ is the Suszko congruence of a filter of $\operatorname{CPC}$. It follows that the consequence relation of $\operatorname{CPC}$ is completely determined by the equational logic of Boolean algebras, and in this way the class of Boolean algebras <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040210.png"/> constitutes a complete algebraic semantics for $\operatorname{CPC}$. In a similar way, the class of Heyting algebras $\text{Alg Mod}^ { *S } \text{ IPC }$ and the class of so-called monadic algebras $\operatorname{Alg} \operatorname{Mod}^ { *S } \operatorname{S} 5$ constitute complete algebraic semantics for $\text{IPC}$ and $\text{S}5$, respectively, and this is the case for almost all the familiar deductive systems. But in general the connection between the consequence relation of a deductive system $\mathcal{D}$ and the equational logic of $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$ is much weaker. A central problem for abstract algebraic logic is the characterization of those deductive systems for which this connection is as strong as for the traditional logics.
  
 
Early work on the Suszko and the closely related Leibniz and Tarski congruences discussed below can be found in {{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}}.
 
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.===
 
===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.
+
The basis of the abstract algebraic logic definition of an algebraizable deductive system is the notion of bisimulation between the consequence relation of $\mathcal{D}$ and the equational consequence relation of a class of algebras.
  
Let <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
+
Let $\mathcal{D}$ be a deductive system and $\mathsf{K}$ 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>
+
\begin{equation*} E ( x , y ) = \{ \epsilon _ { i } ( x , y ) : i \in I \} \end{equation*}
  
be a (possibly infinite) non-empty system of formulas in two variables. <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" />,
+
be a (possibly infinite) non-empty system of formulas in two variables. $E ( x , y )$ is said to be a faithful interpretation of the equational logic of $\mathsf{K}$ in $\mathcal{D}$ if, for every equation $\varphi \approx \psi$ and every set of equations $\Gamma \approx \Delta$,
  
<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>
+
\begin{equation*} \Gamma \approx \Delta \models _ { \text{K} } \varphi \approx \psi \text { iff } E ( \Gamma , \Delta ) \vdash _ { \mathcal{D} } E ( \varphi , \psi ), \end{equation*}
  
where <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" .
+
where $\Gamma \approx \Delta \vDash _ { \mathsf{K} } \varphi \approx \psi$ means that $\wedge \Gamma \approx \Delta \rightarrow \varphi \approx \psi$ is a quasi-identity of $\mathsf{K}$. Also, $E ( \Gamma , \Delta ) = \{ \epsilon _ { i } ( \gamma , \delta ) : \gamma \approx \delta \in \Gamma \approx \Delta , i \in I \}$ and $E ( \varphi , \psi ) = \{ \epsilon _ { i } ( \varphi , \psi ) : i \in I \}$, and $E ( \Gamma , \Delta ) \vdash _ {\cal D } E ( \varphi , \psi )$ is shorthand for the system of entailments $E ( \Gamma , \Delta ) \vdash _ {\cal  D } \epsilon _ { i } ( \varphi , \psi )$ for every $i \in I$;  "iff"  stands for  "if and only if" .
  
 
Let
 
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>
+
\begin{equation*} K ( x ) \approx L ( x ) = \{ \kappa _ { j } ( x ) \approx \lambda _ { j } ( x ) : j \in J \} \end{equation*}
  
be a non-empty system of equations in one variable. <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" />,
+
be a non-empty system of equations in one variable. $K ( x ) \approx L ( x )$ is a faithful interpretation of $\mathcal{D}$ in the equational logic of $\mathsf{K}$ if, for all $\Gamma \cup \{ \varphi \} \subseteq \text{Fm}$,
  
<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>
+
\begin{equation*} \Gamma \vdash _ { \mathcal{D} } \varphi \text { iff } K ( \Gamma ) \approx L ( \Gamma ) \vDash _ { \text{K} } K ( \varphi ) \approx L ( \varphi ), \end{equation*}
  
where <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
+
where $K ( \Gamma ) \approx L ( \Gamma ) = \{ \kappa _ { j } ( \psi ) \approx \lambda _ { j } ( \psi ) : \psi \in \Gamma , j \in J \}$ and $K ( \varphi ) \approx L ( \varphi ) = \{ \kappa _ { j } ( \varphi ) \approx \lambda _ { j } ( \varphi ) : j \in J \}$. The two interpretations are mutual inverses if
  
<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>
+
\begin{equation*} x \dashv \vdash_{\mathcal{D}} E ( K ( x ) , L ( x ) ) \end{equation*}
  
 
and
 
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>
+
<table class="eq" style="width:100%;"> <tr><td style="width:94%;text-align:center;" valign="top"><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]])
+
A pair of mutually invertible interpretations $E ( x , y )$ and $K ( x ) \approx L ( x )$ such as these is called a bisimulation between $\mathcal{D}$ and the equational logic of $\mathsf{K}$. A deductive system $\mathcal{D}$ is algebraizable if there is a bisimulation between $\mathcal{D}$ and the equational logic of some class $\mathsf{K}$ of algebras; it is finitely algebraizable if the interpretations are finite. If $\mathcal{D}$ is algebraizable, then $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$ is the largest class $\mathsf{K}$ with the above properties; it is called the equivalent algebraic semantics of $\mathcal{D}$. In general, $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$ is not elementary (i.e., definable by a set of sentences of the first-order predicate logic), and in fact it is an elementary class just in case $\mathcal{D}$ is finitely algebraizable. In this case $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$ is a quasi-variety (cf. also [[Quasi-variety|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 classical and intuitionistic propositional calculi $\operatorname{CPC}$ and $\text{IPC}$ are finitely algebraizable and their equivalent quasi-varieties are, respectively, the varieties $\textsf{BA}$ of Boolean algebras and $\mathbf{\dashv} \mathsf{A}$ of Heyting algebras. In both cases the faithful interpretation of the equational logic of the equivalent quasi-variety in the deductive system is given by $E ( x , y ) = \{ x \leftrightarrow y \}$, where $\leftrightarrow$ is, respectively, the classical and intuitionistic biconditional, and the inverse faithful interpretation is $K ( x ) \approx L ( x ) = \{ x \approx T \}$. Most of the deductive systems of traditional algebraic logic are finitely algebraizable with similar interpretations. However, there are finitely algebraizable logics with non-standard interpretations, for example the entailment logic $E$.
  
The bisimulation between a finitely algebraizable deductive system <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:
+
The bisimulation between a finitely algebraizable deductive system $\mathcal{D}$ and the equational logic of its equivalent quasi-variety $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$ induces a correspondence between the meta-logical properties of $\mathcal{D}$ and the algebraic properties of $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$. This correspondence has been the focus of considerable attention in abstract algebraic logic. One of the most important aspects of traditional algebraic logic is the way in which it can be used to reformulate meta-logical properties of a particular logical system in algebraic terms. Abstract algebraic logic provides a framework for studying such correspondences in a general context. Known meta-logical or algebraic results can then be applied to obtain new results in the other domain. Some correspondences of this kind that have been established are between:
  
meta-logical interpolation and algebraic amalgamation, e.g., the Craig interpolation theorem of <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" />;
+
meta-logical interpolation and algebraic amalgamation, e.g., the Craig interpolation theorem of $\operatorname{CPC}$ and the amalgamation property of $\textsf{BA}$;
  
 
definability (in the sense of the [[Beth definability theorem]] of first-order predicate logic) and the property that every epimorphism (in the categorical sense) is surjective;
 
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.
+
the deduction theorem and the equational definability of principal congruences. The deduction theorem is the formal expression of one of the most important and useful properties of classical logic: to prove that an implication holds between propositions it suffices to give a proof of the conclusion on the basis of the assumption of the antecedent. It is such a familiar part of ordinary logical argumentation that it is hardly recognizable as being something whose use might be problematic. But in fact it is not part of the usual formalizations of $\operatorname{CPC}$ and must be proved as a meta-theorem. Moreover, while the deduction theorem remains valid for intuitionistic logic, it is known to fail in other important logics, for instance, certain systems of modal logic. It turns out that there is a close connection between the deduction theorem and the universal algebraic notion of definable principal congruence relations. The development of abstract algebraic logic was motivated in part by a desire to provide the proper context in which to formalize this connection precisely. The ultimate goal was to be able to apply the extensive work on the definability of principal congruence relations in [[Universal algebra|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" />:
+
Let $\mathcal{D}$ be a deductive system. A finite non-empty set $\Delta ( x , y ) = \{ \delta _ { 0 } ( x , y ) , \ldots , \delta _ { m - 1 } ( x , y ) \}$ of binary formulas is called a deduction-detachment system for $\mathcal{D}$ if the following equivalence holds for all $\Gamma \cup \{ \varphi , \psi \} \subseteq \operatorname{Fm}$:
  
<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>
+
\begin{equation*} \Gamma , \varphi \vdash_{\mathcal{D}} \psi \end{equation*}
  
<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>
+
\begin{equation*} \text{iff } \Gamma \vdash _ {\cal D } \Delta ( \varphi , \psi ). \end{equation*}
  
A deductive system has the deduction-detachment theorem if it has a deduction-detachment system. The implication <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" />.
+
A deductive system has the deduction-detachment theorem if it has a deduction-detachment system. The implication $x \rightarrow y$ forms a singleton deduction-detachment system for $\operatorname{CPC}$ and $\text{IPC}$, while the formula $\square x \rightarrow y$ forms a singleton deduction-detachment system for the modal systems $\mathbf{S} 4$ and $\text{S}5$.
  
For an algebra <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" />,
+
For an algebra $\mathbf{A}$, let $\operatorname{Co}\mathbf{A}$ be the set of all congruences of $\mathbf{A}$. If $\mathsf{Q}$ is a quasi-variety, then a congruence $\Theta$ on an arbitrary algebra $\mathbf{A}$ (not necessarily in $\mathsf{Q}$) is called a $\mathsf{Q}$-congruence if $\mathbf{A} / \Theta \in \mathsf{Q}$. If $\mathsf{Q}$ is a variety (cf. also [[Algebraic systems, variety of|Algebraic systems, variety of]]) and $\bf A \in \mathsf{Q}$, then every congruence is a $\mathsf{Q}$-congruence. The principal $\mathsf{Q}$-congruence generated by the pair $a$ and $b$, $\Theta_{ \mathsf{Q} } ( a , b )$, is the smallest $\mathsf{Q}$-congruence that identifies $a$ and $b$. A quasi-variety $\mathsf{Q}$ has equationally definable principal relative congruences (EDPRC) if there is a finite system of equations $\epsilon_{ 0,0} ( x , y , z , w ) \approx \epsilon_{ 0,1} ( x , y , z , w ) , \ldots , \epsilon _ { m - 1,0 } ( x , y , z , w ) \approx \epsilon _ { m - 1  , 1} ( x , y , z , w )$, in four variables, such that, for every $\bf A \in \mathsf{Q}$ and all $a , b , c , d \in A$,
  
<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>
+
\begin{equation*} c \equiv d ( \Theta _ { \text{Q} } ( a , b ) ) \end{equation*}
  
<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>
+
\begin{equation*} \text{iff }\epsilon _ { i,0 } ^ { \mathbf{A} } ( a , b , c , d ) = \epsilon _ { i , 1 } ^ { \mathbf{A} } ( a , b , c , d ) \text { for all } i &lt; m, \end{equation*}
  
<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" />.
+
$\epsilon _ { i , j } ^ { \mathbf{A} } ( a , b , c , d ) = h ( \epsilon _ { i , j } ( x , y , z , w ) )$, where $h : \mathbf{Fm} \rightarrow \mathbf{A}$ is any homomorphism such that $h ( x ) = a , \ldots , h ( w ) = d$.
  
<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.
+
$\mathsf{Q}$-congruence generation in the formula algebra can be interpreted as the consequence relation of the equational logic of $\mathsf{Q}$. Thus, if $\mathsf{Q}$ has EDPRC, the defining equations $\epsilon _ { i , 0 } ( x , y , z , w ) \approx \epsilon _ { i , 1 } ( x , y , z , w )$ can be interpreted collectively as an implication connective for the equational logic. This observation is reflected in the following theorem: Let $\mathcal{D}$ be a finitely algebraizable deductive system and let $\mathsf{Q} = \operatorname { Alg } \operatorname { Mod } ^ { * S } \mathcal{D}$ be its equivalent quasi-variety. Then $\mathcal{D}$ has the deduction-detachment theorem if and only if $\mathsf{Q}$ has EDPRC.
  
A correspondence of this kind makes it possible to infer new metalogical properties from known algebraic ones and vice versa. In this way it can be proved that orthomodular logic does not have the deduction-detachment theorem. Orthomodular logic can be viewed as a finitely algebraizable deductive system whose equivalent quasi-variety is the variety of orthomodular lattices. There are several different deductive systems that fit this description. It can be shown that, if a quasi-variety <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 correspondence of this kind makes it possible to infer new metalogical properties from known algebraic ones and vice versa. In this way it can be proved that orthomodular logic does not have the deduction-detachment theorem. Orthomodular logic can be viewed as a finitely algebraizable deductive system whose equivalent quasi-variety is the variety of orthomodular lattices. There are several different deductive systems that fit this description. It can be shown that, if a quasi-variety $\mathsf{Q}$ has EDPRC, then it has the relative congruence extension property. The variety of orthomodular lattices does not have this property. Thus, no orthomodular logic of the kind described above can have the deduction-detachment theorem with respect to any system of binary formulas.
  
 
A definition of an abstract class of deductive systems with the algebraic properties of the traditional logics was first proposed in {{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}}.
 
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.===
 
===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.
+
Finitely algebraizable deductive systems exhibit the strongest connection between the meta-logical properties of $\mathcal{D}$ and the algebraic properties of $\operatorname {Alg} \operatorname {Mod} ^ { * S}  { \cal D }$. But there are deductive systems where the connection is not as strong but which still have a clear algebraic character. One of the goals of abstract algebraic logic is the classification of deductive systems of this kind. This leads to a hierarchy of systems with the finitely algebraizable systems at the top. There are several ways of specifying it. The most natural, in view of the definition of algebraizability, is in terms of progressively weaker notions of bisimulation. The characteristic property of all deductive systems that make up the hierarchy is that equivalence, as expressed by the Suszko congruence, is explicitly definable in some way. The classification of the hierarchy is based on the nature of the definition.
  
Let <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
+
Let $E ( x , y ) = \{ \epsilon _ { i } ( x , y ) : i \in I \}$ be a (possibly infinite) set of formulas in two variables. $E ( x , y )$ is a proto-equivalence system for a deductive system $\mathcal{D}$ if
  
<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>
+
\begin{equation*} \vdash_{\mathcal{D}} E ( x , x ) \text { and } x ,\, E ( x , y )\vdash_{\mathcal{D}} y \end{equation*}
  
(<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040333.png" />-detachment).
+
($E$-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
+
A non-empty proto-equivalence system $E ( x , y )$ 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>
+
\begin{equation*} E ( x , y ) \vdash _ { \mathcal{D} } E ( y , x ) , \quad E ( x , y ) , E ( y , z ) \vdash _ { \mathcal{D} } E ( x , z ), \end{equation*}
  
 
and
 
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>
+
\begin{equation*} E ( x _ { 0 } , y _ { 0 } ) , \ldots , E ( x _ { n  - 1} , y _ { n  - 1} ) \vdash_ { \mathcal{D} } \end{equation*}
  
<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>
+
\begin{equation*} \vdash_\mathcal{D} E ( \lambda x _ { 0 } , \ldots , x _ { n  - 1} , \lambda y 0 , \ldots , y _ { n  - 1} ) \end{equation*}
  
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.
+
for all $\lambda \in \Lambda$ ($n$ is the rank of $\lambda$). The reflexivity and transitivity axioms are superfluous as they are provable from the remaining conditions.
  
The connection between equivalence systems and the Suszko congruence is expressed in the following theorem: A non-empty system <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" />,
+
The connection between equivalence systems and the Suszko congruence is expressed in the following theorem: A non-empty system $E ( x , y )$ of formulas in two variables is an equivalence system for a deductive system $\mathcal{D}$ if and only if it defines Suszko congruences in the sense that, for every algebra $\mathbf{A}$ and $F \in \operatorname{Fi} _ {\cal D } \bf A$,
  
<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>
+
\begin{equation*} \widetilde { \Omega } _ { \mathcal{D} } F = \end{equation*}
  
<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>
+
\begin{equation*} = \{ \langle a , b \rangle \in A ^ { 2 } : \epsilon ^ { \mathbf{A} } ( a , b ) \in F \text {  for all } \epsilon ( x , y ) \in E ( x , y ) \}. \end{equation*}
  
 
A deductive system is protoalgebraic if it has a proto-equivalence system. Every proto-equivalence system includes a finite subset that is also a proto-equivalence system. A deductive system is (finitely) equivalential if it has a (finite) equivalence system.
 
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" />.
+
The formulas that faithfully interpret in a (finitely) algebraizable deductive system the equational logic of its equivalent algebraic semantics form a (finite) equivalence system. This leads to a meta-logical characterization theorem of (finitely) algebraizable deductive systems that is intrinsic in the sense that it does not require a priori knowledge of the equivalent algebraic semantics: A deductive system is (finitely) algebraizable if and only if it has a (finite) equivalence system for which there exists a finite system $K ( x ) \approx L ( x )$ of equations in one variable, called a system of defining equations, such that $x \dashv \vdash_{\mathcal{D}} E ( K ( x ) , L ( x ) )$.
  
This last condition abstracts an important property of the biconditional <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.
+
This last condition abstracts an important property of the biconditional $\leftrightarrow$ of both classical and intuitionistic propositional logic, namely, that $x$ and the biconditional $x \leftrightarrow \top $ are interderivable.
  
The protoalgebraic, (finitely) equivalential and (finitely) algebraizable deductive systems constitute, along with the weakly algebraizable systems discussed shortly, the algebraic hierarchy. Natural deductive systems can be found to separate all levels of the hierarchy. Protoalgebraicity is a very weak condition and almost all known deductive systems have the property. There are some that do not however, for example the conjunction/disjunction fragment of <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.
+
The protoalgebraic, (finitely) equivalential and (finitely) algebraizable deductive systems constitute, along with the weakly algebraizable systems discussed shortly, the algebraic hierarchy. Natural deductive systems can be found to separate all levels of the hierarchy. Protoalgebraicity is a very weak condition and almost all known deductive systems have the property. There are some that do not however, for example the conjunction/disjunction fragment of $\operatorname{CPC}$, subintuitionistic logics and Belnap's logic. Almost all the weak modal logics, without necessitation as a rule of inference, are protoalgebraic but not equivalential. There are also examples of algebraizable logics that are not finitely equivalential, and hence also of logics that are equivalential but not finitely equivalential.
  
 
In addition to the syntactical characterizations considered above, each level of the hierarchy can be characterized by both algebraic and model-theoretic means. The algebraic characterization makes use of the Leibniz congruence, a more primitive but more manageable variant of the Suszko congruence.
 
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" />,
+
Given any algebra $\mathbf{A}$ and any subset $F$ of $A$, there is a largest congruence relation $\Omega F$ on $\mathbf{A}$ compatible with $F$ in the sense that $F$ is a union of equivalence classes of $\Omega F$. $\Omega F$ is called the Leibniz congruence of $F$. The relationship between the Leibniz and Suszko congruences is straightforward: For every deductive system $\mathcal{D}$ and $F \in \operatorname{Fi} _ {\cal D } \bf A$,
  
<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>
+
\begin{equation*} \widetilde { \Omega } _ { \mathcal{D} } F = \bigcap \{ \Omega G : F \subseteq G \in  \operatorname{Fi} _ { \mathcal{D} } \mathbf{A} \}. \end{equation*}
  
<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" />.
+
$\Omega$ and $\tilde { \Omega }$ can both be viewed as operators mapping the lattice of $\mathcal{D}$-filters of $\mathbf{A}$ to the lattice of congruences of $\mathbf{A}$. Note that the Leibniz and Suszko congruences coincide on $\mathcal{D}$-filters just in case the Leibniz operator is order-preserving, i.e., $F \subseteq G$ implies $\Omega F \subseteq \Omega G$ for all $F , G \in \operatorname {Fi} _ { \mathcal{D} } \mathbf{A}$.
  
Let <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:
+
Let $\mathcal{D}$ 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;
+
i) $\mathcal{D}$ is protoalgebraic if and only if the Leibniz operator $\Omega$ is order-preserving, i.e., if and only if the Leibniz and Suszko congruences coincide;
  
ii) <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" />;
+
ii) $\mathcal{D}$ is equivalential if and only if it is protoalgebraic and $\Omega$ commutes with inverse homomorphic images; more precisely, $\Omega h ^ { - 1 } ( F ) = h ^ { - 1 } ( \Omega F )$ for every homomorphism $h : \mathbf{A} \rightarrow \mathbf{B}$ and every $F \in \text{Fi} _ { \mathcal{D} }\mathbf{B}$;
  
iii) <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;
+
iii) $\mathcal{D}$ is finitely equivalential if and only if it is protoalgebraic and $\Omega$ commutes with directed unions; more precisely, $\Omega \cup {\cal F} = \cup _ { F \in {\cal F} } \Omega F$ for every $\mathcal{F} \subseteq \operatorname{Fi} _ { \mathcal{D} } \mathbf{A}$ that is upward-directed by inclusion;
  
iv) <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;
+
iv) $\mathcal{D}$ is algebraizable if and only if it is equivalential and $\Omega$ 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.
+
v) $\mathcal{D}$ is finitely algebraizable if and only if it is finitely equivalential and $\Omega$ 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.
+
A deductive system $\mathcal{D}$ is said to be weakly algebraizable if it is protoalgebraic and the Leibniz operator $\Omega$ is injective. A syntactical characterization of weak algebraizability is also known.
  
Calculation of the Leibniz congruences can be a practical matter for some small algebras. This gives a way of verifying that a deductive system is not finitely algebraizable, or that a quasi-variety is not the equivalent algebraic semantics of any deductive system. This method has been used to show that the relevance logic <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.
+
Calculation of the Leibniz congruences can be a practical matter for some small algebras. This gives a way of verifying that a deductive system is not finitely algebraizable, or that a quasi-variety is not the equivalent algebraic semantics of any deductive system. This method has been used to show that the relevance logic $R$ and the various formalizations of modal logic without the rule of necessitation are not finitely algebraizable. It has also been used to show that the variety of complemented distributive lattices is not the equivalent algebraic semantics of any deductive system.
  
 
There is also a model-theoretic characterization of the algebraic hierarchy similar to the well-known model-theoretic characterizations of equational and quasi-equational classes by G. Birkhoff and A. Mal'cev.
 
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" />.
+
The Leibniz-reduction of a model of a deductive system is defined just like the Suszko-reduction, except that the Leibniz congruence is used in place of the Suszko congruence. $\operatorname { Mod } ^ { * \text{L}}  {\cal D }$ denotes the class of all Leibniz-reduced models of $\mathcal{D}$. If $\mathcal{D}$ is protoalgebraic, then $\operatorname { Mod } ^ { *  S} \mathcal{D}= \operatorname { Mod } ^ { *  \text{L}} \mathcal{ D }$; this equality in fact characterizes protoalgebraic systems. In general, the best one has is that $\operatorname{Mod} ^ { * S}  { \mathcal{D} }$ coincides with the class of all matrices isomorphic to a subdirect product of matrices in $\operatorname { Mod } ^ { * \text{L}}  {\cal D }$, in symbols $\operatorname{Mod} ^ { *  S}  \mathcal{D}  = \mathbf{P} _ { \text{SD} } \operatorname{Mod}  ^ { *\text{L}}  \mathcal{D} $.
  
For any class <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" />.
+
For any class $\mathsf{K}$ of matrices, $\mathbf{S}\mathsf{K}$, $\textsf{PK}$, ${\bf P} _ { \text{SD} } \mathsf{K}$, and ${\bf P} _ { \text{U} } \mathsf{K}$ denote, respectively, the classes of isomorphic images of submatrices, direct products, subdirect products, and ultraproducts of members of $\mathsf{K}$.
  
Let <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:
+
Let $\mathcal{D}$ 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" />;
+
a) $\mathcal{D}$ is protoalgebraic if and only if $\operatorname{Mod} ^ { *  \text{L}} \mathcal{D} = \mathbf{P} _ { \text{SD} } \operatorname{Mod} ^ { *  \text{L}} \mathcal{D}$, i.e., $Mod ^ { * \operatorname{L}}  \mathcal{D} = Mod ^ { * S}  \mathcal{ D }$;
  
b) <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" />;
+
b) $\mathcal{D}$ is equivalential if and only if $\operatorname{Mod} ^ { * \text{ L}} \mathcal{D} = \mathbf{SP} \operatorname{Mod} ^ { * \text{ L}} \mathcal{D}$;
  
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;
+
c) $\mathcal{D}$ is finitely equivalential if and only if $\operatorname{Mod} ^ { * \text{L}}  \mathcal{D} = \mathbf{SPP} _ { \text{U} } \operatorname{Mod} ^ { * \text{L}}  \mathcal{D} $, i.e., $\operatorname { Mod } ^ { * \text{L}}  {\cal D }$ is a quasi-variety in the sense of Mal'cev;
  
d) <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" />;
+
d) $\mathcal{D}$ is algebraizable if and only if it is equivalential and $F$ is the minimal $\mathcal{D}$-filter of $\mathbf{A}$ for each $\langle \mathbf{A} , F \rangle \in \operatorname{Mod} ^ { *  \text{L}} \mathcal{D}$;
  
e) <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" />.
+
e) $\mathcal{D}$ is finitely algebraizable if and only if it is finitely equivalential and $F$ is the minimal $\mathcal{D}$-filter of $\mathbf{A}$ for each $\langle \mathbf{A} , F \rangle \in \operatorname{Mod} ^ { *  \text{L}} \mathcal{D}$.
  
 
For papers on the specific levels of the algebraic hierarchy, see {{Cite|BlPi3}}, {{Cite|BlPi2}}, {{Cite|Cz3}}, {{Cite|CzJa}}, {{Cite|He2}}, {{Cite|He}}. Two references of a more general nature are {{Cite|BlPi4}}, {{Cite|Cz2}}.
 
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.===
 
===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" />.
+
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 $\mathcal{D}$ whose Leibniz-reduced model class $\operatorname { Mod } ^ { * \text{L}}  {\cal D }$ is well behaved in the sense of strict Horn logic with equality, and the key to this is the following correspondence theorem for $\mathcal{D}$-filters that mirrors the correspondence theorem for congruences in universal algebra: Let $\mathcal{D}$ be a protoalgebraic deductive system, and let $\mathbf{A}$ and $\mathbf{B}$ be algebras and $h : \mathbf{A} \twoheadrightarrow \mathbf B$ a surjective homomorphism. Finally, let $F _ { 0 }$ be the smallest $\mathcal{D}$-filter on $\mathbf{B}$. Then the mapping $F \mapsto h ^ { - 1 } ( F )$ is a one-to-one correspondence between the $\mathcal{D}$-filters on $\mathbf{B}$ and the $\mathcal{D}$-filters on $\mathbf{A}$ that include $h ^ { - 1 } ( F _ { 0 } )$.
  
When <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" />.
+
When $\mathbf{A}$ is taken to be $\textbf{Fm}$, the algebra of formulas, this correspondence establishes a close connection between the meta-logical properties of $\mathcal{D}$ and the algebraic properties of the class $\operatorname { Mod } ^ { * \text{L}}  {\cal D }$ of Leibniz-reduced models of $\mathcal{D}$.
  
Every class <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
+
Every class $\mathsf{K}$ of matrices over the same language type $\Lambda$ defines a deductive system $\mathcal D(\mathsf K) = \langle \textbf{F m} , \vDash_{\mathcal K} \rangle$ over $\Lambda$ in the following way. $\psi _ { 0 } , \ldots , \psi _ { n - 1 } \vDash _ { \mathsf{K} } \varphi$ if, for every $\langle {\bf A} , F \rangle \in \mathsf{K}$ and every homomorphism $h : \mathbf{Fm} \rightarrow \mathbf{A}$, $h ( \varphi ) \in F$ whenever $h ( \psi _ { 0 } ) , \ldots , h ( \psi _ { n  - 1} ) \in F$. The following theorem is a generalization of Mal'cev's well-known characterization of the strict universal Horn class generated by an arbitrary class of matrices: Let $\mathsf{K}$ be a class of Leibniz-reduced matrices over the same language type; then
  
if <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 ${\cal D} ( \mathsf{K} )$ is protoalgebraic, then $\operatorname { Mod } ^ { *\operatorname{L} }  \mathcal{D} ( \mathsf{K} ) = ( \textbf{SPP} _ { \operatorname{U} } \mathsf{K} ) ^ { *\operatorname{L} } $;
  
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" />.
+
if ${\cal D} ( \mathsf{K} )$ is equivalential, then $\operatorname { Mod}^ { *\text{L} }  \mathcal{D} ( \mathsf{K} ) = \mathbf{SPP} _ { \text{U} } \mathsf{K}$.
  
The following theorem is an analogue of the finite basis theorem of K. Baker for congruence-distributive varieties and of the corresponding result for relatively congruence-distributive quasi-varieties. It uses the notion of filter-distributive deductive system. A deductive system <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" />.
+
The following theorem is an analogue of the finite basis theorem of K. Baker for congruence-distributive varieties and of the corresponding result for relatively congruence-distributive quasi-varieties. It uses the notion of filter-distributive deductive system. A deductive system $\mathcal{D}$ is filter-distributive if $\operatorname{Fi} _ {\cal  D } \bf A$ is a distributive lattice for every algebra $\mathbf{A}$.
  
Let <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}}.
+
Let $\mathsf{K}$ be a finite set of matrices. If ${\cal D} ( \mathsf{K} )$ is protoalgebraic and filter-distributive, then ${\cal D} ( \mathsf{K} )$ has a presentation by a finite set of axioms and inference rules {{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}}.
 
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}}.
Line 211: Line 219:
  
 
===Second-order algebraizable logics.===
 
===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.
+
There are deductive systems with clear algebraic counterparts that are not protoalgebraic and hence not amenable to the methods of abstract algebraic logic discussed so far. Many examples of this kind arise as fragments of more expressive deductive systems that are finitely algebraizable. A paradigm for deductive systems of this kind is the conjunction/disjunction fragment $\operatorname{CPC}_{\wedge \vee}$ of classical propositional logic. It has a natural algebraic semantics, the variety $\mathsf{DL}$ of distributive lattices. In order to extend the standard theory of algebraizability to a wider class of deductive systems, recent investigations in abstract algebraic logic have switched focus from $\mathcal{D}$-filters to certain special classes of $\mathcal{D}$-filters and to a natural generalization of the Leibniz congruence that applies to classes of $\mathcal{D}$-filters.
  
The non-algebraizability of <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.
+
The non-algebraizability of $\operatorname{CPC}_{\wedge \vee}$ is reflected in the fact that, for an arbitrary algebra $\mathbf{A}$, the Leibniz operator does not give a one-one correspondence between ($\operatorname{CPC}_{\wedge \vee}$)-filters and $\mathsf{DL}$-congruences. The correspondence can in a sense be recovered by replacing single ($\operatorname{CPC}_{\wedge \vee}$)-filters by sets of ($\operatorname{CPC}_{\wedge \vee}$)-filters, each of which is of the form $\mathcal{C} _ { \Gamma }$, where $\mathcal{C} _ { \Gamma }$ consists of all ($\operatorname{CPC}_{\wedge \vee}$)-filters that are compatible with each member of a fixed but arbitrary class $\Gamma$ of congruences on $\mathbf{A}$. The set of congruences $\Gamma$ is completely arbitrary, but it turns out that there is always a single congruence $\Phi$ such that $\mathcal{C} _ { \{ \Phi \} } = \mathcal{C} _ { \Gamma }$, and in fact a smallest one with this property, and it is necessarily a $\mathsf{DL}$-congruence. Moreover, all $\mathsf{DL}$-congruences can be obtained this way.
  
Considerations such as these lead to the following notion. A full second-order filter of <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" />.
+
Considerations such as these lead to the following notion. A full second-order filter of $\mathcal{D}$ on an algebra $\mathbf{A}$ is the set of all $\mathcal{D}$-filters $F$ on $\mathbf{A}$ such that $F$ is compatible with a fixed but arbitrary set of congruences. The set of full second-order filters on $\mathbf{A}$ is denoted by $\operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$. It is easy to check that every $\mathcal{C} \in \operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$ is an algebraic closed-set system of the universe $A$ of $\mathbf{A}$. For each $\mathcal{C} \in \operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$ the Frege relation $\Lambda \mathcal{C}$ is the largest binary relation on $A$ (necessarily an equivalence relation) that is compatible with each $F \in \mathcal{C}$, and the second-order Leibniz congruence, also called the Tarski congruence, $\Omega \mathcal{C}$ is the largest congruence of $\mathbf{A}$ included in $\Lambda \mathcal{C}$.
  
A set <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" />.
+
A set $\mathcal{C}$ of $\mathcal{D}$-filters on $\mathbf{A}$ is a full second-order filter of $\mathcal{D}$ if and only if the set of quotient filters $\{ F / \Omega \mathcal{C} : F \in \mathcal{C} \}$ coincides with the set of all $\mathcal{D}$-filters on the quotient algebra $\mathbf{A} / \Omega \mathcal{C}$. A full second-order model of $\mathcal{D}$ is a second-order matrix $\mathfrak { A } = \langle \mathbf{A} , \mathcal{C} \rangle$ where $\mathcal{C} \in \operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$. $\frak A$ is Leibniz reduced if $\Omega \mathcal{C}$ is the identity relation. $\operatorname{FMod} \mathcal{D}$ (respectively, $\operatorname { FMod} ^ { *  \text{L}} \mathcal{D}$) is the class of all (Leibniz-reduced) full second-order models of $\mathcal{D}$.
  
 
The following assertion generalizes iv) above, the lattice isomorphism characterization of algebraizable deductive systems, and applies to all deductive systems.
 
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.
+
For any deductive system $\mathcal{D}$ and any algebra $\mathbf{A}$ the second-order Leibniz operator $\Omega$ is a dual order-isomorphism between $\operatorname{FFi} _ { \mathcal{D} } \mathbf{A}$ and $\operatorname {Co} _ { \text{Alg}  \operatorname {FMod} ^ { * \text{L}}  \mathcal{ D }} \mathbf{A}$, both partially ordered by set inclusion.
  
A full second-order model, and more generally, any second-order matrix <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
+
A full second-order model, and more generally, any second-order matrix $\langle \mathbf{A} , \mathcal{C} \rangle$ where $\mathcal{C}$ is an algebraic closed-set system on $\mathbf{A}$, can be naturally thought of as a model of a Gentzen system. In the context of abstract algebraic logic a Gentzen system can be viewed as a finitary and substitution-invariant consequence relation between sequents; a sequent is a syntactical expression of the form $\varphi _ { 0 } , \ldots , \varphi _ { n - 1 } \rhd \varphi _ { n }$, where $\varphi _ { 0 } , \ldots , \varphi _ { n  - 1} , \varphi _ { n }$ is any finite, non-empty sequence of formulas. Let $\mathfrak { A } = \langle \mathbf{A} , \mathcal{C} \rangle$ be a second-order matrix, and let $C : \mathcal{P} ( A ) \rightarrow \mathcal{P} ( A )$ be the closure operator on $A$ associated with the algebraic closed-set system $\mathcal{C}$. $\frak A$ is a model of a Gentzen system $\mathcal{G}$ if the following holds. For every entailment
  
<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>
+
\begin{equation*} \varphi _ { 0 } ^ { 0 } , \ldots , \varphi _ { n _ { 0 } - 1} ^ { 0 }  \rhd \psi ^ { 0 } ; \ldots ; \varphi _ { 0 } ^ { m - 1 } , \ldots , \varphi _ { n _ { m - 1 } -1 } ^ { m - 1 }  \rhd \psi ^ { m - 1 } \vdash _ { \mathcal{G} } \end{equation*}
  
<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>
+
\begin{equation*} \vdash _ { \mathcal{G} } \theta _ { 0 } , \ldots , \theta _ { n - 1 } \rhd \xi , \end{equation*}
  
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" />.
+
and every homomorphism $h : \mathbf{Fm} \rightarrow \mathbf{A}$, if $h ( \psi ^ { i } ) \in C ( \{ h ( \varphi _ { 0 } ^ { i } ) , \ldots , h ( \varphi _ { n _ { i } - 1 } ^ { i } ) \} )$ for each $i &lt; m$, then $h ( \xi ) \in C ( \{ h ( \theta _ { 0 } ) , \ldots , h ( \theta _ { n  - 1} ) \} )$.
  
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.)
+
A deductive system $\mathcal{D}$ is said to have a fully adequate Gentzen system if the class of full second-order models of $\mathcal{D}$ is the class of models of a Gentzen system. (Strictly speaking, this is the form the definition takes when $\mathcal{D}$ has at least one theorem. The definition together with the formulation of some of the results stated below must be modified slightly if there are no theorems.)
  
The notion of finite algebraizability for deductive systems can be extended to Gentzen systems in a straightforward way. Just as in the case of deductive systems, if a Gentzen system <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" />.
+
The notion of finite algebraizability for deductive systems can be extended to Gentzen systems in a straightforward way. Just as in the case of deductive systems, if a Gentzen system $\mathcal{G}$ is finitely algebraizable, there is a unique quasi-variety $\mathsf{Q}$ that is equivalent to $\mathcal{G}$ in the sense that there is a bisimulation between the consequence relation of $\mathcal{G}$ (between sequents) and the equational consequence relation of $\mathsf{Q}$. In view of the above observations it is natural to take a deductive system $\mathcal{D}$ to be second-order finitely algebraizable if it has a fully adequate Gentzen system $\mathcal{G}$ such that $\mathcal{G}$ is finitely algebraizable. In this case, $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ turns out to coincide with the equivalent quasi-variety of $\mathcal{G}$, and the consequence relation of $\mathcal{D}$ is definable (as part of the consequence relation of $\mathcal{G}$) in the equational consequence relation of $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$, but not vice versa unless $\mathcal{D}$ is also finitely algebraizable. In the latter case $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ coincides with the equivalent quasi-variety of $\mathcal{D}$. When $\mathcal{D}$ is second-order finitely algebraizable, $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ is called the second-order equivalent quasi-variety of $\mathcal{D}$.
  
 
Strictly speaking, second-order finite algebraizability does not generalize (first-order) finite algebraizability since there are deductive systems that are finitely algebraizable but do not have a fully adequate Gentzen system. However, this new notion of algebraizability goes a long way toward settling some important questions left open by the earlier theory.
 
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.
Line 239: Line 247:
 
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.
 
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.
+
Self-extensionality is a much weakened form of the property of being Fregean. A deductive system $\mathcal{D}$ is self-extensional if $\Lambda _ { \mathcal{D}} \operatorname { Thm }  \mathcal{D}$ is a congruence relation on the formula algebra.
  
Let <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.
+
Let $\mathcal{D}$ be a self-extensional deductive system that has either conjunction or the deduction-detachment theorem with a single deduction-detachment formula. Then $\mathcal{D}$ is second-order finitely algebraizable and its second-order equivalent quasi-variety $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ is actually a variety.
  
The conjunction/disjunction fragment <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 conjunction/disjunction fragment $\operatorname{CPC}_{\wedge \vee}$ of classical propositional calculus is self-extensional (in fact Fregean) with conjunction. Hence it is finitely algebraizable in the second-order (but not the first-order) sense. Its second-order equivalent quasi-variety $\operatorname{Alg FMod}^{* \text{L} }\mathcal{D}$ is the variety $\mathsf{DL}$ of distributive lattices.
  
The modal logic <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
+
The modal logic $\text{S}5$ can be formulated as a deductive system in two ways, both of which have the same set of theorems. The first and more familiar one, the strong form, is denoted by $\operatorname{S}5 ^ { S }$ and has the necessitation rule
  
<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>
+
\begin{equation*} \frac { \varphi } { \square \varphi } \end{equation*}
  
 
as an inference rule (cf. also [[Permissible law (inference)|Permissible law (inference)]]) along with [[Modus ponens|modus ponens]]
 
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>
+
\begin{equation*} \frac { \varphi , \varphi \rightarrow \psi } { \psi }. \end{equation*}
  
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 weak form, $\text{S} 5 ^ { \text{W} }$, has modus ponens as its only rule of inference. $\operatorname{S}5 ^ { S }$ is finitely algebraizable but not self-extensional. $\text{S} 5 ^ { \text{W} }$ is not algebraizable, but it is self-extensional and has both conjunction and the deduction-detachment theorem with a single deduction-detachment formula. So $\text{S} 5 ^ { \text{W} }$ is second-order finitely algebraizable. Moreover, its generalized equivalent quasi-variety is a variety; this turns out to be the variety of monadic algebras, which is also the equivalent quasi-variety of $\operatorname{S}5 ^ { S }$.
  
 
The main source for this section is {{Cite|FoJa}}, where references to other relevant sources can be found. The generalization of algebraizability to Gentzen systems is found in {{Cite|ReVe}}.
 
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.==
 
==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.
+
In this important branch of abstract algebraic logic the fine structure of the interpretations of a deductive system is taken into account. It also features a refinement of the notion of language. Let $\Lambda$ be a language type, assumed to be fixed. For an arbitrary set $P$ disjoint from $\Lambda$, let $\operatorname{Fm} _ { P }$ be the set of formulas built up from the elements of $P$, thought of as abstract atomic formulas, using the connectives of $\Lambda$; the associated formula algebra is denoted by $\textbf{Fm} _ { P }$. For each set $P$ of atomic formulas, let $\mathcal{S} _ { P } = \langle P , \operatorname { Mod } _ { \mathcal{S} _ { P } } , \operatorname { mng } _ { \mathcal{S} _ { P } } , \models _{ \mathcal{S} _ { P }} \rangle$ be a four-tuple, where $\operatorname {Mod}_{\mathcal S _ { P }}$ is a class, called the class of models of $\mathcal{S} _ { P }$; $\operatorname {mng}_{\mathcal{S}_P}$ is a function that assigns to each $\mathfrak { M } \in \operatorname { Mod }_{\mathcal{S}_P}$ a function $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$ with domain $\textbf{Fm} _ { P }$, called the meaning function for $\mathfrak{M}$; and $\models _ { \mathcal{S} _ { P } }$ is a binary relation between $\operatorname {Mod}_{\mathcal S _ { P }}$ and $\operatorname{Fm} _ { P }$, called the validity relation.
  
<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" />:
+
$\mathcal{S} _ { P }$ is a semantical system if the following conditions hold for every model $\mathfrak{M}$:
  
the meaning of a formula does not change if a subformula is replaced by one with the same meaning, i.e., <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040604.png" /> is a homomorphism;
+
the meaning of a formula does not change if a subformula is replaced by one with the same meaning, i.e., $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$ is a homomorphism;
  
the validity of a formula depends only on its meaning, i.e., if <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:
+
the validity of a formula depends only on its meaning, i.e., if $\operatorname {mng} _ { \mathcal{S} _ { P }, \mathfrak { M } } ( \varphi ) = \operatorname { mng } _ { \mathcal{S} _ { P }, \mathfrak { M } } ( \psi )$, then $\mathfrak { M } \models  _ { \mathcal{S}  _ { P }} \varphi$ if and only if $\mathfrak { M } \vDash _ { S _ { P } } \psi$. The meaning algebra of $\mathfrak{M}$, in symbols $\mathbf{Me}_{\mathcal{S} _ { P }} \mathfrak { M }$, is the image of $\textbf{Fm} _ { P }$ under the meaning homomorphism $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$. The final defining condition of a semantical system is the following:
  
every homomorphism from the formula algebra into the meaning algebra of <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" />.
+
every homomorphism from the formula algebra into the meaning algebra of $\mathfrak{M}$ is the meaning function of some model, i.e., if $h : \mathbf{Fm} _ { P } \rightarrow \mathbf{Me} _ { \mathcal{S} _ { P } } \mathfrak { M }$, then there is a $\mathfrak { N } \in \operatorname{Mod}_{\mathcal{S}_P}$ such that $h = \operatorname { mng } _ {{\cal S}_P,  \mathfrak { N } } $.
  
<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" />.
+
$\mathfrak{M}$ is a model of a set $\Gamma$ of formulas if $\mathfrak { M } \vDash _ { S _ { P } } \psi$ for each $\psi \in \Gamma$. The class of all models of $\Gamma$ is $\operatorname {Mod}_{\mathcal{S} _ { P }} \Gamma$. The consequence relation of $\mathcal{S}$ is the relation $\Gamma \vDash_{ \mathcal{S} _ { P }} \varphi$ that holds between a set of formulas $\Gamma$ and an individual formula if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040625.png"/>. $\models _ { \mathcal{S} _ { P } }$ satisfies all the conditions of a consequence relation of a deductive system except possibly finiteness; however, most of the familiar semantical systems are finitary. $\langle \mathbf{Fm} _ { P } , \models_{\mathcal{S}_ { P }} \rangle$ is called the underlying deductive system of $\mathcal{S} _ { P }$ and is denoted by ${\cal D S }_ { P }$.
  
The theory of a model <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" />.
+
The theory of a model $\mathfrak{M}$ of $\mathcal{S} _ { P }$, in symbols $\operatorname { Th } _ { \mathcal{S}  _ { P }}  \mathfrak { M }$, is the set of all formulas valid in $\mathfrak{M}$. The truth filter of $\mathbf{Me}_{\mathcal{S} _ { P }} \mathfrak { M }$, $F _ { \mathcal{S} _ { P } } \mathfrak { M }$, is the image of $\operatorname { Th } _ { \mathcal{S}  _ { P }}  \mathfrak { M }$ under $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$. Because the validity of a formula depends only on its meaning, the meaning matrix $\langle \textbf{Me} _ { \mathcal{S} _ { P } } \mathfrak { M } , F _ { \mathcal{S} _ { P } } \mathfrak { M } \rangle$ together with the meaning function $\operatorname{mng}_{\mathcal{S}_{P} ,} \mathfrak { M }$ is an interpretation of the underlying deductive system of $\mathcal{S} _ { P }$. As before, the Leibniz reduction of the meaning matrix by the Leibniz congruence of the truth filter, $\langle {\bf M e} _ { {\cal S} _ { P }} \mathfrak { M } / \Omega F _ { {\cal S}_P } \mathfrak { M } , F _ { {\cal S} _ { P } } \mathfrak { M } / \Omega F _ { {\cal S}  _ { P }} \mathfrak { M } \rangle$, is denoted by $\langle {\bf M e} _ { {\cal S} _ { P } } ^ { * \text{L} } \mathfrak { M } , F _ { {\cal S} _ { P } } ^ { * \text{L} } \mathfrak { M } \rangle$. The model-theoretic properties of a large class of different logical systems can be studied algebraically in this context. Consider, for example, the relation of elementary equivalence. Two models $\mathfrak{M}$ and $\mathfrak{N}$ of $\mathcal{S} _ { P }$ are elementarily equivalent if $\operatorname { Th } _ { {\cal S} _ { P } } \mathfrak { M } = \operatorname { Th } _ { {\cal S} _ { P } } \mathfrak { N }$.
  
Let <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.,
+
Let $\mathcal{S} _ { P }$ be a semantical system. Two models $\mathfrak{M}$ and $\mathfrak{N}$ of $\mathcal{S} _ { P }$ are elementarily equivalent if and only if there is an isomorphism $h$ between the Leibniz-reduced meaning matrices that commutes with the meaning functions, i.e.,
  
A) <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
+
A) $h$ is an isomorphism between $\mathbf{Me} _ { \mathcal{S} _ { P } } ^ { *L } \mathfrak { M }$ and $\mathbf{Me} ^ { * \text{L} _{\mathfrak { N }}}_{\mathcal{S}_P }$ such that $\operatorname { mng }_{{\cal S} _ { P } , \mathfrak { M }} = \operatorname { mng }_{{\cal S} _ { P } , \mathfrak { M }} \circ h$; and
  
B) <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" />.
+
B) $h$ preserves the truth set, i.e., $h ( F _ { \mathcal S _ { P } } \mathfrak { M } ^ { *  L} ) = F _ { \mathcal S _ { P } } \mathfrak { N } ^ { *  L}$.
  
Two different classes of algebras are associated with each semantical system <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040658.png" />:
+
Two different classes of algebras are associated with each semantical system $\mathcal{S} _ { P }$:
  
<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
+
$\operatorname {Alg} \operatorname {Mod}^{*\text{L}} \mathcal{DS}_{P}$, the algebraic semantics of the underlying deductive system of $\mathcal{S} _ { P }$; 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" />.
+
$\mathsf{Me}\operatorname{Mod}{\cal S}_P= \left\{ {\bf M e} _ { {\cal S} _ { P } }  {\frak M:M}\in \operatorname{Mod}_{{\cal S}_P} \right\}$, the class of meaning algebras of $\mathcal{S} _ { P }$. $\mathcal{S} _ { P }$ is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if its underlying deductive system ${\cal D S }_ { P }$ has the property and the meaning matrix of every model of $\mathcal{S} _ { P }$ is Leibniz-reduced, i.e., if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040666.png"/>. In this case it can be shown that $\operatorname{Alg}\operatorname{Mod}^{*\text{L}} \mathcal{DS}_{P}=\mathfrak{GB}\mathsf{Me}\operatorname{Mod}\mathcal{S}_{P}$.
  
In general, for a deductive system <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" />.
+
In general, for a deductive system $\mathcal{D}$ there are many different semantical systems with underlying deductive system $\mathcal{D}$. A natural semantical system for classical propositional logic is obtained by considering only the interpretations of $\operatorname{CPC}$ whose underlying algebra is a Boolean algebra of sets. More precisely, a model is a pair $\langle X , v \rangle$, where $X$ is a set and $v$ assigns a subset of $X$ to each atomic formula in $P$. The meaning function is the unique homomorphism from $\textbf{Fm} _ { P }$ to the Boolean algebra of subsets of $X$ that extends $v$. $\varphi$ is valid in $\langle X , v \rangle$ if its meaning is $X$.
  
A semantical system for <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" />.
+
A semantical system for $\text{S}5$ is obtained in a similar way. A model is a three-tuple $\langle X , x , v \rangle $, where $X$ is a set, $x \in X$, and $v$ assigns subsets of $X$ to atomic formulas. The meaning function is the unique homomorphism from $\textbf{Fm} _ { P }$ into the Boolean algebra of subsets of $X$ extending $v$ such that, for every formula $\varphi$, the meaning of $\square \varphi$ is $X$ if the meaning of $\varphi$ is $X$; otherwise the meaning of $\square \varphi$ is the empty set. $\varphi$ is valid in $\langle X , x , v \rangle $ if $x$ is contained in the meaning of $\varphi$. $\langle X , x , v \rangle $ represents a so-called  "possible worlds"  model for $\text{S}5$; $X$ is the set of possible worlds and a formula is valid in the model if it is true at the distinguished  "real world"  $x$.
  
One of the standard semantical systems for the first-order predicate logic has as its models structures of the form <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.
+
One of the standard semantical systems for the first-order predicate logic has as its models structures of the form $\langle X , v \rangle$, where $X$ is a non-empty set and $v$ assigns a subset of $X ^ { \omega }$ to each atomic formula. It is assumed that the individual variable symbols are arranged in an $\omega$-sequence. The meaning function is the unique homomorphism from $\textbf{Fm}$ into the Boolean algebra of subsets of $X ^ { \omega }$ extending $v$ such that, for each formula $\varphi$, the meaning of $\exists v_i \varphi$ is the  "cylinder"  that is swept out by moving the meaning of $\varphi$ parallel to the $i$th coordinate. The meaning algebra is the subalgebra of the $\omega$-dimensional cylindric set algebra over $X$ generated by the $\omega$-ary relations that are the meanings of the atomic formulas. Elementary equivalence in first-order logic is essentially captured by the notion of elementary equivalence in the semantical systems of this kind. The characterization of elementary equivalence given by A) and B) provides a way of investigating elementary equivalence algebraically.
  
The algebraic study of some model-theoretic notions, such as definability, require semantical systems over varying sets of atomic formulas. A system <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.
+
The algebraic study of some model-theoretic notions, such as definability, require semantical systems over varying sets of atomic formulas. A system $\mathcal{S} = \langle \mathcal{S} _ { P } : P \ \text {a set } \rangle$ of semantical systems is called a general semantical system if the $\mathcal{S} _ { P }$ are compatible in the sense that, for all $P$ and $P ^ { \prime }$, $\mathcal{S} _ { P }$ and $\mathcal{S} _ { P^{\prime} }$ are isomorphic in the natural sense whenever $P$ and $P ^ { \prime }$ have the same cardinality, and, if $P \subseteq P ^ { \prime }$, then every model of $\mathcal{S} _ { P }$ extends to a model of $\mathcal{S} _ { P^{\prime} }$ and every model of $\mathcal{S} _ { P^{\prime} }$ restricts to a model of $\mathcal{S} _ { P }$. A general semantical system $\mathcal{S}$ is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if each of its component semantical systems $\mathcal{S} _ { P }$ has this property.
  
For every general semantical system <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" />.
+
For every general semantical system $\mathcal{S}$, $\text { Alg } \text {Mod} ^ { *  \text{L}} \mathcal{DS}  = \cup \{ \text { Alg } \text {Mod} ^ { *  \text{L}} \mathcal{DS} _ { P } : P \ \text { a set } \}$ and $\mathsf{Me} \operatorname{Mod} \mathcal{S}= \cup \{ \mathsf{Me} \operatorname{Mod} \mathcal{S}_p \ : \ P \ \text{a set}  \}$.
  
Let <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:
+
Let $\mathcal{S}$ be a general semantical system. Let $P$, $R$ and $R ^ { \prime }$ be disjoint sets of atomic formulas, and let $\square '$ be a bijection between $R$ and $R ^ { \prime }$. Let $\Sigma ( P , R ) \subseteq \operatorname{Fm}_{ P \cup R}$ be a set of formulas whose atomic formulas are in $P \cup R$. Then:
  
<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" />.
+
$\Sigma ( P , R )$ defines $R$ explicitly over $P$ (in $\mathcal{S}$) if for every $r \in R$ there exists a $\varphi _ { r } \in \operatorname{Fm} _ { P }$ such that, for every $\mathfrak{M} \in \operatorname{Mod} _ { \mathcal{S} _{P \cup R}}( \Sigma ( P , R ) )$, $\operatorname{mng}_{\mathcal{S}_{P \cup R}} , \mathfrak { M } ( r ) = \operatorname { mng } _{\mathcal{S}_ { P \cup R }} , \mathfrak { M } ( \varphi _ { r } )$.
  
<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" />,
+
$\Sigma ( P , R )$ defines $R$ implicitly over $P$ (in $\mathcal{S}$) if for every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040759.png"/> and every $r \in R$,
  
<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>
+
<table class="eq" style="width:100%;"> <tr><td style="width:94%;text-align:center;" valign="top"><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" />.
+
here $\Sigma ( P , R ^ { \prime } )$ denotes the set of formulas obtained from $\Sigma ( P , R )$ by replacing each $r \in R$ by $r ^ { \prime }$.
  
<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" />.
+
$\Sigma ( P , R )$ is a strong implicit definition of $R$ over $P$ (in $\mathcal{S}$) if it defines $R$ implicitly over $P$ and every <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040772.png"/> has an extension $\mathfrak{N} \in \operatorname {Mod}_{\mathcal{S}_{P \cup R}} ( \Sigma ( P , R ) )$.
  
<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.
+
$\mathcal{S}$ has the (weak) Beth definability property if for all $\Sigma$, $P$ and $R$ as above, $\Sigma$ defines $R$ implicitly over $P$ (in the strong sense), then $\Sigma$ defines $R$ explicitly over $P$. Explicit definability always implies implicit definability. This is the well-known method of A. Padoa formulated in abstract algebraic logic.
  
The algebraic analogue of the property of Beth is surjectivity of epimorphisms. Let <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" />.
+
The algebraic analogue of the property of Beth is surjectivity of epimorphisms. Let $\mathsf{K}$ be a class of algebras over the same language type. A homomorphism $h : \mathbf{A} \rightarrow \mathbf{B}$, where $\mathbf{A}, \mathbf{B} \in \textsf{K}$, is called an epimorphism over $\mathsf{K}$ if for any pair of homomorphisms $g , g ^ { \prime } : \bf B \rightarrow C$, if $g \circ h = g ^ { \prime } \circ h$, then $g = g ^ { \prime }$.
  
Let <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 $\mathsf{K} _ { 0 } \subseteq \mathsf{K} $ be classes of algebras over the same language type. A homomorphism $h : \mathbf{A} \rightarrow \mathbf{B}$, where $\mathbf{A}, \mathbf{B} \in \textsf{K}$, is said to be $ \mathsf{K} _ { 0 }$-extensible over $\mathsf{K}$ if for any $\mathbf{C} \in \mathsf{K}_0$ and every surjection $f : \mathbf{A} \twoheadrightarrow \mathbf{C}$ there is a ${\bf D} \in \mathsf{K}_0$ and $g : \mathbf{B} \mapsto \mathbf{D}$ such that $\bf C \subseteq D$ and $g \circ h = f$.
  
Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/a/a130/a130040/a130040803.png" /> be a finitely algebraizable generalized semantical system. Then:
+
Let $\mathcal{S}$ 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;
+
I) $\mathcal{S}$ has the Beth definability property if and only if every epimorphism over $\operatorname{Alg} \operatorname{Mod}^{*\text{L}} \cal DS$ is surjective;
  
II) <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.
+
II) $\mathcal{S}$ 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 $\operatorname{Alg} \operatorname{Mod}^{*\text{L}} \cal DS$ is surjective.
  
 
The algebraic characterization of the weak Beth property requires a semantics-based context, but the result on the ordinary Beth property can be reformulated within logistic abstract algebraic logic and extended to equivalence deductive systems.
 
The 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.

Revision as of 15:30, 1 July 2020

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Logistic abstract algebraic logic.

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

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

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

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

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

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

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

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

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

Algebraizable logics.

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

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

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

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

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

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

Let

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

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

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

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

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

and

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

The algebraic hierarchy.

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

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

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

($E$-detachment).

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

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

and

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Protoalgebraic logics.

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

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

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

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

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

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

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

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

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

Second-order algebraizable logics.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Semantics-based abstract algebraic logic.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

References

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