Stanford University

Algebraic Propositional Logic (Stanford Encyclopedia of Philosophy)

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)

  1. (X subseteq Cn(X))
  2. (Cn(Cn(X)) = Cn(X))
  3. (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

  1. 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:

  1. if (a in X), then (X vdash a)
  2. if (X vdash a) and (X subseteq Y), then (Y vdash a)
  3. 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

  1. 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:

  1. Every variable is a formula.
  2. Every 0-ary symbol is a formula.
  3. 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

  1. (bsigma(p) = sigma(p)), for every variable (p),
  2. (bsigma(dagger) = dagger), for every 0-ary connective
    (dagger),
  3. (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:

[C_{bL }^T (Gamma) = C_{bL }(T cup Gamma)]

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

[Gamma vdash_{bL’ } phi txtiff Gamma vdash_{bL } phi,]

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

[Box(phi rightarrow psi) rightarrow(Box phi rightarrow Box psi)]

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

  1. ((phi rightarrow(phi rightarrow psi)) rightarrow(phi
    rightarrow psi))
  2. ((phi rightarrow neg psi) rightarrow(psi rightarrow neg
    psi))
  3. ((phi wedge(psi vee delta)) rightarrow((phi wedge psi)
    vee phi wedge delta)))
  4. (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:

  1. (bv(p) = v(p)), for each variable (p),
  2. (bv(dagger) = dagger^{bA}), if (dagger) is a 0-ary
    connective
  3. (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:

  1. (dagger^{bA/theta} = [dagger^{bA}]), for every 0-ary
    connective (dagger),
  2. (* ^{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)

  1. (h(dagger^{bA }) = dagger^{bB})
  2. (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

[bigwedge_{i le n} phi_i approx psi_i rightarrow phi approx psi.]

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

[tE(bA) := {a in A: a wedge^{bA }(a rightarrow^{bA } a) = a rightarrow^{bA } a}.]

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

  1. a class of algebras (bK),
  2. 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
  3. this set of designated elements is definable (in the same manner
    on every algebra) by an equation in the sense that it is the set of
    elements 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)

[phi^{bA }[a, d_1 , ldots ,d_n] in D txtiff phi^{bA }[b, d_1 , ldots ,d_n] in D.]

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):

  1. 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.]
  2. 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).
  3. 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]]
  4. 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).]
  5. 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.

  1. Conditions
    (4)
    and
    (5)
    imply that (theta(T)) is in fact the Leibniz congruence of
    (langle bFm_L, T rangle).
  2. 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).

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

[begin{align*}
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

[bOmega^{sim}_{bFm_L }(T) = bigcap_{T’ in tTH(bL)^T} bOmega_{bFm_L }(T’)]

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

[{bOmega^{sim}_{bA}}^{bL}(D) = bigcap_{D’ in tFi_{bL}(bA)^D} bOmega_{bA}(D’)]

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

[langle phi , psi rangle in theta(T) txtiff Delta(p/phi , q/psi) subseteq T.]

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

[iEq(Gamma) := bigcup_{phi in Gamma}iEq(phi).]

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

[Delta(iEq) = bigcup_{delta approx varepsilon in iEq} Delta(delta , varepsilon).]

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

[{langle a, b rangle : a, b in A textrm{ and } bA vDash iEq(p, q)[a, b]}.]

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

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

  2. 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:

  1. (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).]

  2. 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.]
  3. 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)).
  4. 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).
  5. 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}).
  6. (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
the set of formulas (Delta(phi , psi)).

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

[Gamma vdash_{bL } phitxtiff iEq(Gamma) vDash_{bK } iEq(phi)]

and condition
(2)
as

[p approx q vDash_{bK } iEq(Delta(p, q)) textrm{ and } iEq(Delta(p, q)) vDash_{bK } p approx q.]

These two conditions imply

  1. ({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

[p vdash_{bL } Delta(iEq(p)) textrm{ and } Delta(iEq(p)) vdash_{bL } p.]

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)

[Gamma cup {phi } vdash_{bL } psitxtiffGamma vdash_{bL } Sigma(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):

[Gamma cup {phi } vdash_{blK } psitxtiff Gamma vdash_{blK } phi rightarrow psi.]

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

[{langle bA, {1^{bA }}rangle : bA in bMA},]

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

[langle phi , psi rangle in theta(T)txtiff {Box^n (phi leftrightarrow psi): n textrm{ a natural number}} subseteq T]

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

[langle phi , psi rangle in bOmega_{bFm }(T)txtiff Delta(phi , psi) subseteq T]

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 lS4 is an example of a non-algebraizable logic
that is finitely equivalential. A set of equivalence formulas for
lS4 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

[p vdash_{bL } Delta(iEq(p)) textrm{ and } Delta(iEq(p)) vdash_{bL } p.]

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:

  1. (bL) is protoalgebraic.
  2. 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’)).
  3. 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:

A diagram of four levels level 1: 'finitely algebraizable' with arrows pointing to level 2 objects: 'finitely equivalential' and 'algebraizable'; both of these have arrows pointing to level 3 object 'equivalential' and the latter also has an arrow pointing to level 3 object 'weakly algebraizable' both level 3 objects have arrows to level 4 object: 'protoalgebraic' and the second also points to 'truth-equational'

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

[Gamma vdash phitxtiffGamma vdash_{bCPL} phi.]

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:

[Gamma vdash_{bSilK } phitxtiffGamma^* vdash_{blK } phi^*.]

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

[bOmega^{sim}_{bA }(cB) = bigcap_{X in cB} bOmega_{bA }(X).]

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)

[phi^{bA }[a, c_1 , ldots ,c_n] in X Leftrightarrow phi^{bA }[b, c_1 , ldots ,c_n] in X]

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.

  1. (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}).
  2. 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.
  3. 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(}).
  4. 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

[phi(p, q) vdash_{bL } p, phi(p, q)vdash_{bL } q, p, q vdash_{bL } phi(p, q).]

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

[a le_{cA } btxtiff C(b) subseteq C(a)txtiff b in C(a).]

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:

[a le btxtiff C(b) subseteq C(a)txtiff C(a wedge^{bA } b) = C(a)txtiff a wedge^{bA } b = a,]

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)

[a le btxtiff C(b) subseteq C(a)txtiff C(a rightarrow^{bA } b) = C(varnothing) = C(a rightarrow^{bA } a)
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.

Follow us