Interpolation in Algebraizable Logics; Semantics for Non-normal Multi-modal Logic

Judit X. Madarász^{∗} Mathematical Institute, Budapest, P.O.Box 127 H-1364 Hungary. e-mail: madarasz@math-inst.hu

ABSTRACT. The two main directions pursued in the present paper are the following.

The first direction was (perhaps) started by Pigozzi in 1969. In [Mak 91] and [Mak 79] Maksimova proved that a normal modal logic (with a single unary modality) has the Craig interpolation property iff the corresponding class of algebras has the superamalgamation property. In this paper we extend Maksimova’s theorem to normal multi-modal logics with arbitrarily many, not necessarily unary modalities, and to not necessarily normal multi-modal logics with modalities of ranks smaller than 2.

To extend the characterization beyond multi-modal logics, we look at arbitrary algebraizable logics. We will introduce an algebraic property equivalent with the Craig interpolation property in algebraizable (and in strongly nice) logics, and prove that the superamalgamation property implies the Craig interpolation property. The problem of extending the characterization result to non-normal non-unary modal logics will be discussed, too.

On the second direction pursued herein: For non-normal modal logic with one unary modality Lemmon [Lem 66] gave a possible worlds semantics. Here we give a more general possible worlds semantics for not necessarily normal multi-modal logics with arbitrarily many not necessarily unary modalities. Strongly related to the above is the theorem, proved e.g. in Jónsson-Tarski [JT 52] and Henkin-Monk-Tarski [HMT 71], that every normal \underline{B}oolean \underline{a}lgebra with \underline{o}perators (BAO) can be represented as a subalgebra of the complex algebra of some relational structure. We extend this result to not necessarily normal BAO’s as follows. We define partial relational structures and show that every not necessarily normal BAO is embeddable into the complex algebra of a partial relational structure. This gives a possible worlds semantics for not necessarily normal multi-modal logics (with arbitrarily many, not necessarily unary modalities).

∗Research supported by Hungarian Scientific Research Foundation OTKA grants No’s F17452, T16448.

1 Introduction

The paper consists of two strongly related parts, Section 3, and Sections 4–6. These are summarized in items 1.1 and 1.2 below respectively.

1.1 Non-normal Semantics

In traditional normal modal logic we have only one unary modality, and it is assumed that the formula □True (“it is necessary that true”) is valid. As we will indicate in Section 2, the omission of this assumption turned out to be well motivated in many applications (e.g. in deontic logic, in logics for computer science). In the case when validity of □True is not assumed, we speak of non-normal modal logics. As opposed to the theory of normal modal logics, the one of non-normal modal logics is not developed yet in great detail. In the present paper we investigate both normal modal logics and non-normal ones, and we do this in the more general framework of multi-modal logics, when the logic is permitted to have an arbitrary number of modalities having arbitrary finite ranks.

For non-normal modal logic with one unary modality, Lemmon [Lem 66] gave a possible worlds semantics. Here we give a more general possible worlds semantics for not necessarily normal multi-modal logics with arbitrarily many not necessarily unary modalities. We will show that this semantics works, that is, that the inference system of basic non-normal multi-modal logic is strongly complete (and strongly sound) with respect to the new semantics. Strongly related to the above is the theorem, proved first by Jónsson and Tarski in [JT 52], that every normal \underline{B}oolean \underline{a}lgebra with \underline{o}perators (BAO) can be represented as a subalgebra of the complex algebra of some relational structure.^{1} In Section 3 we extend this result to not necessarily normal BAO’s, as follows. We define partial relational structures and show that every not necessarily normal BAO is embeddable into the complex algebra of a partial relational structure. As a by-product of this BAO theorem, we obtain the above mentioned possible worlds semantics for not necessarily normal multi-modal logics (with arbitrarily many, not necessarily unary modalities). Restricting the present new semantics to the traditional case, we get back the usual Kripkesemantics.

1.2 Characterizing Interpolation

Throughout this paper, we use methods of algebraic logic for gaining new information about logical systems (logics for short). Roughly speaking, in algebraic logic the following is done. One solves problems in logic by first translating them to algebra; then using the powerful methodology of algebra one solves the translated problem; and then one translates the solutions back to logic. The first step in algebraic logic is that, to any logic L, one associates a class Alg(L) of algebras (this can be done under relatively weak conditions on L, see e.g. Andréka et al. [AKNS 94], Blok-Pigozzi [BP 89], [BP], Henkin-Monk-Tarski [HMT 85] Chapter 4.3). For example, if L is a multi-modal logic then Alg(L) is a class of BAO’s (a class of similar algebras having a Boolean reduct; the extra-Boolean operations correspond to the modalities of L). Then one builds a kind of “bridge” between logic (where L “lives”) and algebra (where Alg(L) “lives”) by, e.g. proving theorems of the following kind:

1It is a theorem of algebraic logic that completeness theorems of logics correspond to (are equivalent with) representation theorems in algebra, cf. e.g. [AKNS 94].

Logic L has property P iff the class Alg(L) of algebras has property alg(P)

where alg(P) is a natural algebraic property. More on this subject can be found, e.g. in the Introduction of Andréka et al. [AKNS 94] and in Blok-Pigozzi [BP 89], [BP].

In Sections 4–6 we prove (or state) equivalence theorems of the above kind. Namely, in [Mak 91] and [Mak 79] Maksimova proved that a normal modal logic (with one unary modality) has the Craig interpolation property iff the corresponding class of algebras has the superamalgamation property. (These notions will be recalled below.) One of the first results of this type (involving Craig property and amalgamation) was obtained by Don Pigozzi, cf. [Pig 72], but this research area goes back to works of Jónsson, Daigneault and others around the 1960’s cf. [Pig 72], [Mar 95] and [Mad b] for more history. Here, we extend Maksimova’s theorem to normal multi-modal logics with arbitrarily many, not necessarily unary modalities, and to not necessarily normal multimodal logics with modalities of ranks smaller than 2.

We will briefly look into the problem of generalizing this characterization from (non-normal, multi etc.) modal logics to arbitrary logical systems. To this end, we need a definition of an “arbitrary logical system”, and we adopt the use of the fairly general notion of strongly nice logics introduced, e.g. in [AKNS 94] (or equivalently the notion of algebraizable logics of Blok & Pigozzi). For the reader not familiar with strongly nice logics we wrote the paper in such a way that it is understandable if the reader substitutes “algebraizable logic” in the sense of Blok-Pigozzi [BP 89], [BP] for every occurrence of strongly nice logic. (All the proofs go through for algebraizable logics, too.)

We will introduce an algebraic property which is equivalent with the Craig interpolation property in so called strongly nice logics, and prove that the superamalgamation property always implies the Craig interpolation property in strongly nice logics.

In the last section we announce some further, related results.

On the structure of this paper:

Section 2 contains definitions of our general notion of a logic (“strongly nice logic” or equivalently “algebraizable logic” ), of multi-modal logic, and Boolean algebras with operators (BAO’s).

Section 3 is devoted to elaborating possible world semantics for non-normal multi-modal logics.

Section 4 is devoted to the superamalgamation property of classes of algebras.

Section 5 studies Craig’s interpolation property and its characterizability via the superamalgamation property.

Section 6 contains related results and some open problems.

2 Strongly Nice Logic, Multi-modal Logic and Boolean Algebras with Operators BAO’s

2.1 Logic, Strongly Nice Logic

First we recall some definitions from Font-Jansana [FJ],[FJ 94], Gabbay [Gab 94] or equivalently from Andréka et al. [AKNS 94].

We start with introducing a general concept of a logic and some variants of it. Roughly speaking, a logic L is a five-tuple

L = ⟨F_{L}, ⊢_{L}, M_{L}, mng_{L}, ⊧_{L}⟩ ,

where

• F_{L} is a set, called the set of all formulas of L;

• ⊢_{L} is a binary relation between sets of formulas and individual formulas, that is, ⊢_{L}⊆ P(F_{L}) × F_{L} (for any set X, P(X) denotes the powerset of X); ⊢_{L} is called the provability relation of L;

• M_{L} is a class, called the class of all models (or possible worlds) of L;

• mng_{L} is a function with domain F_{L} × M_{L}, called the meaning function of L;

• ⊧_{L} is a binary relation, ⊧_{L}⊆ M_{L} × F_{L}, called the validity relation of L;

• there is some connection between ⊧_{L} and mng_{L}, namely for all φ, ψ ∈ F_{L} and M ∈ M_{L} we have

[mng_{L}(φ, M) = mng_{L}(ψ, M) and M ⊧_{L} φ] ⟹ M ⊧_{L} ψ . (∗)

Intuitively, F_{L} is the collection of “texts” or “sentences” or “formulas” that can be “said” in the language L. For Γ ⊆ F_{L} and φ ∈ F_{L}, the intuitive meaning of Γ ⊢_{L} φ is that φ is provable (or derivable) from Γ with the syntactic inference system (or deductive mechanism) of L. In all important cases, ⊢_{L} is subject to certain (well-known) conditions like Γ ⊢_{L} φ and Γ ∪ {φ} ⊢_{L} ψ imply Γ ⊢_{L} ψ for any Γ ⊆ F_{L} and φ, ψ ∈ F_{L}. The meaning function tells us what the texts belonging to F_{L} mean in the possible worlds from M_{L}.^{2}

The validity relation tells us which texts are “true” in which possible worlds (or models) under what conditions. In all the interesting cases the relation ⊧_{L} is definable from mng_{L}. A typical possible definition of ⊧_{L} from mng_{L} is the following.

M ⊧_{L} φ iff (∀ψ ∈ F_{L})[mng_{L}(ψ, M) ⊆ mng_{L}(φ, M)],  (∗∗)

for all φ ∈ F_{L}, M ∈ M_{L}. However, in general, definability of ⊧_{L} from mng_{L} is not required (condition (∗∗) above is not a definition).

When no confusion is likely, we omit the subscripts L from F_{L}, ⊢_{L} etc. Usually F_{L} and ⊢_{L} are defined by what is called a grammar in mathematical

linguistics. ⟨F_{L}, ⊢_{L}⟩ together with the grammar defining them is called the syntactical part of L, while ⟨M_{L}, mng_{L}, ⊧_{L}⟩ is the semantical part of L.

When defining a logic, a typical definition of F has the following recursive form. Two sets, P and Cn(L) are given; P is called the set of primitive or atomic formulas, and Cn(L) is called the set of logical connectives of L (these are operation symbols with finite or infinite ranks). Then we require F to be the smallest set H satisfying

(1) P ⊆ H, and

(2) for every φ_{1},…, φ_{n} ∈ H and f ∈ Cn(L) of rank n, f(φ_{1},…, φ_{n}) ∈ H. For example, in classical propositional logic, if p is some propositional variable (atomic formula according to our terminology), then (¬p) is defined to be a formula (where ¬ is a logical connective of rank 1).

For formulas φ ∈ F and models M ∈ M, mng(φ, M) and M ⊧ φ are defined in uniform ways (by some finite “schemas”).

Given a logic L, for φ ∈ F_{L} we say that φ is valid (in L), in symbols ⊧_{L} φ, iff (∀M ∈ M_{L})M ⊧ φ. For φ as above and Γ ⊆ F_{L} we say that φ is a semantical consequence of Γ, in symbols

Γ ⊧_{L} φ, iff (∀M ∈ M_{L})[(∀ψ ∈ Γ)M ⊧_{L} ψ ⟹ M ⊧_{L} φ].

(We hope that the traditional double use of symbol ⊧ does not cause real ambiguity.) One of the important topics of Logic is the study of the connection between semantic consequence Γ ⊧_{L} φ and the syntactic consequence Γ ⊢_{L} φ. If the two coincide then ⊢_{L} is said to be strongly complete and sound for ⊧_{L}.

2For fixed φ ∈ F_{L} and M ∈ M_{L}, mng_{L}(φ, M) is called meaning or intension of expression φ in model (or “possible environment” or “possible interpretation”) M. The literature makes subtle distinctions between these words. We deliberately ignore these distinctions, because on the present level of abstraction they are not relevant yet.

Sometimes it is inconvenient to define a logic by fixing all ingredients of the above mentioned five-tuple L = ⟨F_{L}, ⊢_{L}, M_{L}, mng_{L}, ⊧_{L}⟩. In such cases, two different traditions are followed.

(i) The syntactical tradition. Here the syntactical part L = ⟨F_{L}, ⊢_{L}⟩ is called a logic, and then the (omitted) semantical part ⟨M_{L}, mng_{L}, ⊧_{L}⟩ is called a possible semantics for the (syntactical) logic L.

(ii) The semantical tradition. The semantical part together with the set F_{L} of formulas, i.e. the four tuple ⟨F_{L}, M_{L}, mng_{L}, ⊧_{L}⟩ is called a logic, and then the (omitted) syntactical part ⊢_{L} is called a possible provability relation for L. In this tradition, ⊢_{L} is usually considered together with the inference system or grammar defining ⊢_{L}. Then it is referred to as a possible inference system for L.

In the semantical tradition, if ⊢_{L} coincides with ⊧_{L} then we say that the inference system defining L is complete for L. In the syntactical tradition, in the same case we say that the possible semantics ⟨M_{L}, mng_{L}, ⊧_{L}⟩ is complete for the syntactical logic L.

As it was already indicated, below we will recall from Font-Jansana [FJ 94], [FJ], Gabbay [Gab 94] or Andréka et al. [AKNS 94] a rather general concept of a logic, i.e. that of a “strongly nice logic”. For those readers who are more familiar with the Blok-Pigozzi approach (cf. e.g. [BP 89], [BP]) we note, that algebraizable logics in the sense of the Blok-Pigozzi works are equivalent with that of strongly nice ones, at least from the point of the view of the present work cf. Font-Jansana [FJ 94], [FJ]. In particular, all the proofs and theorems herein remain true for algebraizable logics in place of strongly nice (or strongly nice general) logics.

DEFINITION 2.1 (Def.3.1.1 in [AKNS 94], strongly nice logic) Let L = ⟨F, M, mng, ⊧⟩ be a logic. We say that L is a strongly nice logic if conditions (1–4) below hold for L.

(1) A set Cn(L), called the set of logical connectives of L, is fixed. Every c ∈ Cn(L) has finite rank.

There is a set P, such that F is the smallest set satisfying conditions (a-b) below.

(a) P ⊆ F

(b) if c ∈ Cn(L), c is k-ary and φ_{1},…, φ_{k} ∈ F then c(φ_{1},…, φ_{k}) ∈ F. This set P is called the set of atomic formulas (or parameters or propositional variables). The word-algebra^{3} generated by P, using the logical connectives from Cn(L) as algebraic operations, is denoted by F, that is, F = ⟨F, c⟩_{c∈Cn(L)}. F is called the formula algebra of L.

3or, equivalently, absolutely free algebra

(2) The function mng_{M} =^{def} ⟨mng(φ, M) : φ ∈ F ⟩ is a homomorphism from F, for every M ∈ M.

(3) There are “derived” connectives ε_{0} ,…, ε_{m−1} and δ_{0}, …, δ_{m−1} (unary) and Δ_{0}, …, Δ_{n−1} (binary) (m, n ∈ ω) of L with the following properties:

(i) (∀M ∈ M)(∀φ, ψ ∈ F)[mng_{M}(φ) = mng_{M}(ψ) ⟺ (∀i < n)M ⊧ φΔ_{i}ψ].

(ii) (∀M ∈ M)(∀φ ∈ F)[M ⊧ φ ⟺ (∀j < m)(∀i < n)M ⊧ ε_{j}(φ)Δ_{i}δ_{j}(φ)].

By “derived” we mean that ε_{j}, δ_{j} and Δ_{i} are not necessarily members of Cn(L).^{4}

(4) (∀s ∈ ^{P} F)(∀M ∈ M)(∃N ∈ M)(∀φ(p_{i_{0}},…, p_{i_{k}}) ∈ F)

nmg_{N} (φ) = mng_{M}(φ(p_{i_{0}}/s(p_{i_{0}}),…, p_{i_{k}}/s(p_{i_{k}}))).  (+)

Let \overline{s} ∈ ^{F} F be the natural extension of s to F. Then (+) says mng_{N} (φ) = mng_{M}(\overline{s}(φ)). If this property holds, then we say that the logic “L has the semantical substitution property” (the model N is the substituted version of M along substitution s).

The works of Blok & Pigozzi call logics satisfying conditions (1), (2), and (4) above structural logics. <

REMARK 2.2 (i) An equivalent of condition (4) above is a very natural condition

(∀M ∈ M)(∀h ∈ Hom(F, mng_{M}(F)))(∃N ∈ M) mng_{N} = h.

(ii) To illustrate condition (3) of Def.2.1, we note that, in the case of classical propositional logic, for the choice n = 1, m = 1, Δ_{0} =↔, ε_{0}(φ) = T rue, δ_{0}(φ) = φ, (3) gives the conditions

(∀M ∈ M)(∀φ, ψ ∈ F)(mng_{M}(φ) = mng_{M}(ψ) ⟺ M ⊧ φ ↔ ψ)
(∀M ∈ M)(∀φ ∈ F)(M ⊧ φ ⟺ M ⊧ φ ↔ T rue).
<

CONVENTION 2.3 (logic in the syntactical sense) As outlined in item (i) above Definition 2.1, a logic L in the syntactical sense (cf. Blok-Pigozzi [BP 89], [BP] p.6, Andréka et al. [AKNS 94], Wójcicki [Wój 88] pp. 45–46 (item 1.6.1 d (or b)) is identified with a consequence relation ⊢_{L} between P(F_{L}) and F_{L} (where F_{L} is the set of all formulas of L). In more detail, ⊢_{L} ⊆ P(F_{L}) × F_{L} satisfying condition (i) below due to Tarski.

(i) For any Γ, Δ ⊆ F_{L} and φ ∈ F_{L},

φ ∈ Γ ⟹ Γ⊢_{L}φ; and
[Γ⊢_{L}φ and (∀ψ ∈ Γ) Δ⊢_{L}ψ] ⟹ Δ⊢_{L}φ.
<

4A derived connective is always specified by a formula from F (algebraically speaking it is a term function).

DEFINITION 2.4 (algebraic counterpart of a logic)

Let L = ⟨F, M, mng, ⊧⟩ be a logic satisfying conditions (1),(2) of Definition 2.1. Let K ⊆ M. Then for every φ, ψ ∈ F

φ ∼_{K} ψ ⟺^{def} (∀M ∈ K) mng_{M}(φ) = mng_{M}(ψ).

Then ∼_{K} is a congruence relation on the formula algebra F (by condition (2) of Def.2.1). F/ ∼_{K} denotes the factor-algebra of F, factorized by ∼_{K}. Now

Alg(L) =^{def} I{F/ ∼_{K} : K ⊆ M},

where for any class K of algebras IK denotes the class of isomorphic copies of members of K.

<

DEFINITION 2.5 (Def.3.2.13 in [AKNS 94], general logic) A general logic is a class

L =^{def} ⟨L^{P} : P is a set⟩,

where for each set P, L^{P} = ⟨F^{P} , M^{P} , mng^{P} , ⊧^{P} ⟩ is a logic in the above sense. L is called a strongly nice general logic iff conditions (1–4) below hold for L.

(1) L^{P} is a strongly nice logic (cf. Def.2.1) for each set P, and P is the set of atomic formulas of logic L^{P}.

(2) For any sets P and Q, Cn(L^{P}) = Cn(L^{Q}) =^{def}: Cn(L). The “special” connectives ε_{j}, δ_{j} and Δ_{i} are the same for any logic L^{P} (cf. Def.2.1 (3)).

(3) For any sets P, Q, if there is a bijection f : P ⟶ Q then logic L^{Q} is an “isomorphic copy” of logic L^{P}, i.e. there are bijections f^{F} : F^{P} ⟶ F^{Q} and f^{M} : M^{P} ⟶ M^{Q} such that

(a) f^{F} is an isomorphism from F^{P} onto F^{Q} extending f;

(b) for all φ ∈ F^{P} , M ∈ M^{P} we have

mng^{P} (φ, M) = mng^{Q}(f^{F} (φ), f^{M}(M))
M ⊧^{P} φ ⟺ f^{M}(M) ⊧^{Q} f^{F} (φ).

(4) For all sets P ⊆ Q,

{mng_{M}^{P} : M ∈ M^{P} } = {(mng_{M}^{Q})⌈F^{P} : M ∈ M^{Q}}.
<

DEFINITION 2.6 (algebraic counterpart of a general logic) Let L = ⟨L^{P} : P is a set⟩ be a strongly nice general logic. Then

Alg(L) =^{def} ⋃{Alg(L^{P}) : P is a set}.
<

THEOREM 2.7 Let L be a strongly nice logic or a strongly nice general logic, and let φ ∈ F. Let m, ε_{j}, δ_{j} (j < m) be as in Def.2.1 (3). Then

⊧_{L} φ  iff  Alg(L) ⊧ ε_{j}(φ) = δ_{j}(φ), for all j < m.

Proof: This is an easy consequence of Theorem 3.1.11 and Corollary 3.2.2 from [AKNS 94].

2.2 Multi-modal Logics and their Connection with BAO’s

We will recall from the literature two notions of central importance. These are multi-modal logics (not necessarily normal) and Boolean algebras with operators (BAO’s). We will see after Def.2.11 that there is a very strong connection between modal logics and BAO’s. Namely, let L be a (not necessarily normal) multi-modal logic. Then V(Alg(L)) ⊆ BAO. In the other direction, every BAO variety coincides with V(Alg(L)) for some multi-modal logic L. Here V(Alg(L)) denotes the variety (equational class) generated by Alg(L). A multi-modal logic L is normal iff Alg(L) consists of normal BAO’s.

DEFINITION 2.8 (propositional multi-modal formulas)

(1) By a (multi-) modal similarity type (type for short) we mean a pair ⟨I, ρ⟩ where ρ is a function, ρ : I ⟶ ω (ω denotes the set of all natural numbers).

(2) Let t = ⟨I, ρ⟩ be an arbitrary but fixed type. Propositional multi-modal formulas of type t are built up from

• a set P (called the set of propositional variables);

• the set of Boolean connectives {∨, ¬, T rue}; and

• the set {◇_{i} : i ∈ I} of logical connectives. The connectives ◇_{i} are called modalities, and ρ(i) is called the rank of ◇_{i} (for any i ∈ I).

Now, the set F_{t}^{P} of multi-modal formulas of type t is defined to be the smallest set satisfying conditions (i)–(iii) below.

(i) P ⊆ F_{t}^{P}.
(ii) For every i ∈ I and φ_{0}, φ_{1},…, φ_{ρ(i)−1} ∈ F_{t}^{P} we have
◇_{i}(φ_{0}, φ_{1},…, φ_{ρ(i)−1}) ∈ F_{t}^{P} .
(iii) If φ, ψ ∈ F_{t}^{P} then (¬φ), (φ ∨ ψ) ∈ F_{t}^{P}. T rue ∈ F_{t}^{P}.

(3) Let t, P be as above. We denote the elements of P by lower case p with an index, like p_{k}, p_{i}. When writing multi-modal formulas, we use the usual conventions that are used in classical propositional logic. E.g. we omit parentheses when it causes no confusion (unary logical connectives bind stronger than others); we use the usual derived connectives ∧, →, ↔, F alse in the usual sense; if ◇_{i} is unary, we often write ◇_{i}φ instead of ◇_{i}(φ).

(4) For each modality ◇_{i}, the dual □_{i} of ◇_{i} is defined as follows:

□_{i}(φ_{0}, φ_{1},…, φ_{ρ(i)−1}) =^{def} ¬◇_{i}(¬φ_{0}, ¬φ_{1},…, ¬φ_{ρ(i)−1}).

Here φ_{0}, φ_{1},…, φ_{ρ(i)−1} are formula variables.

<

We will define the notion of a multi-modal logic using the syntactical tradition (outlined in item (i) above Def.2.1, see also Convention 2.3).

DEFINITION 2.9 Assume that a modal similarity type t = ⟨I, ρ⟩ and a set P of propositional variables is given. In the spirit of Convention 2.3, we call L a multi-modal logic of type t iff

• the set of formulas is F_{t}^{P} as defined in Definition 2.8,

• all validities of classical propositional logic as well as Axiom (K)

(K)  □_{i}(p_{0},…, p_{j−1}, p → p′, p_{j+1},…, p_{ρ(i)−1})  ⟶

(□_{i}(p_{0},…, p_{j−1}, p, p_{j+1},…, p_{ρ(i)−1}) → □_{i}(p_{0},…, p_{j−1}, p′, p_{j+1},…, p_{ρ(i)−1}))

for each modality in each of its arguments are derivable from the empty set by ⊢_{L}, and ⊢_{L} is closed under modus ponens φ, (φ → ψ)⊢_{L}ψ, substitution, and the rule (CN) of Conditional Necessitation, recalled below,

(CN)  φ → ψ  ⊢_{L}

□_{i}(φ_{0},…, φ_{j−1}, φ, φ_{j+1},…, φ_{ρ(i)−1}) → □_{i}(φ_{0},…, φ_{j−1}, ψ, φ_{j+1},…, φ_{ρ(i)−1})

for every i ∈ I, and φ, ψ, φ_{0},…, φ_{ρ(i)−1} ∈ F_{t}^{P}, and j < ρ(i).

A normal multi-modal logic is a multi-modal logic, where ⊢_{L} is closed under Necessitation (N) recalled below.

(N) φ ⊢_{L} □_{i}(φ_{0},…, φ_{j−1}, φ, φ_{j+1},…, φ_{ρ(i)−1}),

for every i ∈ I, and φ, φ_{0},…, φ_{ρ(i)−1} ∈ F_{t}^{P}, and j < ρ(i). <

CONVENTION 2.10 In the theorems through the paper we will tacitly assume that the set P of propositional variables is infinite.

<

A logic L = ⟨F, ⊢_{L}⟩ is called compact if (∀Σ ⊆ F)(∀φ ∈ F) (whenever Σ⊢_{L}φ there exists a finite Σ_{0} ⊆ Σ such that Σ_{0}⊢_{L}φ).

We note that compact multi-modal logics are algebraizable in the sense of [BP 89], [BP], and equivalently, they are strongly nice in the sense of Def.2.1 (recalled from [Gab 94], [FJ], [FJ 94], [AKNS 94], [NA 94]).

A difference between [BP 89], [BP] on the one hand, and [AKNS 94], [NA 94], [FJ],[FJ 94] on the other, is that [BP 89], [BP] require (algebraizable) logics to be compact while [AKNS 94], [NA 94], [FJ], [FJ 94] do not require (strongly nice) logics to be such. We follow here the tradition of [AKNS 94], [NA 94], and thus we do not assume compactness, either. In the rest of this paper we will ignore this difference.

The class BAO of Boolean Algebras with Operators and the concept of normal Boolean Algebras with Operators were introduced in [JT 48], cf. also [JT 52], [Ném 91], [Jón 92] and [Sai 82].

Throughout, BA denotes the class of all Boolean algebras.

DEFINITION 2.11 (Boolean algebras with operators, BAO)

(1) Let t = ⟨I, ρ⟩ be a type in the sense of Def.2.8(1). By a Boolean algebra with operators of type t we understand an algebra

A = ⟨A, ∨, −, 1, f_{i}⟩_{i∈I}

such that ⟨A, ∨, −, 1⟩ ∈ BA, and for every i ∈ I, f_{i} distributes over ∨ in every argument, that is, for every i ∈ I and for every k < ρ(i), the following equation holds in A:

(Dst)  f_{i}(x_{0},…, x_{k−1}, x_{k} ∨ x′_{k}, x_{k+1},…, x_{ρ(i)−1})  =

f_{i}(x_{0},…, x_{k−1}, x_{k}, x_{k+1},…, x_{ρ(i)−1}) ∨ f_{i}(x_{0},…, x_{k−1}, x′_{k}, x_{k+1},…, x_{ρ(i)−1}).

Sometimes the property (Dst) is referred to as additivity of f_{i} (this comes from the tradition when the symbol “+” is used for the denoting the Boolean join ∨, cf. e.g. [HMT 71]).

The class of all Boolean algebras with operators of type t is denoted by BAO_{t}. If A ∈ BAO_{t} for some type t = ⟨I, ρ⟩ then its non-Boolean operations f_{i} (i ∈ I) are called its operators. Sometimes we refer to the operators f_{i} as the extra-Boolean operations of A.

(2) A ∈ BAO is called a normal BAO iff for every n-ary operator f of A, and for every k < n, the following equation holds in A:

(Nrm) f(x_{0},…, x_{k−1}, 0, x_{k+1},…, x_{n−1}) = 0.

<

As we already mentioned at the beginning of the present subsection, there is a very strong connection between modal logics and BAO’s. Namely, let L be a (not necessarily normal) multi-modal logic. Then V(Alg(L)) ⊆ BAO. In the other direction, every BAO variety coincides with V(Alg(L)) for some multi-modal logic L. A multi-modal logic L is normal iff Alg(L) consists of normal BAO’s.

As Prof. Robert Goldblatt has pointed out to us, natural examples of nonnormal BAO’s are fairly common in computer science. E.g. such an example is Dijkstra’s weakest precondition in logics of programs. Indeed, let p be a program and φ a possible output condition for p. Let □_{p}(φ) be true in state w iff all executions of p starting in w terminate and after termination make φ true, cf. Goldblatt [Gol 87] p. 90 and Exercise 2.6.5 (where the notation wp(p, φ) is used for □_{p}(φ)). Then □_{p} is a □-type modality, i.e. it distributes over “∧”, but it is not normal because □_{p}(T rue) is not T rue in all states (but only in those where p terminates). Actually, □_{p}(φ) is the most natural notion of program correctness, since correct programs do not “loop” and do not produce bad outputs (i.e. do not produce outputs that would not satisfy output condition φ).

3 Possible Worlds Semantics for Non-normal Multi-modal Logics

DEFINITION 3.1 Given a set W and n ∈ ω, the set of n-ary partial sequences ^{n}W^{?} over W is defined as follows.

nW^{?} =^{def} {s : s is a function with Dom s ⊆ n and Rng s ⊆ W },

where Dom s and Rng s denote the domain and range of s, respectively.

R is called a partial relation iff R ⊆ ^{n}W^{?} for some n ∈ ω and for some set W.

<

DEFINITION 3.2 Let t = ⟨I, ρ⟩ be a modal similarity type. By a partial frame of type t we mean a structure

F = ⟨W, R_{i}⟩_{i∈I} ,

where W is a set and R_{i} ⊆ ^{ρ(i)+1}W^{?}.

By a normal partial frame of type t we mean a partial frame F = ⟨W, R_{i}⟩_{i∈I} where (∀i ∈ I)(∀s ∈ R_{i}) [0 ∈ Dom s ⇒ (ρ(i) + 1) ⊆ Dom s].

<

At this point we would like to note that all Kripke frames in the usual sense (e.g. [GG 86], [Ven 92]) are examples for our normal partial frames.

DEFINITION 3.3 Let F = ⟨W, R_{i}⟩_{i∈I} be a partial frame of type t = ⟨I, ρ⟩. We define the complex algebra of F, in symbols CmF, to be the algebra

⟨P(W), ∪, −, W, f_{i}⟩_{i∈I} ,

where ⟨P(W), ∪, −, W ⟩ is the powerset Boolean algebra over W, and f_{i} is a ρ(i)-ary operation on P(W) defined as follows.

f_{i}(X_{1}, X_{2},…, X_{ρ(i)})  =^{def}

{w ∈ W : (∃s ∈ R_{i}) (s_{0} = w and (∀j ∈ Dom s \ {0}) s_{j} ∈ X_{j})},

for X_{1}, X_{2},…, X_{ρ(i)} ⊆ W.

<

DEFINITION 3.4 A BAO A is atomic and complete iff its Boolean reduct is atomic and complete. A complete BAO A is completely distributive iff every operator in each of its arguments distributes over arbitrary suprema, i.e.

f(x_{1},…, x_{i−1}, ⋁ X, x_{i+1},…, x_{n}) =

⋁{f(x_{1},…, x_{i−1}, x, x_{i+1} …, x_{n}) : x ∈ X},

for every X ⊆ A, where if Y ⊆ A then ⋁ Y denotes the supremum of Y.

<

PROPOSITION 3.5 The complex algebra of a partial frame is an atomic, complete and completely distributive BAO. A partial frame is normal iff its complex algebra is a normal BAO.

Proof: This is an easy consequence of the definition of the complex algebra of a partial frame.

Let K be a class of algebras. Then SK is the class of isomorphic copies of subalgebras of members of K.

THEOREM 3.6 Let A be a BAO. Then there exists a partial frame F such that A is embeddable to CmF, i.e.

BAO = S{CmF : F is a partial frame}.

For proving Theorem 3.6, we need Theorem 3.7 below.

THEOREM 3.7 (Jónsson-Tarski) Let A be a BAO. Then A is embeddable into a complete, atomic and completely distributive BAO A^{+}, and A^{+} is a normal BAO iff A is a normal BAO.

Proof: cf. e.g. [JT 52], or [HMT 71] Thm.2.7.5 (p.432).

Proof of Theorem 3.6: Let t = ⟨I, ρ⟩ be a modal similarity type, let A = (A, ∨, −, 1, f_{i})_{i∈I} be a BAO_{t}. By Theorem 3.7, A is embeddable into a complete, atomic and completely distributive BAO_{t} A^{+}. AtA^{+} denotes the set of atoms of A^{+}. Let F = ⟨AtA^{+}, R_{i}⟩_{i∈I} be the partial frame of type t, where R_{i} (i ∈ I) is defined as follows. Let s ∈ ^{ρ(i)+1}(AtA^{+})^{?}. Let

s_{j}^{∗} =^{def} \{ \begin{matrix}s_{j} & if j ∈ Dom s \\ 0 & otherwise \end{matrix}

(j < ρ(i) + 1). Now

s ∈ R_{i} ⟺^{def} (s_{0}^{∗} ≤ f_{i}(s_{1}^{∗}, s_{2}^{∗},…, s_{ρ(i)}^{∗}) holds in A^{+}).

To prove the theorem, it is enough to prove A^{+} ≅ CmF. Let the function h, h : A^{+} ⟶ P(AtA^{+}), be defined as follows:

h(x) =^{def} {a ∈ AtA^{+} : a ≤ x}.

We will show that h is an isomorphism between A^{+} and CmF. By the theory of the Boolean algebras, it is an isomorphism between the Boolean reduct of A^{+} and the Boolean reduct of CmF. Thus it is enough to show (1) below.

(1) If f_{i} (i ∈ I) is an operator and x_{1}, x_{2},…, x_{ρ(i)} ∈ A^{+} then h(f_{i}(x_{1}, x_{2},…, x_{ρ(i)})) = f_{i}(h(x_{1}), h(x_{2}),…, h(x_{ρ(i)})).

CmF is completely distributive and so is A^{+}. Therefore to show (1) above, it is enough to prove (2) below.

(2) If f_{i} (i ∈ I) is an operator and a_{1}, a_{2},…, a_{ρ(i)} ∈ (AtA^{+} ∪ {0}) then h(f_{i}(a_{1}, a_{2},…, a_{ρ(i)})) = f_{i}(h(a_{1}), h(a_{2}),…, h(a_{ρ(i)})). To prove (2) let (∀i ∈ I) R_{i}^{∗} be defined as follows.

R_{i}^{∗} =^{def} {s^{∗} : s ∈ R_{i}}, where s^{∗} = ⟨s_{1}^{∗},…, s_{ρ(i)}^{∗}⟩.

Let a_{1}, a_{2},…, a_{ρ(i)} ∈ (AtA^{+} ∪ {0}). Then

x ∈ h(f_{i}(a_{1}, a_{2},…, a_{ρ(i)})) ⟺
⟺ x ≤ f_{i}(a_{1}, a_{2},…, a_{ρ(i)}) and x ∈ AtA^{+} (by the definition of h)
⟺ (x, a_{1}, a_{2},…, a_{ρ(i)}) ∈ R_{i}^{∗} (by the definition of R_{i} and R_{i}^{∗})

⟺ x ∈ f_{i}(h(a_{1}), h(a_{2}),…, h(a_{ρ(i)})) (by the definition of the complex algebra).

(Because h(a_{j}) = {a_{j}} iff a_{j} ≠ 0, and h(a_{j}) = ∅ iff a_{j} = 0.)

DEFINITION 3.8 Let t = ⟨I, ρ⟩ be a modal similarity type, and P be a set of propositional variables. Recall from Def.2.8 that F_{t}^{P} denotes the set of modal formulas of type t. Let F = ⟨W, R_{i}⟩_{i∈I} be a partial frame of type t.

By a valuation of the variables into F we mean a function v : P ⟶ P(W). By a model over F we mean a pair ⟨F, v⟩ where v is a valuation.

Given a model M = ⟨F, v⟩ we define the truth relation |⊢ between the elements of W and the elements F_{t}^{P} inductively, as follows.

w|⊢p ⟺^{def} w ∈ v(p)
w|⊢¬φ ⟺^{def} not w|⊢φ
w|⊢φ ∨ ψ ⟺^{def} w|⊢φ or w|⊢ψ
w|⊢◇_{i}(φ_{1},…, φ_{ρ(i)}) ⟺^{def} (∃s ∈ R_{i})(w = s_{0} and (∀j ∈ Dom s \ {0}) s_{j}|⊢φ_{j})),

where p ∈ P, w ∈ W, i ∈ I, φ, ψ, φ_{1},…, φ_{ρ(i)} ∈ F_{t}^{P}. A formula φ is said to be valid in M, in symbols M ⊧_{L} φ, iff w|⊢φ for all w ∈ W.

Let the function mng_{M} : F_{t}^{P} ⟶ P(W) be defined as follows:

mng_{M}(φ) =^{def} {w ∈ W : w|⊢φ}.

<

Below we define General Modal Logic and General Normal Modal Logic in the spirit of Def.2.5.

DEFINITION 3.9 Let a type t = ⟨I, ρ⟩ be fixed. Let K be the class of all frames of type t, and let K_{0} be the class of all normal frames of type t. We define General Modal Logic (GML) and General Normal Modal Logic (NGML) of type t as follows:

GML_{t} =^{def} GML =^{def} ⟨L^{P} : P is a set⟩,

NGML_{t} =^{def} NGML =^{def} ⟨L_{norm}^{P} : P is a set⟩, where

for each set P,

L^{P} =^{def} ⟨F_{t}^{P} , M(K), mng, ⊧_{L}⟩ and L_{norm}^{P} =^{def} ⟨F_{t}^{P} , M(K_{0}), mng, ⊧_{L}⟩ are logics

satisfying the conditions below.

• F_{t}^{P} is the set of multi-modal formulas as defined in Definition 2.8.

• M(K) and M(K_{0}) are the classes of all models over K and K_{0}, respectively.

• The function mng and the relation ⊧_{L} are as defined in Def.3.8.

<

PROPOSITION 3.10 Let t be a type. Then Alg(GML_{t}) = BAO_{t} and Alg(NGML_{t}) coincides with the class of all normal BAO_{t}’s.

Proof: This is a consequence of Thm.3.6.

THEOREM 3.11 Let a modal similarity type t = ⟨I, ρ⟩ be fixed. The inference system consisting of the axioms of classical propositional logic, Axiom (K) (defined in Def.2.9), and the inference rules modus ponens and conditional necessitation (CN) is strongly complete and sound for GML.

The inference system consisting of the axioms of classical propositional logic, Axiom (K) and the inference rules modus ponens and necessitation (N) is strongly complete and sound for NGML.

Outline of proof: Alg(GML_{t}) = BAO_{t} by Theorem 3.6. Therefore using the methods of Thm.3.2.3 from [AKNS 94] it is easy to see that the inference system (⊢_{∗}) defined below is strongly complete and sound for GML: Definition of (⊢_{∗}): The Axioms of (⊢_{∗}) are the axioms of classical propositional logic together with the axiom (Bao) (recalled below) for each modality in each of its arguments φ_{j}.

(Bao)  ◇_{i}(φ_{1},…, φ_{j−1}, φ ∨ φ′, φ_{j+1},…, φ_{ρ(i)})  ⟷

◇_{i}(φ_{1},…, φ_{j−1}, φ, φ_{j+1},…, φ_{ρ(i)}) ∨ ◇_{i}(φ_{1},…, φ_{j−1}, φ′, φ_{j+1},…, φ_{ρ(i)}).

The derivation rules of (⊢_{∗}) are modus ponens and the rule (R), for each modality in each of its arguments, recalled below.

(R)  φ ↔ ψ  ⊢_{L}

◇_{i}(φ_{1},…, φ_{j−1}, φ, φ_{j+1},…, φ_{ρ(i)}) ↔ ◇_{i}(φ_{1},…, φ_{j−1}, ψ, φ_{j+1},…, φ_{ρ(i)}).

At this point, we have a completeness theorem for (⊢_{∗}). From this, one proves the desired result by proving that the inference system (⊢_{∗}) is equivalent with the inference system in Theorem 3.11.

The proof for normal multi-modal logic is similar.

4 The Superamalgamation Property of Classes of Algebras

The definition of the superamalgamation property of classes of partially ordered algebras is due to Maksimova.^{5} Though Janis Cirulis pointed out that the idea seems to go back to references Jurie [67] and Pinter [73b’] of [HMT 71] and [HMT 85]. We will generalize this definition, in that the relations on our algebras are not necessarily partial orderings. From our version of the superamalgamation property the strong amalgamation property does not follow (although the strong amalgamation property follows from Maksimova’s version). Our (generalized version of) superamalgamation property is a useful property of algebras, in that it characterizes the Craig interpolation property. We will write “SUPAP” for superamalgamation property. Maksimova writes “SAP” for SUPAP.^{6}

5This notion seems to be related to the lattice theoretic notion of “pasting”, c.f. e.g.

Fried-Grätzer [FG 90].

DEFINITION 4.1 Let t be an algebraic similarity type, let e(x, y) be an equation of type t containing 2 variables, x and y. Let K be a class of algebras of similarity type t. For every A ∈ K, we define a binary relation R_{e} corresponding to equation e as follows:

(∀a, b ∈ A) (aR_{e}b iff e(a, b) holds in A).
<

DEFINITION 4.2 Let A_{0}, A_{1}, A_{2}, A be similar algebras, e be an equation containing 2 variables and R_{e} be the binary relation corresponding to e in the sense of Definition 4.1. We say that

[figure: A_{0}; A; A_{2}; A_{1}; i_{1}; i_{2}; m_{1}; m_{2}]

is an (R_{e} SUPAP) diagram iff i_{1}, i_{2}, m_{1}, m_{2} are embeddings, m_{1} ∘ i_{1} = m_{2} ∘ i_{2}, and

(∀x ∈ A_{j})(∀y ∈ A_{k})[(m_{j}(x)R_{e}m_{k}(y) ⇒ (∃z ∈ A_{0})(xR_{e}i_{j}(z) and i_{k}(z)R_{e}y)],

where {j, k} = {1, 2}.

<

6We write SUPAP because a large part of the literature uses SAP to abbreviate “strong amalgamation property” cf. [Mar 95], [AN 94], [ANS 94a], [KMPT 83] etc.

From now on, K always denotes a class of similar algebras (unless specified otherwise). Further, whenever we say that “K is a class of algebras and e is an equation”, we mean that K is a class of similar algebras and e is an equation of the similarity type of K.

DEFINITION 4.3 Let K be a class of algebras, and e be an equation containing 2 variables. Let R_{e} be the binary relation corresponding to e in the sense of Definition 4.1. We say that K has (R_{e} SUPAP) iff for every A_{0}, A_{1}, A_{2} ∈ K and embeddings i_{1} : A_{0} ⟶ A_{1}, i_{2} : A_{0} ⟶ A_{2} there exist A ∈ K and embeddings m_{1} : A_{1} ⟶ A, m_{2} : A_{2} ⟶ A such that

[figure: A_{0}; A; A_{2}; A_{1}; i_{1}; i_{2}; m_{1}; m_{2}]

is an (R_{e} SUPAP) diagram.

<

Let K be a class of algebras and X be an arbitrary set. FK(X) denotes the K-free algebra generated by X. (For the definition of K-free algebra see e.g. [HMT 71].) For any class K of algebras SPK denotes the class of subalgebras of direct product of members of K. It is important to know that FK(X) = FSPK(X). In particular FK(X) need not be a member of K, c.f. [HMT 71].

DEFINITION 4.4 Let K be a class of algebras and e be an equation containing 2 variables. Let R_{e} be the binary relation corresponding to e in the sense of Definition 4.1. We say that K has (Free R_{e} SUPAP) iff for arbitrary sets X, Y satisfying FK(X ∩ Y) ≠ ∅,

[figure: FK(X ∩ Y); FK(X ∪ Y); FK(Y); FK(X); i_{1}; i_{2}; m_{1}; m_{2}]

is an (R_{e} SUPAP) diagram, where i_{1}, i_{2}, m_{1}, m_{2} are natural embeddings, i.e. i_{1}⌈(X ∩ Y), i_{2}⌈(X ∩ Y), m_{1}⌈X, m_{2}⌈Y are identity functions.

<

CONVENTION 4.5 V(K) := HSP(K) denotes the variety generated by the class K.

<

LEMMA 4.6 Let K be a class of algebras and e be an equation containing 2 variables. Let R_{e} be the binary relation corresponding to e in the sense of Definition 4.1. Then conditions (i) and (ii) below are equivalent.

(i) K has (Free R_{e} SUPAP).

(ii) For every X, Y if FK(X ∩ Y) ≠ ∅ then there exist an A ∈ V(K) and embeddings m_{1} and m_{2} such that

[figure: FK(X ∩ Y); A; FK(Y); FK(X); i_{1}; i_{2}; m_{1}; m_{2}]

is an (R_{e} SUPAP) diagram, where i_{1} and i_{2} are natural embeddings.

Proof: Let K be as in the formulation of the lemma. Throughout this proof, whenever X ⊆ Y then we pretend FK(X) ⊆ FK(Y). Proof of (ii)⇒(i): Assume (ii). Let e be as in the formulation of Lemma 4.6. Let X, Y be such that FK(X ∩ Y) ≠ ∅. To prove (i), let i_{1}, i_{2}, n_{1}, n_{2} be the following natural embeddings:

[figure: FK(X ∩ Y); FK(X ∪ Y); FK(Y); FK(X); i_{1}; i_{2}; n_{1}; n_{2}]

It is enough to show that the above diagram is an (R_{e} SUPAP) diagram.

To see this, let x ∈ FK(X), y ∈ FK(Y) such that n_{1}(x)R_{e}n_{2}(y). (For the case n_{2}(y)R_{e}n_{1}(x) the proof is similar.) It is enough to show that

(∃z ∈ FK(X ∩ Y))(xR_{e}i_{1}(z) and i_{2}(z)R_{e}y).

By (ii), there exist A ∈ V(K), and m_{1}, m_{2} such that

[figure: FK(X ∩ Y); A; FK(Y); FK(X); i_{1}; i_{2}; m_{1}; m_{2}]

is an (R_{e} SUPAP) diagram. m_{1}⌈(X ∩ Y) = m_{2}⌈(X ∩ Y) because the diagram above is commutative. Therefore the function m_{1}⌈X ∪ m_{2}⌈Y exists. It can be uniquely extended to a homomorphism h : FK(X ∪ Y) ⟶ A. By the definition of R_{e} and by n_{1}(x)R_{e}n_{2}(y), h ∘ n_{1}(x)R_{e}h ∘ n_{2}(y). (We used here that R_{e} is a relation corresponding to an equation, thus R_{e} is preserved under homomorphism.) It is easy to see that h⌈FK(X) = m_{1} and h⌈FK(Y) = m_{2}. Therefore h∘n_{1}(x)R_{e}h∘n_{2}(y) implies that m_{1}(x)R_{e}m_{2}(y). The diagram above is (R_{e} SUPAP), so ∃z ∈ FK(X ∩ Y) such that xR_{e}i_{1}(z) and i_{2}(z)R_{e}y. Thus K has (Free R_{e} SUPAP). (i)⟹ (ii) is obvious.

5 Craig Interpolation

The main results of this section are Thm.5.6, Thm.5.7, and Thm.5.8.

To understand this section it is not necessary to be familiar with the notion of strongly nice logic (recalled in Section 2). As we said in Section 1 all the proofs and theorems herein remain true for algebraizable logics in place of strongly nice (or strongly nice general) logics.

The Craig interpolation property is a distinguished property of logics which has been investigated ever since 1957 when William Craig proved that this property holds for usual first order logic. It was shown in [ANS 94b] that it is most useful to know if this property holds for a logic.

This property has two major versions, (⊧ Craig) and (→ Craig). In (→ Craig), “→” is a connective of the logic L under consideration, and need not be the usual implication of classical logic (it can be e.g. intuitionistic implication or the derived connective □(φ → ψ) of modal logic, or □(φ → ⟨Future⟩ψ) of temporal logic etc.). Therefore, to make our definition flexible enough we will speak about (♡ Craig) property where ♡ is an arbitrary but fixed (derived) connective of our logic. (In most applications ♡ is some kind of implication, though.)

Recall from Def.2.1 (3) that by a derived connective of a logic we mean an operation which is built up from logical connectives by “compositions”.^{7}

DEFINITION 5.1 Let L be a logic satisfying condition (1) in Definition 2.1, and let ♡ be a derived binary connective of L. We say that L has the (♡ Craig) interpolation property ((♡ Craig) for short) iff the following condition holds. For every φ, ψ ∈ F_{L}, whenever ⊧_{L} (φ♡ψ) and (∗) below holds then also ⊧_{L} (φ♡χ) and ⊧_{L} (χ♡ψ) hold for some χ ∈ F_{L} with Voc(χ) ⊆ Voc(φ) ∩ Voc(ψ), where Voc(γ) denotes the set of atomic formulas occurring in γ, for any formula γ.

{χ ∈ F_{L} : Voc(χ) ⊆ Voc(φ) ∩ Voc(ψ)} ≠ ∅.  (∗)
<

THEOREM 5.2 Let L be a strongly nice general logic in the sense of Def.2.5 or a strongly nice logic with an infinite set of propositional variables in the sense of Def.2.1. Let m, ε_{j}, δ_{j} (j < m) be as in (3) of Def.2.1. Assume m = 1, and ε = ε_{0}, δ = δ_{0}. Assume L has a derived binary logical connective ♡. Let R♡ be the binary relation which corresponds to the equation ε(x♡y) = δ(x♡y) in the sense of Definition 4.1. Then statements (i)–(v) below hold.

(i) Assume the similarity type of Alg(L) contains at least one

constant symbol. Then

(L has (♡ Craig)) ⟺ (Alg(L) has (Free R♡ SUPAP)).
(ii) (L has(♡ Craig)) ⟸ (Alg(L) has (Free R♡ SUPAP)).
(iii) Assume that (∀φ, ψ ∈ F_{L}) ⊧_{L} (φ♡ψ) implies

{χ ∈ F_{L} : Voc(χ) ⊆ Voc(φ) ∩ Voc(ψ)} ≠ ∅. Then

(L has (♡ Craig)) ⟹ (Alg(L) has (Free R♡ SUPAP)).
(iv) (L has (♡ Craig)) ⟸ (Alg(L) has (R♡ SUPAP)).
(v) (L has (♡ Craig)) ⟸ (V(Alg(L)) has (R♡ SUPAP)).

We will give the proof of Thm.5.2 after Remark 5.3.

REMARK 5.3 Let us notice that if L is a strongly nice logic then Alg(L) contains the Alg(L)-free algebras generated by any subset of the set P of atomic formulas of L, and if L is strongly nice general logic then Alg(L) contains the Alg(L)-free algebras.

<

7I.e., it is the logical counterpart of a “term function” of algebra.

Proof of Theorem 5.2: We will give the proof for strongly nice general logics. The proof for strongly nice logics with infinite set of propositional variables is similar. Proof of (ii): Assume Alg(L) has (Free R♡ SUPAP), and let φ, ψ ∈ F_{L} such that ⊧_{L} (φ♡ψ) and (∗) in Definition 5.1 holds. ⊧_{L} (φ♡ψ) implies Alg(L) ⊧ ε(φ♡ψ) = δ(φ♡ψ) by Thm.2.7. Consider φ and ψ as elements of F_{Alg(L)}(Voc(φ) ∪ Voc(ψ)), then φR♡ψ by the definition of R♡. F_{Alg(L)}(Voc(φ) ∩ Voc(ψ)) ≠ ∅ because of (∗) in Def.5.1. Thus the following diagram is (R♡ SUPAP) (i_{1}, i_{2}, m_{1}, m_{2} are natural embeddings).

[figure: F_{Alg(L)}(Voc(φ)); F_{Alg(L)}(Voc(ψ)); F_{Alg(L)}(Voc(φ) ∪ Voc(ψ)); F_{Alg(L)}(Voc(φ) ∩ Voc(ψ)); i_{1}; i_{2}; m_{1}; m_{2}]

Therefore φR♡ψ implies that there exists χ ∈ F_{Alg(L)}(Voc(φ) ∩ Voc(ψ)) such that φR♡χ and χR♡φ. By the definition of R♡, it follows that ε(φ♡χ) = δ(φ♡χ) and ε(χ♡ψ) = δ(χ♡ψ) in F_{Alg(L)}(Voc(φ)∪Voc(ψ)). Thus by Thm.2.7, ⊧_{L} (φ♡χ) and ⊧_{L} (χ♡ψ), and Voc(χ) ⊆ Voc(φ) ∩ Voc(ψ).

Proof of (iii): Let F_{Alg(L)}(X ∩Y) ≠ ∅. The following diagram is commutative (i_{1}, i_{2}, m_{1}, m_{2} are natural embeddings).

[figure: F_{Alg(L)}(X ∩ Y); F_{Alg(L)}(X ∪ Y); F_{Alg(L)}(Y); F_{Alg(L)}(X); i_{1}; i_{2}; m_{1}; m_{2}]

We will show that the diagram above is (R♡ SUPAP). To see this let φ ∈ F_{Alg(L)}(X), ψ ∈ F_{Alg(L)}(Y) and φR♡ψ in F_{Alg(L)}(X ∪ Y). Thus ε(φ♡ψ) = δ(φ♡ψ) by the definition of R♡. Therefore ⊧_{L} (φ♡ψ) by Theorem 2.7. Then {χ ∈ F_{L} : Voc(χ) ⊆ Voc(φ) ∩ Voc(ψ)} ≠ ∅ because we assumed this. L has (♡ Craig), so there exists χ ∈ F_{L} such that Voc(χ) ⊆ Voc(φ) ∩ Voc(ψ), ⊧_{L} (φ♡χ) and ⊧_{L} (χ♡ψ). If we consider χ as an element of F_{Alg(L)}(Voc(φ) ∩ Voc(ψ)) then χ ∈ F_{Alg(L)}(X ∩ Y), and φR♡χ and χR♡ψ in F_{Alg(L)}(X ∪ Y) by ⊧_{L} (φ♡χ) and ⊧_{L} χ♡ψ, and by Thm.2.7.

Proof of (i): It follows from (ii) and (iii) because for every φ, ψ ∈ F_{L} (∗) in Definition 5.1 holds.

Proof of (iv): Let Alg(L) have (R♡ SUPAP). L is strongly nice general logic therefore Alg(L) contains the Alg(L)-free algebras, by Remark 5.3. Then Alg(L) has (Free R♡ SUPAP) by Lemma 4.6. By (ii), it follows that L has (♡ Craig).

Proof of (v): Let V(Alg(L)) have (R♡ SUPAP). Similarly as in (iv) it implies that Alg(L) has (Free R♡ SUPAP) by Lemma 4.6. By (ii), it follows that L has (♡ Craig).

Assume that L is either an algebraizable logic in the sense of [BP 89], [BP] or equivalently, it is a strongly nice general logic in the sense of Definition 2.5. If Alg(L) ⊆ BAO then the usual propositional connectives, e.g. “→”, are available in L. Let “≤” be a distinguished relation on the elements of V(Alg(L)) corresponding to →, i.e. corresponding to the equation −x ∨ y = 1 in the sense of Definition 4.1. Then we will call (≤ SUPAP) simply SUPAP. In the following Theorem 5.6 we use the terminology of Section 2 or [BP 89], [BP]. (Of course it is enough if the reader is familiar with only one of these).

We will use the strong amalgamation property ((SAP) for short) below without recalling its definition. The definition can be found in e.g. [KMPT 83], [Mar 95],[FG 90].

PROPOSITION 5.4 In BAO-varieties we have:

SUP AP ⟹ SAP

Moreover, every SUPAP diagram is a SAP diagram.

Proof: This follows from the fact that ≤ reflexive and antisymmetric.

DEFINITION 5.5 We recall from [ANS 94a] that a BAO A is weakly normal if for every n-ary operator f of A and for every i < n

A ⊧ f(0,…, 0) = f(x_{0},…, x_{i−1}, 0, x_{i+1},…, x_{n−1}).

That is, if at least one argument is 0, then the result is the same as if all arguments were 0. But f(0,…, 0) does not have to be 0.

<

THEOREM 5.6 Assume that L is either an algebraizable logic in the sense of [BP 89], [BP] or equivalently, it is a strongly nice general logic in the sense of Def.2.5 (i.e. [Gab 94], [FJ], [FJ 94], [AKNS 94], [NA 94]). Assume Alg(L) consists of weakly normal BAO’s. Then

(L has (→ Craig)) ⟺ (V(Alg(L)) has SUPAP).

THEOREM 5.7 Let L be a normal multi-modal logic (possibly with modalities of ranks greater than 1). Then

(L has (→ Craig)) ⟺ (V(Alg(L)) has SUPAP).

THEOREM 5.8 Let L be a multi-modal logic with all modalities of ranks smaller than 2. (Note that L need not be normal.) Then

(L has (→ Craig)) ⟺ (V(Alg(L)) has SUPAP).

The proofs of Theorems 5.6, 5.7, and 5.8 are based on Lemma 5.13 and Theorem 5.14 below. We also need some propositions and definitions.

Let A be a BAO. By an ideal of A we mean a congruence class of 0 by some congruence relation Θ of A. We denote the class of all ideals of A by IlA.

For any A ∈ BAO, BlA denotes the Boolean reduct of A. If I ∈ IlA then I ∈ IlBlA, thus, by the theory of Boolean algebras, any congruence Θ of A is completely determined by the class represented by 0, i.e. if I ∈ IlA then

(∃!Θ ∈ Con(A))(0/Θ = I and aΘb ⇔ a ⊕ b ∈ I),

where a ⊕ b =^{def} (a − b) ∨ (b − a). By A/I and a/I we mean, respectively, the quotient algebra A/Θ and the congruence class a/Θ, where Θ is the congruence relation which corresponds to I.

THEOREM 5.9 (Sain cf. e.g [Sai 82]) Let A ∈ BAO and I ⊆ A. Then

I ∈ IlA
⟺
[(∀ n-ary operator f of A)(∀p_{0}, p_{1},…, p_{n−1} ∈ A)(∀i < n)(∀x ∈ I)

(f(p_{0},…, p_{i−1}, x, p_{i+1},…, p_{n−1}) − f(p_{0},…, p_{i−1}, 0, p_{i+1},…, p_{n−1}) ∈ I) and

I ∈ IlBlA].

First we will prove Claim 5.10 below.

Claim 5.10 (Proposition 7.4 in [Sai 82]) Let A ∈ BAO and assume that all its operators are unary and constant. Let I ⊆ A. Then

I ∈ IlA
⟺

[(∀ unary operator f of A)(∀x ∈ I)(f(x) − f(0) ∈ I) and I ∈ IlBlA].

Proof of Claim 5.10: (⟸): Let A ∈ BAO with all unary and constant operators. Let I ∈ IlBlA. Assume that (∀ unary operator f)(∀x ∈ A)(x ∈ I ⇒ f(x) − f(0) ∈ I) To prove that I ∈ IlA it is enough to prove the following:

(∀a, b ∈ A)(∀f unary operator of A)(a ⊕ b ∈ I ⇒ f(a) ⊕ f(b) ∈ I)

Let a, b ∈ A and let f be an unary operator of A. Assume that a ⊕ b ∈ I. We will prove f(a) ⊕ f(b) ∈ I. By f(a) ⊕ f(b) = (f(a) − f(b)) ∨ (f(b) − f(a)) and by I ∈ IlBlA, it is enough to prove that f(a) − f(b) ∈ I and f(b) − f(a) ∈ I.

f(a) = f(a − b) ∨ f(a ∧ b)  (5)

by additivity of f and by the theory of Boolean algebras.

f(a) − f(b) = (f(a − b) ∨ f(a ∧ b)) − f(b)  (6)

by (5).

(f(a − b) ∨ f(a ∧ b)) − f(b) = f(a − b) − f(b)  (7)

because f is monotone by additivity.

f(a − b) − f(b) ≤ f(a − b) − f(0)  (8)

because f(b) ≥ f(0). Thus by (6), (7) and (8), we have

f(a) − f(b) ≤ f(a − b) − f(0).  (9)

(a − b) ∈ I and by assumption (∀x ∈ I) f(x) − f(0) ∈ I, we have f(a−b)−f(0) ∈ I. Therefore by (9), f(a)−f(b) ∈ I. Similarly f(b)−f(a) ∈ I. We proved I ∈ IlA.

(⟹): Let I ∈ IlA and let x ∈ I be arbitrary. Then (∃Θ ∈ Con(A)) I = 0/Θ. Hence for every unary operator f f(x)Θf(0). f(x)Θf(0) is equivalent with f(x) ⊕ f(0) ∈ I. Thus f(x) − f(0) ∈ I.

QED (Claim 5.10)

Proof of Thm.5.9: Let A be a BAO and I ⊆ A. For every n-ary operator f and for every p_{0},…, p_{n−1} ∈ A and for every i < n we define a new unary

operator f_{\overline{p},i}, f_{\overline{p},i} =^{def} f(p_{0},…, p_{i−1}, x, p_{i+1},…, p_{n−1}). Let A^{∗} be the BAO

such that A^{∗} has the same Boolean reduct as A, and the operators of A^{∗} are f_{\overline{p},i}’s defined above. It is known from Universal Algebra that A and A^{∗} has the same congruences.

Thus the ideals of A and A^{∗} coincide. Applying Claim 5.10 completes the proof.

PROPOSITION 5.11 Let A be a weakly normal BAO and I ⊆ A. Then

I ∈ IlA
⟺
[(∀ n-ary operator f of A)(∀ i < n)(∀x_{i} ∈ I)
(f(1,…, 1, x_{i}, 1,…, 1) − f(0,…, 0) ∈ I) and I ∈ IlBlA],

where f(1,…, 1, x_{i}, 1,…, 1) denotes the following term: we put x_{i} in the i’th argument of f, and 1 in the rest of the arguments of f, and f(0,…, 0) denotes the term which we get from f by putting 0’s in each argument of f.

Proof: (⟹): Let I ∈ IlA and x_{i} ∈ I. By Theorem 5.9,

f(1,…, 1, x_{i}, 1,…, 1) − f(1,…, 1, 0, 1,…, 1) ∈ I.

f(1,…, 1, 0, 1,…, 1) = f(0,…, 0) because A is a weakly normal BAO. Thus f(1,…, 1, x_{i}, 1,…, 1) − f(0,…, 0) ∈ I. I ∈ IlBlA is obvious.

(⟸): Let f be an n-ary operator, and let x_{i} ∈ I, where i < n. f is additive, thus f is monotone. Hence for every p_{0},…, p_{n−1} ∈ A we have:

f(p_{0},…, p_{i−1}, x_{i}, p_{i+1},…, p_{n−1}) ≤ f(1,…, 1, x_{i}, 1,…, 1).

From this, and from f(p_{0},…, p_{i−1}, 0, p_{i+1},…, p_{n−1}) = f(0,…, 0) (it is true, because A is weakly normal) follows that

f(p_{0},…, p_{i−1}, x_{i}, p_{i+1},…, p_{n−1}) − f(p_{0},…, p_{i−1}, 0, p_{i+1},…, p_{n−1}) ≤

f(1,…, 1, x_{i}, 1,…, 1) − f(0,…, 0).  (10)

f(1,…, 1, x_{i}, 1,…, 1) − f(0,…, 0) ∈ I and I is a Boolean ideal, thus

f(p_{0},…, p_{i−1}, x_{i}, p_{i+1},…, p_{n−1}) − f(p_{0},…, p_{i−1}, 0, p_{i+1},…, p_{n−1}) ∈ I,

by (10). Therefore I ∈ IlA by Theorem 5.9.

If A is a BAO and X ⊆ A then Ilg_{A}(X) denotes the ideal generated by X.

PROPOSITION 5.12 Let A be a weakly normal BAO, B ⊆ A and I_{B} ∈ IlB. Then Ilg_{A}(I_{B}) = Ilg_{BlA}(I_{B}).

Proof: Ilg_{A}(I_{B}) ⊇ Ilg_{BlA}(I_{B}) is obvious, therefore it is enough to prove that Ilg_{BlA}(I_{B}) ∈ IlA. For proving this we will use Proposition 5.11.

Let a ∈ Ilg_{BlA}(I_{B}), let f be an n-ary operator of A, and let i < n. By the theory of Boolean algebras,

Ilg_{BlA}(I_{B}) = {x ∈ A : (∃y ∈ I_{B}) x ≤ y}.

Thus there exists b ∈ I_{B} such that a ≤ b. By Proposition 5.11, f(1,…, 1, b, 1,…, 1) − f(0,…, 0) ∈ I_{B}.

f(1,…, 1, a, 1,…, 1) − f(0,…, 0) ≤

f(1,…, 1, b, 1,…, 1) − f(0,…, 0),

because a ≤ b and the term function f(1,…, 1, x, 1,…, 1) is monotone. Therefore

f(1,…, 1, a, 1,…, 1) − f(0,…, 0) ∈ Ilg_{BlA}(I_{B}).

By Proposition 5.11, Ilg_{BlA}(I_{B}) ∈ IlA. Thus Ilg_{A}(I_{B}) = Ilg_{BlA}(I_{B}).

LEMMA 5.13 Let A be a weakly normal BAO and B, C ⊆ A. Let I_{B} ∈ IlB and I_{C} ∈ IlC. Then

Ilg_{A}(I_{B} ∪ I_{C}) = Ilg_{BlA}(I_{B} ∪ I_{C}).

Proof : Let A be a weakly normal BAO. Let B, C ⊆ A and I_{B} ∈ IlB and I_{C} ∈ IlC. Ilg_{A}(I_{B} ∪ I_{C}) ⊇ Ilg_{BlA}(I_{B} ∪ I_{C}) is obvious, so it remains to prove that Ilg_{BlA}(I_{B} ∪ I_{C}) ∈ IlA. For proving this, we will use Proposition 5.12.

It is easy to see that

Ilg_{BlA}(I_{B} ∪ I_{C}) = Ilg_{BlA}(Ilg_{BlA}(I_{B}) ∪ Ilg_{BlA}(I_{C})).  (11)

By Proposition 5.12, we have

Ilg_{BlA}(I_{B}) = Ilg_{A}(I_{B}) and Ilg_{BlA}(I_{C}) = Ilg_{A}(I_{C}).  (12)

It is known from Universal Algebra that if A is an algebra and Θ_{1} and Θ_{2} are congruence relations on A then equivalence relation generated by Θ_{1} and Θ_{2} is a congruence relation. Thus (13) below holds.

Ilg_{BlA}(Ilg_{A}(I_{B}) ∪ Ilg_{A}(I_{C})) = Ilg_{A}(Ilg_{A}(I_{B}) ∪ Ilg_{A}(I_{C})).  (13)

It is easy to see that

Ilg_{A}(Ilg_{A}(I_{B}) ∪ Ilg_{A}(I_{C})) = Ilg_{A}(I_{B} ∪ I_{C}).  (14)

Thus Ilg_{BlA}(I_{B} ∪ I_{C}) = Ilg_{A}(I_{B} ∪ I_{C}) by (11), (12), (13), (14).

THEOREM 5.14 Let K be a class of weakly normal BAO’s. Then

V(K) has SUPAP ⟺ K has (Free SUPAP).

Proof: (⟹): V(K) has SUPAP, so condition (ii) in Lemma 4.6 holds, hence it is equivalent with condition (i) in Lemma 4.6. Thus K has (Free SUPAP).

(⟸): Suppose K has (Free SUPAP). Let A_{0}, A_{1}, A_{2} ∈ V(K), and let

i_{1} : A_{0} ⟶ A_{1} and i_{2} : A_{0} ⟶ A_{2}

be embeddings. We may assume that

A_{2} ⊇ A_{0} ⊆ A_{1}, A_{0} = A_{1} ∩ A_{2},
FK(A_{0}) = FK(A_{1} ∩ A_{2}) ⊆ FK(A_{1}) ⊆ FK(A_{1} ∪ A_{2}) and
FK(A_{1} ∩ A_{2}) ⊆ FK(A_{2}) ⊆ FK(A_{1} ∪ A_{2}).

Now, FK(A_{1}) ⊇ FK(A_{0}) ⊆ FK(A_{2}) forms a “Free-AP” fork and then, by our assumption on K, this can be completed to a (Free SUPAP) diagram. By the definition of a (Free SUPAP) diagram we have that

(⋆) this SUPAP diagram coincides with the following:

[figure: FK(A_{1}); FK(A_{2}); FK(A_{1} ∪ A_{2}); FK(A_{0})]

We will “project” this SUPAP diagram “down onto” A_{0}, A_{1}, A_{2} to obtain a SUPAP diagram completing the A_{1} ⟵ A_{0} ⟶ A_{2} fork too.

Let

g_{1} : FK(A_{1}) ⟶ A_{1} and
g_{2} : FK(A_{2}) ⟶ A_{2}

be homomorphisms such that g_{1}⌈A_{1} and g_{2}⌈A_{2} are identity functions. Let I_{A_{1}} ∈ IlA_{1} and I_{A_{2}} ∈ IlA_{2} such that

I_{A_{1}} = 0/ker g_{1} and I_{A_{2}} = 0/ker g_{2}.
g_{1}⌈(A_{1} ∩ A_{2}) = g_{2}⌈(A_{1} ∩ A_{2}),

hence g_{1}⌈FK(A_{1} ∩ A_{2}) = g_{2}⌈FK(A_{1} ∩ A_{2}). Therefore

0/ker (g_{1}⌈FK(A_{1} ∩ A_{2})) = I_{A_{1}} ∩ FK(A_{1} ∩ A_{2}) and
0/ker (g_{2}⌈FK(A_{1} ∩ A_{2})) = I_{A_{2}} ∩ FK(A_{1} ∩ A_{2}) are equal.

By this, by (⋆) and by Proposition 5.4, (15) below holds.

I_{A_{1}} ∩ FK(A_{1} ∩ A_{2}) = I_{A_{2}} ∩ FK(A_{1} ∩ A_{2}) = I_{A_{1}} ∩ I_{A_{2}}.  (15)

Let b_{1}, b_{2}, b_{0} be the natural isomorphisms, which exist by the Homomorphism Theorem:

b_{1} : A_{1} ⟶ FK(A_{1})/I_{A_{1}},
b_{2} : A_{2} ⟶ FK(A_{2})/I_{A_{2}},
b_{0} : A_{0} ⟶ FK(A_{1} ∩ A_{2})/(I_{A_{1}} ∩ I_{A_{2}}).

We claim that

[figure: FK(A_{1} ∩ A_{2})/(I_{A_{1}} ∩ I_{A_{2}}); FK(A_{1} ∪ A_{2})/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}); FK(A_{2})/I_{A_{2}}; FK(A_{1})/I_{A_{1}}; j_{1}; j_{2}; n_{1}; n_{2}]

is a SUPAP diagram, where j_{1}, j_{2}, n_{1}, n_{2} are defined in the following way:

j_{1} : x/(I_{A_{1}} ∩ I_{A_{2}}) ⟼ x/I_{A_{1}},
j_{2} : x/(I_{A_{1}} ∩ I_{A_{2}}) ⟼ x/I_{A_{2}},
n_{1} : x/I_{A_{1}} ⟼ x/(Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}})),
n_{2} : x/I_{A_{2}} ⟼ x/(Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}})).

It is easy to see that j_{1} and j_{2} are embeddings. To prove that the diagram above is SUPAP, we have to prove (i)–(iii) below.

(i) n_{1} ∘ j_{1} = n_{2} ∘ j_{2}.

(ii) Suppose that x ∈ FK(A_{1})/I_{A_{1}}, y ∈ FK(A_{2})/I_{A_{2}} and n_{1}(x) ≤ n_{2}(y). Then there exists z ∈ FK(A_{1} ∩ A_{2})/(I_{A_{1}} ∩ I_{A_{2}}) such that x ≤ j_{1}(z) and j_{2}(z) ≤ y.

(iii) n_{1} and n_{2} are embeddings.

Proof of (i): It follows from definition of j_{1}, j_{2}, n_{1}, n_{2}.

Proof of (ii): Suppose that x ∈ FK(A_{1})/I_{A_{1}}, y ∈ FK(A_{2})/I_{A_{2}} and n_{1}(x) ≤ n_{2}(y). There exist a_{1} ∈ FK(A_{1}) and a_{2} ∈ FK(A_{2}) such that x = a_{1}/I_{A_{1}} and y = a_{2}/I_{A_{2}}. n_{1}(a_{1}/I_{A_{1}}) ≤ n_{2}(a_{2}/I_{A_{2}}), so

a_{1}/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) ≤ a_{2}/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}).

Hence

a_{1} ∧ (−a_{2}) ∈ Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}),

because p ≤ q is equivalent with p ∧ (−q) = 0. By Lemma 5.13, Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) is the Boolean ideal generated by I_{A_{1}} ∪ I_{A_{2}}. Hence by the theory of Boolean algebras, (∃u ∈ I_{A_{1}}) (∃w ∈ I_{A_{2}}) (a_{1} ∧ (−a_{2}) ≤ u ∨ w). This implies a_{1} ∧ (−u) ≤ a_{2} ∨ w. Let us notice that a_{1} ∧ (−u) ∈ FK(A_{1}) and a_{2} ∨ w ∈ FK(A_{2}). K has (Free SUPAP), so the following diagram is SUPAP.

[figure: FK(A_{1}); FK(A_{2}); FK(A_{1} ∪ A_{2}); FK(A_{1} ∩ A_{2})]

Hence there exists c ∈ FK(A_{1} ∩ A_{2}) such that a_{1} ∧ (−u) ≤ c ≤ a_{2} ∨ w. a_{1} ∧ (−u) ≤ c implies a_{1} ∧ (−c) ≤ u. u ∈ I_{A_{1}}, so a_{1} ∧ (−c) ∈ I_{A_{1}}. Thus

a_{1}/I_{A_{1}} ≤ c/I_{A_{1}}.  (16)

c ≤ a_{2} ∨ w implies c ∧ (−a_{2}) ≤ w. w ∈ I_{A_{2}}, so c ∧ (−a_{2}) ∈ I_{A_{2}}. Thus

c/I_{A_{2}} ≤ a_{2}/I_{A_{2}}.  (17)

Finally x ≤ j_{1}(z) and j_{2}(z) ≤ y holds for the choice z = c/(I_{A_{1}} ∩ I_{A_{2}}) by (16) and (17).

Proof of (iii): To prove that n_{1} is an embedding, it is enough to prove that a ∈ FK(A_{1}) together with a ∈ Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) imply that a ∈ I_{A_{1}}, because of the following: n_{1} is an embedding iff (∀b, c ∈ FK(A_{1}))

b/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) = c/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) ⇒ b/I_{A_{1}} = c/I_{A_{1}}, and this is equivalent with (∀b, c ∈ FK(A_{1}))

b ⊕ c ∈ Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) ⇒ b ⊕ c ∈ I_{A_{1}}.

To see the above let a ∈ FK(A_{1}) and a ∈ Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}). We can apply (ii) for x = a/I_{A_{1}} and y = 0/I_{A_{2}}, because

n_{1}(x) = a/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) = 0/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}) = n_{2}(y).

So there exists

c/(I_{A_{1}} ∩ I_{A_{2}}) ∈ FK(A_{1} ∩ A_{2})/(I_{A_{1}} ∩ I_{A_{2}}) such that
a/I_{A_{1}} ≤ j_{1}(c/(I_{A_{1}} ∩ I_{A_{2}})) and j_{2}(c/(I_{A_{1}} ∩ I_{A_{2}})) ≤ 0/I_{A_{2}}.

Hence a/I_{A_{1}} ≤ c/I_{A_{1}} and c/I_{A_{2}} ≤ 0/I_{A_{2}}. c/I_{A_{2}} ≤ 0/I_{A_{2}} implies that c ∈ I_{A_{2}}. c ∈ I_{A_{2}} and c ∈ FK(A_{1} ∩ A_{2}) and (15) (approx. two pages back) imply that c ∈ I_{A_{1}}. By c ∈ I_{A_{1}} and a/I_{A_{1}} ≤ c/I_{A_{1}}, it follows that a ∈ I_{A_{1}}.

We proved that n_{1} is an embedding. n_{2} is an embedding, too. The proof is similar.

By (i), (ii) and (iii) we proved that the diagram above the formulation of items (i)–(iii) (approx. two pages back) is SUPAP.

The following diagram is commutative:

[figure: FK(A_{1})/I_{A_{1}}; FK(A_{2})/I_{A_{2}}; FK(A_{1} ∪ A_{2})/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}); FK(A_{1} ∩ A_{2})/(I_{A_{1}} ∩ I_{A_{2}}); A_{0}; A_{1}; A_{2}; ⟩; ⟩; ⟩; b_{1}; b_{0}; b_{2}; n_{1}; n_{2}; j_{1}; j_{2}; i_{1}; i_{2}]

Therefore the diagram

[figure: A_{0}; FK(A_{1} ∪ A_{2})/Ilg_{FK(A_{1}∪A_{2})}(I_{A_{1}} ∪ I_{A_{2}}); A_{2}; A_{1}; i_{1}; i_{2}; n_{1} ∘ b_{1}; n_{2} ∘ b_{2}]

is a SUPAP diagram, because the diagram above the formulation of items (i)– (iii) is SUPAP. Thus V(K) has SUPAP.

Proof of Theorem 5.6: Assume L is a strongly nice general logic such that Alg(L) consists of weakly normal BAO’s. Then (L has (→ Craig))⇔ (Alg(L) has (Free SUPAP)) by Theorem 5.2 (i). (Alg(L) has (Free SUPAP)) ⇔ (V(Alg(L)) has SUPAP) by Theorem 5.14. Thus (L has (→ Craig)) ⇔ (V(Alg(L)) has SUPAP).

Proof of Theorem 5.7, and Theorem 5.8: Assume that L is a normal multi-modal logic or not necessarily normal modal logic with all modalities of ranks smaller than 2. Then it is easy to check V(Alg(L)) consists of weakly normal BAO’s. Thus Thm.5.7 and 5.8 are a corollaries of Thm.5.6.

To put Theorems 5.7, 5.8 in perspective, we recall the following theorem from [ANS 94a].

THEOREM 5.15 ( Thm.7 in [ANS 94a])

(i) There is a multi-modal logic L with one binary modality ◇, such that L is not equivalent with any normal multi-modal logic, i.e. for no normal multimodal logic L_{1} is V(Alg(L)) term definitionally equivalent with V(Alg(L_{1})). (ii) There is a variety V of BAO’s such that V is not term definitionally equivalent to any variety of normal BAO’s.

PROPOSITION 5.16 Let t be a similarity type for some BAO’s. Then the class BAO_{t} of all (not necessarily normal) BAO’s of type t has (SUPAP). Therefore, the corresponding general multi-modal logic has the (→ Craig) interpolation property.

On the proof: The proof in Németi [Ném 85] goes through with the obvious modifications. There are two things to be checked: (i) that the construction therein yields SUPAP (and not only SAP as stated there) and (ii) that the argument given there works for non-normal non-unary operations, too, if we use partial frames introduced in Section 2 of the present paper. Both of these are straightforward to check.

6 Related Results

In this section we announce without proofs some related results. We will also mention problems which we plan to study in the near future.

THEOREM 6.1 There is a multi-modal logic L having (→ Craig) such that Alg(L) does not have SUPAP.

The reason for this is that Alg(L) is only a quasivariety (but not a variety) and V(Alg(L)) has SUPAP.

Proof: in [ANS 94a].

It would be nice to see the limits (i.e. the approximate range of applicability) of our characterization of the (→ Craig) property (or more generally of (♡ Craig)) via SUPAP or (R♡ SUPAP). Since direction “(♡ Craig) ⟸ (R♡ SUPAP)” was proved under quite general condition, the question here is to see the limits of direction “(♡ Craig) ⟹ (R♡ SUPAP)”.

We already saw in Thm.6.1 above that the condition that Alg(L) is a variety is needed for “⟹”. Therefore below we will assume this condition.

THEOREM 6.2 There is a strongly nice general logic L with binary connective ♡ such that the following properties hold.

• Alg(L) is a variety.

• R♡ is a partial ordering.

• L has (♡ Craig) but Alg(L) does not have (R♡ SUPAP).

Let us continue investigating how far can the characterization of (→ Craig) by SUPAP be generalized from Theorems 5.6– 5.8.

In Thm.6.2 above we already saw that assuming that L is algebraizable and Alg(L) is a variety is not enough. However, it would be nice to see a more natural counterexample where ♡ is a familiar, and natural kind of implication (like →) and where ♡ corresponds (in a natural way) to the natural partial order ≤ of our algebras.

Let us turn to the problem of finding such a natural counterexample. In this direction, we know only the following.

THEOREM 6.3 Let DL, DL_{1}, DL_{2} be the varieties of distributive lattices (DL’s), of DL’s with greatest element 1, and of DL’s with endpoints 1, 0. Then

(i) each of DL, DL_{1}, DL_{2} has (Free SUPAP), and (ii) each of DL, DL_{1}, DL_{2} fails to have SAP. That is

(Free SUP AP) ≠⇒ SAP

in each one of these varieties.

We note that Thm.6.3 extends from DL_{1} to any variety V of DL_{1}’s with order preserving operators. The latter means that each element A of V is of the form A = ⟨A, ∨, ∧, 1, f_{i}⟩_{i∈I} with ⟨A, ∨, ∧, 1⟩ ∈ DL_{1} and f_{i} preserving ≤ in each of its arguments. An example of such a variety is that of cylindric distributive lattices (which are cylindric algebras without complementation but with dual cylindrifications c_{i}^{∂} included.)

What is missing from Thm.6.3 above is a connective ♡ which would nicely correspond to the DL-ordering ≤. We do not know whether there is such an example. If we simply add the following operation “⇝” to DL_{2}, then (Free SUPAP) goes away (and so does (⇝ Craig)), where

(x ⇝ y) = \{ \begin{matrix}1 & if x ≤ y \\ 0 & otherwise. \end{matrix}

Next we recall ArL, one of the weakest arrow logics or two dimensional logics studied by the van Benthem school, or by Vaughan Pratt, cf. e.g. [AKNS 94]. Let BS be the variety of algebras of type A = ⟨A, ∨, −,; ⟩ where ⟨A, ∨, −⟩ is a Boolean algebra and ⟨A,; ⟩ is a semigroup. ArL denotes the strongly nice logic for which BS=Alg(ArL).

CONJECTURE 6.4 We conjecture that BS has (Free SUPAP), i.e. equivalently, that arrow logic ArL has (→ Craig).

One of the reasons for conjecturing this is Viktor Gyuris’ paper on the free algebras of BS.

PROPOSITION 6.5 If Conjecture 6.4 above is true, then

(→ Craig) ≠⇒ (SAP)

for the logic ArL, since BS fails to have SAP.

It will have to be checked in the future whether (→ Craig) can be characterized by SUPAP in arbitrary BAO varieties (i.e. without assuming any form of normality), c.f. Problem 6.12 way below. Further, we conjecture that there should exist an algebraizable counterexample L with Alg(L) a variety having a Boolean reduct and “→” being the usual Boolean one. (Such an example might be easier [than a BAO-example] to find, because here we do not assume that the extra Boolean operations of Alg(L) distribute over Boolean join.)

THEOREM 6.6 Let V be a weakly normal BAO-variety. Then (i), (ii) below are equivalent.

(i) V has EDPC (equationally definable principle congruences, c.f. e.g. [BP]). (ii) There is a unary term τ(x) in the language of V such that for any x ∈ A ∈ V, the BAO-ideal I generated by x in A is

I = {y ∈ A : y ≤ τ(x)}.

CONJECTURE 6.7 We conjecture that Thm.6.6 above does not generalize to arbitrary BAO’s (instead of weakly normal BAO’s).

<

If the answer to the above conjecture would be negative, then Condition (ii) in Corollary 6.8 below can be replaced with the weaker condition saying that V has EDPC.

The following corollary is a corollary of Thm.5.6 and [ANS 94a].

COROLLARY 6.8 Let L be a strongly nice logic and assume that Alg(L) is a variety of BAO’s. Then any one of conditions (i), (ii) below is sufficient for the conclusion:

(L has (→ Craig) ) ⟺ (Alg(L) has SUPAP).

(i) V is term definitionally equivalent with a weakly normal BAO-variety. (ii) V is a discriminator variety.

We note that in Corollary 6.8 (ii)⟹(i), c.f. [ANS 94a].

THEOREM 6.9 Let L be a strongly nice general logic such that L contains the classical propositional logic as a fragment (i.e. Alg(L) has a Boolean reduct). Assume that Alg(L) forms a variety. Assume, L has the local deduction property in the following sense. (∀φ, ψ ∈ F_{L}) there is a unary derived connective # of L, such that

(φ ⊧_{L} ψ ⟹ ⊧_{L} #(φ) → ψ) and φ ⊧_{L} #(φ).

Then (L has (→ Craig)) ⟺ (Alg(L) has SUPAP).

At this point, we realize that one should check whether the global deduction property in the sense of Blok and Pigozzi (or the local one in the sense of Czelakowski) is enough for the proof of the above theorem to go through. (We did not think about this yet.)

COROLLARY 6.10 Assume, L is an algebraizable logic and Alg(L) is a discriminator variety of partially ordered (say by ≤) algebras with greatest and smallest elements 1 and 0. Assume, L has a connective “→” corresponding to ≤ in the usual way (i.e. x ≤ y ⟺ (x → y) = 1)). Then:

(L has (→ Craig)) ⟺ (Alg(L) has SUPAP).

Proof: This follows from Theorem 6.9.

For a class K of algebras, we say that K has ES iff all epimorphisms in the category theoretic sense of K are surjective, cf. e.g. Kiss et al. [KMPT 83]. Sir(K) denotes the class of subdirectly irreducible algebras in K (together with the one element algebra).

Part (i) of the following Thm.6.11 generalizes a result of Comer [Com 86] which in turn generalized a result of Sain [Sai 82] ((ii) and (iii) already follows from Comer’s result).

THEOREM 6.11 Let V be a discriminator variety. Then,

(i)  (V has ES) ⟺ (Sir(V) has ES).
(ii) (V has SAP) ⟸ (Sir(V) has SAP).
(iii) (V has SAP) ⟺ (Sir(V) has SAP), assuming

that V does not have a one-element member.

Proof: will be in [Mad a].

It remains to be investigated later whether the conclusion of Thm.6.11 (i) remains true for every BAO variety V.

PROBLEM 6.12 (i) Is there a logic L with Alg(L) ⊆ BAO such that V(Alg(L)) has CEP (congruence extension property) but

(L has (→ Craig)) ≠⇒ (V(Alg(L)) has SUPAP)?

(ii) What is the answer without assuming CEP?

References

[AKNS 94] H. Andréka, Á. Kurucz, I. Németi, I. Sain, Applying algebraic logic; A general methodology, Proceedings of the Summer School of Algebraic Logic, Kluwer, to appear Shortened version of this appeared as Applying algebraic logic to logic in “Algebraic Methodology and Software Technology” (eds. M. Nivat et al.) Springer-Verlag, (1994) pp. 5–26.

[AN 94] H. Andréka, I. Németi, Craig’s Interpolation does not imply amalgamation, after all, Manuscript, (1994).

[ANS 94a] H. Andréka, I. Németi and I. Sain, On Interpolation, Amalgamation, Universal Algebra and Boolean Algebras with Operators, Mathematical Institute, Budapest, Preprint, (1994).

[ANS 94b] H. Andréka, I. Németi, and I. Sain, Craig property of a logic and decomposability of theories, In Dekker and Stokhof: Proceeding of the 9th Amsterdam Colloquium, Universiteit van Amsterdam, (1994), pp. 87–92.

[BF 85] J. Barwise, S. Feferman (Eds.), Model-Theoretic Logics, Springer Verlag, Berlin, (1985).

[BRV] P. Blackburn, M. de Rijke, Y. Venema, Lecture notes on modal logic, Proceedings of the Summer School of Algebraic Logic, Kluwer, to appear.

[BP 89] W. J. Blok, D. Pigozzi, Algebraizable logics, Memoirs Amer. Math. Soc., Vol. 77, No. 396, (1989), vi+78 pp.

[BP] W. J. Blok, D. Pigozzi, Abstract Algebraic Logic, Proceedings of the Summer School of Algebraic Logic, Kluwer, to appear.

[Com 86] S. D. Comer, Epimorphisms in discriminator varieties, In: Lectures in Universal Algebra, edited by L. Szabó and A. Szendrei, Colloquia Mathematica Societatis, János Bolyai, 43, Published by János Bolyai Mathematical Society and Elsevier Science Publishers BV, (1986).

[Fit 93] M. Fitting, Basic Modal Logic in Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1 (Logical Foundation) Eds: D. M. Gabbay, C. J. Hogger and J. A. Robinson, Oxford Science Publication, Clarendon Press, Oxford, (1993), pp. 368–449.

[FJ 94] J. M. Font, R. Jansana, On the Sentential Logics Associated with strongly nice and Semi-Nice General Logics, Bulletin of the IGPL, Vol. 2, No. 1, (1994), pp. 55–76.

[FJ] J. M. Font, R. Jansana, A comparison of two general approaches to the algebraization of logics, Proceedings of the Summer School of Algebraic Logic, Kluwer, to appear.

[FG 90] E. Fried, G. Grätzer, The unique amalgamation property for lattices, Annales Univ. Sci. Budapest, 33 (1990), pp. 167–176.

[Gab 94] D. M. Gabbay, What is a Logical System?, Calendron Press, Oxford, (1994).

[GG 86] D. M. Gabbay, F. Guenthner (Eds.), Handbook of Philosophical Logic, Vol.İI, D. Reidel, Dortrecht/Boston/Lancaster, (1986).

[Gol 87] R. I. Goldblatt, Logics of time and computation, CSLI Lecture Notes 7, Stanford, (1987).

[Gol] R. I. Goldblatt, Algebraic Polymodal Logic, Draft Chapter for Handbook of Algebraic Logic (eds. Andréka et al.), to be published by Oxford University Press.

[HMT 71] L. Henkin, J. D. Monk, A. Tarski, Cylindric Algebras Part I, North-Holland, Amsterdam (1971).

[HMT 85] L. Henkin, J. D. Monk, A. Tarski, Cylindric Algebras Part II, North-Holland, Amsterdam (1985).

[JT 48] B. Jónsson, A. Tarski, Boolean algebras with operators, Bulletin of the Amer. Math. Soc., Vol. 54 (1948), pp. 79–80.

[JT 52] B. Jónsson, A. Tarski, Boolean algebras with operators, Parts I–II, Amer. J. Math., Vol. 73, 74 (1951, 1952), pp. 891–939, 127–162.

[Jón 92] B. Jónsson, A survey of Boolean algebras with operators, Vanderbilt University, Preprint, (1992).

[KMPT 83] E. W. Kiss, L. Márki, P. Pröhle, W. Tholen, Categorial algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity, Studia Sci. Math. Hungar., 18 (1983), pp. 79–141.

[Lem 66] E. Lemmon, Algebraic semantics for modal logics, Journal of Symbolic Logic, 31 (1966), I–II pp. 46–65,191–218.

[Mad 95] J. X. Madarász, The Craig interpolation theorem in multi-modal logics, Bulletin of the Section of Logic, Vol. 24, No. 3, (1995), pp. 147–151.

[Mad a] J. X. Madarász, Epimorphisms in discriminator varieties, In preparation.

[Mad b] J. X. Madarász, Interpolation in algebraizable logics, in preparation.

[Mak 91] L. L. Maksimova, Amalgamation and interpolation in normal modal logics, Studia Logica, L(3/4), (1991), pp. 457–471.

[Mak 79] L. L. Maksimova, Interpolation theorems in modal logics and amalgamable varieties of topoboolean algebras, (in Russian), Algebra i logika 18, 5 (1979), pp. 556–586.

[Mak 95] L. L. Maksimova, On variable separation in modal logics, Bulletin of the Section of Logic, Vol. 24, No. 1, pp. 21–25 (1995).

[Mar 95] M. Marx, Algebraic relativization and arrow logic, PhD thesis, Institute for Logic, Language and Computation, Universiteit van Amsterdam, (1995).

[Ném 91] I. Németi, Algebraization of quantifier logics: an overview, version 11.4, Preprint, Math. Inst. Hungar. Acad. Sci., Shortened version (without proofs etc) of this appeared in Studia Logica, L(3/4), (1991), pp. 485–569.

[Ném 85] I. Németi, Cylindric-relativised set algebras have strong amalgamation, Journal of Symbolic Logic, Vol. 50, No. 3, (1985).

[NA 94] I. Németi, H. Andréka, General algebraic logic: A perspective on “What is logic”, in “What is a Logical System?” (ed. D. Gabbay), Clarendon Press, Oxford, (1994), pp. 394–443.

[Pig 72] D. Pigozzi, Amalgamation, congruence extension and interpolation properties in algebras, Algebra Universalis, 1(3), (1972), pp. 269–394,

[Sai 82] I. Sain, Strong amalgamation and epimorphisms of cylindric algebras and Boolean algebras with operators, Preprint, Math. Inst. Hungar. Acad. Sci., (1979), revised (1982).

[Sai 90] I. Sain, Beth’s and Craig’s properties via epimorphisms and amalgamation in algebraic logic, in Algebraic logic and universal algebra in computer science, Vol. 24 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, (1990), pp. 209–226.

[Ven 92] Y. Venema, Many-Dimensional Modal Logics, PhD thesis, Institute for Logic, Language and Computation, Universiteit van Amsterdam, (1992).

[Wój 88] R. Wójcicki, Theory of Logical Calculi (Basic Theory of Consequence Operation), Kluwer Academic Publishers, (1988).