Stanford Encyclopedia of Philosophy
This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Propositional Consequence Relations and Algebraic Logic

First published Tue Dec 19, 2006

George Boole was the first to present logic as a mathematical theory in algebraic style. In his work, and in that of the other algebraists of the algebraic tradition of logic of the nineteenth century the distinction between a formal language and a mathematically rigorous semantics for it was still not drawn. What the algebraists in this tradition did was to build algebraic theories (of Boolean algebras, and relation algebras) with among other interpretations a logical one.

The works of Frege and Russell introduced a different perspective on the way to approach logic. In those works a logic system was given by a formal language and a deductive calculus, namely a set of axioms and a set of inference rules. Let us call such a pair a logical deduction system, and the formulas derivable in the calculus the theorems of the system (nowadays it is common practice to call this kind of calculi Hilbert style calculi). In Frege and Russell's approach a formal (mathematical) semantics of whatever kind (algebraic, model-theoretic, etc.) for the formal languages they used was lacking. The only semantics present was of an intuitive informal kind.

The systems introduced by Frege and Russell were systems of classical logic, but soon after systems of non-classical logics were considered by other logicians. The first influential attempts to introduce logics different from classical logic remained within the Frege-Russell tradition of presenting a logical deduction system without any formal semantics. They include the first modal systems of C.I. Lewis (1918) and the axiomatization of intuitionistic logic by Heyting (1930).

The idea underlying the design of Frege and Russell's logical deduction systems is that the theorems should be the formulas that correspond (intuitively) to the logical truths or logical validities. The concept of logical consequence was not central to the development and this was also the case in the many systems of non-classical logics that were to be designed following in the footsteps of the first modal systems of C.I. Lewis. This situation influenced the way in which the research on some non-classical logics has usually been presented and sometimes also its real evolution. However the concept of logical consequence has been the one that logic has traditionally dealt with. Tarski put it once again into the center of modern logic, both semantically and syntactically. Nowadays, a general theory of the algebraization of logics around the concept of logical consequence has grown from the different algebraic treatments of the different logics obtained during the last century.

The concept of consequence has proved much more fruitful than those of theorem and of logical validity for the development of such a general theory. The first attempts in the process of building the general theory of the algebraization of logics can be found in the study of the class of implicative logics by Rasiowa (Rasiowa, 1974) and in the systematic presentation by Wójcicki (Wójcicki, 1988) of the investigations of a general nature on propositional logics as consequence operations carried out mainly by Polish logicians, following the studies of Tarski, Lindenbaum, Łukasiewicz and others in the first part of the twentieth century.

It was only in the 1920s that algebras and logical matrices (an algebra plus a set of designated elements) started to be taken as models of logical deduction systems, that is, as providing a formal semantics for logical formal languages. Moreover, they were also used to define sets of formulas with similar properties to the ones the sets of theorems of the known logical deduction systems have, in particular the property of being closed under substitution instances and more recently they have also been used to define logics as consequence relations.

Algebraic logic can be described in very general terms as the discipline that studies logics by associating with them classes of algebras, classes of logical matrices and other algebra related mathematical structures and relating the properties of logics with algebraic properties of the associated algebras (or algebra related structures), so that the understanding of these algebras can be used to better understand the logic at hand.

From the algebraic study of specific logics a general theory of the algebraization of logics slowly emerged during the last century with the aim, more or less explicitly stated during the process, of obtaining general and informative results relating the properties a logic may have with the algebraic properties the class of algebras (or algebra related structures) associated with it might posses. Those algebraic studies assumed somehow an implicit conception of what is the process by which to associate with any given logic a class of algebras as its natural class. The development of the general theory speeded up and consolidated at the beginning of the 1980s with the introduction of the notion of algebraizable logic, and then the assumptions about the class of algebras that deserve to be taken as the natural to associate with a given logic started to be made more and more explicit.

In this entry we concentrate on the general theory of the algebraization of propositional logics taken as consequence relations. This theory is becoming to be known as Abstract Algebraic Logic (AAL).

1. Abstract consequence relations

Tarski's work on the methodology of the deductive sciences of the 1920s and 1930s (Tarski 1930a, 1930b, 1935, 1936) studies the axiomatic method abstractly and introduces for the first time the abstract concept of consequence operation. Tarski had in mind mainly the different mathematical axiomatic theories. On these theories the sentences that are proved from the axioms are consequences of them but (of course) almost all of them are not logical truths, and under a suitable formalization of these theories a logical calculus like Frege's or Russell's can be used to derive the consequences of the axioms. Tarski set the framework to study the most general properties of the operation that assigns to a set of axioms its consequences.

Given a logical deduction system H and an arbitrary set X of formulas, a formula a is deducible from X if there is a finite sequence of formulas any one of which belongs to X or is an axiom of H or is obtained from previous formulas in the sequence by one of the inference rules of H. Such a sequence is a deduction (or proof) of a with premises or hypotheses in X. Let Cn(X) be the set of formulas deducible from the formulas in X taken as premises or hypothesis by means of the axioms and rules of the calculus. This set is called the set of consequences of X (relative to the logical deduction system). Cn is then an operation that is applied to sets of formulas to obtain new sets of formulas. It has the following properties: For every set X of formulas

  1. X ⊆ Cn(X)
  2. Cn(Cn(X)) = Cn(X)
  3. Cn(X) = ∪{Cn(Y): Y ⊆ X, Y finite}

Clause 3 stipulates that Cn(X) is equal to the union of the set of formulas derivable from finite subsets of X. Tarski took these properties to define axiomatically the notion of consequence operation. In fact he added that there is a formula x such that Cn({x}) is the set A of all the formulas and that this set must be finite or of the cardinality of the natural numbers. Condition (3) implies the weaker, and important, condition of monotonicity

  1. if X ⊆ Y ⊆ A, then Cn(X) ⊆ Cn(Y).

To encompass the whole class of logic systems one finds in the literature, a slightly more general definition than Tarski's is required. We will say that an abstract consequence operation C on an arbitrary set A is an operation that applied to subsets of A gives subsets of A and for all X, Y ⊆ A satisfies conditions (1), (2) and (4) above. If in addition C satisfies (3) we say that it is a finitary consequence operation.

Consequence operations are present not only in logic but in many areas of mathematics. Abstract consequence operations are known as closure operators in universal algebra and lattice theory, for instance. In topology the operation that sends a subset of a topological space to its topological closure is a closure operator. In fact the topologies on a set A can be identified with the closure operators on A that satisfy the additional conditions that C(∅) = ∅ and C(X ∪ Y) = C(X) ∪ C(Y) for all X, Y ⊆ A.

Given a consequence operation C on A, a subset X of A is said to be C-closed, or a closed set of C, if C(X) = X.

A different, but mathematically equivalent, (formal) approach is to consider consequence relations on a set of formulas instead of consequence operations. A(n) (abstract) consequence relation on the set of formulas of a formal language is a relation ⊢ between sets of formulas and formulas that satisfies the following conditions:

  1. if a ∈ X, then X ⊢ a
  2. if X ⊢ a and X ⊆ Y, then Y ⊢ a
  3. if X ⊢ a and for every b ∈ X, Y ⊢ b, then Y ⊢ a

It is finitary if in addition it satisfies

  1. if X ⊢ a, then there is a finite set Y ⊆ X such that Y ⊢ a.

Given a logical deduction system H the relation ⊢ defined by X ⊢ a if a is deducible from X in H is a finitary consequence relation. Nonetheless we are used not only to syntactic definitions of consequence relations but also to semantic definitions. For example we define classical propositional consequence by means of truth valuations, first-order consequence relation by means of structures, the intuitionistic consequence relation by means of Kripke models etc. Sometimes these model-theoretic definitions of consequence relations define non-finitary consequence relations, for example the consequence relations for infinitary formal languages and the consequence relation of second-order logic (with so-called standard semantics, of course).

In general, an abstract consequence relation on a set A is a relation ⊢ between subsets of A and elements of A that satisfies conditions (1)–(3) above. If it also satisfies (4) it is said to be finitary. If ⊢ is an abstract consequence relation and X ⊢ a we can say that X is a set of premises or hypothesis with conclusion a according to ⊢ and that a follows from X (according to ⊢). These relations correspond to Koslow's implication structures; see (Koslow 1992) for the closely related but different approach to logics (in a broad sense) as consequence relations introduced by Koslow.

Consequence operations on a set A are in one-to-one correspondence with consequence relations on A. The move from a consequence operation C to a consequence relation ⊢C and, conversely, from a consequence relation ⊢ to a consequence operation C ⊢ is easy and given by the definitions:

X ⊢C a   iff   a ∈ C(X)       and       a ∈ C⊢(X)   iff   X ⊢ a.

Moreover, if C is finitary, so is  ⊢C and if ⊢ is finitary, so is C⊢.

For a general discussion on logical consequence see the entry on logical consequence.

2. Logics as consequence relations

In this section we define what propositional logics are and explain the basic concepts relating to them. We will call the propositional logics (as defined below) simply logic systems.

One of the main traits of the consequence relations we study in logic is their formal character. This roughly means that if a sentence a follows from a set of sentences X and we have another sentence b and another set of sentences Y that share the same form with a and X, then b also follows from Y. In propositional logics this boils down to saying that if we uniformly replace sub-sentences of the sentences in X ∪ {a} by other sentences obtaining Y and b, then b follows from Y. (The reader can find more information on the idea of formality in the entry on logical consequence.)

To turn the idea of the formal character of logics into a rigorous definition we need to introduce the concept of propositional language and the concept of substitution.

A propositional language L is a set of connectives, that is, a set of symbols each one of which has an arity n that tells us in case that n = 0 that the symbol is a propositional constant, and in case that n > 0 whether the connective is unary, binary, ternary, etc. For example {∧, ∨, →, ⊥, ⊤} is the language of several logics, like classical and intuitionistic, (⊥ and ⊤ are 0-ary and the other connectives are binary), {¬, ∧, ∨ →, □, ◊} is the language of several modal logics, (¬, □, ◊ are unary and the other connectives binary) and {⊥, 0, ∧, ∨, ∗, ⊤} is the language of many-valued logics and also of relevance logic and a fragment of linear logic (⊥ and 0 are 0-ary and the other connectives are binary).

Given a language L and a set of propositional variables V (which does not have elements in common with L), the formulas of L, or L-formulas, are defined inductively as follows:

  1. Every variable is a formula.
  2. Every 0-ary symbol is a formula.
  3. If ∗ is a connective and n > 0 is its arity, then for all formulas φ1,…, φn, ∗φ1…φn also is a formula.

A substitution σ for L is a map from the set of variables V to the set of formulas of L. It tells us which formula must replace which variable when we perform the substitution. If p is a variable, σ(p) will denote the formula that the substitution σ assigns to p. The result of applying a substitution σ to a formula φ is the formula σ(φ) obtained from φ by simultaneously replacing the variables in φ, say p1, … , pk, by, respectively, the formulas σ(p1), … , σ(pk). In this way a substitution σ gives a unique map σ from the set of formulas to itself that satisfies

  1. σ(p) = σ(p), for every variable p,
  2. σ(†) = †, for every 0-ary connective †,
  3. σ(∗φ1…φn) = ∗σ(φ1)…σ(φn), for every connective ∗ and formulas φ1, … , φn, where n is the arity of ∗.

A formula ψ is a substitution instance of a formula φ if there is a substitution σ such that when applied to φ gives ψ, that is, if σ(φ) = ψ.

In order to avoid unnecessary complications we will assume in the sequel that all the logics use the same set V of variables, so that the definition of formula of L depends only on L. A logic system (or logic for short) is given by a language L and a consequence relation ⊢ on the set of formulas of L that is formal in the sense that for every substitution σ, every set of formulas Γ and every formula φ,

if Γ⊢ φ, then σ[Γ] ⊢ σ(φ)

where σ[Γ] is the set of the formulas obtained by applying the substitution σ to the formulas in Γ. The consequence relations on the set of formulas of a language that satisfy this property are called structural and also substitution-invariant in the literature. They were considered for the first time by Łós and Suszko (Łós, Suszko 1958). Tarski only explicitly considered closed sets also closed under substitution instances for some consequence relations; he never considered (at least explicitly) the substitution invariance condition for consequence relations.

We will refer to logic systems by the letter L with possible subindices, and we set L = < L, ⊢L > and Ln = < Ln, ⊢Ln > with the understanding that L (Ln) is the language of L (Ln) and ⊢ (⊢Ln) its consequence relation. A logic system L is finitary if ⊢L is a finitary consequence relation.

The consequence relation of a logic system can be given in several ways, some proof-theoretic, others semantic. One can define a substitution-invariant consequence relation by means of a Hilbert style axiom system, by means of a Gentzen calculus or a natural deduction style calculus, etc. One can also define a substitution-invariant consequence relation semantically by means of a class of mathematical objects (algebras, Kripke models, topological models, etc.) and a satisfaction relation.

If L1 = < L, ⊢L1 > is a logic system with ⊢L1 defined by a proof-system (a Hilbert-calculus, a Gentzen style calculus, a natural deduction style calculus, etc.) and L2 = < L, ⊢L2 > is a logical system over the same language with ⊢L2 defined semantically, we say that the proof-system used to define ⊢L1 is sound for the semantics used to define ⊢L2 if  ⊢L1 is included in ⊢L2, namely if Γ ⊢L1 φ implies Γ ⊢L2 φ. If the other inclusion holds the proof-system is said to be complete with respect to the semantics that defines ⊢L2, that is when Γ ⊢L2 φ implies Γ ⊢L1 φ.

A set of formulas Γ is called a theory of a logic system L, or L-theory, if it is closed under the relation ⊢L, that is, if whenever Γ ⊢L φ it also holds that φ ∈ Γ. In other words, the theories of L are the closed sets of the consequence operation C⊢L on the set of L-formulas. In order to simplify the notation we denote this consequence operation by CL. A formula φ is a theorem (or validity) of L if ∅ ⊢L φ. CL(∅) is the set of theorems of L and is the least theory of L. The set of all theories of L will be denoted by Th(L).

Given a logic L, the consequence operation CL is substitution-invariant, which means that for every Γ and every substitution σ, σ[C(Γ)] ⊆ C(σ[Γ]). Moreover, for every theory T of L we have a new consequence operation defined as follows:

CLT(Γ) = CL(T ∪ Γ)

that is, CLT(Γ) is the set of formulas that follow from Γ and T according to L. It turns out that T is closed under substitutions if and only if CLT is substitution-invariant.

If L is a logic and Γ, Δ are sets of sentences, we will use the notation Γ⊢ L Δ to state that for every ψ ∈ Δ, Γ ⊢L ψ. Thus Γ ⊢L Δ if and only if Δ ⊆ CL(Γ).

If L = < L, ⊢L > is a logic system and L′ ⊆ L, the L′-fragment of L is the logic system L′ = < L′,  ⊢L′ > whose language is L′ (hence all the L′-formulas are L-formulas) and whose consequence relation is defined by

Γ ⊢L′ φ   iff   Γ ⊢L φ,

for every set of L′-formulas Γ and every L′-formula φ.

3. Some examples of logics

We give some examples of logic systems that we will refer to in the course of this essay, which are assembled here for the reader's convenience. Whenever possible we refer to the corresponding entries.

We use the standard convention of writing (φ ∗ ψ) instead of ∗φψ for binary connectives and omit the external parenthesis in the formulas.

3.1 Classical propositional logic

We take the language of classical propositional logic to be the set Lc = {∧, ∨, →, ⊤, ⊥}. We assume the consequence relation defined by the usual truth-table method (⊤ is interpreted as true and ⊥ as false), so

Γ  ⊢CPL φ   iff   every truth valuation that assigns true to all ψ ∈ Γ assigns true to φ.

The formulas φ such that ∅ ⊢CPL φ are the tautologies. For more information, see the entry on classical logic

3.2 Intuitionistic propositional logic

We take the language of Intuitionistic propositional logic to be the set {∧, ∨, →, ⊤, ⊥}. The consequence relation is defined by the following Hilbert style calculus.

Axioms:

C0. ⊤
C1. φ → (ψ → φ)
C2. φ → (ψ → (φ ∧ ψ))
C3. (φ ∧ ψ) → φ
C4. (φ ∧ ψ) → ψ
C5. φ → (φ ∨ ψ)
C6. ψ → (φ ∨ ψ)
C7. (φ ∨ ψ) → ((φ → δ) → ((ψ → δ) → δ))
C8. (φ → ψ) → ((φ → (ψ → δ)) → (φ → δ))
C9. ⊥ → φ

Rule of inference

φ, φ → ψ / ψ (Modus Ponens)

For more information, see the entry on intuitionistic logic

3.3 Local Normal Modal logics

The language of modal logic we consider here is the set Lm = {∧, ∨, →, ¬, □, ⊤, ⊥}. In the standard literature on modal logic a normal modal logic is defined not as a consequence relation but as a set of formulas with certain properties. A normal modal logic is a set Λ of formulas of Lm which contains all the tautologies of the language of classical logic, the formulas of the form

□(φ → ψ) → (□ φ → □ ψ)

and is closed under the rules

φ, φ → ψ / ψ (Modus Ponens)

φ / □ φ (Modal Generalization)

φ /σ(φ) for every substitution σ (Substitution)

The least normal modal logic is called K and can be axiomatized by the Hilbert calculus that contains as axioms the tautologies of classical logic and the formulas □(φ → ψ) → (□ φ → □ ψ) and as rules of inference Modus Ponens, Modal Generalization and Substitution.

With a normal modal logic Λ it is associated the consequence relation defined by the calculus that takes as axioms all the formulas in Λ and as the only rule of inference Modus Ponens. The logic system given by this consequence relation is called the local consequence of Λ. We denote it by lΛ. Its theorems are the elements of Λ. It holds that

Γ ⊢ lΛ φ     iff     φ ∈ Λ or there are φ1, … , φn ∈ Γ such that (φ1 ∧ … ∧ φn) → φ ∈ Λ.

3.4 Global Normal Modal logics

Another consequence relation is associated with each normal modal logic Λ. It is defined by the calculus that has as axioms the formulas of Λ and as rules of inference Modus Ponens and Modal Generalization. The logic system given by this consequence relation is called the global consequence of Λ and will be denoted by gΛ. It has the same theorems as the local lΛ, namely the elements of Λ. The difference between lΛ and gΛ lies in the consequences they allow to draw from nonempty sets of premises. This difference has an enormous effect on their algebraic behaviour.

For more information on modal logic, see the entry on modal logic. The reader can find specific information on modal logics as consequence relations in (Kracht 2006).

3.5 Intuitionistic Linear Logic without exponentials

We take as the language of Intuitionistic Linear Logic without exponentials the set {∧, ∨, →, ∗, 0, 1, ⊤, ⊥}. We denote the logic by ILL. The axioms and rule of inference below provide a Hilbert style axiomatization of this logic.

Axioms:

L1. 1
L2. (φ → ψ) → (ψ → δ) → (φ → δ))
L3. (φ → (ψ → δ)) → (ψ → (φ → δ))
L4. φ → (ψ → (φ ∗ ψ))
L5. (φ → (ψ → δ)) → ((φ ∗ ψ) → δ)
L6. (φ → ψ) → (ψ → δ) → (φ → δ))
L7. 1 → (φ → φ))
L8. (φ ∧ ψ) → φ
L9. (φ ∧ ψ) → ψ
L10. (φ ∧ ψ) → φ
L11. ψ → (φ ∨ ψ)
L12. φ → (φ ∨ ψ)
L13. ((φ → ψ) ∧ (ψ → δ)) → (φ → (ψ ∧δ))
L14. ((φ → δ) ∧ (ψ → δ)) → ((φ ∨ ψ) → δ)
L15. φ → ⊤
L16. ⊥ → ψ

Rules of inference:

φ, φ → ψ / ψ (Modus Ponens)

φ, ψ / φ ∗ ψ (Adjunction)

The 0-ary connective 0 is used to define a negation by ¬ φ := φ → 0. No specific axiom schema deals with 0.

For more information, see the entry on linear logic

3.6 The system R of Relevance Logic

The language is the set {∧, ∨, →, ∗, 0}. A Hilbert style axiomatization for R can be given by the rules of Intuitionistic Linear Logic without exponentials and the axioms L1-L4 of this logic plus the axioms

1. (φ → (φ → ψ)) → (φ → ψ)
2. (φ ∧ (ψ ∨ δ)) → ((φ ∧ ψ) ∨ φ ∧ δ))
3. ((φ ∨ ψ) ∧ (φ ∨ δ)) → (φ ∨ (ψ ∧ δ))
4. ¬ ¬ φ → φ

Negation is defined as in Intuitionistic Linear Logic without exponentials.

For more information, see the entry on relevance logic.

4. Algebras

The algebraic study of a specific logic has to provide first of all the formal language of the logic with an algebraic semantics using a class of algebras whose properties are exploited to understand which properties the logic has. In this section we present how the formal languages of propositional logics are given an algebraic interpretation. In the next section we go into the question of what is an algebraic semantics for a logic system.

We start by describing the first two steps involved in the algebraic study of propositional logics. Both are needed in order to endow propositional languages with algebraic interpretations. To expound them we will assume knowledge of first-order logic (see the entries on classical logic and first-order model theory) and we will call algebraic first-order languages, or simply algebraic languages, the first-order languages with equality and without any relational symbols, so that these languages have only operation symbols, if any, among their non-logical symbols.

The two steps we are about to expound can be summarized in the slogan:

Propositional formulas are terms.

The first step consist in looking at the formulas of any propositional language L as the terms of the algebraic first-order language with L as its set of operation symbols. This means that (i) every connective of L of arity n is taken as an operation symbol of arity n and that (ii) the propositional formulas of L are taken as the terms of this first-order language. From this point of view the definition of L-formula is exactly the definition of L-term. We will call the algebraic language with L as its set of operation symbols the L-algebraic language.

The second step is to interpret the propositional formulas in the way in which terms of a first-order language are interpreted in a structure. In this way the concept of L-algebra comes into play. On a given set A, an n-ary connective is interpreted by a n-ary function on A (a map that assigns an element of A to every sequence < a1, … , an> of elements of A). This procedure is a generalization of the truth-table interpretations of the languages of logic systems like classical logic and Łukasiewicz and Post's finite-valued logics. In those cases, given the set of truth-values at play the function that interprets a connective is given by its truth-table.

A way to introduce algebras is as the models of some algebraic first-order language. We follow an equivalent route and give the definition of algebra using the setting of propositional languages. Let L be a propositional language. An algebra A of type L, or L-algebra for short, is a set A, called the carrier of A, together with a function ∗A on A of the arity of ∗, for every connective ∗ in L (if ∗ is 0-ary, ∗A is an element of A). A valuation on an algebra A is a map v from the set of variables into its carrier A. Algebras together with valuations are used to interpret in a compositional way the formulas of L, assuming that a connective ∗ of L is interpreted in an L-algebra A by the function ∗A. Let A be an algebra of type L and v a valuation on A, the value of a compound formula ∗φ1…φn is computed by applying the function ∗A that interprets ∗ in A to the previously computed values v(φ1), … , v(φn) of the formulas φ1,… ,φn. Precisely speaking the value v(φ) of a formula φ is defined inductively as follows:

  1. v(p) = v(p), for each variable p,
  2. v(†) = †A, if † is a 0-ary connective
  3. v(∗φ1…φn) = ∗A(v(φ1), …, v(φn)), if ∗ is a n-ary (n > 0) connective.

In fact, the value of a formula under a valuation depends only on the propositional variables that actually appear in the formula. Accordingly, if φ is a formula we use the notation φ(p1, …, pn) to indicate that the variables that appear in φ are in the list p1, …, pn, and given elements a1, …, an of an algebra A by φA[a1, …, an] we refer to the value of φ(p1, …, pn) under any valuation v on A such that v(p1) = a1, …, v(pn) = an.

A third and fundamental step in the algebraic study of logics is to turn the set of formulas of a language L into an algebra, the algebra of formulas of L, denoted by FmL. This algebra has the set of L-formulas as carrier and the operations are defined as follows. For every n-ary connective ∗ with n > 0, the function ∗FmL is the map that sends each tuple of formulas (φ1, …, φn) (where n is the arity of ∗) to the formula ∗φ1…φn, and for every 0-ary connective †, †FmL is †. If no confusion is likely we will suppress the subindex in FmL and write Fm instead.

4.1 Some concepts of universal algebra and model theory

Algebras are a particular type of structure or model. An L-algebra is a structure or model for the L-algebraic first-order language. Therefore the concepts of model theory for the first-order languages apply to them (see the entries on classical logic and first-order model theory). We need some of these concepts. They are also used in universal algebra, a field that to some extent can be considered the model theory of the algebraic languages. We introduce the definitions of the concepts we need.

Given an algebra A of type L, a congruence of A is an equivalence relation θ on the carrier A of A that satisfies for every n-ary connective ∗ ∈ L the following compatibility property: for every a1, …, an, b1, …, bn ∈ A,

if a1θ b1, …, an θ b1, then ∗A(a1,…,an) θ ∗A(b1,…,bn).

Given a congruence θ of A we can reduce the algebra by identifying the elements which are related by θ. The algebra obtained is the quotient algebra of A modulo θ. It is denoted by A/θ, its carrier is the set A/θ of equivalence classes [a] of the elements a of A modulo the equivalence relation θ, and the operations are defined as follows

  1. †A/θ = [†A], for every 0-ary connective †,
  2. ∗A/θ([a1], …, [an]) = [∗A(a1,…,an)], for every connective ∗ whose arity is n and n > 0.

The compatibility property ensures that the definition is sound.

Let A and B be L-algebras. A homomorphism h from A to B is a map h from A to B such that for every 0-ary symbol † ∈ L and every n-ary connective ∗ ∈ L

h(†A) = †B

h(∗A(a1,…,an)) = ∗B(h(b1),…,h(bn)), for all a1, …, an ∈ A.

We say that B is a homomorphic image of A if there is a homomorphism from A to B which is an onto map from A to B.

Let A and B be L-algebras. A is a subalgebra of B if A ⊆ B, the interpretations of the 0-ary symbols of L in B belong to A, the interpretations of them in A coincide with their interpretations in B, and the interpretations on A of the other symbols in L are the restrictions to A of their interpretations in B.

We refer the reader to the entry on first-order model theory for the notions of direct product (called product there) and ultraproduct.

4.2 Varieties and quasivarieties

The majority of classes of algebras that provide semantics for propositional logics are quasivarieties and in most cases varieties.

A variety of L-algebras is a class of L-algebras that is definable in a very simple way (by equations) using the L-algebraic language. An L-equation is a formula φ ≈ ψ where φ and ψ are terms of the L-algebraic language (that is, L-formulas if we take the propositional logics point of view). An equation φ ≈ ψ is valid in an algebra A, or A is a model of φ ≈ ψ, if for every valuation v on A, v(φ) = v(ψ). This is exactly the same as to saying that the universal closure of φ ≈ ψ is a sentence true in A according to the usual semantics for first-order logic with equality. A variety of L-algebras is a class of L-algebras which is the class of all the models of some set of L-equations.

Quasivarieties of L-algebras are classes of L-algebras definable using the L-algebraic language in a slightly more complex way than varieties. A proper L-quasiequation is a formula of the form

∧i ≤ n φi ≈ ψi → φ ≈ ψ.

An L-quasiequation is a formula of the above form but possibly with an empty antecedent, in which case it is just the equation φ ≈ ψ. Hence, the L-quasiequations are the proper L-quasiequations and the L-equations. An L-quasiequation is valid in an L-algebra A, or the algebra is a model of it, if the universal closure of the quasiequation is true in A. A quasivariety of L-algebras is a class of algebras which is the class of the models of some set of L-quasiequations. Since equations are quasiequations, each variety is a quasivariety. The converse is false.

Varieties and quasivarieties can be characterized by the closure properties they enjoy. A class of L-algebras is a variety if and only if it is closed under subalgebras, direct products and homomorphic images. The variety generated by a class K of L-algebras is the least class of L-algebras that includes K and is closed under subalgebras, direct products and homomorphic images. It is also the class of the algebras that are models of the equations valid in K. For example, the variety generated by the algebra of the two truth-values for classical logic is the class of Boolean algebras. If we restrict that algebra to the operations for conjunction and disjunction only, it generates the variety of distributive lattices and if we restrict it to the operations for conjunction and disjunction and the interpretations of ⊤ and ⊥, it generates the variety of bounded distributive lattices.

A class of L-algebras is a quasivariety if and only if it is closed under subalgebras, direct products and ultraproducts. The quasivariety generated by a class K of L-algebras is the least class of L-algebras that includes K and is closed under subalgebras, direct products and ultraproducts.

An SP-class of L-algebras is a class of L-algebras closed under subalgebras and direct products. Thus quasivarieties and varieties are all SP-classes. The SP-class generated by a class K of L-algebras is the least class of L-algebras that includes K and is closed under subalgebras and direct products.

The theory of varieties and quasivarieties is one of the main subjects of universal algebra.

5. Algebraic semantics

The term 'algebraic semantics' was (and many times still is) used in the literature in a loose way. To provide a logic with an algebraic semantics was to interpret its language in a class of algebras, define a notion of satisfaction of a formula in an algebra of the class and prove a soundness and completeness theorem, usually for the theorems of the logic only. Nowadays we have a precise concept of algebraic semantics for a logic system. It was introduced by Blok and Pigozzi in (Blok-Pigozzi, 1989). In it we find a general way to state in mathematically precise terms what is common to the many cases of purported algebraic semantics for specific logic systems found in the literature. We expose the notion in this section. To motivate the definition we discuss several examples first, stressing what is common to all of them. The reader does not need to know about the classes of algebras that provide algebraic semantics we refer to in the examples. Its existence is what is important.

The prototypical examples of algebraic semantics for propositional logics are the class BA of Boolean algebras, which is the algebraic semantics for classical logic, and the class HA of Heyting algebras, which is the algebraic semantics for intuitionistic logic. Every Boolean algebra and every Heyting algebra A has a greatest element according to their natural order, that is denoted usually by 1A and interprets the symbol ⊤. This element is taken as the designated element relative to which the algebraic semantics is given. The algebraic semantics of these two logics works as follows:

Let L be classical or intuitionistic logic and let K(L) be the corresponding class of algebras BA or HA. It holds that

Γ ⊢L φ   iff   for every A ∈ K(L) and every valuation v on A, if for all ψ ∈ Γ v(ψ) = 1A, then v(φ) = 1A

This is the precise content of the statement that BA and HA are an algebraic semantics for classical logic and for intuitionistic logic respectively. The implication from left to right in the expression above is an algebraic soundness theorem and the implication from right to left an algebraic completeness theorem.

There are logics for which an algebraic semantics is provided in the literature in a slightly different way from the one given by the schema above. Let us consider the example in Section 3 of Intuitionistic Linear Logic without exponentials. We denote by IL0 the class of IL-algebras with zero defined in (Troelstra, 1992). On each one of these algebras A there is a designated element 1A that may be different from the greatest element. The greatest element is the interpretation of ⊤ and 1A the interpretation of 1. Moreover, each A ∈ IL0 is a lattice with extra operations and thus has its lattice order ≤A. It holds:

Γ ⊢ILL φ   iff   for every A ∈ IL0 and every valuation v on A, if for all ψ ∈ Γ 1A ≤ A v(ψ), then 1A ≤ A v(φ)

In this case one does not consider only a designated element in every algebra A but a set of designated elements, namely the elements of A equal to or greater than 1A. Let us denote this set by D(A), and notice that D(A) = {a ∈ A: 1A ∧A a = 1A}. Hence,

Γ ⊢ILL φ   iff   for every A ∈ IL0 and every valuation v on A, if v[Γ] ⊆ D(A), then v(φ) ∈ D(A).

Still there are even more complex situations. One of them is the system R of relevance logic. Consider the class of algebras Ral defined in (Font, Rodríguez, 1990) and denoted there by 'R'. Let us consider for every A ∈ Ral the set

E(A) := {a ∈ A: a →A(a →A a) = a →A a}.

Then Ral is said to be an algebraic semantics for R because the following holds:

Γ ⊢R φ   iff   for every A ∈ Ral and every valuation v on A, if v[Γ] ⊆ E(A), then v(φ) ∈ E(A).

The common pattern in the examples above is that the algebraic semantics is given by

  1. a class of algebras K,
  2. in each algebra in K a set of designated elements that plays the role 1A (more precisely the set {1A}) plays in the cases of classical and intuitionistic logic, and
  3. this set of designated elements is definable (in the same manner on every algebra) by an equation in the sense that it is the set of elements that satisfy the equation. For BA and HA the equation is p ≈ ⊤. For Ral it is p → (p → p) ≈ p → p, and for IL0 it is 1 ∧ p ≈ 1, which is the equational way of defining the order.

The main point in Blok and Pigozzi's concept of algebraic semantics comes from the realization, mentioned in (3) above, that the set of designated elements considered in the algebraic semantics of known logics is in fact the set of solutions of an equation, and that what practice forced reserachers to look for when they tried to obtain algebraic semantics for new logics was in fact, although not explicitly formulated in these terms, an equational way to define uniformly in every algebra a set of designated elements in order to obtain an algebraic soundness and completeness theorem.

We are now in a position to expose the mathematically precise concept of algebraic semantics. To develop a fruitful and general theory of the algebraization of logics some generalizations beyond the well-known concrete examples have to be made. In the definition of algebraic semantics one takes the move from a single equation to a set of them in the definability condition for the set of designated elements.

Before stating Blok and Pigozzi's definition let us introduce a notational convention. Given an algebra A and a set of equations Eq in one variable, we denote by Eq(A) the set of elements of A that satisfy all the equations in Eq. Then a logic L is said to have an algebraic semantics if there is a class of algebras K and a set of equations Eq in one variable such that

(**)     Γ ⊢L φ   iff   for every A ∈ K and every valuation v on A, if v[Γ] ⊆ Eq(A), then v(φ) ∈ Eq(A).

In this situation we say that the class of algebras K is an Eq-algebraic semantics for L, or that the pair (K, Eq) is an algebraic semantics for L. If Eq consists of a single equation δ(p) ≈ ε(p) we will simply say that K is a δ(p) ≈ ε(p)-algebraic semantics for L. In fact, Blok and Pigozzi required that Eq should be finite in their definition of algebraic semantics. But it is better to be more general. The definition clearly encompasses the situations encountered in the examples.

If K is an Eq-algebraic semantics for a finitary logic L and Eq is finite, then the quasivariety generated by K is also an Eq-algebraic semantics. The same does not hold in general if we consider the generated variety. For this reason it is customary and useful when developing the theory of the algebraization of finitary logics to consider quasivarieties of algebras as algebraic semantics instead of arbitrary subclasses that generate them. Conversely, if a quasivariety is an Eq-algebraic semantics for a finitary L and Eq is finite, so is any subclass that generates it.

In the best behaved cases the typical algebraic semantics of a logic is a variety, for instance in all the examples above. But there are cases in which it is not.

A quasivariety can be an Eq-algebraic semantics for a logic and an Eq′-algebraic semantics for another logic (with Eq and Eq′ different). For example, due to Glivenko's theorem (see the entry on intuitionistic logic) the class of Heyting algebras is a {¬ ¬ p ≈ 1}-algebraic semantics for classical logic and it is the standard {p ≈ 1}-algebraic semantics for intuitionistic logic. Moreover, different quasivarieties of algebras can be a Eq-algebraic semantics for the same logic. It is known that there is a quasivariety that properly includes the variety of Boolean algebras and is a {p ≈ 1}-algebraic semantics for classical propositional logic. It is also known that for some logics with an algebraic semantics (relative to some set of equations), the natural class of algebras that corresponds to the logic is not an algebraic semantics (for any set of equations) of it. One example where this situation holds is in the local normal modal logic lK. Finally, not every logic has an algebraic semantics.

These facts highlight the need for some criteria of the goodness of a pair (K, Eq) to provide a natural algebraic semantics for a logic L when some exists. One such criterion would be that L is an algebraizable logic with (K, Eq) as an algebraic semantics. Another that K is the natural class of algebras associated with the the logic. The notion of the natural class of algebras of a logic system will be discussed in Section 8 and the concept of algebraizable logic in Section 9.

6. Logical matrices

In the last section we saw that in order to provide a logic with an algebraic semantics we need in many cases to consider in every algebra a set of designated elements instead of a single designated one. In the examples we discussed, the set of designated elements was definable in the algebras by one equation. This motivated the definition of algebraic semantics in Section 5. For many logics, to obtain a semantics similar to an algebraic semantics using the class of algebras naturally associated with them for every algebra one needs a set of designated elements that cannot be defined using only the equations of the algebraic language or is not even definable by using only this language. As we already mentioned, one example where this is the case is the local consequence of the normal modal logic K.

To endow every logic with a semantics of an algebraic kind one has to consider, at least, algebras plus a set of designated elements, without any requirement about its definability using the corresponding algebraic language. These pairs are the logical matrices. Tarski defined the general concept of logical matrix in the 1920's but the concept was already implicit in previous work by Łukasiewicz, Bernays, Post and others, who used truth-tables, either in independence proofs or to define logics different from classical logic. A logical matrix is a pair < A, D > where A is an algebra and D a subset of the carrier A of A; the elements of D are called the designated elements of the matrix and D is called the set of designated elements. Logical matrices where first used as models of the theorems of specific logic systems, for instance in the work of McKinsey and Tarski, and also to define sets of formulas with similar properties to the set of theorems of a logic system, namely closure under substitution instances. This was the case of the n-valued logics of Łukasiewicz and of his infinite-valued logic. It was Tarski who first considered logical matrices as a general tool to define this kind of sets.

The general theory of logical matrices explained in this entry is due mainly to Polish logicians, starting with (Łós, 1949) and continuing in (Łós and Suszko, 1958), building on previous work by Lindenbaum. In Łós and Suszko's paper matrices are used for the first time both as models of logic systems (in our sense) and to define logic systems.

In the rest of this section we present the relevant concepts of the theory of logical matrices using modern terminology.

Given a logic L, a logical matrix < A, D > is said to be a model of L if wherever Γ ⊢L φ then every valuation v on A that maps the elements of Γ to some designated value (i.e. an element of D) also maps φ to a designated value. When < A, D > is a model of L it is said that D is an L-filter of the algebra A. The set of L-filters of an algebra A plays a crucial role in the theory of the algebraization of logic systems. We will come to this point later.

A class M of logical matrices is said to be a matrix semantics for a logic L if

(*)   Γ ⊢L φ   iff   for every < A, D > ∈ M and every valuation v on A, if v[Γ] ⊆ D, then v(φ) ∈ D.

The implication from right to left says that L is sound relative to M, and the other implication says that it is complete. In other words, M is a matrix semantics for L if every matrix in M is a model of L and moreover for every Γ and φ such that Γ ⊬L φ there is a model of L in M that witnesses the fact, namely there is a valuation on the model that sends the formulas in Γ to designated elements and φ to a non-designated one.

Logical matrices are also used to define logics semantically. If M = < A, D > is a logical matrix, the relation defined by

Γ ⊢M φ   iff   for every valuation v on A if v(ψ) ∈ D for all ψ ∈ Γ, then v(φ) ∈ D

is a consequence relation which is substitution-invariant; therefore < L, ⊢M > is a logic system. Similarly we can define the logic of a class of matrices M by taking condition (*) as a definition of a consequence relation. In the entry on many-valued logic the reader can find several logics defined in this way.

Every logic (independently of how it is defined) has a matrix semantics. Moreover, every logic has a matrix semantics whose elements have the property of being reduced in the following sense: A matrix < A, D > is reduced if there are no two different elements of A that behave in the same way. We say that a, b ∈ A behave in the same way in < A, D > if for every formula φ (q, p1, …, pn) and all elements d1, …, dn ∈ A

φA[a, d1, …, dn] ∈ D   iff   φA[b, d1, …, dn] ∈ D

Thus a, b ∈ A behave differently if there is a formula φ(q, p1, …, pn) and elements d1, …, dn ∈ A such that one of φA[a, d1, …, dn] and φA[b, d1, …, dn] belongs to D but not both. The relation of behaving in the same way in < A, D > is a congruence relation of A. This relation is known after (Blok-Pigozzi, 1986, 1989) as the Leibniz congruence of the matrix < A, D > and is denoted by ΩA(D). It can be characterized as the greatest congruence relation of A that is compatible with D, that is, that does not relate elements in D with elements not in D. The concept of Leibniz congruence plays a fundamental role in the general theory of the algebraization of the logic systems developed during the 1980's by Blok and Pigozzi. The reader is addressed to (Font, Jansana, Pigozzi 2003) and (Czelakowski, 2001) for extensive information on the developments around the concept of Leibniz congruence during this period.

Every matrix M can be turned into a new reduced matrix by identifying the elements related by its Leibniz congruence. This matrix is called the reduction of M and is usually denoted by M*. A matrix and its reduction are models of exactly the same logic systems, and since reduced matrices have no redundant elements, the classes of reduced matrices that are matrix semantics for logic systems are usually taken as the classes of matrices that deserve study; they are better suited to encoding in algebraic-like terms the properties of the logics of which they are the semantics.

The proof that every logic system has a reduced matrix semantics is as follows. Let L be a logic system. Consider the matrices < FmL, T > over the formula algebra, where T is a theory of L. These matrices are known as Lindenbaum matrices. It is not difficult to see that the class of those matrices is a matrix semantics for L. Since a matrix and its reduction are models of the same logics, the reductions of the Lindenbaum matrices of L constitute a reduced matrix semantics for L too. Moreover, any class of reduced matrix models of L that includes the reduced Lindenbaum matrices automatically is a complete matrix semantics for L. Thus the class of all reduced matrix models of L is a complete matrix semantics for L. We denote this class by RMatr(L).

The above proof can be seen as a generalization of the Lindenbaum-Tarski method for proving algebraic completeness theorems that we will discuss in the next section.

The class of the algebras of the matrices in RMatr(L) plays a prominent role in the theory of the algebraization of logics and it is denoted by Alg*L. It has been considered for a long time the natural class of algebras that has to be associated with a given logic L. For instance, in the examples considered above, the classes of algebras that were given as algebraic semantics of the different logics (Boolean algebras, Heyting algebras, etc.) are exactly the class Alg*L of the corresponding logic L. And in fact Alg*L coincides with what was taken to be the natural class of algebras for all the logics L studied up to the 1990's. In the 1990's, due to the knowledge adquired of several logics not studied before, some authors proposed another way to define what has to be counted as the natural class of algebras to be associated with a given logic. For many logics L it leads exactly to the class Alg*L but for others it gives a class that extends it properly.

7. The Lindenbaum-Tarski method for proving algebraic completeness theorems

We now discuss the method that is most commonly used to prove that a class of algebras K is a δ(p) ≈ ε(p)-algebraic semantics for a logic L, namely the Lindenbaum-Tarski method. This method is the standard method to prove that the classes of algebras of the examples mentioned in Section 5 are algebraic semantics for the corresponding logics.

The Lindenbaum-Tarski method contributed in two respects to the elaboration of important notions in the theory of the algebraization of logics. It underlies Blok and Pigozzi's notion of algebraizable logic and reflecting on it some ways to define for each logic a class of algebras can be justified as providing a natural class. We will consider this issue on Section 8.

The Lindenbaum-Tarski method can be outlined as follows. To prove that a class of algebras K is a δ(p) ≈ ε(p)-algebraic semantics for a logic L first it is shown that K gives a sound δ(p) ≈ ε(p)-semantics for L, namely that if Γ ⊢L φ, then for every A ∈ K and every valuation v in A if the values of the formulas in Γ satisfy δ(p) ≈ ε(p), then the value of φ does too. Secondly, the other direction, that is, the completeness part, is proved by what is really known as the Lindenbaum-Tarski method. This method uses the theories of L to obtain matrices on the algebra of formulas and then reduces these matrices in order to get for each one a matrix whose algebra is in K and whose set of designated elements is the set of elements of the algebra that satisfy δ(p) ≈ ε(p). We describe the method step by step in the sequel.

Let L be one of the logics discussed in the examples in Section 5. Let K be the corresponding class of algebras we considered there and let δ(p) ≈ ε(p) be the equation in one variable involved in the soundness and completeness theorem. To prove the completeness theorem one proceeds as follows. Given any set of formulas Γ:

  1. We consider the theory CL(Γ) = {φ: Γ ⊢L φ} of Γ, which we denote by T, and define the binary relation θ(T) on the set of formulas using the formula p ↔ q as follows:
    < φ, ψ > ∈ θ(T)   iff   φ ↔ ψ ∈ T
  2. It is shown that θ(T) is a congruence relation on FmL. The set [φ] of the formulas related to the formula φ is called the equivalence class of φ.
  3. A new matrix < Fm/θ(T), T/θ(T) > is obtained by identifying the formulas related by θ(T), that is, Fm/θ(T) is the quotient algebra of Fm modulo θ(T) and T/θ(T) is the set of equivalence classes of the elements of T. Recall that the algebraic operations of the quotient algebra are defined by:
    ∗Fm/θ(T)([φ1],…,[φn]) = [∗φ1…φn]         †Fm/θ(T) = [†]
  4. It is shown that if < φ, ψ > ∈ θ(T) and if φ ∈ T, then ψ ∈ T. That is, it is shown that θ(T) is a relation compatible with T. This implies that
    φ ∈ T   iff   [φ] ⊆ T   iff   [φ] ∈ T/θ(T)
  5. It is proved that the matrix < Fm/θ(T), T/θ(T) > is reduced, that Fm/θ(T) belongs to K and that T/θ(T) is the set of elements of Fm/θ(T) that satisfy the equation δ(p) ≈ ε(p) in Fm/θ(T).

The proof of the completeness theorem now goes as follows. (4) and (5) imply that for every formula ψ, Γ ⊢L ψ if and only if [ψ] satisfies the equation δ(p) ≈ ε(p) in the algebra Fm/θ(T). Thus, considering the identity valuation id mapping every variable p to its equivalence class [p], whose extension id to the set of all formulas is such that id(φ) = [φ] for every formula φ, we have that for every formula ψ,

Γ ⊢L ψ   iff   id(ψ) satisfies the equation δ(p) ≈ ε(p) in Fm/θ(T).

Hence, since by (6) Fm/θ(T) ∈ K, if Γ ⊬L φ, there is an algebra A (namely Fm/θ(T)) and a valuation v (namely id) such that the elements of v[Γ] satisfy the equation on A but v(φ) does not.

The Lindenbaum-Tarski method, when successful, shows that the class of algebras {Fm/θ(T): T a theory of L} is a δ(p) ≈ ε(p)-algebraic semantics for L. Therefore it also shows that every class of algebras K which is δ(p) ≈ ε(p)-sound for L and includes {Fm/θ(T): T a theory of L} is also a δ(p) ≈ ε(p)-algebraic semantics for L.

Let us make some remarks on the Lindenbaum-Tarski method just described. The first is important for the generalizations leading to the classes of algebras associated with a logic. The other to obtain the conditions in the definition of the concept of algebraizable logic.

1. Conditions (4) and (5) imply that θ(T) is in fact the Leibniz congruence of < FmL, T >.

2. When the Lindenbaum-Tarski method succeeds, it usually holds that in every algebra A ∈ K, the relation defined by the equation

δ(p ↔ q) ≈ ε(p ↔ q),

which is the result of replacing in δ(p) ≈ ε(p) the letter p by the formula p ↔ q that defines the congruence relation of a theory, is the identity relation on A.

3. For every formula φ, the formulas δ(p/φ) ↔ ε(p/φ) and φ are interderivable in L (i.e. φ ⊢L δ(p/φ) ↔ ε(p/φ) and δ(p/φ) ↔ ε(p/φ) ⊢L φ).

The concept of algebraizable logic introduced by Blok and Pigozzi, which we will discuss in Section 9, can be described roughly by saying that a logic L is algebraizable if it has an algebraic semantics (K, Eq) such that (1) K is included in the natural class of algebras associated with L and (2) the fact that (K, Eq) is an algebraic semantics can be proved by using the Lindenbaum-Tarski method slightly generalized.

8. The natural class of algebras of a logic system

We shall now expose for each logic L the two definitions of classes of algebras that have been considered as giving natural classes of algebras associated with L. Both definitions can be seen as arising from an abstraction of the Lindenbaum-Tarski method and we follow this path in introducing them. The common feature of these abstractions is that we disregard the way in which the relation θ(T) is defined in the Lindenbaum-Tarski method.

It has to be remarked that, nonetheless, for many logics both definitions lead to the same class. But both classes obtained from the definitions have been considered in the algebraic studies of many specific logics (for some logics one, for other the other) the natural class to study.

We already encountered the first generalization in Section 6 when we showed that every logic has a reduced matrix semantics. It leads to the class of algebras Alg*L and it comes from the realization that the relation θ(T) defined in the different completeness proofs in the literature using the Lindenbaum-Tarski method is in fact the Leibniz congruence of the matrix < FmL, T > and that then the matrix < Fm/θ(T), T/θ(T) > is its reduction. As we mentioned in Section 6, for every logic L every L-sound class of matrices M that contains all the matrices < Fm/ΩFmL(T), ΩFmL(T) > for T a theory of L is a complete reduced matrix semantics for L. From this perspective the definition of the Leibniz congruence of a matrix can be taken as a generalization to arbitrary matrices of the idea that comes from the Lindenbaum-Tarski procedure of proving completeness. Following this course of reasoning the class Alg*L of the algebras of the reduced matrix models of a logic L is the natural class of algebras to associate with L. This class is

{A/ΩA(F): A is an L-algebra and F is a L-filter of A}.

The second way of generalizing the Lindenbaum-Tarski method uses another fact, namely that in the examples discussed in Section 3 the relation θ(T) is also the relation Ω̃FmL(T) defined by the condition

< φ, ψ > ∈ Ω̃FmL(T)   iff   ∀T ′ ∈ Th(L), ∀p ∈ V, ∀γ(p) ∈ FmL (T ⊆ T ′ ⇒ (γ(p/φ) ∈ T ′ ⇔ γ(p/ψ) ∈ T ′)).

For every logic L and every L-theory T the relation Ω̃FmL(T) defined in this way is a congruence. In fact it is the greatest congruence compatible with all the L-theories that extend T. Therefore it holds that

Ω̃FmL(T) = ∩T ′ ∈ Th(L)T/ ΩFmL(T ′)

where Th(L)T = {T ′ ∈ Th(L): T ⊆ T ′}. The relation Ω̃FmL(T) is known as the Suszko congruence of T. Suszko defined it (in an equivalent way) in (Suszko, 1977).

For every logic L, the notion of the Suszko congruence can be extended to its matrix models. The Suszko congruence of a matrix model < A, D > of L is the greatest congruence of A compatible with every L-filter of A that includes D. It is the relation given by

Ω̃AL(D) = ∩D′ ∈ Fi L (A)D ΩA(D′)

where FiL(A)D = {D′: D′ is a L-filter of A and D ⊆ D′}. Notice that unlike the intrinsic notion of Leibniz congruence of a matrix model of L, the Suszko congruence is not intrinsic to the matrix: it depends on the logic under consideration. The theory of the Suszko congruence of matrices has been developed in (Czelakowski, 2003).

In the same manner that the concept of Leibniz congruence gives rise to the concept of a reduced matrix, the notion of Suszko congruence gives rise to the notion of a Suszko-reduced matrix. A matrix model of L is Suszko-reduced if its Suszko congruence is the identity. Then we can consider the class of algebras of the Suszko-reduced matrix models of a logic L as a natural class of algebras to associate with L. It is the class of algebras

AlgL = {A/Ω̃A(F): A is an L-algebra and F is a L-filter of A}

According to some authors, this class of algebras is the natural class to be associated with L.

For an arbitrary logic L the relation between AlgL and Alg*L is that AlgL is the closure of Alg*L under subdirect products, in particular Alg*L ⊆ AlgL. In general both classes may be different. If L is the (∧, ∨)-fragment of classical propositional logic, AlgL is the variety of distributive lattices (the class that has been always taken to be the natural class of algebras associated with L) but Alg*L is not this class — in fact it is not even a quasivariety. Nonetheless, for many logics L, in particular for the algebraizable ones and the protoalgebraic ones to be discussed in the next sections, and also when Alg*L is a variety, the classes AlgL and Alg*L are the same class. This fact can be considered a reason why in the 1980s, before the algebraic study of non-protoalgebraic logics was considered worth pursuing, the conceptual difference between both definitions of the natural class of algebras of a protoalgebraic logic was not needed and so not considered (or even discovered).

9. When a logic is algebraizable and what does this mean?

The algebraizable logics are purported to be the logics with the strongest possible link with their natural class of algebras. This includes that the natural class of algebras should be an algebraic semantics but also something else, present in the best behaved specific logics known. The mathematically precise concept of algebraizable logic characterizes this link. Blok and Pigozzi introduced that fundamental concept in (Blok and Pigozzi, 1989). Its introduction can be considered the starting point of the unification and growth of the field of abstract algebraic logic in the 1980's. Blok and Pigozzi defined the notion of algebraizable logic only for finitary logics. Later Czelakowski and Herrmann generalized it to arbitrary logics and also weakened some conditions in the definition. We present the generalized concept.

We said in Section 7 that, roughly speaking, a logic L is algebraizable when it has an algebraic semantics, i.e. a class of algebras K and a set of equations Eq(p) such that K is a Eq-algebraic semantics, and this can be proved by using the Lindenbaum-Tarski method slightly generalized and moreover K ⊆ Alg*L. The generalization of the Lindenbaum-Tarski method (as we described it in Section 7) consists in allowing (as in the definition of algebraic semantics) in step (5) a set of equations Eq(p) in one variable instead of a single equation δ(p) ≈ ε(p) and in allowing in a similar manner a set of sentences Δ(p, q) in (at most) two variables to play the role of the formula p ↔ q in the definitions of the congruence of a theory. Then, given a theory T the relation θ(T), which has to be the greatest congruence on the formula algebra compatible with T (i.e. the Leibniz congruence of T), is defined by

< φ, ψ > ∈ θ(T)   iff   Δ(p/φ, q/ψ) ⊆ T.

We need some notational conventions before engaging in the definition of algebraizable logic. Given a set of equations Eq(p) and a formula φ, let Eq(φ) be the set of equations obtained by replacing in all the equations in Eq the variable p by φ. If Γ is a set of formulas, let

Eq(Γ) := ∪φ ∈ ΓEq(φ)

Similarly, given a set of formulas in two variables Δ(p, q) and an equation δ ≈ ε, let Δ(δ, ε) denote the set of formulas obtained by replacing p by δ and q by ε in all the formulas in Δ. Moreover, if Eq is a set of equations, let

Δ(Eq) = ∪δ ≈ ε ∈ Eq Δ(δ, ε)

Given a set of equations Eq(p, q) in two variables, this set defines on every algebra A a binary relation, namely the set of pairs < a, b> of elements of A that they satisfy in A all the equations in Eq(p, q). In standard model-theoretic notation, it is the relation

{< a, b >: a, b ∈ A and A ⊨ Eq(p, q)[a, b]}.

The formal definition of algebraizable logic is as follows. A logic L is algebraizable if there is a class of algebras K, a set of equations Eq(p) in one variable and a set of formulas Δ(p, q) in two variables such that

  1. K is an Eq-algebraic semantics for L, namely
    Γ ⊢L φ   iff   for every A ∈ K and every valuation v on A, if v[Γ] ⊆ Eq(A), then v(φ) ∈ Eq(A).
  2. For every A ∈ K, the relation defined by the set of equations in two variables Eq(Δ(p, q)) is the identity relation on A.

A class of algebras K for which there are sets Eq and Δ with these two properties is said to be an equivalent algebraic semantics for L. The set of formulas Δ is called a set of equivalence formulas and the set of equations Eq a set of defining equations.

The conditions of the definition imply:

  1. p is inter-derivable in L with the set of formulas Δ(Eq), that is
    Δ(Eq) ⊢L p     and     p ⊢L Δ(Eq).
  2. For every L-theory T, the Leibniz congruence of < FmL, T> is the relation defined by Δ(p, q), namely
    < φ, ψ > ∈ ΩFm(T)   iff   Δ(p/φ, q/ψ) ⊆ T.
  3. If Δ and Δ′ are two sets of equivalence formulas, Δ ⊢L Δ′ and Δ′ ⊢L Δ. Similarly, if Eq(p) and Eq′(p) are two sets of defining equations, for every algebra A ∈ K, Eq(A) = Eq′(A).
  4. The class of algebras Alg*L also satisfies conditions (1) and (2) and is the largest equivalent algebraic semantics of L. It is called the equivalent algebraic semantics of L.
  5. For every A ∈ Alg*L there is exactly one L-filter F such that the matrix < A, F> is reduced, and this filter is the set Eq(A). Or, to put it in other terms, the class of reduced matrix models of L is {< A, Eq(A) >: A ∈ Alg*L}.
  6. Alg*L is an SP-class and includes any class of algebras K which is an equivalent algebraic semantics for L.

Blok and Pigozzi's definition in (Blok-Pigozzi, 1989) was given only for finitary logics and moreover they imposed that the sets of defining equations and of equivalence formulas should be finite. Today we say that an algebraizable logic is finitely algebraizable if the sets of equivalence formulas Δ and of defining equations Eq can both be taken finite.

If L is finitary and finitely algebraizable then Alg*L is not only an SP-class, but a quasivariety and it is the quasivariety generated by any class of algebras K which is an equivalent semantics for L.

We have just seen that in algebraizable logics the class of algebras Alg*L plays a prominent role. Moreover, in these logics the classes of algebras obtained by the two ways of generalizing the Lindenbaum-Tarski method coincide, that is, Alg*L = AlgL. Hence for every algebraizable logic L its natural class of algebras AlgL is its greatest equivalent algebraic semantics, whatever perspective is taken.

Conditions (1) and (2) of the definition of algebraizable logic encode the fact that there is a very strong link between an algebraizable logic L and its class of algebras AlgL, so that this class of algebras reflects the metalogical properties of L by algebraic properties of AlgL and conversely.

The definition of algebraizable logic can be formulated in terms of translations between the logic and an equational consequence relation associated with an equivalent algebraic semantics, which is the same no matter what algebraic semantics we choose for the logic.

The equational consequence is defined as follows. Let K be a class of algebras. Its equational consequence relation ⊨K is given by

{φi ≈ ψi: i ∈ I} ⊨K φ ≈ ψ   iff   for every A ∈ K and every valuation v on A, if v(φi) = v(ψi), for all i ∈ I, then v(φ) = v(ψ).

The translations are given by the set of defining equations and the set of equivalence formulas. A set of equations Eq in one variable defines a translation from formulas to sets of equations: each formula is translated into the set of equations Eq(φ). Similarly, a set of formulas Δ(p, q) in two variables defines a translation from equations to sets of formulas: each equation φ ≈ ψ is translated into the set of formulas Δ(φ, ψ).

Condition (1) in the definition of algebraizable logic can be reformulated as

Γ ⊢L φ   iff   Eq(Γ) ⊨K Eq(φ)

and condition (2) as

p ≈ q ⊨K Eq(Δ(p, q))     and     Eq(Δ(p, q)) ⊨K p ≈ q.

These two conditions imply

  1. {φi ≈ ψi: i ∈ I} ⊨K φ ≈ ψ   iff   Δ({φi ≈ ψi: i ∈ I})  ⊢L Δ(φ, ψ)

and (3) above is

p ⊢L Δ(Eq(p))     and     Δ(Eq(p)) ⊢L p.

Thus an algebraizable logic L is faithfully interpreted into the equational logic of the equivalent algebraic semantics (condition (2)) by means of the translation of formulas into sets of equations given by a set of defining equations, and the equational logic of the equivalent algebraic semantics is faithfully interpreted by the logic L (condition (9)) by means of the translation of equations into sets of formulas given by an equivalence set of formulas. Moreover, both translations are inverses of each other (conditions (2) and (3)) modulo logical equivalence. In this way we see that the link between L and its greatest equivalent algebraic semantics is really very strong and that the properties of L should translate into properties of the associated equational consequence relation. The properties that this relation actually has depend on the properties of the class of algebras AlgL.

Given an algebraic semantics (K, Eq) for a logic L, a way to stress the difference between it being merely an algebraic semantics and being an algebraic semantics that makes L algebraizable is that the translation, say τ, of formulas into equations that satisfies condition (1) is invertible in the sense that there is a translation, say Δ, of equations into formulas given by a set of formulas in two variables that satisfies the analog of (1), namely condition (9), and such that τ and Δ are mutually inverses.

This link between an algebraizable logic and its greatest equivalent algebraic semantics allows us to prove a series of general theorems that relate the properties of an algebraizable logic with the properties of its greatest equivalent algebraic semantics. We will mention as a sample only three of them.

The first concerns the deduction theorem. To prove a general theorem relating the existence of a deduction theorem with an algebraic property, first a concept of deduction theorem applicable to any logic has to be defined. A logic L has the deduction-detachment property if there is a finite set of formulas Δ(p, q) such that for every set of formulas Γ and all formulas φ, ψ

Γ ∪ {φ} ⊢L ψ   iff   Γ ⊢L Δ(φ, ψ)

Note that this is a generalization of the standard deduction theorem plus Modus Ponens that several logics have for a connective →. In those cases Δ(p, q) = {p → q}.

Theorem 1. A finitary and finitely algebraizable logic L has the deduction-detachment property if and only if the principal relative congruences of the algebras in AlgL are equationally definable.

The second theorem refers to Craig interpolation. Several notions of interpolation are applicable to arbitrary logics. We consider only one of them. A logic L has the Craig interpolation property for the consequence relation if whenever Γ ⊢L φ there is a finite set of formulas Γ' with variables shared by φ and the formulas in Γ such that Γ ⊢L Γ′ and Γ′ ⊢L φ.

Theorem 2. Let L be a finitary and finitely algebraizable logic with the deduction-detachment property. Then L has the Craig interpolation property if and only if AlgL has the amalgamation property.

Finally, the third theorem deals with the Beth definability property. The interested reader can find the definition in (Font, Jansana, Pigozzi, 2003). It is too involved in the general setting we are in to give it here.

Theorem 3. A finitary and finitely algebraizable logic has the Beth property if and only if all the epimorphisms of the category with objects the algebras in AlgL and morphisms the algebraic homomorphisms are surjective homomorphisms.

For several classes of algebras that are the equivalent algebraic semantics of some algebraizable logic it has been known for a long time that for every algebra in the class there is an isomorphism between the lattice of congruences of the algebra and a lattice of subsets of the algebra with important algebraic meaning. For example, in Boolean algebras and Heyting algebras these sets are the lattice filters and in modal algebras they are the lattice filters that are closed under the operation that interprets □. In all those cases, those sets are exactly the L-filters of the corresponding algebraizable logic L.

Algebraizable logics can be characterized by the existence of this kind of isomorphism between congruences and logic filters. To spell out this characterization we need a couple of definitions. Let L be a logic. The Leibniz operator on an algebra A (relative to L) is the map from the L-filters of A to the set of congruences of A that sends every L-filter D of A to its Leibniz congruence ΩA(D). We say that the Leibniz operator of a logic L commutes with the inverses of homomorphisms between algebras in a class K if for every homomorphism h from an algebra A ∈ K to an algebra B ∈ K and every L-filter D of B, h−1[ΩB(D)] = ΩA(h−1[D]).

Theorem 4. A logic L is algebraizable if and only if for every algebra A ∈ AlgL the Leibniz operator commutes with inverse homomorphisms between algebras in AlgL and is an isomorphism between the set of all L-filters of A, ordered by inclusion, and the set of congruences θ of A such that A/θ ∈ AlgL, ordered also by inclusion.

The theorem provides a logical explanation of the known isomorphisms mentioned above and similar ones for other classes of algebras. For example the isomorphism between the congruences and the normal subgroups of a group can be explained by the existence of an algebraizable logic L of which the class of groups is its equivalent algebraic semantics and the normal subgroups of a group are its L-filters.

A different but related characterization of algebraizable logics is this:

Theorem 5 A logic L is algebraizable if and only if on the algebra of formulas FmL, the map that sends every theory T to its Leibniz congruence is an isomorphism that commutes with the inverses of homomorphisms from FmL to FmL between the set Th(L) of theories of L, ordered by inclusion, and the set of congruences θ of FmL such that FmL/θ ∈ AlgL, also ordered by inclusion.

10. A classification of logics

Unfortunately not every logic is algebraizable. A typical example of a non-algebraizable logic is the local consequence of the normal modal logic K. Let us discuss this example.

The local modal logic lK and the corresponding global one gK are not only different, but their metalogical properties differ. For example lK has the deduction-detachment property for →:

Γ ∪ {φ} ⊢lK ψ   iff   Γ ⊢lK φ → ψ

But gK does not have the deduction-detachment property (at all).

The logic gK is algebraizable and lK is not. The equivalent algebraic semantics of gK is the variety MA of modal algebras, the set of equivalence formulas is the set {p ↔ q} and the set of defining equations is {p ≈ 1}. Interestingly, lK and gK have the same associated class of algebras (i.e., Alg lK = Alg lK), namely, the variety of normal modal algebras.

A lesson to draw from this example is that the class of algebras AlgL of a logic L does not necessarily fully encode the properties of L. The class of modal algebras encodes the properties of gK because this logic is algebraizable and so the link between gK and Alg gK is as great as possible. But Alg lK cannot completely encode the properties of lK.

What causes this difference between gK and lK is that the class of reduced matrix models of gK is

{< A, {1A}>: A ∈ MA},

but the class of reduced matrix models of lK properly includes this class so that for some algebras A ∈ MA, in addition to {1A} there is some other lK-filter F such that < A, F > is reduced. This fact gives a way of showing that lK can not be algebraizable by showing that the lK-filters of the reduced matrices are not equationally definable from the algebras, since if they where then for every A ∈ Alg lK there would be exactly one lK-filter F of A such that < A, F > is reduced.

Nonetheless we can perform some of the steps of the Lindenbaum-Tarski method in the lK case. We can define the Leibniz congruence of every lK-theory in a uniform way by using formulas in two variables. Now it turns out that in this case the set of formulas has to be infinite. Let Δ(p, q) = {□n(p ↔ q): n a natural number}, where for every formula φ, □0φ is φ and □nφ for n > 0 is the formula φ with a sequence of n boxes in front (□ … n … □ φ). Then, for every lK-theory T the relation θ(T) defined by

< φ, ψ > ∈ θ(T)   iff   {□n(φ ↔ ψ): n a natural number } ⊆ T

is the Leibniz congruence of T. It happens that there are two different lK-theories with the same Leibniz congruence, something that does not hold for lK.

The logics L with the property that there is a set of formulas (possibly infinite) Δ(p, q) in two variables which defines in every L-theory its Leibniz congruence are known as the equivalential logics. If Δ(p, q) is finite, the logic is said to be finitely equivalential. A set Δ(p, q) that defines in every L-theory its Leibniz congruence is called a set of equivalence formulas for L. It is clear that every algebraizable logic is equivalential and every finitely algebraizable logic is finitely equivalential.

The logic lK is, according to the definition, equivalential, and it can be shown that it is not finitely equivalential. The local modal logic lS4 is an example of a non-algebraizable logic that is finitely equivalential. A set of equivalence formulas for lS4 is {□ (p↔ q)}.

There is a syntactic characterization of the sets of equivalence formulas. A set Δ(p, q) of L-formulas is a set of equivalence formulas for a logic L if and only if

  1. ⊢L Δ(p, p)
  2. p, Δ(p, q) ⊢L q
  3. Δ(p, q) ⊢L Δ(q, p)
  4. Δ(p, q) ∪ Δ(q, r) ⊢L Δ(p, r)
  5. Δ(p1, q1) ∪ … ∪ Δ(pn, qn) ⊢L Δ(∗p1…pn, ∗q1…qn), for every connective ∗ of L of arity n greater that 0.

A set of equivalence formulas for a logic L should be considered as a generalized biconditional, in the sense that collectively the formulas in the set have the relevant properties of the biconditional that make it suitable to define the Leibniz congruences of theories, for example in classical logic. This comes out very clearly from the syntactic characterization.

Equivalential logics were first considered as a class in (Prucnal and Wrónski 1974), and have been studied extensively by Czelakowski in (Czelakowski,1981), see also (Czelakowski, 2001).

There are logics that are not equivalential but have the property of having a set of formulas [p ⇒ q] which collectively behave in a very weak sense as the implication → does in many logics. Namely, it has the properties (1) and (2) in the syntactic characterization of the set of equivalence formulas, i.e.

  1. ⊢L [p ⇒ p]
  2. p, [p ⇒ q] ⊢L q

If such a set exists and the logic is finitary, one can always find a finite subset with the same properties. The logics with such a set (finitr or not) of formulas are called protoalgebraic. So, every equivalential logic and every algebraizable logic are protoalgebraic.

Protoalgebraic logics were first studied by Czelakowski, who called them non-pathological, and a slightly later by Blok and Pigozzi (Blok, Pigozzi, 1986). The label ‘protoalgebraic logic’ is due to these last authors.

The class of protoalgebraic logics turned out to be the class of logics for which the theory of logical matrices works really well in the sense that many results of universal algebra have counterparts for the classes of reduced matrix models of these logics; therefore the algebraic study of protoalgebraic logics using their matrix semantics has been very fruitful. As we will see, some interesting logics are not protoalgebraic.

An important characterization of protoalgebraic logics is via the behaviour of the Leibniz operator. The following conditions are equivalent:

  1. L is protoalgebraic.
  2. The Leibniz operator ΩFmL is monotone on the set of L-theories with respect to the inclusion relation, that is, if T ⊆ T ′ are L-theories then ΩFmL(T) ⊆ ΩFmL(T ′).
  3. For every algebra A, the Leibniz operator ΩA is monotone on the set of L-filters of A with respect to the inclusion relation.

Due to the monotonicity property of the Leibniz operator, for any protoalgebraic logic L the classes of algebras Alg*L and AlgL coincide.

There are also characterizations of equivalential and finitely equivalential logics by the behaviour of the Leibniz operator. The reader is addressed to (Czelakowski, 2001) and (Font, Jansana, Pigozzi, 2003).

The classes of logics we have considered so far are the main classes in what has come to be known as the Leibniz hierarchy because it members are classes of logics that can be characterized by the behaviour of the Leibniz operator. We described only the most important classes of logics in the hierarchy. The reader is refereed to (Czelakowski, 2001) and (Font, Jansana, Pigozzi, 2003) for more information. In particular the book (Czelakowski, 2001) gathers extensively the information on the different classes of the Leibniz hierarchy known at the time of its publication. The relations between the classes of the Leibniz hierarchy considered in this entry are sumarized as follows:

Finitely Algebraizable ⊊ Finitely Equivalential ⊊ Equivalential ⊊ Protoalgebraic

and

Finitely Algebraizable ⊊ Algebraizable ⊊ Equivalential ⊊ Protoalgebraic

11. Replacement principles

Two classes of logics not in the Leibniz hierarchy have been extensively studied in AAL. They are defined from a completely different perspective from the one provided by the behaviour of the Leibniz operator, namely from the perspective given by the replacement principles a logic might enjoy.

The strongest replacement principle that a logic system L might have, shared for example by classical, intuitionistic and all its axiomatic extensionss, says that for any set of formulas Γ, any formulas φ, ψ, Δ and any variable p

if Γ, φ ⊢L ψ and Γ, ψ ⊢L φ, then Γ, Δ(p/φ) ⊢L Δ(p/ψ) and Γ, Δ(p/φ) ⊢L Δ(p/ψ),

where Δ(p/φ) and Δ(p/ψ) are the formulas obtained by substituting respectively φ and ψ for p in Δ. This replacement property is taken by some authors as the formal counterpart of Frege's compositionality principle for truth. Logics satisfying this strong replacement property are called Fregean in (Czelakowski, Pigozzi 2004a). In that paper and in (Czelakowski, Pigozzi 2004b) they are studied thoroughly.

Many important logics do not satisfy this strong replacement property, for instance almost all the logics (local or global) of the modal family, but some, like the local consequence relation of a normal modal logic, satisfy a weaker replacement principle: for all formulas φ, ψ, Δ,

if φ ⊢Lψ and ψ ⊢Lφ, then Δ(p/φ) ⊢L Δ(p/ψ) and Δ(p/φ) ⊢L Δ(p/ψ).

A logic satisfying this weaker replacement property is called selfextensional by Wójcicki and congruential by Humberston (Humberstone, 2005). We will use the first terminology because it seems more common.

Selfextensional logics have a very good behaviour from several points of view. Their systematic study started in (Wóojcicki, 1969) and has recently been continued in the context of AAL in (Font, Jansana 1996), (Jansana 2005, 2006) and (Jansana, Palmigiano, 2006).

There are selfextensional and non-selfextensional logics in any of the classes of the Leibniz hierarchy and also in the class of non-protoalgebraic logics. This shows that the perspective that leads to the consideration of the classes in the Leibniz hierarchy and the perspective that leads to the definition of the selfextensional and the Fregean logics as classes of logics worthy of study as a whole are really different. Nonetheless, one of the trends of today's research in AAL is to determined the interplay between the two perspectives and study the classes of logics that arise when crossing both classifications. In fact there is a connection between the replacement principles and the Suszko congruence (and thus with the Leibniz congruence). A logic L satisfies the strong replacement principle if and only if for every L-theory T its Suszko congruence is the interderivability relation relative to T, namely the relation {< φ, ψ>: T, φ ⊢L ψ and T, ψ ⊢L φ}. And a logic L satisfies the weak replacement principle if and only if the Suszko congruence of the set of theorems of L is the interderivability relation {< φ, ψ>: φ ⊢L ψ and ψ ⊢L φ}.

12. Beyond protoalgebraic logics

Not all interesting logics are protoalgebraic. In this section we will briefly discuss four examples of non-protoalgebraic logics: the logic of conjunction and disjunction, positive modal logic, the strict implication fragment of lK and Visser's subintuitionistic logic. All of them are selfextensional. In the next section we will expound the semantics of abstract logics and generalized matrices that serves to develop a really general theory of the algebraization of logic systems. As we will see the perspective changes in an important respect from the perspective taken by logical matrix model theory.

12.1 The logic of conjunction and disjunction

This logic is the {∧, ∨, ⊥, ⊤}-fragment of Classical Propositional Logic. Hence its language is the set {∧, ∨, ⊤, ⊥} and its consequence relation is given by

Γ ⊢ φ   iff   Γ ⊢CPL φ.

It turns out that it is also the {∧, ∨, ⊥, ⊤}-fragment of Intuitionistic Propositional Logic. Let us denote it by L{∧, ∨}.

The logic L{∧, ∨} is not protoalgebraic and it is Fregean. Its classes of algebras Alg*L{∧, ∨} and AlgL{∧, ∨} are different. Moreover AlgL{∧, ∨} is the variety of bounded distributive lattices, the natural class expected to be the associated class of algebras, but Alg*L{∧, ∨} is not. In fact this class of algebras is first-order definable but is not a quasivariety.

The logic L{∧, ∨} is a natural example of logic where the class of its reduced matrix models does not give the right class of algebras (see (Font, Verdú, 1991)). It was the example that motivated the systematic study in (Font, Jansana, 1986) of another kind of models for sentential logics considered first by Suszko (Brown, Suszko, 1973): abstract logics.

12.2 Positive Modal Logic

It is the {∧, ∨, □, ◊, ⊥, ⊤}-fragment of the local normal modal logic lK. We denote it by PML.

The logic PML is not protoalgebraic, it is selfextensional and it is non-Fregean. Its class of algebras Alg PML is the class of positive modal algebras introduced by Dunn in (Dunn, 1995). The logic is studied in (Jansana, 2002) from the the perspective of algebraic logic. AlgPML is different from Alg*PML. PML has some interest in Computer Science.

12.3 Visser's subintuitionistic logic

This logic is the logic in the language of intuitionistic logic that has to the modal logic K the same relation that intutitionistic logic has to the system of modal logic S4. It was introduced in (Visser, 1981) and has been studied by several authors like Ardeshir, Alizadhe and Ruitenburg. It is not protoalgebraic and is not Fregean.

12.4 The strict implication fragment of the local modal logic lK

The strict implication of the language of modal logic is defined using the □ operator and the material implication →. We will use ⇒ for the strict implication. Its definition is φ ⇒ ψ := □(φ → ψ). The language of the logic SilK we call the strict implication fragment of the local modal logic lK is the language L = {∧, ∨, ⊥, ⊤, ⇒}. We can translate the formulas of L to formulas of the modal language by systematically replacing in a L-formula φ every subformula of the form ψ ⇒ δ by □ (ψ → δ) and repeating the process until no appearence of ⇒ is left. Let us denote by φ* the translation of φ and by Γ* the set of the translations of the formulas in Γ. Then the definition of the consequence relation of SilK is:

Γ ⊢SilK ψ   iff   Γ* ⊢ lK φ*.

The logic SilK is not protoalgebraic. It is selfextensional and non-Fregean. Its class of algebras Alg SilK is the class of bounded distributive lattices with a binary operation with the properties of the strict implication of lK. This class of algebras is introduced and studied in (Celani, Jansana 2005) where it is called the class of Weakly Heyting algebras. Alg SilK does not coincide with Alg* SilK.

13. Abstract logics and generalized matrices

The matrix models of a logic can be thought of as algebraic generalizations of its theories, more precisely, of the Lindenbaum matrices of the logic. They come from a local perspective that is centered around the theories and its analogues, the logic filters, one by one. But, as we will see, the properties of a logic depend in general on the global behaviour of the set of its theories as a bunch, or -to put it otherwise- on its consequence relation due to the duality between the closed sets (the theories) and the consequence operation. To consider this global behaviour introduces a global perspective on the semantics for logic systems. The abstract logics that we are going to define can be seen, in contrast to logical matrices, as algebraic generalizations of the logic itself and its extensions. They are the natural objects to consider when one takes that global perspective seriously.

Let L be a propositional language. An L-abstract logic is a pair A = < A, C > where A is an L-algebra and C an abstract consequence operation on A.

Given a logic L, an L-abstract logic A = < A, C > is a model of L if for every set of formulas Γ and every formula φ

Γ ⊢L φ   iff   for every valuation v on A, v(φ) ∈ C(v[Γ]).

This definition has an equivalent in terms of the closed sets of C: an abstract logic A = < A, C > is a model of L if and only if for every C-closed set X the matrix < A, X > is a model of L.

This observation leads to another point of view on abstract logics as models of a logic system. It transforms them into a collection of logical matrices (given by the closed sets) over the same algebra, or, put more simply, into a pair < A, B > where B is a collection of subsets of A. A structure of this type is called in the literature a generalized matrix (Wójcicki [1973]) and more recently has been called atlas in (Dunn, Hardegree, 2001). It is said to be a model of a logic L if for every X ∈ B, < A, X > is a matrix model of L.

A logic system L = < L, ⊢L > clearly gives an equivalent abstract logic < FmL, C⊢L > and an equivalent generalized matrix < FmL, Th(L) >, where Th(L) is the set of C⊢L-closed sets of formulas, namely the L-theories. We will move freely from one to the other.

The generalized matrices < A, B > that correspond to abstract logics have the properties that A ∈ B and that B is closed under intersections of arbitrary nonempty families. A family B of subsets of a set A with these two properties is known as a closed-set system and also as a closure system. There is a dual correspondence between abstract consequence operations on a set A and closed-set system on A. Given an abstract consequence operation C on A, there is the corresponding closed-set system C(C) of the C-closed sets and given a closed-set system C there is the abstract consequence operation C(C) defined by C(C)(X) = ∩ {Y ∈ C: X ⊆ Y}, for every X ⊆ A. In general, every generalized matrix < A, B > can be turned into a closed-set system by adding to B ∪ {A} the intersections of arbitrary nonempty families, and therefore into an abstract logic, which we denote by < A, C(B)>. In that situation we say that B is a base for C(B). An abstract logic can have more than one base. Any family of closed sets such that every closed set is an intersections of elements of the family is a base. The study of bases for the closed set system of the theories of a logic usually plays an important role in its study. For example, in classical logic an important base for the family of theories is the family of maximal consistent theories and in intuitionistic logic the family of prime theories. In a similar way the systematic study of bases for generalized matrix models of a logic becomes important.

In order to make the exposition smooth we will now move from abstract logics to generalized matrices. Let A = < A, B > be a generalized matrix. There is the greatest congruence of A compatible with all the sets in B. In the literature this congruence is called the Tarski congruence of A. We denote it by Ω̃A(B). It has a characterization using the Leibniz operator

Ω̃A(B) = ∩X ∈ B ΩA(X).

It can also be characterized by the condition:

< a, b > ∈ Ω̃A(B)   iff   for every φ(p, q1, …, qn), every c1, …, cn ∈ A and all X ∈ B
φA[a, c1, …, cn] ∈ X ⇔ φA[b, c1, …, cn] ∈ X

or equivalently by

< a, b > ∈ Ω̃A(B)   iff   for every φ(p, q1, …, qn) and every c1, …, cn ∈ A, C(B)(φA[a, c1, …, cn]) = C(B)(φA[b, c1, …, cn])

A generalized matrix is reduced if its Tarski congruence is the identity. Every generalized matrix < A, B > can be turned into an equivalent reduced one by identifying the elements related by its Tarski congruence; the result is the quotient < A/Ω̃A(B), B/Ω̃A(B) >, where B/Ω̃A(B) = {X/Ω̃A(B): X ∈ B} and for X ∈ B, X/Ω̃A(B) is the set of equivalence classes of the elements of X.

The properties of a logic L depend in general, as we already said, on the global behaviour of the family of its theories. In some logics this behaviour is reflected in the behaviour of its set of theorems, as in classical and intuitionistic logic due to the deduction-detachment property, but this is by no means the most general situation, as it is witnessed by the example of the local and global modal logic of the normal modal logic K: both logics have the same theorems. In a similar way, the properties of a logic are in general better encoded in an algebra-like manner if we consider families of L-filters on the algebras than if we consider a single L-filter as is done in the logical matrix model theory.

The generalized matrix models that have naturally attacted most the attention in the research on the algebraization of logics are the generalized matrices of the form < A, FiLA > where FiLA is the set of all the L-filters of A. For example it is known (see (Czelakowski, 2001)) that for every finitary protoalgebraic logic L, L has the deduction-detachment property if and only if for every algebra A the join-subsemilattice of the lattice of all L-filters of A that consists of the finitely generated L-filters is dually residuated. This is an example of a property of logics encoded in the structure of the lattices of L-filters of the L-algebras.

The generalized matrices of the form < A, FiLA > are called the basic full models of L. The interest in these models lead to a consideration of the class of generalized matrix such that the quotient by its Tarski congruence is a basic full model. These generalized matrices (and their corresponding abstract logics) are called full models. The theory of the full models of an arbitrary logic is developed in (Font, Jansana, 1996). We will mention some of the main results obtained there.

Let L be a logic system.

  1. L is protoalgebraic if and only if for every full model < A, C > there is an L-filter F of A such that C = {G ∈ FiLA: F ⊆ G}.
  2. If L is finitary, L is finitely algebraizable if and only if for every algebra A and every L-filter F of A, the generalized matrix < A, {G ∈ FiLA: F ⊆ G} > is a full model and AlgL is a quasivariety.
  3. The class AlgL is both the class of algebras of the reduced generalized matrix models of L, and the class {A: < A, FiLA > is reduced}.
  4. For every algebra A there is an isomorphism between the family of closed-set systems C on A such that < A, C > is a full model of L and the family of congruences θ of A such that A/θ ∈ AlgL. The isomorphism is given by the Tarski operator that sends a generalized matrix to its Tarski congruence.

This isomorphism theorem (4) is a generalization of the isomorphism theorems we encountered earlier for algebraizable logics. The interesting thing here is that the theorem holds for every logic system. Using (2) it gives the isomorphism theorem for finitary and finitely algebraizable logics. Thus (4) can be seen as the most general formulation of the mathematical logical phenomena that underlies the isomorphism theorems between the congruences of the algebras in a certain class and some kind of subsets of them we mentioned in Section 9.

The use of generalized matrices and abstract logics as models for logic systems has proved very useful for the study of selfextensional logics in general and more in particular for the study of the non-protoalgebraic and selfextensional logics such as the logics in Section 12. In particular, they have proved very useful for the study of the class of finitary selfextensional logics with a conjunction and the class of finitary selfextensional logics with the deduction-detachment property for a single term, say p → q; the logics in this last class are nevertheless protoalgebraic. A logic L has a conjunction if there is a formula in two variables φ(p, q) such that

φ(p, q) ⊢L p,       φ(p, q)⊢L q,       p, q ⊢L φ(p, q)

The logics in those two classes have the following property: for every full model < A, C > its Tarski relation is the relation {< a, b > ∈ A × A: C(a) = C(b)}. A way of saying it is to say that for these logics the property that defines selfextensionality, namely that the interderivability condition is a congruence, lifts or transfers to every full model. The selfextensional logics with this property are called fully selfextensional. This notion was introduced in (Font, Jansana, 1996) under the name 'strongly selfextensional'. All the known and natural selfextensional logics are fully selfextensional, in particular the logics discussed in Section 12, but Babyonyshev showed in (Babyonishev, 2005) an ad hoc example of a selfextensional logic that is not fully selfextensional.

An interesting result on the finitary logics in the classes of fully selfextensional logics with conjunction and the ones with the deduction-detachment property for a single term is that their class of algebras AlgL is always a variety. The researchers in AAL are somehow surprised by the fact that several finitary and finitely algebraizable logics have a variety as its equivalent algebraic semantics, when the theory of algebraizable logics allows us in general to prove only that the equivalent algebraic semantics of a finitary and finitely algebraizable logic is a quasivariety. The result explains this phenomenon for the finitary and finitely algebraizable logics to which it applies. For many other finitary and finitely algebraizable logics to find a convincing explanation is still an open problem.

Every abstract logic A = < A, C > determines a quasi-order (a reflexive and transitive relation) on A. It is the relation defined by

a ≤A b   iff   C(b) ⊆ C(a)   iff   b ∈ C(a)

Thus a ≤A b if and only if b belongs to every C-closed set to which A belongs. For a fully selfextensional logic L this quasi-order turns into a partial order in the reduced full models, which are in fact the reduced basic full models, that is, the abstract logics < A, FiLA > with A ∈ AlgL. Consequently, in a fully selfextensional logic L every algebra A ∈ AlgL carries a partial order definable in terms of the family of the L-filters. If the logic is fully selfextensional with a conjunction this partial order is definable by an equation of the L-algebraic language alone since in this case for every algebra A ∈ AlgL

a ≤ b   iff   C(b) ⊆ C(a)   iff   C(a ∧ b) = C(a)   iff   a ∧ b = a

A similar situation holds for fully selfextensional logics with the deduction-detachment property for a single term, say p → q, for then for every algebra A ∈ AlgL

a ≤ b   iff   C(b) ⊆ C(a)   iff   C(a → b) = C(∅) = C(a → a)   iff   a → b = a → a

These observations lead us to view the finitary fully selfextensional logics L with conjunction and those with the deduction-detachment property for a single term as logics definable by an order which is definable in the algebras in AlgL by using an equation of the L-algebraic language. The following result is known.

Theorem 6. A finitary logic with conjunction L is fully selfextensional iff there is a class of algebras K such that for every A ∈ K the reduct < A, ∧A> is a meet-semilattice and if ≤ is the order of the semilattice then
φ1, …, φn⊢L φ   iff   for all A ∈ K and every valuation v on A v(φ1) ∧A… ∧A v(φn) ≤ v(φ)

and

⊢L φ   iff   for all A ∈ K and every valuation v on A a ≤ v(φ), for every a ∈ A.

Moreover, in this case the class of algebras AlgL is the variety generated by K.

Similar results can be obtained for the selfextensional logics with the deduction-detachment property for a single term. The reader is referred to (Jansana 2006) for a study of the selfextensional logics with conjunction and to (Jansana 2005) for a study of the selfextensional logics with the deduction-detachment property for a single term.

Bibliography

Other Internet Resources

[Please contact the author with suggestions.]

Related Entries

algebra | Boole, George | Boolean algebra: the mathematics of | logic: classical | logic: intuitionistic | logic: linear | logic: many-valued | logic: modal | logic: relevance | logical consequence | model theory: first-order | Tarski, Alfred