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 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 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 . This is the  "absolutely free"  algebra of type with an -ary operation for each of arity such that is the formula , in prefix notation, or when and infix notation is used. The operation of simultaneously substituting fixed but arbitrary formulas for variables is identified with the unique endomorphism of it determines. A logistic or deductive system is a pair , where , the consequence relation of , is a binary relation between sets of formulas and individual formulas satisfying the following well-known conditions: For all and ,

for all ;

and for every imply ;

implies for some finite (finiteness);

implies for every substitution (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 is a theorem of if (i.e., it is a consequence of the empty set of formulas). The set of theorems, which may be empty, is denoted by . A set of formulas is a theory of a deductive system if it is closed under consequence, i.e., whenever and . is the smallest theory. The set of all theories of is denoted by . The theory axiomatized by an arbitrary set of formulas is the set of all formulas such that .

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 and , the intermediate logics (cf. also Intermediate logic), the various modal logics, including and (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 , where is an algebra (of the same language type as ), the underlying algebra of , and , the designated set of . An interpretation of is a matrix together with a homomorphism from the algebra of formulas into the underlying algebra of . is to be thought of as the  "sense"  or  "meaning"  of the formula under the interpretation, and is  "true"  or  "false"  depending on whether or not . By the Frege principle, this truth value is the denotation of under the interpretation. Truth must be preserved under consequence in the sense that, if and each is true under the interpretation, then must also be true. A set of formulas is said to define a class of interpretations if is the class of all interpretations in which each formula of is true. Because truth is preserved under consequence, the theory axiomatized by also defines ; it turns out that it is the unique theory with this property.

The formulas and are equivalent over a given class of interpretations (in the Fregean sense) if they have the same truth value, i.e., if and only if for each in . They are logically equivalent (with respect to ) 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 [a24], [a34]; for more recent work, see [a35]. For relation, polyadic and cylindric algebras, see [a9], [a19], [a22]. For the origin of the notion of a deductive system, see [a33].

Logistic abstract algebraic logic.

The assumption that the deductive system is uninterpreted implies that one need consider only those matrices with the property that is an interpretation for every . Such a matrix is called a (matrix) model of ; the class of all models of is denoted by . 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 and are equivalent over a theory , or -equivalent, in the Fregean sense, if, for every theory that extends , if and only if ; the binary relation between formulas defined this way is called the Frege relation of and denoted by . and are logically equivalent (with respect to ) if they are equivalent over every theory, or, equivalently, if they are equivalent over , the set of theorems. In terms of the consequence relation, and are logically equivalent over if and only if and are each consequences of the other over ; symbolically, if and .

If, as in the case of the classical and intuitionistic propositional calculi, has a binary implication connective for which the deduction theorem holds, then if and only if and , or equivalently if there is a biconditional, . So, under these rather weak conditions on 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 is the classical propositional calculus or the intuitionistic propositional calculus . If in any formula a subformula is replaced by an equivalent formula , the resulting formula is equivalent to . In algebraic terms this says that for every theory of or , is a congruence relation on the algebra of formulas . A deductive system for which -equivalence is compositional for every theory is called Fregean or extensional; non-Fregean systems are called intensional.

If is Fregean, it is possible to form the quotient matrices , where ranges over all theories. These are called the Lindenbaum–Tarski models of . 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 of the strong form of the modal system , with necessitation as a rule of inference (see below), one has if and only if and if and only if and . But this relation is not, in general, compositional. includes however a largest compositional equivalence relation, called the Suszko congruence of over and denoted by . It can be shown that if and only if . So captures the usual notion of -equivalence for .

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 of the underlying set of an algebra , of the same language type as , is called a filter of if is a model of ; thus is a filter if and only if it is closed under consequence in the sense that, if , one has for every such that for every . The set of filters of on is denoted by . 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 in a natural way. The Frege relation is the set of all pairs of elements of such that, for every filter on that includes , if and only if . The Suszko congruence is the largest congruence relation on that is included in ; it always exists.

The quotient matrix is called the Suszko-reduction of and is denoted by . It can be shown that coincides with (or, more precisely, is isomorphic to) . A model is Suszko-reduced if , i.e., is the identity relation. The class of all Suszko-reduced models of is denoted by . The Suszko-reduced models of 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 is denoted by . The underlying algebras of are the Boolean algebras. Each filter of on a Boolean algebra is completely determined by its Suszko congruence ; more precisely, it coincides with the set of all elements of equivalent under to the unit element of . Moreover, every congruence relation on is the Suszko congruence of a filter of . It follows that the consequence relation of 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 . In a similar way, the class of Heyting algebras and the class of so-called monadic algebras constitute complete algebraic semantics for and , 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 and the equational logic of 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 [a24], [a31]. [a32] contains historical information on the Tarski–Lindenbaum process. The essential idea of Fregean logic as presented here originated with R. Suszko [a4], [a30].

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 and the equational consequence relation of a class of algebras.

Let be a deductive system and a class of algebras over the same language type. Let be a (possibly infinite) non-empty system of formulas in two variables. is said to be a faithful interpretation of the equational logic of in if, for every equation and every set of equations , where means that is a quasi-identity of . Also, and , and is shorthand for the system of entailments for every ;  "iff"  stands for  "if and only if" .

Let be a non-empty system of equations in one variable. is a faithful interpretation of in the equational logic of if, for all , where and . The two interpretations are mutual inverses if and

A pair of mutually invertible interpretations and such as these is called a bisimulation between and the equational logic of . A deductive system is algebraizable if there is a bisimulation between and the equational logic of some class of algebras; it is finitely algebraizable if the interpretations are finite. If is algebraizable, then is the largest class with the above properties; it is called the equivalent algebraic semantics of . In general, 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 is finitely algebraizable. In this case is a quasi-variety (cf. also Quasi-variety)

The classical and intuitionistic propositional calculi and are finitely algebraizable and their equivalent quasi-varieties are, respectively, the varieties of Boolean algebras and 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 , where is, respectively, the classical and intuitionistic biconditional, and the inverse faithful interpretation is . 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 .

The bisimulation between a finitely algebraizable deductive system and the equational logic of its equivalent quasi-variety induces a correspondence between the meta-logical properties of and the algebraic properties of . 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 and the amalgamation property of ;

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 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 be a deductive system. A finite non-empty set of binary formulas is called a deduction-detachment system for if the following equivalence holds for all : A deductive system has the deduction-detachment theorem if it has a deduction-detachment system. The implication forms a singleton deduction-detachment system for and , while the formula forms a singleton deduction-detachment system for the modal systems and .

For an algebra , let be the set of all congruences of . If is a quasi-variety, then a congruence on an arbitrary algebra (not necessarily in ) is called a -congruence if . If is a variety (cf. also Algebraic systems, variety of) and , then every congruence is a -congruence. The principal -congruence generated by the pair and , , is the smallest -congruence that identifies and . A quasi-variety has equationally definable principal relative congruences (EDPRC) if there is a finite system of equations , in four variables, such that, for every and all , , where is any homomorphism such that .

-congruence generation in the formula algebra can be interpreted as the consequence relation of the equational logic of . Thus, if has EDPRC, the defining equations can be interpreted collectively as an implication connective for the equational logic. This observation is reflected in the following theorem: Let be a finitely algebraizable deductive system and let be its equivalent quasi-variety. Then has the deduction-detachment theorem if and only if 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 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 [a6]; earlier definitions, notably that in [a28], 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 ([a14], [a10], [a21], [a20]). For entailment logic and its algebraizability, see [a1], [a6]. For the deduction theorem in abstract algebraic logic, see [a5], [a11]. The result on orthomodular logic is found in [a37], [a25].

The algebraic hierarchy.

Finitely algebraizable deductive systems exhibit the strongest connection between the meta-logical properties of and the algebraic properties of . 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 be a (possibly infinite) set of formulas in two variables. is a proto-equivalence system for a deductive system if (-detachment).

A non-empty proto-equivalence system is an equivalence system if and for all ( is the rank of ). 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 of formulas in two variables is an equivalence system for a deductive system if and only if it defines Suszko congruences in the sense that, for every algebra and ,

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 of equations in one variable, called a system of defining equations, such that .

This last condition abstracts an important property of the biconditional of both classical and intuitionistic propositional logic, namely, that and the biconditional 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 , 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 and any subset of , there is a largest congruence relation on compatible with in the sense that is a union of equivalence classes of . is called the Leibniz congruence of . The relationship between the Leibniz and Suszko congruences is straightforward: For every deductive system and ,

and can both be viewed as operators mapping the lattice of -filters of to the lattice of congruences of . Note that the Leibniz and Suszko congruences coincide on -filters just in case the Leibniz operator is order-preserving, i.e., implies for all .

Let be a deductive system. Then the following characterizations hold:

i) is protoalgebraic if and only if the Leibniz operator is order-preserving, i.e., if and only if the Leibniz and Suszko congruences coincide;

ii) is equivalential if and only if it is protoalgebraic and commutes with inverse homomorphic images; more precisely, for every homomorphism and every ;

iii) is finitely equivalential if and only if it is protoalgebraic and commutes with directed unions; more precisely, for every that is upward-directed by inclusion;

iv) is algebraizable if and only if it is equivalential and is injective;

v) is finitely algebraizable if and only if it is finitely equivalential and is injective.

A deductive system is said to be weakly algebraizable if it is protoalgebraic and the Leibniz operator 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 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. denotes the class of all Leibniz-reduced models of . If is protoalgebraic, then ; this equality in fact characterizes protoalgebraic systems. In general, the best one has is that coincides with the class of all matrices isomorphic to a subdirect product of matrices in , in symbols .

For any class of matrices, , , , and denote, respectively, the classes of isomorphic images of submatrices, direct products, subdirect products, and ultraproducts of members of .

Let be a deductive system. Then the following characterizations hold:

a) is protoalgebraic if and only if , i.e., ;

b) is equivalential if and only if ;

c) is finitely equivalential if and only if , i.e., is a quasi-variety in the sense of Mal'cev;

d) is algebraizable if and only if it is equivalential and is the minimal -filter of for each ;

e) is finitely algebraizable if and only if it is finitely equivalential and is the minimal -filter of for each .

For papers on the specific levels of the algebraic hierarchy, see [a7], [a6], [a13], [a10], [a21], [a20]. Two references of a more general nature are [a8], [a12].

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 whose Leibniz-reduced model class is well behaved in the sense of strict Horn logic with equality, and the key to this is the following correspondence theorem for -filters that mirrors the correspondence theorem for congruences in universal algebra: Let be a protoalgebraic deductive system, and let and be algebras and a surjective homomorphism. Finally, let be the smallest -filter on . Then the mapping is a one-to-one correspondence between the -filters on and the -filters on that include .

When is taken to be , the algebra of formulas, this correspondence establishes a close connection between the meta-logical properties of and the algebraic properties of the class of Leibniz-reduced models of .

Every class of matrices over the same language type defines a deductive system over in the following way. if, for every and every homomorphism , whenever . 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 be a class of Leibniz-reduced matrices over the same language type; then

if is protoalgebraic, then ;

if is equivalential, then .

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 is filter-distributive if is a distributive lattice for every algebra .

Let be a finite set of matrices. If is protoalgebraic and filter-distributive, then has a presentation by a finite set of axioms and inference rules [a27]. An important related axiomatizability result can be found in [a38].

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 [a11], [a12].

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 [a8], [a13], [a15], [a17], [a16].

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 of classical propositional logic. It has a natural algebraic semantics, the variety 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 -filters to certain special classes of -filters and to a natural generalization of the Leibniz congruence that applies to classes of -filters.

The non-algebraizability of is reflected in the fact that, for an arbitrary algebra , the Leibniz operator does not give a one-one correspondence between ()-filters and -congruences. The correspondence can in a sense be recovered by replacing single ()-filters by sets of ()-filters, each of which is of the form , where consists of all ()-filters that are compatible with each member of a fixed but arbitrary class of congruences on . The set of congruences is completely arbitrary, but it turns out that there is always a single congruence such that , and in fact a smallest one with this property, and it is necessarily a -congruence. Moreover, all -congruences can be obtained this way.

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

A set of -filters on is a full second-order filter of if and only if the set of quotient filters coincides with the set of all -filters on the quotient algebra . A full second-order model of is a second-order matrix where . is Leibniz reduced if is the identity relation. (respectively, ) is the class of all (Leibniz-reduced) full second-order models of .

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

For any deductive system and any algebra the second-order Leibniz operator is a dual order-isomorphism between and , both partially ordered by set inclusion.

A full second-order model, and more generally, any second-order matrix where is an algebraic closed-set system on , 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 , where is any finite, non-empty sequence of formulas. Let be a second-order matrix, and let be the closure operator on associated with the algebraic closed-set system . is a model of a Gentzen system if the following holds. For every entailment and every homomorphism , if for each , then .

A deductive system is said to have a fully adequate Gentzen system if the class of full second-order models of is the class of models of a Gentzen system. (Strictly speaking, this is the form the definition takes when 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 is finitely algebraizable, there is a unique quasi-variety that is equivalent to in the sense that there is a bisimulation between the consequence relation of (between sequents) and the equational consequence relation of . In view of the above observations it is natural to take a deductive system to be second-order finitely algebraizable if it has a fully adequate Gentzen system such that is finitely algebraizable. In this case, turns out to coincide with the equivalent quasi-variety of , and the consequence relation of is definable (as part of the consequence relation of ) in the equational consequence relation of , but not vice versa unless is also finitely algebraizable. In the latter case coincides with the equivalent quasi-variety of . When is second-order finitely algebraizable, is called the second-order equivalent quasi-variety of .

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 is self-extensional if is a congruence relation on the formula algebra.

Let be a self-extensional deductive system that has either conjunction or the deduction-detachment theorem with a single deduction-detachment formula. Then is second-order finitely algebraizable and its second-order equivalent quasi-variety is actually a variety.

The conjunction/disjunction fragment 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 is the variety of distributive lattices.

The modal logic 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 and has the necessitation rule as an inference rule (cf. also Permissible law (inference)) along with modus ponens The weak form, , has modus ponens as its only rule of inference. is finitely algebraizable but not self-extensional. is not algebraizable, but it is self-extensional and has both conjunction and the deduction-detachment theorem with a single deduction-detachment formula. So 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 .

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

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 be a language type, assumed to be fixed. For an arbitrary set disjoint from , let be the set of formulas built up from the elements of , thought of as abstract atomic formulas, using the connectives of ; the associated formula algebra is denoted by . For each set of atomic formulas, let be a four-tuple, where is a class, called the class of models of ; is a function that assigns to each a function with domain , called the meaning function for ; and is a binary relation between and , called the validity relation.

is a semantical system if the following conditions hold for every model :

the meaning of a formula does not change if a subformula is replaced by one with the same meaning, i.e., is a homomorphism;

the validity of a formula depends only on its meaning, i.e., if , then if and only if . The meaning algebra of , in symbols , is the image of under the meaning homomorphism . The final defining condition of a semantical system is the following:

every homomorphism from the formula algebra into the meaning algebra of is the meaning function of some model, i.e., if , then there is a such that .

is a model of a set of formulas if for each . The class of all models of is . The consequence relation of is the relation that holds between a set of formulas and an individual formula if . satisfies all the conditions of a consequence relation of a deductive system except possibly finiteness; however, most of the familiar semantical systems are finitary. is called the underlying deductive system of and is denoted by .

The theory of a model of , in symbols , is the set of all formulas valid in . The truth filter of , , is the image of under . Because the validity of a formula depends only on its meaning, the meaning matrix together with the meaning function is an interpretation of the underlying deductive system of . As before, the Leibniz reduction of the meaning matrix by the Leibniz congruence of the truth filter, , is denoted by . 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 and of are elementarily equivalent if .

Let be a semantical system. Two models and of are elementarily equivalent if and only if there is an isomorphism between the Leibniz-reduced meaning matrices that commutes with the meaning functions, i.e.,

A) is an isomorphism between and such that ; and

B) preserves the truth set, i.e., .

Two different classes of algebras are associated with each semantical system :

, the algebraic semantics of the underlying deductive system of ; and

, the class of meaning algebras of . is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if its underlying deductive system has the property and the meaning matrix of every model of is Leibniz-reduced, i.e., if . In this case it can be shown that .

In general, for a deductive system there are many different semantical systems with underlying deductive system . A natural semantical system for classical propositional logic is obtained by considering only the interpretations of whose underlying algebra is a Boolean algebra of sets. More precisely, a model is a pair , where is a set and assigns a subset of to each atomic formula in . The meaning function is the unique homomorphism from to the Boolean algebra of subsets of that extends . is valid in if its meaning is .

A semantical system for is obtained in a similar way. A model is a three-tuple , where is a set, , and assigns subsets of to atomic formulas. The meaning function is the unique homomorphism from into the Boolean algebra of subsets of extending such that, for every formula , the meaning of is if the meaning of is ; otherwise the meaning of is the empty set. is valid in if is contained in the meaning of . represents a so-called  "possible worlds"  model for ; is the set of possible worlds and a formula is valid in the model if it is true at the distinguished  "real world"  .

One of the standard semantical systems for the first-order predicate logic has as its models structures of the form , where is a non-empty set and assigns a subset of to each atomic formula. It is assumed that the individual variable symbols are arranged in an -sequence. The meaning function is the unique homomorphism from into the Boolean algebra of subsets of extending such that, for each formula , the meaning of is the  "cylinder"  that is swept out by moving the meaning of parallel to the th coordinate. The meaning algebra is the subalgebra of the -dimensional cylindric set algebra over generated by the -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 of semantical systems is called a general semantical system if the are compatible in the sense that, for all and , and are isomorphic in the natural sense whenever and have the same cardinality, and, if , then every model of extends to a model of and every model of restricts to a model of . A general semantical system is protoalgebraic, equivalential, finitely equivalential, algebraizable, or finitely algebraizable if each of its component semantical systems has this property.

For every general semantical system , and .

Let be a general semantical system. Let , and be disjoint sets of atomic formulas, and let be a bijection between and . Let be a set of formulas whose atomic formulas are in . Then:

defines explicitly over (in ) if for every there exists a such that, for every , .

defines implicitly over (in ) if for every and every , here denotes the set of formulas obtained from by replacing each by .

is a strong implicit definition of over (in ) if it defines implicitly over and every has an extension .

has the (weak) Beth definability property if for all , and as above, defines implicitly over (in the strong sense), then defines explicitly over . 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 be a class of algebras over the same language type. A homomorphism , where , is called an epimorphism over if for any pair of homomorphisms , if , then .

Let be classes of algebras over the same language type. A homomorphism , where , is said to be -extensible over if for any and every surjection there is a and such that and .

Let be a finitely algebraizable generalized semantical system. Then:

I) has the Beth definability property if and only if every epimorphism over is surjective;

II) has the weak Beth definability property if and only if every )-extensible epimorphism of 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 [a26], [a2], [a3]. For the results on definability, see [a23] and [a36].

References