## 1. Abstract consequence relations

Tarski’s work (1930a, 1930b, 1935, 1936) on the methodology of

the deductive sciences of the 1920s and 1930s 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; 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 of

formulas (X), a formula (a) is *deducible* in (H) 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) in (H) of (a) with premises

or hypotheses in (X). Let (Cn(X)) be the set of formulas deducible

in (H) from the formulas in (X) taken as premises or hypothesis.

This set is called the set of consequences of (X) (relative to the

logical deduction system (H)). (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 of formulas (X)

- (X subseteq Cn(X))
- (Cn(Cn(X)) = Cn(X))
- (Cn(X) = bigcup{Cn(Y): Y subseteq X, Y textrm{

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 the notion of consequence operation

axiomatically. 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

- if (X subseteq Y subseteq A), then (Cn(X)

subseteq 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 subseteq

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(varnothing) =

varnothing) and (C(X cup Y) = C(X) cup C(Y)) for all (X, Y

subseteq A).

Given a consequence operation (C) on a set (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 (vdash)

between sets of formulas and formulas that satisfies the following

conditions:

- if (a in X), then (X vdash a)
- if (X vdash a) and (X subseteq Y), then (Y vdash a)
- if (X vdash a) and for every (b in X, Y vdash b), then (Y

vdash a).

It is *finitary* if in addition it satisfies

- if (X vdash a), then there is a finite set (Y subseteq X)

such that (Y vdash a).

Given a logical deduction system (H), the relation (vdash)

defined by (X vdash 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 using truth valuations, first-order consequence relation

using structures, intuitionistic consequence relation using 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 the so-called

standard semantics.

In general, an *abstract consequence relation* on a set (A)

(not necessarily the set of formulas of some formal language) is a

relation (vdash) 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 (vdash) is an abstract

consequence relation and (X vdash a) we can say that (X) is a set

of premises or hypothesis with conclusion (a) according to

(vdash) and that (a) follows from (X), or is entailed by (X)

(according to (vdash)). 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 this author.

Consequence operations on a set (A) are in one-to-one correspondence

with abstract consequence relations on (A). The move from a

consequence operation (C) to a consequence relation (vdash_C)

and, conversely, from a consequence relation (vdash) to a

consequence operation (C_{vdash}) is easy and given by the

definitions:

X vdash_C a txtiff a in C(X) textrm{ and } a in C_{vdash}(X) txtiff X vdash a.

]

Moreover, if (C) is finitary, so is (vdash_C) and if (vdash)

is finitary, so is (C_{vdash}).

For a general discussion on logical consequence see the entry

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) respectively, then (b) also follows from (Y). In

propositional logics this boils down to saying that if we uniformly

replace basic sub-sentences of the sentences in (X cup {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

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 gt 0) whether the connective is unary, binary,

ternary, etc. For example ({wedge , vee , rightarrow , bot ,

top }) is (or can be) the language of several logics, like

classical and intuitionistic, ((bot) and (top) are 0-ary and the

other connectives are binary), ({neg , wedge , vee rightarrow ,

Box , Diamond }) is the language of several modal logics, ((neg

, Box , Diamond) are unary and the other connectives binary) and

({ wedge , vee , rightarrow , * , top , bot , 1, 0}) is the

language of many-valued logics and also of a fragment of linear logic

((bot , top , 1), and 0 are propositional constants and the other

symbols binary connectives).

Given a language (L) and a set of propositional variables (V)

(which is disjoint from (L)), the *formulas* of (L), or

(L)-*formulas*, are defined inductively as follows:

- Every variable is a formula.
- Every 0-ary symbol is a formula.
- If (*) is a connective and (n gt 0) is its arity, then for

all formulas (phi_1 ,ldots ,phi_n, * phi_1 ldots phi_n) is

also a formula.

A *substitution* (sigma) 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, (sigma(p)) denotes the formula that the

substitution (sigma) assigns to (p). The result of applying a

substitution (sigma) to a formula (phi) is the formula

(bsigma(phi)) obtained from (phi) by simultaneously replacing

the variables in (phi), say (p_1 , ldots ,p_k), by,

respectively, the formulas (sigma(p_1), ldots ,sigma(p_k)). In

this way a substitution (sigma) gives a unique map (bsigma) from

the set of formulas to itself that satisfies

- (bsigma(p) = sigma(p)), for every variable (p),
- (bsigma(dagger) = dagger), for every 0-ary connective

(dagger), - (bsigma(* phi_1 ldots phi_n) = * bsigma(phi_1)ldots

bsigma(phi_n)), for every connective (*) of arity (n gt 0) and

formulas (phi_1 , ldots ,phi_n).

A formula (psi) is a *substitution instance* of a formula

(phi) if there is a substitution (sigma) such that when applied

to (phi) gives (psi), that is, if (bsigma(phi) = psi).

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 (vdash) on the set of

formulas of (L) that is *formal* in the sense that for every

substitution (sigma), every set of formulas (Gamma) and every

formula (phi),

textrm{if } Gamma vdash phi, textrm{ then } bsigma[Gamma] vdashbsigma(phi)

]

where (bsigma[Gamma]) is the set of the formulas obtained by

applying the substitution (sigma) to the formulas in (Gamma).

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 in Łoś & 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 (bL) with possible

subindices, and we set (bL = langle L, vdash_{bL } rangle) and

(bL_n = langle L_n, vdash_{bL_n } rangle) with the

understanding that (L ; (L_n)) is the language of (bL ;(bL_n)) and

(vdash_{bL }; (vdash_{bL_n })) its consequence relation. A logic

system (bL) is *finitary* if (vdash_{bL}) is a finitary

consequence relation.

The consequence relation of a logic system can be given in several

ways, some using proof-theoretic tools, others semantic means. One can

define a substitution-invariant consequence relation using a proof

system like a Hilbert-style axiom system, a Gentzen-style sequent

calculus or a natural deduction style calculus, etc. One can also

define a substitution-invariant consequence relation semantically

using a class of mathematical objects (algebras, Kripke models,

topological models, etc.) and a satisfaction relation.

If (bL_1 = langle L,vdash_{bL_1 } rangle) is a logic system

with (vdash_{bL_1}) defined by a proof-system and (bL_2 =

langle L, vdash_{bL_2 } rangle) is a logic system over the same

language with (vdash_{bL_2}) defined semantically, we say that the

proof-system used to define (vdash_{bL_1}) is *sound* for

the semantics used to define (vdash_{bL_2}) if (vdash_{bL_1})

is included in (vdash_{bL_2}), namely if (Gamma vdash_{bL_1 }

phi) implies (Gamma vdash_{bL_2 } phi). If the other inclusion

holds the proof-system is said to be *complete* with respect to

the semantics that defines (vdash_{bL_2}), that is when (Gamma

vdash_{bL_2 } phi) implies (Gamma vdash_{bL_1 } phi).

A set of (L)-formulas (Gamma) is called a *theory* of a

logic system (bL), or (bL)-theory, if it is closed under the

relation (vdash_{bL}), that is, if whenever (Gamma vdash_{bL }

phi) it also holds that (phi in Gamma). In other words, the

theories of (bL) are the closed sets of the consequence operation

(C_{vdash_{ bL}}) on the set of (L)-formulas. In order to

simplify the notation we denote this consequence operation by

(C_{bL}). A formula (phi) is a *theorem* (or validity) of

(bL) if (varnothing vdash_{bL } phi). Then (C_{bL

}(varnothing)) is the set of theorems of (bL) and is the least

theory of (bL). The set of all theories of (bL) will be denoted

by (tTH(bL)).

Given a logic (bL), the consequence operation (C_{bL}) is

substitution-invariant, which means that for every set of

(L)-formulas (Gamma) and every substitution

(sigma,bsigma[C_{bL}(Gamma)] subseteq C_{bL}(bsigma[Gamma])). Moreover,

for every theory (T) of (bL) we have a new consequence operation

defined as follows:

that is, (C_{bL }^T (Gamma)) is

the set of formulas that follow from (Gamma) and (T) according to

(bL). It turns out that (T) is closed under substitutions if and

only if (C_{bL }^T) is substitution-invariant.

If (bL) is a logic and (Gamma , Delta) are sets of

(L)-formulas, we will use the notation (Gamma vdash_{bL }

Delta) to state that for every (psi in Delta , Gamma

vdash_{bL } psi). Thus (Gamma vdash_{bL } Delta) if and only

if (Delta subseteq C_{bL }(Gamma)).

If (bL = langle L, vdash_{bL } rangle) is a logic system (bL’

= langle L’, vdash_{bL’ } rangle) whose language is (L’) (hence

all the (L’)-formulas are (L)-formulas) and whose consequence

relation is defined by

for every set of (L’)-formulas

(Gamma) and every (L’)-formula (phi). In this situation we

also say that (bL) is an *expansion* of (bL’).

## 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 ((phi * psi)) instead of

(* phi psi) for binary connectives and omit the external

parenthesis in the formulas.

### 3.1 Classical propositional logic

We take the language of Classical propositional logic (bCPL) to be

the set (L_c = {wedge , vee , rightarrow , top , bot },)

where

(wedge , vee , rightarrow) are binary connectives and (top , bot)

propositional constants. We

assume the consequence relation defined by the usual truth-table

method ((top) is interpreted as true

and (bot) as false), that is,

(Gamma vdash_{bCPL } phitxtiff) every truth valuation that

assigns true to all (psi in Gamma)

assigns true to (phi).

The formulas (phi) such that (varnothing vdash_{bCPL } phi)

are the *tautologies*. Note that using the language (L_c),

the negation of a formula (phi) is defined as (phi rightarrow

bot). 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

same as that of classical propositional logic, namely the set

({wedge , vee , rightarrow , top , bot }). The consequence

relation is defined by the following Hilbert-style calculus.

#### Axioms:

All the formulas of the forms

- C0. (top)
- C1. (phi

rightarrow(psi rightarrow phi)) - C2. (phi

rightarrow(psi rightarrow(phi wedge psi))) - C3. ((phi wedge

psi) rightarrow phi) - C4. ((phi wedge

psi) rightarrow psi) - C5. (phi

rightarrow(phi vee psi)) - C6. (psi

rightarrow(phi vee psi)) - C7. ((phi vee psi)

rightarrow((phi rightarrow delta) rightarrow((psi rightarrow

delta) rightarrow delta))) - C8. ((phi

rightarrow psi) rightarrow((phi rightarrow(psi rightarrow

delta)) rightarrow(phi rightarrow delta))) - C9. (bot rightarrow

phi)

#### Rule of inference

[phi , phi rightarrow psi / psi tag{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 (L_m =

{wedge , vee , rightarrow , neg , Box , top , bot }) that

expands (L_c) by adding the unary connective (Box). 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 (Lambda) of formulas of

(L_m) which contains all the tautologies of the language of

classical logic, the formulas of the form

and is closed

under the rules

begin{align*}

phi , phi rightarrow psi / psi tag{Modus Ponens}\

phi / Box phi tag{Modal Generalization}\

phi/ bsigma(phi), textrm{ for every substitution } sigma tag{Substitution}\

end{align*}

]

Note that the set (Lambda) is closed under substitution instances,

namely for every substitution (sigma), if (phi in L_m), then

(bsigma(phi) in L_m).

The least normal modal logic is called (K) and can be axiomatized by

the Hilbert-style calculus with axioms the tautologies of classical logic

and the formulas (Box(phi rightarrow psi) rightarrow(Box phi

rightarrow Box psi)), and with rules of inference Modus Ponens,

Modal Generalization and Substitution.

With a normal modal logic (Lambda) it is associated the consequence

relation defined by the calculus that takes as axioms all the formulas

in (Lambda) and as the only rule of inference Modus Ponens. The

logic system given by this consequence relation is called the

*local consequence* of (Lambda). We denote it by

(blLambda). Its theorems are the elements of (Lambda). It holds

that

(Gamma vdash_{blLambda} phitxtiffphi in Lambda) or there are

(phi_1 , ldots ,phi_n in Gamma) such that ((phi_1 wedge

ldots wedge phi_n) rightarrow phi in Lambda).

### 3.4 Global Normal Modal logics

Another consequence relation is associated with each normal modal

logic (Lambda). It is defined by the calculus that has as axioms

the formulas of (Lambda) and as rules of inference Modus Ponens and

Modal Generalization. The logic system given by this consequence

relation is called the *global consequence* of (Lambda) and

will be denoted by (bgLambda). It has the same theorems as the

local (blLambda), namely the elements of (Lambda). The

difference between (blLambda) and (bgLambda) lies in the

consequences they allow to draw from nonempty sets of premises. This

difference has an enormous effect on their algebraic behavior.

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 ({wedge , vee , rightarrow , * , 0, 1, top

, bot }), where (wedge , vee , rightarrow, *) are binary connectives and (0, 1,top , bot)

propositional constants. We denote the logic by (bILL). The axioms and rule of

inference below provide a Hilbert-style axiomatization of this logic.

#### Axioms:

- L1. 1
- L2. ((phi

rightarrow psi) rightarrow((psi rightarrow delta)

rightarrow(phi rightarrow delta))) - L3. ((phi

rightarrow(psi rightarrow delta)) rightarrow(psi

rightarrow(phi rightarrow delta))) - L4. (phi

rightarrow(psi rightarrow(phi * psi))) - L5. ((phi

rightarrow(psi rightarrow delta)) rightarrow((phi * psi)

rightarrow delta)) - L6. (1

rightarrow(phi rightarrow phi)) - L7. ((phi wedge

psi) rightarrow phi) - L8. ((phi wedge

psi) rightarrow psi) - L9. (psi

rightarrow(phi vee psi)) - L10. (phi

rightarrow(phi vee psi)) - L11. (((phi

rightarrow psi) wedge(phi rightarrow delta)) rightarrow(phi

rightarrow(psi wedge delta))) - L12. (((phi

rightarrow delta) wedge(psi rightarrow delta)) rightarrow((phi

vee psi) rightarrow delta)) - L13. (phi

rightarrow top) - L14. (bot

rightarrow psi)

#### Rules of inference:

[begin{align*}

phi , phi rightarrow psi / psi tag{Modus Ponens}\

phi , psi / phi wedge psi tag{Adjunction}\

end{align*}

]

The 0-ary connective 0 is used to define a negation by (neg phi :=

phi rightarrow 0). No specific axiom schema deals with 0.

For more information, see the entry on

linear logic

### 3.6 The system (bR) of Relevance Logic

The language we consider is the set ({wedge , vee , rightarrow ,

neg }), where (wedge , vee , rightarrow) are binary connectives and (neg) a unary connective. A Hilbert style axiomatization for (bR) can be given by

the rules of Intuitionistic Linear Logic without exponentials and the

axioms L2, L3, L7-L12 of this logic together with the axioms

- ((phi rightarrow(phi rightarrow psi)) rightarrow(phi

rightarrow psi)) - ((phi rightarrow neg psi) rightarrow(psi rightarrow neg

psi)) - ((phi wedge(psi vee delta)) rightarrow((phi wedge psi)

vee phi wedge delta))) - (neg neg phi rightarrow phi)

For more information, see the entry on

relevance logic.

## 4. Algebras

The algebraic study of a particular logic has to provide first of all

its formal language 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 address 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 (also called function symbols), if any, in the set

of 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) (thus every 0-ary symbol of (L) is taken as an

individual constant) and that (ii) the propositional formulas of (L)

are taken as the terms of this first-order language; in particular the

propositional variables are the variables of the first-order language.

From this point of view the definition of (L)-formula is exactly the

definition of (L)-term. We will refer to the algebraic language with

(L) as its set of operation symbols as the (L)-*algebraic
language*.

The *second step* is to interpret the propositional formulas in

the same manner 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 (langle a_1 , ldots

,a_nrangle) 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* (bA) of

type (L), or (L)-algebra for short, is a set (A), called the

carrier of (bA), together with a function (* ^{bA}) on (A) of

the arity of (*), for every connective (*) in (L) (if (*) is

0-ary, (* ^{bA}) is an element of (A)). An algebra (bA) is

*trivial* if its carrier is a one element set.

A *valuation* on an (L)-algebra (bA) 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 (bA) by the function (* ^{bA}). Let (bA) be

an algebra of type (L) and (v) a valuation on (bA). The value

of a compound formula (* phi_1 ldots phi_n) is computed by

applying the function (* ^{bA}) that interprets (*) in (bA) to

the previously computed values (bv(phi_1), ldots ,bv(phi_n)) of

the formulas (phi_1 ,ldots ,phi_n). Precisely speaking the value

(bv(phi)) of a formula (phi) is defined inductively as

follows:

- (bv(p) = v(p)), for each variable (p),
- (bv(dagger) = dagger^{bA}), if (dagger) is a 0-ary

connective - (bv(* phi_1 ldots phi_n) = * ^{bA }(bv(phi_1), ldots

,bv(phi_n))), if (*) is a (n)-ary ((n gt 0))

connective.

Note that in this way we have obtained a map (bv) from the set of

(L)-formulas to the carrier of (bA). It is important to notice

that the value of a formula under a valuation depends only on the

propositional variables that actually appear in the formula.

Accordingly, if (phi) is a formula we use the notation (phi(p_1 ,

ldots ,p_n)) to indicate that the variables that appear in (phi)

are in the list (p_1 , ldots ,p_n), and given elements (a_1 ,

ldots ,a_n) of an algebra (bA) by (phi^{bA }[a_1 , ldots

,a_n]) we refer to the value of (phi(p_1 , ldots ,p_n)) under any

valuation (v) on (bA) such that (v(p_1) = a_1 , ldots ,v(p_n) =

a_n).

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

(bFm_L). This algebra has the set of (L)-formulas as carrier and

the operations are defined as follows. For every (n)-ary connective

(*) with (n gt 0), the function (* ^{bFm_L}) is the map that

sends each tuple of formulas ((phi_1 , ldots ,phi_n)) (where

(n) is the arity of (* )) to the formula (* phi_1 ldots

phi_n), and for every 0-ary connective (dagger ,

dagger^{bFm_L}) is (dagger). If no confusion is likely we

suppress the subindex in (bFm_L) and write (bFm) 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 (bA) of type (L), a *congruence* of

(bA) is an equivalence relation (theta) on the carrier of

(bA) that satisfies for every (n)-ary connective (* in L) the

following compatibility property: for every (a_1 , ldots ,a_n, b_1 ,

ldots ,b_n in A),

textrm{if } a_1theta b_1 , ldots ,a_n theta b_1, textrm{ then } *^{bA}(a_1 ,ldots ,a_n) theta *^{bA}(b_1 ,ldots ,b_n).

]

Given a congruence (theta) of (bA) we can reduce the algebra by

identifying the elements which are related by (theta). The algebra

obtained is the *quotient algebra* of (bA) modulo

(theta). It is denoted by (bA/theta), its carrier is the set

(A/theta) of equivalence classes ([a]) of the elements (a) of

(A) modulo the equivalence relation (theta), and the operations

are defined as follows:

- (dagger^{bA/theta} = [dagger^{bA}]), for every 0-ary

connective (dagger), - (* ^{bA/theta}([a_1], ldots, [a_n]) = [* ^{bA }(a_1 ,ldots

,a_n)]), for every connective (*) whose arity is (n) and (n gt

0).

The compatibility property ensures that the definition is sound.

Let (bA) and (bB) be (L)-algebras. A *homomorphism*

(h) from (bA) to (bB) is a map (h) from (A) to (B) such

that for every 0-ary symbol (dagger in L) and every (n)-ary

connective (* in L)

- (h(dagger^{bA }) = dagger^{bB})
- (h(* ^{bA }(a_1 ,ldots ,a_n)) = * ^{bB }(h(b_1),ldots

,h(b_n))), for all (a_1 , ldots ,a_n in A).

We say that (bB) is a *homomorphic image* of (bA) if

there is a homomorphism from (bA) to (bB) which is an onto map

from (A) to (B). An homomorphism from (bA) to (bB) is an

*isomorphism* if it is a one-to-one and onto map from (A) to

(B). If an isomorphism from (bA) to (bB) exists, we say that

(bA) and (bB) are *isomorphic* and that (bB) is an

*isomorphic image* (or a copy) of (bA).

Let (bA) and (bB) be (L)-algebras. (bA) is a

*subalgebra* of (bB) if (1) (A subseteq B), (2) the

interpretations of the 0-ary symbols of (L) in (bB) belong to

(A) and (A) is closed under the functions of (bB) that

interpret the non 0-ary symbols, and (3) the interpretations of the

0-ary symbols in (bA) coincide with their interpretations in

(bB) and the interpretations on (bA) of the other symbols in

(L) are the restrictions to (bA) of their interpretations in

(bB).

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.

The theory of varieties and quasivarieties is one of the main subjects

of universal algebra.

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

(phi approx psi) where (phi) and (psi) are terms of the

(L)-algebraic language (that is, (L)-formulas if we take the

propositional logics point of view). An equation (phi approx psi)

is *valid* in an algebra (bA), or (bA) is a

*model* of (phi approx psi), if for every valuation (v)

on (bA, bv(phi) = bv(psi)). This is exactly the same as to

saying that the universal closure of (phi approx psi) is a

sentence true in (bA) 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 a

given 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 in varieties. A *proper (L)-quasiequation*

is a formula of the form

An (L)-*quasiequation*

is a formula of the above form but possibly with an empty antecedent,

in which case it is just the equation (phi approx psi). Hence,

the (L)-quasiequations are the proper (L)-quasiequations and the

(L)-equations. An (L)-quasiequation is *valid* in an

(L)-algebra (bA), or the algebra is a model of it, if the

universal closure of the quasiequation is sentence true in (bA). A

*quasivariety* of (L)-algebras is a class of algebras which

is the class of the models of a given 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 (bK) of

(L)-algebras is the least class of (L)-algebras that includes

(bK) 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 (bK). 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

(top) and (bot), 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, ultraproducts, isomorphic

images, and contains a trivial algebra. The quasivariety generated by

a class (bK) of (L)-algebras is the least class of (L)-algebras

that includes (bK), the trivial algebras and is closed under

subalgebras, direct products, ultraproducts, and isomorphic images.

An SP-*class* of (L)-algebras is a class of (L)-algebras

that contains a trivial algebra and is closed under isomorphic images,

subalgebras, and direct products. Thus quasivarieties and varieties

are all SP-classes. The SP-class generated by a class (bK) of

(L)-algebras is the least class of (L)-algebras that includes

(bK), the trivial algebras and is closed under subalgebras, direct

products and isomorphic images.

## 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 (under a

valuation) in an algebra of the class and prove a soundness and

completeness theorem, usually for the theorems of the logic only.

Nowadays there is a precise concept of algebraic semantics for a logic

system. It was introduced by Blok and Pigozzi in Blok & Pigozzi

1989. In this concept 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 (bA) has a

greatest element according to their natural order; this element is

denoted usually by (1^{bA}) and interprets the propositional

constant symbol (top). It is taken as the distinguished element

relative to which the algebraic semantics is given. The algebraic

semantics of these two logics works as follows:

Let (bL) be classical or intuitionistic logic and let (bK(bL))

be the corresponding class of algebras **BA** or

**HA**. It holds that

(Gamma vdash_{bL } phitxtiff) for every (bA in bK(bL))

and every valuation (v) on (bA), if (bv(psi) = 1^{bA}) for all (psi in Gamma ), then (bv(phi) = 1^{bA}).

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.5

of Intuitionistic Linear Logic without exponentials. We denote by

(bILsubZ) the class of IL-algebras with zero defined in Troelstra

1992 (but adapted to the language of (bILL)). Each (bA in

bILsubZ) is a lattice with extra operations and thus has its lattice

order (le^{bA}). This lattice order has a greatest element which

we take as the interpretation of (top). On each one of these

algebras (bA) there is a designated element (1^{bA}) (the

interpretation of 1) that may be different from the greatest element.

It holds:

(Gamma vdash_{bILL } phitxtiff) for every (bA in bILsubZ)

and every valuation (v) on (bA), if (1^{bA } le^{bA } bv(psi)) for all (psi in Gamma ), then (1^{bA } le^{bA }

bv(phi)).

In this case one does not consider only a designated element in every

algebra (bA) but a set of designated elements, namely the elements

of (bA) greater than or equal to (1^{bA}), to provide the

definition. Let us denote this set by (tD (bA)), and notice that

(tD (bA) = {a in A: 1^{bA } wedge^{bA} a = 1^{bA }}).

Hence,

(Gamma vdash_{bILL } phitxtiff) for every (bA in bILsubZ)

if (bv[Gamma] subseteq tD (bA)), then (bv(phi) in tD

(bA)).

Still there are even more complex situations. One of them is the

system (bR) of relevance logic. Consider the class of algebras

(bRal) defined in Font & Rodríguez 1990 (see also Font

& Rodríguez 1994) and denoted there by

‘(bR)’. Let us consider for every (bA in bRal) the

set

Then (bRal) is said to be an algebraic semantics

for (bR) because the following holds:

(Gamma vdash_{bR } phitxtiff) for every (bA in bRal) and

every valuation (v) on (bA), if (bv[Gamma] subseteq tE

(bA)), then (bv(phi) in tE (bA)).

The common pattern in the examples above is that the algebraic

semantics is given by

- a class of algebras (bK),
- in each algebra in (bK) a set of designated elements that plays

the role (1^{bA}) (more precisely the set ({1^{bA }})) plays

in the cases of classical and intuitionistic logic, and - 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 of the algebra that satisfy the equation (i.e., its

solutions). For**BA**and**HA**the

equation is (p approx top). For (bRal) it is (p rightarrow(p

wedge p) approx p rightarrow p), and for (bILsubZ) it is (1

wedge p approx 1).

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 researchers 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 we need to

introduce a notational convention. Given an algebra (bA) and a set

of equations (iEq) in one variable, we denote by (iEq(bA)) the

set of elements of (bA) that satisfy all the equations in (iEq).

Then a logic (bL) is said to have an *algebraic semantics*

if there is a class of algebras (bK) and a set of equations

(iEq) in one variable such that

- (**) ( Gamma

vdash_{bL } phi txtiff) for every (bA in bK) and every

valuation (v) on (bA), if (bv[Gamma] subseteq iEq(bA)),

then (bv(phi) in iEq(bA)).

In this situation we say that the class of algebras (bK) is an

(iEq)-*algebraic semantics* for (bL), or that the pair

((bK, iEq)) is an *algebraic semantics* for (bL). If

(iEq) consists of a single equation (delta(p) approx

varepsilon(p)) we will simply say that (bK) is a (delta(p)

approx varepsilon(p))-algebraic semantics for (bL). In fact,

Blok and Pigozzi required that (iEq) 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 (bK) is an (iEq)-algebraic semantics for a finitary logic

(bL) and (iEq) is finite, then the quasivariety generated by

(bK) is also an (iEq)-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 (iEq)-algebraic

semantics for a finitary (bL) and (iEq) is finite, so is any

subclass of the quasivariety that generates it.

In the best-behaved cases, the typical algebraic semantics of a logic

is a variety, for instance in all the examples discussed above. But

there are cases in which it is not.

A quasivariety can be an (iEq)-algebraic semantics for a logic and

an (iEq’)-algebraic semantics for another logic (with (iEq) and

(iEq’) different). For example, due to Glivenko’s theorem

(see the entry on

intuitionistic logic)

the class of Heyting algebras is a ({neg neg p approx

1})-algebraic semantics for classical logic and it is the standard

({p approx 1})-algebraic semantics for intuitionistic logic.

Moreover, different quasivarieties of algebras can be an

(iEq)-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 approx 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

(blK). Finally, there are logics that do not have any algebraic

semantics.

These facts highlight the need for some criteria of the goodness of a

pair ((bK, iEq)) to provide a natural algebraic semantics for a

logic (bL) when some exists. One such criterion would be that

(bL) is an algebraizable logic with ((bK, iEq)) as an algebraic

semantics. Another that (bK) is the natural class of algebras

associated with the logic (bL). 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 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

one needs for every algebra a set of designated elements that cannot

be defined using only the equations of the algebraic language or is

not even definable by using this language only. As we already

mentioned, one example where this happens 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 together with 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 1920s 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 (langle bA, D

rangle) where (bA) is an algebra and (D) a subset of the

carrier (A) of (bA); the elements of (D) are called the

*designated elements* of the matrix and accordingly (D) is

called *the set of designated elements* (sometimes it is also

called the *truth set* of the matrix). Logical matrices were

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 those of 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 Łoś 1949 and

continuing in Łoś & Suszko 1958, building on previous

work by Lindenbaum. In Łoś and Suszko’s paper matrices

are used for the first time both as models of logic systems (in our

sense) and to define these kinds of systems.

In the rest of this section, we present the relevant concepts of the

theory of logical matrices using modern terminology.

Given a logic (bL), a logical matrix (langle bA, D rangle) is

said to be a *model* of (bL) if wherever (Gamma

vdash_{bL } phi) then every valuation (v) on (bA) that maps

the elements of (Gamma) to some designated value (i.e., an element

of (D)) also maps (phi) to a designated value. When (langle

bA, D rangle) is a model of (bL) it is said that (D) is an

(bL)-*filter* of the algebra (bA). The set of

(bL)-filters of an algebra (bA) plays a crucial role in the

theory of the algebraization of logic systems. We will come to this

point later.

A class (bM) of logical matrices is said to be a *matrix
semantics* for a logic (bL) if

- (*)( Gamma

vdash_{bL } phitxtiff) for every (langle bA, tD rangle in

bM) and every valuation (v) on (bA), if (bv[Gamma] subseteq

D), then (bv(phi) in D).

The implication from left to right says that (bL) is sound relative

to (bM), and the other implication says that it is complete. In

other words, (bM) is a matrix semantics for (bL) if and only if

every matrix in (bM) is a model of (bL) and moreover for every

(Gamma) and (phi) such that (Gamma notvdash_{bL } phi)

there is a model (langle bA, tD rangle) of (bL) in (bM)

that witnesses the fact, namely there is a valuation on the model that

sends the formulas in (Gamma) to designated elements and (phi)

to a non-designated one.

Logical matrices are also used to define logics semantically. If (cM

= langle bA, D rangle) is a logical matrix, the relation defined

by

(Gamma vdash_{cM } phitxtiff) for every valuation (v) on

(bA) if (bv(psi) in D) for all (psi in Gamma), then

(bv(phi) in D)

is a consequence relation which is substitution-invariant; therefore

(langle L, vdash_{cM } rangle) is a logic system. Similarly, we

can define the logic of a class of matrices (bM) 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

(langle bA, D rangle) is *reduced* if there are no two

different elements of (A) that behave in the same way. We say that

(a, b in A) *behave in the same way* in (langle bA, D

rangle) if for every formula (phi (q, p_1 , ldots ,p_n)) and all

elements (d_1 , ldots ,d_n in A)

Thus (a, b in A)

behave differently if there is a formula (phi(q, p_1 , ldots

,p_n)) and elements (d_1 , ldots ,d_n in A) such that one of

(phi^{bA }[a, d_1 , ldots ,d_n]) and (phi^{bA }[b, d_1 ,

ldots ,d_n]) belongs to (D) but not both. The relation of behaving

in the same way in (langle bA, D rangle) is a congruence relation

of (bA). This relation is known after Blok & Pigozzi 1986, 1989

as the *Leibniz congruence* of the matrix (langle bA, D

rangle) and is denoted by (bOmega_{bA }(D)). It can be

characterized as the greatest congruence relation of (bA) 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 1980s by Blok and Pigozzi.

The reader is referred 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 (cM) can be turned into a reduced matrix by

identifying the elements related by its Leibniz congruence. This

matrix is called the *reduction* of (cM) and is usually

denoted by (cM^*). A matrix and its reduction are models of 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 that have them as their matrix

semantics.

The proof that every logic system has a reduced matrix semantics

(i.e., a matrix semantics consisting of reduced matrices) is as

follows. Let (bL) be a logic system. Consider the matrices

(langle bFm_L, T rangle) over the formula algebra, where (T) is

a theory of (bL). These matrices are known as the *Lindenbaum
matrices* of (bL). It is not difficult to see that the class of

those matrices is a matrix semantics for (bL). Since a matrix and

its reduction are models of the same logics, the reductions of the

Lindenbaum matrices of (bL) constitute a matrix semantics for

(bL) too, and indeed a reduced one. Moreover, any class of reduced

matrix models of (bL) that includes the reduced Lindenbaum matrices

of (bL) is automatically a complete matrix semantics for (bL).

In particular, the class of all reduced matrix models of (bL) is a

complete matrix semantics for (bL). We denote this class by

(bRMatr(bL)).

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 (bRMatr(bL)) plays a

prominent role in the theory of the algebraization of logics and it is

denoted by (bAlg^*bL). It has been considered for a long time the

natural class of algebras that has to be associated with a given logic

(bL) as its algebraic counterpart. 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 (bAlg^*bL) of the corresponding logic

(bL). And in fact the class (bAlg^*bL) coincides with what was

taken to be the natural class of algebras for all the logics (bL)

studied up to the 1990s. In the 1990s, due to the knowledge acquired

of several logics not studied before, some authors proposed another

way to define the class of algebras that has to be counted as the

algebraic counterpart to be associated with a given logic (bL). For

many logics (bL) it leads exactly to the class (bAlg^*bL) but

for others it gives a class that extends it properly. We will see it

in

Section 8.

## 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 (bK) is a (delta(p) approx

varepsilon(p))-algebraic semantics for a logic (bL), namely the

Lindenbaum-Tarski method. It is the standard method used 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 in

Section 8.

The Lindenbaum-Tarski method can be outlined as follows. To prove that

a class of algebras (bK) is a (delta(p) approx

varepsilon(p))-algebraic semantics for a logic (bL) first it is

shown that (bK) gives a sound (delta(p) approx

varepsilon(p))-semantics for (bL), namely that if (Gamma

vdash_{bL } phi), then for every (bA in bK) and every

valuation (v) in (bA) if the values of the formulas in (Gamma)

satisfy (delta(p) approx varepsilon(p)), then the value of

(phi) does too. Secondly, the other direction, that is, the

completeness part, is proved by what is properly known as the

Lindenbaum-Tarski method. This method uses the theories of (bL) 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

(bK) and whose set of designated elements is the set of elements of

the algebra that satisfy (delta(p) approx varepsilon(p)). We

proceed to describe the method step by step.

Let (bL) be one of the logics discussed in the examples in

Section 5.

Let (bK) be the corresponding class of algebras we considered

there and let (delta(p) approx varepsilon(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 (Gamma):

- The theory (C_{bL }(Gamma) = {phi : Gamma

vdash_{bL } phi }) of (Gamma), which we denote by (T), is

considered and the binary relation (theta(T)) on the set of

formulas is defined using the formula (p leftrightarrow q) as

follows: [langle phi , psi rangle in theta(T) txtiff phi leftrightarrow psi in T.] - It is shown that (theta(T)) is a congruence relation

on (bFm_L). The set ([phi]) of the formulas related to the

formula (phi) by (theta(T)) is called the equivalence class of (phi). - A new matrix (langle bFm/theta(T), T/theta(T)

rangle) is obtained by identifying the formulas related by

(theta(T)), that is, (bFm/theta(T)) is the quotient algebra of

(bFm) modulo (theta(T)) and (T/theta(T)) is the set of

equivalence classes of the elements of (T). Recall that the

algebraic operations of the quotient algebra are defined by: [* ^{bFm/theta(T) }([phi_1],ldots ,[phi_n]) = [* phi_1 ldots phi_n ] dagger^{bFm/theta(T) } = [dagger]] - It is shown that (theta(T)) is a relation compatible

with (T), i.e., that if (langle phi , psi rangle in

theta(T)) and (phi in T), then (psi in T). This implies that [phi in T txtiff [phi] subseteq T txtiff [phi] in T/theta(T).] - It is proved that the matrix (langle bFm/theta(T),

T/theta(T) rangle) is reduced, that (bFm/theta(T)) belongs to

(bK) and that (T/theta(T)) is the set of elements of

(bFm/theta(T)) that satisfy the equation (delta(p) approx

varepsilon(p)) in (bFm/theta(T)).

The proof of the completeness theorem then goes as follows.

(4)

and

(5)

imply that for every formula (psi , Gamma vdash_{bL } psi) if

and only if ([psi]) satisfies the equation (delta(p) approx

varepsilon(p)) in the algebra (bFm/theta(T)). Thus, considering

the valuation (id) mapping every variable (p) to its equivalence

class ([p]), and whose extension (boldsymbol{id}) to the set of

all formulas is such that (boldsymbol{id}(phi) = [phi]) for every

formula (phi), we have for every formula (psi),

(Gamma vdash_{bL } psitxtiffboldsymbol{id}(psi)) satisfies

the equation (delta(p) approx varepsilon(p)) in

(bFm/theta(T)).

Hence, since by

(5)

(bFm/theta(T) in bK), it follows that if (Gamma

notvdash_{bL }phi), then there is an algebra (bA) (namely

(bFm/theta(T))) and a valuation (v) (namely (id)) such that

the elements of (bv[Gamma]) satisfy the equation on (bA) but

(bv(phi)) does not.

The Lindenbaum-Tarski method, when successful, shows that the class of

algebras ({bFm/theta(T): T) is a theory of (bL}) is a

(delta(p) approx varepsilon(p))-algebraic semantics for (bL).

Therefore it also shows that every class of algebras (bK) which is

(delta(p) approx varepsilon(p))-sound for (bL) and includes

({bFm/theta(T): T) is a theory of (bL}) is also a (delta(p)

approx varepsilon(p))-algebraic semantics for (bL).

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.

- Conditions

(4)

and

(5)

imply that (theta(T)) is in fact the Leibniz congruence of

(langle bFm_L, T rangle). - When the Lindenbaum-Tarski method succeeds, it usually holds that

in every algebra (bA in bK), the relation defined by the equation [delta(p leftrightarrow q) approx varepsilon(p leftrightarrow q),]which is the result of replacing in (delta(p) approx

varepsilon(p)) the letter (p) by the formula (p leftrightarrow

q) that defines the congruence relation of a theory, is the identity

relation on (A). - For every formula (phi), the formulas (delta(p/phi)

leftrightarrow varepsilon(p/phi)) and (phi) are interderivable

in (bL) (i.e., (phi vdash_{bL } delta(p/phi) leftrightarrow

varepsilon(p/phi)) and (delta(p/phi) leftrightarrow

varepsilon(p/phi) vdash_{bL } phi)).

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 (bL) is

algebraizable if it has an algebraic semantics ((bK, iEq)) such

that (1) (bK) is included in the natural class of algebras

(bAlg^*bL) associated with (bL) and (2) the fact that ((bK,

iEq)) 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 discuss the two definitions that have been considered as

providing natural classes of algebras associated with a logic (bL).

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 in them the specific

way in which the relation (theta(T)) is defined in the

Lindenbaum-Tarski method is disregarded.

It has to be remarked that, nonetheless, for many logics both

definitions lead to the same class. But the classes obtained from both

definitions have been considered in the algebraic studies of many

particular logics (for some logics one, for others the other) the

natural class that deserves to be studied.

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 (bAlg^*bL); that its definition is

a generalization of the Lindenbaum-Tarski method comes from the

realization that the relation (theta(T)), associated with an (bL)-theory, defined in the different

completeness proofs in the literature that use the Lindenbaum-Tarski

method is in fact the Leibniz congruence of the matrix (langle

bFm_L, T rangle) and that therefore the matrix (langle

bFm/theta(T), T/theta(T) rangle) is its reduction. As we

mentioned in

Section 6,

for every logic (bL) every (bL)-sound class of matrices (bM)

that contains all the matrices (langle bFm/bOmega_{bFm_L }(T), T/

bOmega_{bFm_L }(T) rangle), where (T) is a theory of (bL), is

a complete reduced matrix semantics for (bL). From this perspective

the notion 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 (bAlg^*bL) of the algebras of the

reduced matrix models of a logic (bL) is the natural class of

algebras to associate with (bL). It is the class

({bA/bOmega_{bA }(F): bA) is an (bL)-algebra and (F) is a

(bL)-filter of (bA}).

The second way of generalizing the Lindenbaum-Tarski method uses

another fact, namely that in the examples discussed in

Section 3

the relation (theta(T)) is also the relation

(Omega^{sim}_{bFm_L }(T)) defined by the condition

langle phi , psi rangle in bOmega^{sim}_{bFm_L }(T)txtiff & forall T’ in tTH(bL),\

& forall p in V, \

&forall gamma(p) in bFm_L (T subseteq T’ Rightarrow (gamma(p/phi) in T’ Leftrightarrow gamma(p/psi) in T’)).

end{align*}]

For every logic (bL) and every (bL)-theory (T) the relation

(bOmega^{sim}_{bFm_L }(T)) defined in this way is the greatest

congruence compatible with all the (bL)-theories that extend (T).

Therefore it holds that

where (tTH(bL)^T = {T’ in

tTH(bL): T subseteq T’}). The relation (bOmega^{sim}_{bFm_L

}(T)) is known as the *Suszko congruence* of (T) (w.r.t.

(bL)). Suszko defined it—in an equivalent way—in

1977.

For every logic (bL), the notion of the Suszko congruence can be

extended to its matrix models. The *Suszko congruence* of a

matrix model (langle bA, D rangle) of (bL) (w.r.t. (bL)) is

the greatest congruence of (bA) compatible with every

(bL)-filter of (bA) that includes (D), that is, it is the

relation given by

where (tFi_{bL}(bA)^D = {D’: D’)

is a (bL)-filter of (bA) and (D subseteq D’}). Notice that

unlike the intrinsic notion of Leibniz congruence, the Suszko

congruence of a matrix model of (bL) is not intrinsic to the

matrix: it depends in an essential way on the logic under

consideration. The theory of the Suszko congruence of matrices has

been developed in Czelakowski 2003 and recently in Albuquerque &

Font & Jansana 2016.

In the same manner that the concept of Leibniz congruence leads to the

concept of reduced matrix, the notion of Suszko congruence leads to

the notion of Suszko-reduced matrix. A matrix model of (bL) is

*Suszko-reduced* if its Suszko congruence is the identity. Then

the class of algebras of the Suszko-reduced matrix models of a logic

(bL) is another class of algebras that is taken as a natural class

of algebras to associate with (bL). It is the class of algebras

(bAlgbL = {bA / {bOmega^{sim}_{bA}}^{bL}(F): bA) is an

(bL)-algebra and (F) is a (bL)-filter of (bA}).

This class of algebras is nowadays taken in abstract algebraic logic

as *the* natural class to be associated with (bL) and it

called its *algebraic counterpart*.

For an arbitrary logic (bL) the relation between the classes

(bAlgbL) and (bAlg^*bL) is that (bAlgbL) is the closure of

(bAlg^*bL) under subdirect products, in particular (bAlg^*bL

subseteq bAlgbL). In general, both classes may be different. For

example, if (bL) is the ((wedge , vee))-fragment of classical

propositional logic, (bAlgbL) is the variety of distributive

lattices (the class that has been always taken to be the natural class

of algebras associated with (bL)) while (bAlg^*bL) is not this

class—in fact it is not a quasivariety. Nonetheless, for

many logics (bL), in particular for the algebraizable and the

protoalgebraic ones to be discussed in the next sections, and also

when (bAlg^*bL) is a variety, the classes (bAlgbL) and

(bAlg^*bL) are equal. This fact can explain 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 logic was not needed and

accordingly it was 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 algebraic counterpart. This

requirement demands that the algebraic counterpart of the logic should

be an algebraic semantics but requires a more robust connection

between the logic and the algebraic counterpart than that. This more

robust connection is present in the best behaved particular logics

known. The mathematically precise concept of algebraizable logic

characterizes this type of link. Blok and Pigozzi introduced that

fundamental concept in Blok & Pigozzi 1989 and its introduction

can be considered the starting point of the unification and growth of

the field of abstract algebraic logic in the 1980s. 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 here the

generalized concept.

We said in

Section 7

that, roughly speaking, a logic (bL) is algebraizable when 1) it

has an algebraic semantics, i.e., a class of algebras (bK) and a

set of equations (iEq(p)) such that (bK) is a (iEq)-algebraic

semantics for (bL, 2)) this fact can be proved by using the

Lindenbaum-Tarski method slightly generalized and, moreover, 3) (bK

subseteq bAlg^*bL). The generalization of the Lindenbaum-Tarski

method (as we described it in

Section 7)

consists in allowing in step (5) (as already done in the definition of algebraic

semantics) a set of equations (iEq(p)) in one variable instead of a

single equation (delta(p) approx varepsilon(p)) and in allowing

in a similar manner a set of formulas (Delta(p, q)) in at most two

variables to play the role of the formula (p leftrightarrow q) in

the definition of the congruence of a theory. Then, given a theory

(T), the relation (theta(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

We need some notational conventions before engaging in the precise

definition of algebraizable logic. Given a set of equations

(iEq(p)) in one variable and a formula (phi), let (iEq(phi))

be the set of equations obtained by replacing in all the equations in

(iEq) the variable (p) by (phi). If (Gamma) is a set of

formulas, let

Similarly, given a set of formulas in two variables (Delta(p, q))

and an equation (delta approx varepsilon), let (Delta(delta ,

varepsilon)) denote the set of formulas obtained by replacing (p)

by (delta) and (q) by (varepsilon) in all the formulas in

(Delta). Moreover, if (iEq) is a set of equations, let

Given a set of equations (iEq(p, q)) in two variables, this set

defines on every algebra (bA) a binary relation, namely the set of

pairs (langle a, brangle) of elements of (A) that satisfy in

(bA) all the equations in (iEq(p, q)). In standard

model-theoretic notation, this set is the relation

The formal definition of algebraizable logic is as follows. A logic

(bL) is *algebraizable* if there is a class of algebras

(bK), a set of equations (iEq(p)) in one variable and a set of

formulas (Delta(p, q)) in two variables such that

- (bK) is an (iEq)-algebraic semantics for

(bL), namely(Gamma vdash_{bL } phitxtiff) for every (bA in bK) and

every valuation (v) on (bA), if (bv[Gamma] subseteq

tEq(bA)), then (bv(phi) in tEq(bA)). - For every (bA in bK), the relation defined by the

set of equations in two variables (iEq(Delta(p, q))) is the

identity relation on (A).

A class of algebras (bK) for which there are sets (iEq(p)) and

(Delta(p, q)) with these two properties is said to be an

*equivalent algebraic semantics* for (bL). The set of

formulas (Delta) is called a *set of equivalence formulas*

and the set of equations (iEq) a *set of defining
equations*.

The conditions of the definition imply:

- (p) is inter-derivable in (bL) with the set of

formulas (Delta(iEq)), that is[Delta(iEq) vdash_{bL } p textrm{ and } p vdash_{bL } Delta(iEq).]

- For every (bL)-theory (T), the Leibniz congruence

of (langle bFm_L, Trangle) is the relation defined by (Delta(p,

q)), namely [langle phi , psi rangle in bOmega_{bFm }(T)txtiffDelta(p/phi , q/psi) subseteq T.] - If (Delta) and (Delta ‘) are two sets of

equivalence formulas, (Delta vdash_{bL } Delta ‘) and (Delta ‘

vdash_{bL } Delta). Similarly, if (iEq(p)) and (iEq'(p)) are

two sets of defining equations, for every algebra (bA in bK,

iEq(bA) = iEq'(bA)). - The class of algebras (bAlg^*bL) also satisfies

conditions

(1)

and

(2),

and hence it is an equivalent algebraic semantics for (bL).

Moreover, it includes every other class of algebras that is an

equivalent algebraic semantics for (bL). Accordingly, it is called

*the greatest equivalent algebraic semantics*of (bL). - For every (bA in bAlg^*bL) there is exactly one

(bL)-filter (F) such that the matrix (langle bA, Frangle) is

reduced, and this filter is the set (iEq(bA)). Or, to put it in

other terms, the class of reduced matrix models of (bL) is

({langle bA, iEq(bA) rangle : bA in bAlg^*bL}). - (bAlg^*bL) is an SP-class and includes any class

of algebras (bK) which is an equivalent algebraic semantics for

(bL). The class (bAlg^*bL) is then the greatest equivalent

algebraic semantics for (bL) and thus it deserves to be called

*the*equivalent algebraic semantics of (bL).

Blok and Pigozzi’s definition of algebraizable logic 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

(Delta) and of defining equations (iEq) can both be taken

finite. And we say that a logic is Blok-Pigozzi algebraizable

(BP-algebraizable) if it is finitary and finitely algebraizable.

If (bL) is finitary and finitely algebraizable, then (bAlg^*bL)

is not only an SP-class, but a quasivariety and it is the quasivariety

generated by any class of algebras (bK) which is an equivalent

algebraic semantics for (bL).

We have just seen that in algebraizable logics the class of algebras

(bAlg^*bL) 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, (bAlg^*bL =

bAlgbL)—this is due to the fact that for any algebraizable

logic (bL, bAlg^*bL) is closed under subdirect products. Hence

for every algebraizable logic (bL) its algebraic counterpart

(bAlgbL) is its greatest equivalent algebraic semantics, whatever

perspective is taken on the generalization of the Lindenbaum-Tarski

method.

Conditions

(1)

and

(2)

of the definition of algebraizable logic (instantiated to (bAlg^*bL)) encode the fact that there

is a very strong link between an algebraizable logic (bL) and its

class of algebras (bAlgbL), so that this class of algebras

reflects the metalogical properties of (bL) by algebraic properties

of (bAlgbL) and conversely.

The definition of algebraizable logic can be stated in terms of

translations between the logic and an equational consequence relation

(vDash_{bK}) associated with any equivalent algebraic semantics

(bK) for it—which is the same relation no matter what equivalent

algebraic semantics we choose.

The equational consequence (vDash_{bK}) of a class of algebras

(bK) is defined as follows.

({phi_i approx psi_i: i in I} vDash_{bK } phi approx

psitxtiff) for every (bA in bK) and every valuation (v) on

(bA), if (bv(phi_i) = bv(psi_i)), for all (i in I), then

(bv(phi) = bv(psi)).

The translations needed are given by the set of defining equations and

the set of equivalence formulas. A set of equations (iEq(p)) in one

variable defines a *translation from formulas to sets of
equations*: each formula is translated into the set of equations

(iEq(phi)). Similarly, a set of formulas (Delta(p, q)) in two

variables defines a

*translation from equations to sets of*

formulas: each equation (phi approx psi) is translated into

formulas

the set of formulas (Delta(phi , psi)).

Condition

(1)

in the definition of algebraizable logic can be reformulated as

and condition

(2)

as

These two conditions imply

- ({phi_i approx psi_i : i in I } vDash_{bK }

phi approx psitxtiffDelta({phi_i approx psi_i : i in I})

vdash_{bL } Delta(phi , psi))

and condition

(3)

above is

Thus an algebraizable logic (bL) is faithfully interpreted in the

equational logic of its 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 its

equivalent algebraic semantics is faithfully interpreted in the logic

(bL) (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

(bL) and its greatest equivalent algebraic semantics is really very

strong and that the properties of (bL) 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 (bAlgbL).

Given an algebraic semantics ((bK, iEq)) for a logic (bL), a

way to stress the difference between it being merely an algebraic

semantics and being an algebraic semantics that makes (bL)

algebraizable is that the translation of formulas into equations given

by the set of equations (iEq) is invertible in the sense that there

is a translation, say (Delta), of equations into formulas given by

a set of formulas in two variables that satisfies condition

(9)

above, and such that (iEq) and (Delta) provide mutually

inverses translations (i.e., conditions

(2)

and

(3)

hold).

The link between an algebraizable logic (bL) and its greatest

equivalent algebraic semantics given by the set of defining equations

and the set of equivalence formulas allows us to prove a series of

general theorems that relate the properties of (bL) with the

properties of (bAlgbL). 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 requires first that a concept of deduction theorem applicable

to any logic has to be defined. A logic (bL) has the

*deduction-detachment property* if there is a finite set of

formulas (Sigma(p, q)) such that for every set of formulas

(Gamma) and all formulas (phi , psi)

Note that this is a generalization of the standard deduction theorem

(the direction from left to right in the above expression) and Modus

Ponens (equivalent to the implication from right to left) that several

logics have for a connective (rightarrow). In those cases

(Sigma(p, q) = {p rightarrow q}).

**Theorem 1.**

A finitary and finitely algebraizable logic (bL) has the

deduction-detachment property if and only if the principal relative

congruences of the algebras in (bAlgbL) 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 (bL) has the *Craig interpolation property*

for the consequence relation if whenever (Gamma vdash_{bL } phi)

there is a finite set of formulas (Gamma)’ with variables

shared by (phi) and the formulas in (Gamma) such that (Gamma

vdash_{bL } Gamma ‘) and (Gamma ‘ vdash_{bL } phi).

**Theorem 2.**

Let (bL) be a finitary and finitely algebraizable logic with

the deduction-detachment property. Then (bL) has the Craig

interpolation property if and only if (bAlgbL) has the

amalgamation property.

Finally, the third theorem concerns 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 (bAlgbL) and morphisms the algebraic homomorphisms are

surjective homomorphisms.

Other results relating properties of an algebraizable logic with a

property of its natural class of algebras can be found in Raftery

2011, 2013. They concern respectively a generalization of the property

of having the deduction-detachment property and the property that

generalize the inconsistency lemmas of classical and intuitionistic

logic. Also an abstract notion of having a theorem like

Glivenko’s theorem relating classical and intuitionistic logic

has been proposed and related to an algebraic property in the case of

algebraizable logics in Torrens 2008.

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 subsets are the lattice

filters and in modal algebras they are the lattice filters that are

closed under the operation that interprets (Box). In all those

cases, the sets are exactly the (bL)-filters of the corresponding

algebraizable logic (bL).

Algebraizable logics can be characterized by the existence of this

kind of isomorphism between congruences and logic filters on the

algebras of their algebraic counterpart. To spell out this

characterization we need a couple of definitions. Let (bL) be a

logic. The *Leibniz operator* on an algebra (bA) (relative

to (bL)) is the map from the (bL)-filters of (bA) to the set

of congruences of (bA) that sends every (bL)-filter (D) of

(bA) to its Leibniz congruence (bOmega_{bA }(D)). We say that

the Leibniz operator of a logic (bL) *commutes with the inverses
of homomorphisms* between algebras in a class (bK) if for every

homomorphism (h) from an algebra (bA in bK) to an algebra (bB

in bK) and every (bL)-filter (D) of (bB, h^{-1}[bOmega_{bB

}(D)] = bOmega_{bA }(h^{-1}[D])).

**Theorem 4.**

A logic (bL) is algebraizable if and only if for every algebra

(bA in bAlgbL) the Leibniz operator commutes with the inverses

of homomorphisms between algebras in (bAlgbL) and is an isomorphism

between the set of all (bL)-filters of (bA), ordered by

inclusion, and the set of congruences (theta) of (bA) such that

(bA/theta in bAlgbL), 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 (bL) of which the class of groups is its

greatest equivalent algebraic semantics and the normal subgroups of a

group are its (bL)-filters.

A different but related characterization of algebraizable logics is

this:

**Theorem 5.**

A logic (bL) is algebraizable if and only if on the algebra of

formulas (bFm_L), the map that sends every theory (T) to its

Leibniz congruence commutes with the inverses

of homomorphisms from (bFm_L) to (bFm_L) and is an isomorphismbetween the set

(tTH(bL)) of theories of (bL), ordered by inclusion, and the

set of congruences (theta) of (bFm_L) such that (bFm_L /theta

in bAlgbL), 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 (blK) and the corresponding global one

(bgk) are not only different, but their metalogical properties

differ. For example (blK) has the deduction-detachment property for

(rightarrow):

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

The logic (bgk) is algebraizable and (blK) is not. The

equivalent algebraic semantics of (bgk) is the variety (bMA) of

modal algebras, the set of equivalence formulas is the set ({p

leftrightarrow q}) and the set of defining equations is ({p

approx top }). Interestingly, (blK) and (bgk) have the same

algebraic counterpart (i.e., (bAlg blK = bAlg blK)), namely, the

variety of modal algebras.

A lesson to draw from this example is that the algebraic counterpart

of a logic (bL), i.e, the class of algebras (bAlgbL), does not

necessarily fully encode the properties of (bL). The class of modal

algebras encodes the properties of (bgk) because this logic is

algebraizable and so the link between (bgk) and (bAlg bgk) is

as strong as possible. But (bAlg blK), the class of modal

algebras, cannot by itself completely encode the properties of

(blK).

What causes this difference between (bgk) and (blK) is that the

class of reduced matrix models of (bgk) is

but the

class of reduced matrix models of (blK) properly includes this

class so that for some algebras (bA in bMA), in addition to

({1^{bA }}) there is some other (blK)-filter (F) with

(langle bA, F rangle) reduced. This fact provides a way to show

that (blK) can not be algebraizable by showing that the

(blK)-filters of the reduced matrices are not equationally

definable from the algebras; if they where, then for every (bA in

bAlg blK) there would exists exactly one (blK)-filter (F) of

(bA) such that (langle bA, F rangle) is reduced.

Nonetheless, we can perform some of the steps of the Lindenbaum-Tarski

method in the logic (blK). We can define the Leibniz congruence of

every (blK)-theory in a uniform way by using formulas in two

variables. But in this particular case the set of formulas has to be infinite.

Let (Delta(p, q) = {Box^n (p leftrightarrow q): n) a natural

number(}), where for every formula (phi , Box^0phi) is

(phi) and (Box^nphi) for (n gt 0) is the formula (phi)

with a sequence of (n) boxes in front ((Box ldots^n ldots Box

phi)). Then, for every (blK)-theory (T) the relation

(theta(T)) defined by

is the Leibniz congruence of (T). In this case, it happens though

that there are two different (blK)-theories with the same Leibniz

congruence, something that does not hold for (bgk).

The logics (bL) with the property that there is a set of formulas

(possibly infinite) (Delta(p, q)) in two variables which defines in

every (bL)-theory (T) its Leibniz congruence, that is, that for

all (L)-formulas (phi , psi) it holds

are known as

the *equivalential logics*. If (Delta(p, q)) is finite, the

logic is said to be *finitely equivalential*. A set (Delta(p,

q)) that defines in every (bL)-theory its Leibniz congruence is

called a *set of equivalence formulas* for (bL). It is clear

that every algebraizable logic is equivalential and that every

finitely algebraizable logic is finitely equivalential.

The logic (blK) is, according to the definition, equivalential, and

it can be shown that it is not finitely equivalential. The local modal

logic **lS**4 is an example of a non-algebraizable logic

that is finitely equivalential. A set of equivalence formulas for

**lS**4 is ({Box(pleftrightarrow q)}).

A set of equivalence formulas for a logic (bL) should be considered

as a generalized biconditional, in the sense that collectively the

formulas in the set have the relevant properties of the biconditional,

for example of classical logic, that makes it suitable to define the

Leibniz congruences of its theories. This comes out very clearly from

the following syntactic characterization of the sets of equivalence

formulas.

**Theorem 6.**

A set (Delta(p, q)) of (L)-formulas is a set of equivalence

formulas for a logic (bL) if and only if

- ((tR_{Delta}))(vdash_{bL

} Delta(p, p)) - ((tMP_{Delta}))(

p, Delta(p, q) vdash_{bL } q) - ((tS_{Delta})) (

Delta(p, q) vdash_{bL } Delta(q, p)) - ((tT_{Delta}))(

Delta(p, q) cup Delta(q, r) vdash_{bL } Delta(p,

r)) - ((tRe_{Delta}))(

Delta(p_1, q_1) cup ldots cup Delta(p_n, q_n) vdash_{bL }

Delta(* p_1 ldots p_n, * q_1 ldots q_n)), for every connective

(*) of (L) of arity (n) greater that 0.

There is some redundancy in the theorem. Conditions

((tS_{Delta})) and ((tT_{Delta})) follow from

((tR_{Delta}),(tMP_{Delta})) and ((tRe_{Delta})).

Equivalential logics were first considered as a class of logics

deserving to be studied in Prucnal & Wroński 1974, and they

have been studied extensively in Czelakowski 1981; see also

Czelakowski 2001.

We already mentioned that the algebraizable logics are equivalential.

The difference between an equivalential logic and an algebraizable one

can be seen in the following syntactic characterization of

algebraizable logics:

**Theorem 7.**

A logic (bL) is algebraizable if and only if there exists a

set (Delta(p, q)) of (L)-formulas and a set (iEq(p)) of

(L)-equations such that the conditions

((tR_{Delta}))–((tRe_{Delta})) above hold for

(Delta(p, q)) and

The set (Delta(p, q)) in the theorem is then an equivalence set of

formulas for and the set (iEq(p)) a set of defining equations.

There are logics that are not equivalential but have the property of

having a set of formulas ([p Rightarrow q]) which collectively

behave in a very weak sense as the implication (rightarrow) does in

many logics. Namely, it has the properties ((tR_{Delta})) and

((tMP_{Delta})) in the syntactic characterization of a set of

equivalence formulas, i.e.,

- ((tR_{Rightarrow})) (vdash_{bL

} [p Rightarrow p]) - ((tMP_{Rightarrow}))

(p, [p Rightarrow q] vdash_{bL } q)

If a logic is finitary and has a set of formulas with these

properties, there is always a finite subset with the same properties.

The logics with a set of formulas (finite or not) with properties

(1)

and

(2)

above are called *protoalgebraic*. in particular, 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 in

Blok & Pigozzi 1986. The label ‘protoalgebraic logic’

is due to these last two 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 and many methods

of universal algebra can be adapted to its study; consequently the

algebraic study of protoalgebraic logics using their matrix semantics

has been extensively and very fruitfully pursued. But, as we will see,

some interesting logics are not protoalgebraic.

An important characterization of protoalgebraic logics is via the

behavior of the Leibniz operator. The following conditions are

equivalent:

- (bL) is protoalgebraic.
- The Leibniz operator (bOmega_{bFm_L}) is monotone on the set

of (bL)-theories with respect to the inclusion relation, that is,

if (T subseteq T’) are (bL)-theories, then (bOmega_{bFm_L

}(T) subseteq bOmega_{bFm_L }(T’)). - For every algebra (bA), the Leibniz operator (bOmega_{bA})

is monotone on the set of (bL)-filters of (bA) with respect to

the inclusion relation.

Due to the monotonicity property of the Leibniz operator, for any

protoalgebraic logic (bL) the class of algebras (bAlg^*bL) is

closed under subdirect products and therefore it is equal to

(bAlgbL). Hence for protoalgebraic logics the two ways we

encountered to associate a class of algebras with a logic produce, as

we already mentioned, the same result.

There are also characterizations of equivalential and finitely

equivalential logics by the behavior of the Leibniz operator. The

reader is referred to Czelakowski 2001 and Font & Jansana &

Pigozzi 2003.

In his Raftery 2006b, Raftery studies Condition 7 in the list of

properties of an algebraizable logic we gave just after the

definition. The condition says:

For every (bA in bAlg^*bL) the class of reduced matrix models of

(bL) is ({langle bA, iEq(bA) rangle : bA in

bAlg^*bL}), where (iEq(p)) is the set of defining equations for

(bL).

The logics with a set of equations (iEq(p)) with this property,

namely such that for every (bA in bAlg^*bL) the class of reduced

matrix models of (bL) is ({langle bA, iEq(bA) rangle : bA

in bAlg^*bL}), are called *truth-equational*, a name

introduced in Raftery 2006b. Some truth-equational logics are

protoalgebraic but others are not. We will see later an example of the

last situation.

The protoalgebraic logics that are truth-equational are in fact the

*weakly algebraizable logics* studied already in Czelakowski

& Jansana 2000. Every algebraizable logic is weakly algebraizable.

In fact, the algebraizable logics are the equivalential logics that

are truth-equational. But not every weakly algebraizable logic is

equivalential. An example is the quantum logic determined by the

ortolattices, namely by the class of the matrices (langle bA, {1}

rangle) where (bA) is an ortolattice and 1 is its greatest

element (see Czelakowski & Jansana 2000 and Malinowski 1990).

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

its members are classes of logics that can be characterized by the

behavior of the Leibniz operator. We described only the most important

classes of logics in the hierarchy. The reader is referred to

Czelakowski 2001, Font 2016b, Font, Jansana & Pigozzi 2003, and

Font 2016b for more information. In particular, 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 summarized in the following diagram:

Figure. The Leibniz Hierarchy

Recently the Leibniz hierarchy has been refined in Cintula &

Noguera 2010, 2016. The idea is to consider instead of sets of

equivalence formulas (Delta) (that correspond to the biconditional)

sets of formulas ([pRightarrow q]) with properties of the

conditional ((rightarrow)), among which ((R_{Rightarrow})) and

((MP_{Rightarrow})), and such that the set ([pRightarrow q]
cup[pRightarrow q]) is a set of equivalence formulas. New classes

arise when the set ([pRightarrow q]) has a single element.

## 11. Replacement principles

Two classes of logics that are not classes of the Leibniz hierarchy

have been extensively studied in abstract algebraic logic. They are

defined from a completely different perspective from the one provided

by the behavior 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 (bL) might

have, shared for example by classical logic, intuitionistic logic and

all its axiomatic extensions, says that for any set of formulas

(Gamma), any formulas (phi , psi , delta) and any variable

(p)

if (Gamma , phi vdash_{bL } psi) and (Gamma , psi

vdash_{bL } phi), then (Gamma , delta(p/phi) vdash_{bL }

delta(p/psi)) and (Gamma , delta(p/psi) vdash_{bL }

delta(p/phi)),

where (delta(p/phi)) and (delta(p/psi)) are the formulas

obtained by substituting respectively (phi) and (psi) for (p)

in (delta). This replacement property is taken by some authors as

the formal counterpart of Frege’s principle of compositionality

for truth. Logics satisfying this strong replacement property are

called *Fregean* in Font& Jansana 1996 and are thoroughly studied in

Czelakowski & Pigozzi 2004a, 2004b.

Many important logics do not satisfy the 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

(phi , psi , delta),

if (phi vdash_{bL }psi) and (psi vdash_{bL }phi), then

(delta(p/phi) vdash_{bL } delta(p/psi)) and (delta(p/psi)

vdash_{bL } delta(p/phi)).

A logic satisfying this weaker replacement property is called

*selfextensional* by Wójcicki (e.g., in Wójcicki

1969, 1988) and *congruential* in Humberstone 2005. We will use

the first terminology because it seems more common—at least in

the abstract algebraic logic literature.

Selfextensional logics have a very good behavior from several points

of view. Their systematic study started in Wójcicki 1969 and

has recently been continued in the context of abstract algebraic logic

in Font & Jansana 1996; Jansana 2005, 2006; and Jansana &

Palmigiano 2006.

There are selfextensional and non-selfextensional logics in any one of

the classes of the Leibniz hierarchy and also in the class of

non-protoalgebraic logics. These facts show 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 to a large extent different. Nonetheless, one of the trends of

today’s research in abstract algebraic logic is to determine 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 (bL)

satisfies the strong replacement principle if and only if for every

(bL)-theory (T) its Suszko congruence is the interderivability

relation relative to (T), namely the relation ({langle phi ,

psi rangle : T, phi vdash_{bL } psi) and (T, psi vdash_{bL

} phi }). And a logic (bL) satisfies the weak replacement

principle if and only if the Suszko congruence of the set of theorems

of (bL) is the interderivability relation ({langle phi , psi

rangle : phi vdash_{bL } psi) and (psi vdash_{bL } phi

}).

## 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 (blK) 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 in logical matrix model theory.

### 12.1 The logic of conjunction and disjunction

This logic is the ({wedge , vee , bot , top })-fragment of

Classical Propositional Logic. Hence its language is the set

({wedge , vee , top , bot }) and its consequence relation is

given by

It turns out that it is also the ({wedge , vee , bot , top

})-fragment of Intuitionistic Propositional Logic. Let us denote it

by (bL^{{wedge , vee }}).

The logic (bL^{ {wedge , vee }}) is not protoalgebraic but it

is Fregean. Its classes of algebras (bAlg^*bL^{ {wedge , vee

}}) and (bAlgbL^{ {wedge , vee }}) are different. Moreover,

(bAlgbL^{{wedge , vee }}) is the variety of bounded

distributive lattices, the class of algebras naturally expected to be

the associated with (bL^{ {wedge , vee }}), but (bAlg^*bL^{

{wedge , vee }}) is strictly included in it. In fact, this last

class of algebras is not a quasivariety, but it is first-order

definable still.

The logic (bL^{{wedge , vee }}) is thus a natural example of a logic

where the class of algebras of its reduced matrix models is not the

right class of algebras expected to correspond to it (see Font &

Verdú 1991 where the logic is studied at length). The

properties of this example and its treatment in Font &

Verdú 1991 motivated the systematic study in Font & Jansana

1996 of the kind of

models for sentential logics considered in Brown & Suszko 1973,

namely, abstract logics.

### 12.2 Positive Modal Logic

Positive Modal Logic is the ({wedge , vee , Box , Diamond , bot

, top })-fragment of the local normal modal logic (blK). We

denote it by (bPML). This logic has some interest in Computer

Science.

The logic (bPML) is not protoalgebraic, it is not truth-equational,

it is selfextensional and it is not Fregean. Its algebraic counterpart

(bAlg bPML) is the class of positive modal algebras introduced by

Dunn in Dunn 1995. The logic is studied in Jansana 2002 from the

perspective of abstract algebraic logic. The class of algebras

(bAlgbPML) is different from (bAlg^*bPML).

### 12.3 Visser’s subintuitionistic logic

This logic is the logic in the language of intuitionistic logic that

has to the least normal modal logic (K) the same relation that

intuitionistic logic has to the normal modal logic (S4). It was

introduced in Visser 1981 (under the name Basic Propositional Logic)

and has been studied by several authors, such as Ardeshir, Alizadeh,

and Ruitenburg. It is not protoalgebraic, it is truth-equational and

it is Fregean (hence also selfextensional).

### 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 (Box) operator and the material implication (rightarrow). We

will use (Rightarrow) for the strict implication. Its definition is

(phi Rightarrow psi := Box(phi rightarrow psi)). The language

of the logic (bSilK), that we call the strict implication fragment

of the local modal logic (blK), is the language (L = {wedge ,

vee , bot , top , Rightarrow }). We can translate the formulas

of (L) to formulas of the modal language by systematically replacing

in an (L)-formula (phi) every subformula of the form (psi

Rightarrow delta) by (Box(psi rightarrow delta)) and

repeating the process until no appearance of (Rightarrow) is left.

Let us denote by (phi^*) the translation of (phi) and by

(Gamma^*) the set of the translations of the formulas in

(Gamma). Then the definition of the consequence relation of

(bSilK) is:

The logic (bSilK) is not protoalgebraic and is not

truth-equational. It is selfextensional but it is not Fregean. Its

algebraic counterpart (bAlg bSilK) is the class of bounded

distributive lattices with a binary operation with the properties of

the strict implication of (blK). This class of algebras is

introduced and studied in Celani & Jansana 2005, where its members

are called Weakly Heyting algebras. (bAlg bSilK) does not coincide

with (bAlg^* bSilK).

The logic (bSilK) belongs, as Visser’s logic, to the family

of so-called subintuitionistic logics. A reference to look at for

information on these logics is Celani & Jansana 2003.

## 13. Abstract logics and generalized matrices

The logical matrix models of a given logic can be thought of as

algebraic generalizations of its theories, more precisely, of its

Lindenbaum matrices. They come from taking a local perspective

centered around the theories of the logic considered one by one, and

its analogs the logic filters (also taken one by one). But, as we will

see, the properties of a logic depend in general on the global

behavior of the set of its theories taken together as a bunch;

or—to put it otherwise—on its consequence relation. The

consideration of this global behavior introduces a global perspective

on the design of 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 the global

perspective seriously.

Let (L) be a propositional language. An (L)-*abstract
logic* is a pair (cA = langle bA), C (rangle) where

(bA) is an (L)-algebra and (C) an abstract consequence

operation on (A).

Given a logic (bL), an (L)-abstract logic (cA = langle bA, C

rangle) is a *model* of (bL) if for every set of formulas

(Gamma) and every formula (phi)

(Gamma vdash_{bL } phitxtiff) for every valuation (v) on

(bA, bv(phi) in C(bv[Gamma])).

This definition has an equivalent in terms of the closed sets of

(C): an abstract logic (cA = langle bA, C rangle) is a model

of (bL) if and only if for every (C)-closed set (X) the matrix

(langle bA, X rangle) is a model of (bL) (i.e., (X) is an

(bL)-filter).

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,

to put it more simply, into a pair (langle bA, cB rangle) where

(cB) 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 it has been called an

*atlas* in Dunn & Hardegree 2001. It is said to be a model

of a logic (bL) if for every (X in cB, langle bA, X rangle)

is a matrix model of (bL).

A logic system (bL = langle L, vdash_{bL } rangle)

straightforwardly provides us with an equivalent abstract logic

(langle bFm_L, C_{vdash_{ bL} } rangle) and an equivalent

generalized matrix (langle bFm_L,tTH(bL) rangle), where

(tTH(bL)) is the set of (C_{vdash_{ bL}})-closed sets of

formulas (i.e., the (bL)-theories). We will move freely from one to

the other.

The generalized matrices (langle bA, cB rangle) that correspond

to abstract logics have the following two properties: (A in cB)

and (cB) is closed under intersections of arbitrary nonempty

families. A family (cB) 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 systems

on (A). Given an abstract consequence operation (C) on (A), the

set (cC_C) of (C)-closed sets is a closed-set system and given a

closed-set system (cC) the operation (C_{cC}) defined by

(C_{cC }(X) = bigcap {Y in cC: X subseteq Y}), for every (X

subseteq A), is an abstract consequence operation. In general, every

generalized matrix (langle bA, cB rangle) can be turned into a

closed-set system by adding to (cB cup {A}) the intersections of

arbitrary nonempty subfamilies, and therefore into an abstract logic,

which we denote by (langle bA, C_{cB }rangle). In that situation

we say that (cB) is a *base* for (C_{cB}). It is obvious

that an abstract logic can have more than one base. Any family of

closed sets with the property that every closed set is an intersection

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 its 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 (cA = langle bA, cB rangle)

be a generalized matrix. There exists the greatest congruence of

(bA) compatible with all the sets in (cB); it is known as the

*Tarski congruence* of (cA). We denote it by

(bOmega^{sim}_{bA }(cB)). It has the following characterization

using the Leibniz operator

It can also be characterized by the condition:

(langle a, b rangle in bOmega^{sim}_{bA }(cB)txtiff) for

every (phi(p, q_1 , ldots ,q_n)), every (c_1 , ldots ,c_n in

A) and all (X in cB)

or equivalently by

(langle a, b rangle in bOmega^{sim}_{bA }(cB)txtiff) for

every (phi(p, q_1 , ldots ,q_n)) and every (c_1 , ldots ,c_n in

A, C_{cB }(phi^{bA }[a, c_1 , ldots ,c_n]) = C_{cB }(phi^{bA

}[b, c_1 , ldots ,c_n])).

A generalized matrix is *reduced* if its Tarski congruence is

the identity. Every generalized matrix (langle bA, cB rangle)

can be turned into an equivalent reduced one by identifying the

elements related by its Tarski congruence. The result is the quotient

generalized matrix (langle bA / bOmega^{sim}_{bA }(cB),

cB/bOmega^{sim}_{bA }(cB) rangle), where

(cB/bOmega^{sim}_{bA }(cB) = {X/bOmega^{sim}_{bA }(cB): X

in cB}) and for (X in cB, X/bOmega^{sim}_{bA }(cB)) is the

set of equivalence classes of the elements of (X).

The properties of a logic (bL) depend in general, as we already

said, on the global behavior of the family of its theories. In some

logics, this behavior is reflected in the behavior 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 logics of the normal modal logic (K). Both have the

same theorems but do not share the same properties. Recall that the

local logic has the deduction-detachment property but the global one

not. In a similar way, the properties of a logic are *in
general* better encoded in an algebraic setting if we consider

families of (bL)-filters on the algebras than if we consider a

single (bL)-filter as it is done in logical matrices model

theory.

The generalized matrix models that have naturally attracted most of

the attention in the research on the algebraization of logics are the

generalized matrices of the form (langle bA, tFi_{bL }bA

rangle) where (tFi_{bL }bA) is the set of all the

(bL)-filters of (bA). An example of a property of logics encoded

in the structure of the lattices of (bL)-filters of the

(L)-algebras is that for every finitary protoalgebraic logic (bL,

bL) has the deduction-detachment property if and only if for every

algebra (bA) the join-subsemilattice of the lattice of all

(bL)-filters of (bA) that consists of the finitely generated

(bL)-filters is dually residuated; see Czelakowski 2001.

The generalized matrices of the form (langle bA, tFi_{bL }bA

rangle) are called the *basic full g-models* of (bL) (the

letter ‘g’ stands for generalized matrix). The interest in

these models lead to the consideration of the class of generalized

matrix models of a logic (bL) with the property that their quotient

by their Tarski congruence is a basic full g-model. These generalized

matrices (and their corresponding abstract logics) are called *full
g-models*. The theory of the full g-models of an arbitrary logic

is developed in Font & Jansana 1996, where the notion of full

g-model and basic full g-model is introduced. We will mention some of

the main results obtained there.

Let (bL) be a logic system.

- (bL) is protoalgebraic if and only if for every full

g-model (langle bA, cC rangle) there exists an (bL)-filter

(F) of (bA) such that (cC = {G in tFi_{bL }bA: F subseteq

G}). - If (bL) is finitary, (bL) is finitely

algebraizable if and only if for every algebra (bA) and every

(bL)-filter (F) of (bA), the generalized matrix (langle bA,

{G in tFi_{bL }bA: F subseteq G} rangle) is a full g-model

and (bAlgbL) is a quasivariety. - The class (bAlgbL) is both the class of algebras of

the reduced generalized matrix models of (bL), and the class

({bA: langle bA, tFi_{bL }bA rangle) is reduced(}). - For every algebra (bA) there is an isomorphism

between the family of closed-set systems (cC) on (A) such that

(langlebA, cCrangle) is a full g-model of (bL) and the family

of congruences (theta) of (bA) such that (bA/theta in

bAlgbL). The isomorphism is given by the Tarski operator that sends

a generalized matrix to its Tarski congruence.

The isomorphism

theorem (4)

above is a generalization of the isomorphism theorems we encountered

earlier for algebraizable logics. What is interesting here is that the

theorem holds for every logic system. Using

(2) above,

theorem (4) entails the isomorphism theorem for finitary and finitely

algebraizable logics. Thus

theorem (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

selextenional logics that are not protoalgebraic such as the logics discused 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 rightarrow q); the logics in

this last class are nevertheless protoalgebraic. A logic (bL) has a

*conjunction* if there is a formula in two variables (phi(p,

q)) such that

The logics in those two classes have the following property: the

Tarski relation of every full g-model (langle bA, C rangle) is

({langle a, b rangle in A times 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 g-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 (Babyonyshev 2003) an

*ad hoc*example of

a selfextensional logic that is not fully selfextensional.

An interesting result on the finitary logics which are fully

selfextensional logics with a conjunction or with the

deduction-detachment property for a single term is that their class of

algebras (bAlgbL) is always a variety. The researchers in abstract

algebraic logic 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 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 area of research.

Every abstract logic (cA = langle bA, C rangle) determines a

quasi-order (a reflexive and transitive relation) on (A). It is the

relation defined by

Thus (a le_{cA } b) if and only if (b) belongs to every

(C)-closed set to which (A) belongs. For a fully selfextensional

logic (bL), this quasi-order turns into a partial order in the

reduced full g-models, which are in fact the reduced basic full

g-models, namely, the abstract logics (langle bA, tFi_{bL }bA

rangle) with (bA in bAlgbL). Consequently, in a fully

selfextensional logic (bL) every algebra (bA in bAlgbL)

carries a partial order definable in terms of the family of the

(bL)-filters. If the logic is fully selfextensional with a

conjunction this partial order is definable by an equation of the

(L)-algebraic language because in this case for every algebra (bA

in bAlgbL) we have:

where (C) is the abstract

consequence operation that corresponds to the closed-set system

(tFi_{bL }bA), and (wedge^{bA}) is the operation defined on

(bA) by the formula that is a conjunction for the logic

(bL).

A similar situation holds for fully selfextensional logics with the

deduction-detachment property for a single term, say (p rightarrow

q), for then for every algebra (bA in bAlgbL)

txtiff \ a rightarrow^{bA } b = a rightarrow^{bA } a.]

These observations lead us to view the finitary fully selfextensional

logics (bL) with a 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 (bAlgbL) by using

an equation of the (bL)-algebraic language. Related to this, the

following result is known.

**Theorem 8.**

A finitary logic (bL) with a conjunction is fully

selfextensional if and only if there is a class of algebras (bK) such that for

every (bA in bK) the reduct (langle A, wedge^{bA }rangle)

is a meet-semilattice and if (le) is the order of the semilattice,

then

(phi_1 , ldots ,phi_nvdash_{bL } phitxtiff) for all (bA in

bK) and every valuation (v) on (bA ; bv(phi_1) wedge^{bA

}ldots wedge^{bA } bv(phi_n) le bv(phi))

and

(vdash_{bL } phitxtiff) for all (bA in bK) and every

valuation (v) on (bA ; a le bv(phi)), for every (a in A).

Moreover, in this case the class of algebras (bAlgbL) is the

variety generated by (bK).

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.

The class of selfextensional logics with a

conjunction includes the so-called logics preserving degrees of truth

studied in the fields of substructural logics and of many-valued

logics. The reader can look at Bou et al. 2009 and the references

therein.

## 14. Extending the setting

The research on logic systems described in the previous sections has

been extended to encompass other consequence relations that go beyond

propositional logics, like equational logics and the consequence

relations between sequents built from the formulas of a propositional

language definable using sequent calculi. The interested reader can

consult the excellent paper Raftery 2006a.

This research arose the need for an, even more, abstract way of

developing the theory of consequence relations. It has lead to a

reformulation (in a category-theoretic setting) of the theory of logic

systems as explained in this entry. The work has been done mainly by

G. Voutsadakis in a series of papers, e.g., Voutsadakis 2002.

Voutsadakis’s approach uses the notion of a pi-institution,

introduced by Fiadeiro and Sernadas, as the analog of the logic

systems in his category-theoretic setting. Some work in this direction

is also found in Gil-Férez 2006. A different approach to a

generalization of the studies encompassing the work done for logic

systems and for sequent calculi is found in Galatos & Tsinakis

2009; Gil-Férez 2011 is also in this line. The work presented

in these two papers originates in Blok & Jónsson 2006. The

Galatos-Tsinakis approach has been recently extended in a way that

also encompasses the setting of Voutsadakis in Galatos &

Gil-Férez 2017.

Another recent line of research that extends the framework described

in this entry develops a theory of algebraization of many-sorted logic

systems using instead of the equational consequence relation of the

natural class of algebras a many-sorted behavioral equational

consequence (a notion coming from computer science) and a weaker

concept than algebraizable logic: behaviorally algebraizable logic.

See Caleiro, Gonçalves & Martins 2009.

## Add Comment