APPLYING ALGEBRAIC LOGIC; A GENERAL METHODOLOGY

Hajnal Andréka, Ágnes Kurucz, István Németi and Ildikó Sain

Mathematical Institute of the Hungarian Academy of Sciences Budapest, P.O.B. 127, H-1364, Hungary August 12, 1993; revised in July and in September, 1994

Abstract. Connections between Algebraic Logic and (ordinary) Logic. Algebraic counterpart of model theoretic semantics, algebraic counterpart of proof theory, and their connections. The class Alg(L) of algebras associated to any logic L. Equivalence theorems stating that L has a certain logical property iff Alg(L) has a certain algebraic property. (E.g. L admits a strongly complete Hilbert-style inference system iff Alg(L) is a finitely axiomatizable quasi-variety. Similarly, L is compact iff Alg(L) is closed under taking ultraproducts; L has the Craig interpolation property iff Alg(L) has the amalgamation property, etc.)

Contents

1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2. General framework for studying logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2.1. Defining the framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2. Distinguished logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 Answers/solutions for important and hard exercises of section 2.2 . . . . . . . . . . .32

3. Bridge between the world of logics and the world of algebras. . . . . . . . . . . . . . . . . . . . . . .34 3.1. Fine-tuning the framework. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .34 3.2. Algebraic characterizations of completeness and compactness properties

via Alg_{m} and Alg_{⊧} (main theorems) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

4. Generalizations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 Appendix A: New kinds of logics. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .63 Appendix B: Further equivalence results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 References. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .71

Research supported by Hungarian National Foundation for Scientific Research grant No’s 1911, T7255 and T7567.

1. Introduction

The idea of solving problems in logic by first translating them to algebra, then using the powerful methodology of algebra for solving them, and then translating the solution back to logic, goes back to Leibnitz and Pascal. Papers on the history of Logic (e.g. Anellis–Houser [AH91], Maddux [Ma91]) point out that this method was fruitfully applied in the 19^{th} century not only to propositional logics but also to quantifier logics (De Morgan, Peirce, etc. applied it to quantifier logics too). The number of applications grew ever since. (Though some of these remained unnoticed, e.g. the celebrated Kripke–Lemmon completeness theorem for modal logic w.r.t. Kripke models was first proved by Jónsson and Tarski in 1948 using algebraic logic.)

For brevity, we will refer to the above method or procedure as “applying Algebraic Logic (AL) to Logic”. This expression might be somewhat misleading since AL itself happens to be a part of logic, and we do not intend to deny this. We will use the expression all the same, and hope, the reader will not misunderstand our intention.

In items (i) and (ii) below we describe two of the main motivations for applying AL to Logic.

(i) This is the more obvious one: When working with a relatively new kind of problem, it is often proved to be useful to “transform” the problem into a well understood and streamlined area of mathematics, solve the problem there and translate the result back. Examples include the method of Laplace Transform in solving differential equations (a central tool in Electrical Engineering).

At this point we should dispell a misunderstanding: In certain circles of logicians there seems to be a belief that AL applies only to syntactical problems of logic and that semantical and model-theoretic problems are not treated by AL or at least not in their original model theoretic form. Nothing can be as far from the truth as this belief, as e.g. looking into the present work should reveal. A variant of this belief is that the main bulk of AL is about offering a cheap pseudo semantics to Logics as a substitute for intuitive, model theoretic semantics. Again, this is very far from being true. (This is a particularly harmful piece of misinformation, because, this “slander” is easy to believe if one looks only superficially into a few AL papers.) To illustrate how far this belief is from truth, the semantical-model theoretic parts of the present work emphasize that they start out from a logical system L whose semantics is as intuitive and as non-algebraic as it wants to be, and then we transform L into algebra, paying special attention to not distorting its semantics in the process; and anyway, finally we translate the solutions back to the very original non-algebraic framework (including model theoretical semantics).

In the present paper we define the algebraic counterpart Alg(L) of a logic L together with the algebraic counterpart Alg_{m}(L) of the semantical-model theoretical ingredients of L. Then we prove equivalence theorems, which to essential logical properties of L associate natural and well investigated properties of Alg(L) such that if we want to decide whether L has a certain property, we will know what to ask from our algebraician colleague about Alg(L). The same devices are suitable for finding out what one has to change in L if we want to have a variant of L having a desirable property (which L lacks). To illustrate these applications we include several exercises (which deal with various concrete Logics). For all this, first we have to define what we understand by a logic L in general (because otherwise it is impossible to define e.g. the function Alg associating a class Alg(L) of algebras to each logic L.

(ii) With the rapidly growing variety of applications of logic (in diverse areas like computer science, linguistics, AI, law, etc.) there is a growing number of new logics to be investigated. In this situation AL offers us a tool for economy and a tool for unification in various ways. One of these is that Alg(L) is always a class of algebras, therefore we can apply the same machinery namely Universal Algebra to study all the new logics. In other words we bring all the various logics to a kind of “normal form” where they can be studied by uniform methods. Moreover, for most choices of L, Alg(L) tends to appear in the same “area” of Universal Algebra, hence specialized powerful methods lend themselves to studying L. There is a fairly well understood “map” available for the landscape of Universal Algebra. By using our algebraization process and equivalence theorems we can project this “map” back to the (far less understood) landscape of possible logics.

∗ ∗ ∗

The approach reported here is strongly related to works of Blok and Pigozzi cf. e.g. [BP89], [BP94], [BP91], [Pi91], Czelakowski [Cz93], Font–Jansana [FJ93]. A more ambitious version of the present approach is in Andréka–Németi–Sain–Kurucz [ANSK] (cf. also Henkin–Monk–Tarski [HMT85] §5.6). However, the paper [ANSK] is harder to read than the present work, therefore it is advisable to read the present one before seriously studying [ANSK]. On the other hand, the investigation of Hilbert-style inference systems done herein are not yet pushed through in that (more ambitious) setting. Anyway, it is advisable to consider [ANSK] as a kind of second part of this work. But after having read a reasonably large part of the present work, it might be a good idea to experiment with looking into [ANSK] in a parallel manner.

The present paper grew out of course materials used mainly (but not solely) at the Logic Graduate School, Budapest. Therefore the style is often that of a lecturer writing to her/his students. E.g. there is a large number of exercises written in an informal imperative style, and there are explanations which would be omitted from any research paper or research monograph. We hope, this style will not offend the reader.

In the paper we follow the notation of Sain [Sa94]. A summary of prerequisites from universal algebra, Boolean and cylindric algebras, logic and naive set theory can also be found therein.

ACKNOWLEDGEMENT: The authors are grateful to Wim Blok, Josep M. Font, Ramon Jansana and Don Pigozzi for most valuable suggestions. Special thanks are due to Font and Jansana for carefully reading the paper, suggesting improvements, and writing a paper on the connection between the presently reported approach and the Blok–Pigozzi approach. Thanks are due to Johan van Benthem, Ágoston Eiben and Yde Venema for careful reading and helpful remarks. Also thanks are due to the following students (listed in alphabetical order) of Logic Graduate School Budapest for helpful remarks, suggestions, solving exercises: Viktor Gyuris, Ben Hansen, Maarten Marx, Szabolcs Mikulás and András Simon.

2. General framework for studying logics

2.1. Defining the framework

Those readers who are interested only in the technical parts of this paper, and who do not care for intuitive motivation, mathematical motivation, applicability, connections with the various more traditional conceptions of a logic, may skip the beginning of this section and start reading with Definition 2.1.3.

Defining a logic is an experience similar to defining a language. (This is no coincidence if you think about the applications of logic in e.g. theoretical linguistics.) So how do we define a language, say a programming language like PASCAL. First one defines the syntax of PASCAL. This amounts to defining the set of all PASCAL programs. This definition tells us which strings of symbols count as PASCAL programs and which do not. But this information in itself is not very useful, because having only this information enables the user to write programs but the user will have no idea what his programs will do. (This is more sensible if instead of PASCAL we take a more esoteric language like ALGOL 68.) Indeed, the second, and more important step in defining PASCAL amounts to describing what the various PASCAL programs will do when executed. In other words, we have to define the meaning, or semantics of the language, e.g. of PASCAL. Defining semantics can be done in two steps, (i) we define the class M of possible machines that understand PASCAL, and then (ii) to each machine 𝔐 and each string φ of symbols that counts as a PASCAL program we tell what 𝔐 will do if we “ask” it to execute φ. In other words we define the meaning mng(φ, 𝔐) of program φ in machine 𝔐.

The procedure remains basically the same if the language in question is not a programming language but something like a natural language or a simple declarative language like first-order logic. When teaching a foreign language, e.g. German, one has to explain which strings of symbols are German sentences and which are not (e.g. “Der Tisch ist rot” is a German sentence while “Das Tisch ist rot” is not). This is called explaining the syntax of German. Besides this, one has to explain what the German sentences mean. This amounts to defining the semantics of German. If we want to formalize the definition of semantics (for, say, a fragment of German) then one again defines a class M of possible situations or with other words, “possible worlds” in which our German sentences are interpreted, and then to each situation 𝔐 and each sentence φ we define the meaning or denotation mng(φ, 𝔐) of φ in situation (or possible world) 𝔐.

At this point we could discuss the difference between a language and a logic, but we do not do that. For our present purposes it is enough to say that the two things are very-very similar.^{1}

1The philosophical minded reader might enjoy looking into the book [P89], cf. e.g. B.Partee’s paper therein. More elementary ones are: Sain [S80/a] and [S80/b].

Soon (in Definition 2.1.3 below) we will define what we mean by a logic. (A more carefully chosen word would be “logical system”.) 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_{L} we have

(⋆)  [mng_{L}(φ, 𝔐) = mng_{L}(ψ, 𝔐) and 𝔐 ⊧_{L} φ] ⟹ 𝔐 ⊧_{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 (wellknown) 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 from mng_{L} the relation ⊧_{L} is definable. A typical possible definition of ⊧_{L} from mng_{L} is the following.

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

for all φ ∈ F_{L}, 𝔐 ∈ 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.

2For fixed φ ∈ F_{L} and 𝔐 ∈ M_{L}, mng_{L}(φ, 𝔐) is called meaning or denotation or intension of expression φ in model (or “possible environment” or “possible interpretation”) 𝔐. 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.

For example, in 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, mng(φ, 𝔐) and 𝔐 ⊧ φ 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_{L})𝔐 ⊧ φ. For φ as above and Γ ⊆ F_{L} we say that φ is a semantical consequence of Γ, in symbols Γ ⊧_{L} φ, iff (∀𝔐 ∈ M_{L})[(∀ψ ∈ Γ)𝔐 ⊧_{L} ψ ⟹ 𝔐 ⊧_{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).

Figure 2.1.1 below illustrates the general pattern of a logic.

Exercises 2.1.1 below are designed to illuminate the intuitive content of the conception of a logic as outlined above, and to show how familiar logics are special cases of our general concept.

⋮
F  ⋮
φ
⋮  ⋮
𝔐
⊢  ⋮  mng(φ, 𝔐)  M

(huge) collection of

⋮  ⋮  possible worlds

(or models)

⋮

meaning function

syntactical part  semantical part

Figure 2.1.1

Exercises 2.1.1:

(1) Create an illustration for the above outlined conception of a logic, that is, for L = ⟨F_{L}, ⊢_{L}, M_{L}, mng_{L}, ⊧_{L}⟩, by formalizing classical sentential logic in this spirit; and do this in the following way. Let P be a set, called the set of atomic formulas of L_{S}. Let {∧, ¬} = Cn(L_{S}) be a set disjoint from P, called the set of logical connectives of L_{S} (usually called Boolean connectives). Define the set F_{S} (of formulas) to be the smallest set H satisfying the two conditions: P ⊆ H and [φ, ψ ∈ H ⟹ (φ ∧ ψ), ¬φ ∈ H]. Further, define the class M_{S} (of models) as M_{S} =^{def} {⟨W, v⟩ : W is a non-empty set, and v : P ⟶ P(W)}. Now, you want to recast sentential logic L_{S} in the form L_{S}^{0} = ⟨F_{S}, ⊢_{S}^{0}, M_{S}, mng_{S}^{0}, ⊧_{S}^{0}⟩ such that it could be a concrete example of our general ideas outlined above. For this, F_{S} and M_{S} are already defined. We leave ⊢_{S}^{0} to the end. Let Sets denote the class of all sets. Define mng_{S}^{0} : F_{S} × M_{S} → Sets in the following way. Let 𝔐 = ⟨W, v⟩ ∈ M_{S} be arbitrary but fixed. For any p ∈ P define mng_{S}^{0}(p, 𝔐) =^{def} v(p). For any φ, ψ ∈ F_{S} define mng_{S}^{0}((φ ∧ ψ), 𝔐) =^{def} mng_{S}^{0}(φ, 𝔐) ∩ mng_{S}^{0}(ψ, 𝔐)

and mng_{S}^{0}(¬φ, 𝔐) =^{def} W ∖ mng_{S}^{0}(φ, 𝔐). For any 𝔐 = ⟨W, v⟩ ∈ M_{S}, φ ∈ F_{S}

let 𝔐 ⊧_{S}^{0} φ iff mng_{S}^{0}(φ, 𝔐) = W. Check that you indeed defined (the set of formulas together with) the “semantical part” ⟨F_{S}, M_{S}, mng_{S}^{0}, ⊧_{S}^{0}⟩ of a logic in the sense outlined above these exercises.

Let us turn to defining a possible choice of ⊢_{S}^{0}.

Throughout, we use (φ → ψ) as an abbreviation for ¬(φ ∧ ¬ψ) and (φ ↔ ψ) as that for (φ → ψ) ∧ (ψ → φ). List a set Ax of valid formulas of L_{S} and call these logical axioms.^{3} Possible elements of this list are (φ → φ) for all φ ∈ F_{S}, (φ ∧ ψ) → (ψ ∧ φ), (φ ∧ ψ) → φ, (φ ∧ ¬φ) → (ψ ∧ ¬ψ), φ → (ψ → φ), for all φ, ψ ∈ F_{S}. Having defined your set Ax of logical axioms, add the inference rule {φ, (φ → ψ)} ⊢ ψ (for all φ, ψ ∈ F_{S}) which is called Modus Ponens. If you wish, you may add similar rules like {φ, ψ} ⊢ (φ ∧ ψ) (but they are not really needed). For Γ ⊆ F_{S}, define Γ ⊢_{S}^{0} φ to hold iff φ ∈ H for the smallest set H ⊆ F_{S} such that Γ ∪ Ax ⊆ H and H is closed under your inference rules, e.g. whenever ψ, (ψ → ρ) ∈ H then also ρ ∈ H. With this, you defined your choice of ⊢_{S}^{0} for L_{S}^{0}. If (Γ ⊢_{S}^{0} φ ⟹ Γ ⊧_{S}^{0} φ) for all Γ, φ then ⊢_{S}^{0} is called sound. If the other direction “⟸” holds, then ⊢_{S}^{0} is called strongly complete. Spend a little time with trying to guess whether your ⊢_{S}^{0} has one of these properties. Now, check that you indeed defined a logic

L_{S}^{0} = ⟨F_{S}, ⊢_{S}^{0}, M_{S}, mng_{S}^{0}, ⊧_{S}^{0}⟩

in the sense outlined above the present exercises.

(2) Compare the just defined version L_{S}^{0} of sentential logic with the ideas outlined above.

(3) Compare L_{S}^{0} with your own previous conception of sentential logic, and try to prove that they are the same thing (perhaps in different forms).

3If the instructions below would be too vague for the non-logician reader then s/he has three options:

(i) Consult Definitions 3.1.12–3.1.15 together with the 11 lines preceding Definition 3.1.12 in section 3 herein. There we define and discuss inference systems ⊢_{L} in detail, so that should suffice. (ii) Recall any of the known inference systems for propositional logic from the literature. (iii) Ignore this “⊢-part”

of this exercise, since we will not rely on it later.

(4) Change the logic L_{S}^{0} obtaining L_{S}^{1} in the following way. Leave F_{S} and ⊢_{S}^{0} unchanged. Define the new M_{S}^{1} by postulating that its elements are functions 𝔐 : P → {0, 1}. (Identify 0 with False and 1 with True.) Define mng_{S}^{1} : F_{S} × M_{S}^{1} → {0, 1} and ⊧_{S}^{1} in the natural way. (Hint: If p ∈ P then mng_{S}^{1}(p, 𝔐) =^{def} 𝔐(p), and mng_{S}^{1}(¬φ, 𝔐) =^{def} 1 − mng_{S}^{1}(φ, 𝔐), etc.) Check that what you obtained, L_{S}^{1} = ⟨F_{S}, ⊢_{S}^{0}, M_{S}^{1}, mng_{S}^{1}, ⊧_{S}^{1}⟩, is again an example of our general concept of a logic.

(5) Try to compare logics L_{S}^{0} and L_{S}^{1}. Try to find ways in which they could be called equivalent. (Hint: Prove e.g. that they have the same semantic consequence relation, i.e. (∀Γ ∪ {φ} ⊆ F_{S}) Γ ⊧_{S}^{0} φ ⇔ Γ ⊧_{S}^{1} φ.)

(6) Let φ ∈ F_{S} be arbitrary. Prove that φ is valid in every model of L_{S}^{0} iff it is valid in every model of L_{S}^{1}. That is, the validities of L_{S}^{0} and L_{S}^{1} coincide. Try to find further similar “equivalence properties”. ◀

Instead of the general conception of a logic outlined above, in many cases we will consider only four of its five components: F_{L}, M_{L}, mng_{L} and ⊧_{L}. Namely, we found that we can simplify the theory without loss of generality by not dragging ⊢_{L} along with us for the following reason.^{4} The validity relation ⊧_{L} (or the function mng_{L} if you like) induces the semantical consequence relation ⊧_{L} ⊆ P(F_{L}) × F_{L}, given above Exercises 2.1.1. There is a natural temptation to try to replace ⊢_{L} with ⊧_{L} in the theory, though at several places (e.g. at completeness theorems) this would be a grave oversimplification. Surprisingly enough, we found that all the theorems we prove for ⊧_{L} carry over to ⊢_{L}, whenever the theorems are not about connections between ⊧_{L} and ⊢_{L} (see explanation below). Therefore we decided to drop ⊢_{L} for the time being and introduce it only where we must say something about ⊢_{L} which cannot be said about ⊧_{L} in itself.

The reader interested in logics in the purely syntactical sense ⟨F_{L}, ⊢_{L}⟩ is invited to read our paper in the way described as follows.

Let L_{syn} = ⟨F, ⊢⟩ be a logic in the syntactical sense. To simplify the arguments below, we assume that L_{syn} has a derived logical connective “↔” just as classical logics do, see Ex.2.1.1 (1) above. Of course, we assume the usual properties of “↔”, e.g. {φ, (φ ↔ ψ)} ⊢ ψ etc. (cf. the ⊢_{S}^{0} part of Ex.2.1.1 (1)). Intuitively, (φ ↔ ψ) expresses that φ and ψ are equivalent. In Remark 2.1.2 below the present discussion, we discuss how to eliminate the assumption of the expressibility of “↔”. (However, the reader may safely skip Remark 2.1.2, since we will not rely on it later.)

Assume we want to study the “syntactical logic” L_{syn} = ⟨F, ⊢⟩. To be able to apply the theorems of the present paper, we will associate a class M_{⊢} of pseudo-models, a mng_{⊢} etc. to L_{syn}. The class of pseudo-models is

M_{⊢} =^{def} {T ⊆ F : T is closed under ⊢}.

4The following considerations, together with Remark 2.1.2, grew out from discussions with Wim Blok, Joseph M. Font, Ramon Jansana and Don Pigozzi. In particular, Remark 2.1.2 is due to Font and Jansana.

For any pseudo-model T ∈ M_{⊢} and formula φ ∈ F,

mng_{⊢}(φ, T) =^{def} {ψ ∈ F : T ⊢ (φ ↔ ψ)} .

Further, validity in pseudo-models T ∈ M_{⊢} is defined as

T ⊧_{⊢} φ ⟺^{def} φ ∈ T .

Now, if we want to investigate the “syntactic logic” ⟨F, ⊢⟩, we apply our theorems to the logic

L_{⊢} =^{def} ⟨F, M_{⊢}, mng_{⊢}, ⊧_{⊢}⟩ .

Then condition (⋆) above holds for L_{⊢} and the semantical consequence relation induced by ⊧_{⊢} coincides with the original syntactical one ⊢. (These are easy to check.) Hence, applying the theorems to the logic L_{⊢} yields results about ⟨F, ⊢⟩ as was desired. In other words, L_{⊢} is an equivalent reformulation of the “syntactic logic” ⟨F, ⊢⟩, hence studying L_{⊢} is the same as studying ⟨F, ⊢⟩.

REMARK 2.1.2 (Eliminating the assumption of expressibility of “↔”): Here we show that in the above argument showing that our results can be applied to a wider class of syntactical logics L_{syn} = ⟨F, ⊢⟩, the assumption of expressibility of “↔” in L_{syn} is not needed. It will turn out in Definition 3.1.1 in section 3 that for any logic L, the set F of formulas has an algebraic structure, that is F is the universe of an algebra 𝔉. (The operations of 𝔉 are the logical connectives of L collected in Cn(L).) Let

M_{⊢} =^{def} {⟨T, h⟩ : T ⊆ F, T is closed under ⊢, h is a homomorphism from 𝔉 into 𝔉}.

For any φ ∈ F, ⟨T, h⟩ ∈ M_{⊢}, let

mng_{⊢}(φ, ⟨T, h⟩) =^{def} h(φ)

⟨T, h⟩ ⊧_{⊢} φ ⟺^{def} h(φ) ∈ T.

Then L_{⊢} =^{def} ⟨F, M_{⊢}, mng_{⊢}, ⊧_{⊢}⟩ is a logic such that for all Γ ∪ {φ} ⊆ F, (Γ ⊧_{⊢} φ iff Γ ⊢ φ) holds. Moreover, if ⊢ satisfies some natural conditions then L_{⊢} is a “structural” logic (cf. Def.3.1.1), therefore all the theorems of this paper can be applied to it. For more information in this line see [FJ94]. ◀

Summing up, for a while we will concentrate our attention on the simplified form

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

of a logic. For the reasons outlined above, this temporary restriction of attention will not result in any loss of generality.

To conclude this section, we turn to nailing down our definitions formally in the form we will use them.

For any set X, we let X^{∗} denote the set of all finite sequences (“words”) over X. That is, X^{∗} =^{def} ⋃_{n∈ω} (^{n}X) (cf. [Sa94]).

DEFINITION 2.1.3 (logic):

By a logic L we mean an ordered quadruple

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

where (i)–(v) below hold.

(i) F_{L} (called the set of formulas) is a subset of finite sequences (called words) over some set X (called the alphabet of L) that is, F_{L} ⊆ X^{∗}.

(ii) M_{L} is a class (called the class of models).

(iii) mng_{L} is a function with domain F_{L} × M_{L} (called the meaning function).

(iv) ⊧_{L} (called the validity relation) is a relation between M_{L} and F_{L} that is, ⊧_{L}⊆ M_{L} × F_{L}. (According to the tradition, instead of “⟨𝔐, φ⟩ ∈ ⊧_{L}” we write “𝔐 ⊧_{L} φ”.)

(v) For all φ, ψ ∈ F_{L} and 𝔐 ∈ M_{L} we have

(⋆)  [mng_{L}(φ, 𝔐) = mng_{L}(ψ, 𝔐) and 𝔐 ⊧_{L} φ] ⟹ 𝔐 ⊧_{L} ψ .  ◀

REMARK 2.1.4: In the above definition, we nailed down the expression “model of L” instead of the more suggestive one “possible world of L” only for purely technical reasons, namely, to avoid a danger of potential ambiguity with the literature. ◀

DEFINITION 2.1.5 (semantical consequence, valid formulas):

Let L = ⟨F_{L}, M_{L}, mng_{L}, ⊧_{L}⟩ be a logic. For every 𝔐 ∈ M_{L} and Σ ⊆ F_{L},

𝔐 ⊧_{L} Σ ⟺^{def} (∀φ ∈ Σ) 𝔐 ⊧_{L} φ,
Mod_{L}(Σ) =^{def} {𝔐 ∈ M_{L} : 𝔐 ⊧_{L} Σ}.

Mod_{L}(Σ) is called the class of models of Σ.

A formula φ is said to be valid, in symbols ⊧_{L} φ, iff Mod_{L}({φ}) = M_{L}.

For any Σ ∪ {φ} ⊆ F_{L},

Σ ⊧_{L} φ ⟺^{def} Mod_{L}(Σ) ⊆ Mod_{L}({φ}),
Csq_{L}(Σ) =^{def} {φ ∈ F_{L} : Σ ⊧_{L} φ} .

If φ ∈ Csq_{L}(Σ) then we say that φ is a semantical consequence of Σ (in logic L). Csq abbreviates “\underline{c}on\underline{s}e\underline{q}ence”. ◀ DEFINITION 2.1.6 (theory, set of validities):

Let L = ⟨F_{L}, M_{L}, mng_{L}, ⊧_{L}⟩ be any logic. For any K ⊆ M_{L} let the theory of K in L be defined as

Th_{L}(K) =^{def} {φ ∈ F_{L} : (∀𝔐 ∈ K) 𝔐 ⊧_{L} φ}.

If K = {𝔐} for some 𝔐 ∈ M_{L} then instead of Th_{L}({𝔐}) we write Th_{L}(𝔐). The set Th_{L}(M_{L}) is called the set of validities of L. ◀

For any set X^{∗} of “strings of symbols”, the notion of a decidable subset H ⊆ X^{∗} is introduced in almost any introductory book on logic or on the theory of computation (see e.g. [M76]). The same applies to H ⊆ X^{∗} being recursively enumerable (r.e.). DEFINITION 2.1.7 (decidability of logics):

We say that a logic L = ⟨F_{L}, M_{L}, mng_{L}, ⊧_{L}⟩ is decidable iff the set Th_{L}(M_{L}) of validities of L is a decidable subset of the set F_{L} of formulas. ◀

2.2. Distinguished logics

Now we define some basic logics. Some of them are well-known, but we recall their definitions for illustrating that they are special cases of the concept defined in Definition 2.1.3 above, and also for fixing our notation. DEFINITION 2.2.1 (propositional or sentential logic L_{S}):

Let P be a set, called the set of atomic formulas of L_{S}. Let {∧, ¬} be a set disjoint from P, called the set of logical connectives of L_{S} (usually called Boolean connectives).

Propositional (or sentential) logic (corresponding to P) is defined to be a quadruple

L_{S} =^{def} ⟨F_{S}, M_{S}, mng_{S}, ⊧_{S}⟩,

for which conditions (i)–(iii) below hold.

(i) The set F_{S} of formulas is the smallest set H satisfying • P ⊆ H

• φ, ψ ∈ H ⟹ (φ ∧ ψ) ∈ H and (¬φ) ∈ H. (That is, the alphabet of this logic is {∧, ¬} ∪ P.)

(ii) The class M_{S} of models of L_{S} is defined by

M_{S} =^{def} {⟨W, v⟩ : W is a non-empty set and v : P → P(W)} .

If 𝔐 = ⟨W, v⟩ ∈ M_{S} then W is called the set of possible states (or worlds^{5} or situations) of 𝔐.

(iii) Let ⟨W, v⟩ ∈ M_{S}, w ∈ W, and φ ∈ F_{S}. We define the binary relation w ⊩_{v} φ by

recursion on the complexity of the formulas:

• if p ∈ P then (w ⊩_{v} P ⟺^{def} w ∈ v(p))

• if ψ_{1}, ψ_{2} ∈ F_{S}, then

w ⊩_{v} ¬ψ_{1} ⟺^{def} w ⊮_{v} ψ_{1}
w ⊩_{v} (ψ_{1} ∧ ψ_{2}) ⟺^{def} w ⊩_{v} ψ_{1} and w ⊩_{v} ψ_{2}.

If w ⊩_{v} φ then we say that φ is true in w, or w forces φ.

Now mng_{S}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}.

⟨W, v⟩ ⊧_{S} φ (φ is valid in ⟨W, v⟩), iff for every w ∈ W, w ⊩_{v} φ. ◀

It is important to note that the set P of atomic formulas is a parameter in the definition of L_{S}. Namely, in the definition above, P is a fixed but arbitrary set. So in a sense L_{S} is a function of P, and we could write L_{S}(P) to make this explicit. However, the choice of P has only limited influence on the behaviour of L_{S}, therefore, following the literature we write simply L_{S} instead of L_{S}(P). From time to time, however, we will have to remember that P is a freely chosen parameter because in certain investigations the choice of P does influence the behaviour of L_{S} = L_{S}(P).

Exercises 2.2.2:

(1) Think of P = ∅, of P = {p} a singleton, or of infinite P. Write up explicitly what L_{S} is like in each of these three cases. What is the cardinality |F_{S}| of the formulas in each case? What is the cardinality | {Mod_{L_{S}}(Σ) : Σ ⊆ F_{S}} | of axiomatizable model classes in each case?

(2) Let (φ → ψ) ⟺^{def} ¬(φ ∧ ¬ψ) and (φ ↔ ψ) ⟺^{def} ((φ → ψ) ∧ (ψ → φ)). Prove

that • {φ} ⊧_{S} ψ ⟺ ⊧_{S} (φ → ψ)

• ({φ} ⊧_{S} ψ and {ψ} ⊧_{S} φ) ⟺ ⊧_{S} (φ ↔ ψ). ◀ Exercises 2.2.3:

5It is important to keep the two senses in which “possible world” can be used separate. The elements ⟨W, v⟩ of M_{S} can be called possible worlds since we inherit this usage from the general concept of a logic. At the same time, the elements w ∈ W can be called “possible states or worlds” as a technical expression of modal logic. So there is a potential confusion here, which has to be kept in mind.

(1) Prove that L_{S} is a decidable logic (cf. Def.2.2.1).

(2) (Important!) Let Ax ⊆ F_{S} be an arbitrary but finite set of formulas. Prove that the set Csq_{L_{S}}(Ax) of consequences of Ax (cf. Def.2.1.7) is decidable.

(3) (This might be too hard. Then ignore it.) Show that (2) becomes false if we generalize it to all decidable sets Ax. (Hint: Use an infinite set P.)

(4) Assume that P is finite. Prove that then (2) becomes true for any set Ax. (Might be too hard; then come back to this after doing the next Ex.(5).)

(5) (Important!) Assume P is finite. Let 𝔐 ∈ M_{S} be arbitrary. Prove that Th_{L_{S}}(𝔐) is decidable. (Hint: Let φ ≡ ψ iff 𝔐 ⊧_{S} (φ ↔ ψ). Prove that F_{S}/≡ is finite (use that P is finite). But then F_{S}/≡ together with the logical connectives is a finite algebra. Show that in such a finite algebra we can always compute the “meaning” of any formula.) ◀

As Ex’s.2.2.3 show, logic L_{S} has a lot of “nice” properties. On the other hand, L_{S} is a very “weak” logic. It is well-known that e.g. first-order logic L_{FOL} (cf. Def.2.2.23 below) is much stronger than L_{S}. However, to build up L_{FOL} from L_{S} we have to modify the notion of a model, of an atomic formula, etc. in the usual way. We do not want to “throw out” L_{S} so drastically, we want to increase the expressive power without changing the class of models or without any other “major surgery”. Is it possible to leave M_{S} unchanged and to obtain some significantly stronger (and more interesting) logic (e.g. by adding some new connectives)? The answer is affirmative according to Def.2.2.4 and Ex’s.2.2.6 below. However, we are also interested in how far we can push this procedure of obtaining stronger and stronger logics without changing the models (or other parts) of L_{S}. What is the price of this increasing expressive power? How far do the nice properties of L_{S} remain true?

DEFINITION 2.2.4 (modal logic S5):

The set of connectives of modal logic S5 is {∧, ¬, ♢}.

The set of formulas (denoted as F_{S5}) of S5 is defined as that of propositional logic L_{S} together with the following clause:

φ ∈ F_{S5} ⟹ ♢φ ∈ F_{S5}.

Let M_{S5} =^{def} M_{S}. The definition of w ⊩_{v} φ is the same as in the propositional case but we also have the case of ♢:

w ⊩_{v} ♢φ ⟺^{def} (∃w′ ∈ W) w′ ⊩_{v} φ.

Then mng_{S5}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{S5} is defined as follows.

⟨W, v⟩ ⊧_{S5} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Now, modal logic S5 is S5 =^{def} ⟨F_{S5}, M_{S5}, mng_{S5}, ⊧_{S5}⟩. ◀ REMARK 2.2.5: According to a rather respectable (and useful) tradition, an extra-Boolean connective is called a modality iff it distributes over disjuction. This will not be true for all of our connectives that we will call modalities (Homework: check for which ones is it true). Thus, regrettably, we sometimes ignore this useful tradition. For this tradition cf. e.g. Venema [V92, Appendix A (pp. 143–152)]. ◀

Exercises 2.2.6:

(1) Prove that S5 is a decidable logic. (Hint: Prove that if ⟨W, v⟩ |̸=_{S5} φ then ⟨W_{0}, v⟩ |̸=_{S5} φ for some finite W_{0} ⊆ W in the following way. Let P_{0} be the set of atomic formulas occurring in φ. Define an equivalence relation ∼ on W by stipulating that w_{1} ∼ w_{2} iff they agree on every element of P_{0}. Then from each equivalence class of W/∼ keep only one element in W_{0}.)

Note that this amounts to repeating Ex’s.2.2.3 (1) above for S5 in place of L_{S}.

(2) Repeat Ex’s.2.2.3 (2) above for S5 in place of L_{S}.

(3) (Important!) Repeat Ex’s.2.2.3 (5) above for S5 in place of L_{S}.

(4) Try doing Ex’s.2.2.3 (4) for S5. ◀

The following logic is discussed e.g. in Sain [S83, S86], Venema [V92], Roorda [Ro91], but see also Segerberg [Se70] who traces this logic back to von Wright. DEFINITION 2.2.7 (difference logic L_{D}):

The set of connectives of difference logic L_{D} is {∧, ¬, D}.

The set of formulas (denoted as F_{D}) of L_{D} is defined as that of propositional logic L_{S} together with the following clause:

φ ∈ F_{D} ⟹ Dφ ∈ F_{D}.

Let M_{D} =^{def} M_{S5}(= M_{S}). The definition of w ⊩_{v} φ is the same as in the propositional case but we also have the case of D:

w ⊩_{v} Dφ ⟺^{def} (∃w′ ∈ W ∖ {w}) w′ ⊩_{v} φ.

Then mng_{D}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{D} is defined as follows.

⟨W, v⟩ ⊧_{D} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Now, difference logic L_{D} is L_{D} =^{def} ⟨F_{D}, M_{D}, mng_{D}, ⊧_{D}⟩. We note that L_{D} is also called “Some-other-time logic” (cf. Sain [Sa86], Segerberg [Se70]). ◀

Exercises 2.2.8:

(1) The definition above defines difference logic L_{D} indirectly via earlier definitions. Write up a self-contained definition of L_{D} without referring back to earlier texts.

(2) (Important!) Try to guess whether Ex’s.2.2.3 (1), (4), (5) extend to L_{D}. Try hard, do not give up too soon and remember that you are required to guess only. Try to formulate some reasons why you are guessing the outcome you do. Try to guess the same for Ex’s.2.2.3 (2) and (3).

(3) Prove that Ex’s.2.2.3 (1), (4), (5) do generalize to L_{D}! (Hint: Use the same equivalence relation ∼ defined on W as in Ex’s.2.2.6 (1). But now, from each equivalence class keep two elements (if there are more than one there) in W_{0}.)

(4) Prove that the connective ♢ of S5 is expressible in L_{D}. Prove that D is not expressible in S5. (Hint: If the second one is too hard, postpone it to the end of this section.) ◀

The logics L_{κ-times} to be introduced below play quite an essential rôle in Artificial Intelligence in the theory what is called there “stratified logic”, cf. e.g. works of H.J.Ohlbach, see e.g. [CGHO]. DEFINITION 2.2.9 (κ-times logic L_{κ-times}, twice logic T w):

Let κ be any cardinal. The set of connectives of κ-times logic L_{κ-times} is {∧, ¬, ♢_{κ}}. The set of formulas (denoted as F_{♢_{κ}}) of L_{κ-times} is defined as that of propositional

logic L_{S} together with the following clause:

φ ∈ F_{♢_{κ}} ⟹ ♢_{κ}φ ∈ F_{♢_{κ}}.

Let M_{♢_{κ}} =^{def} M_{S5}(= M_{S}). The definition of w ⊩_{v} φ is the same as in the propositional case but we also have the case of ♢_{κ}:

w ⊩_{v} ♢_{κ}φ ⟺^{def} (∃H ⊆ W)(|H| = κ and (∀w′ ∈ H) w′ ⊩_{v} φ) .

Then mng_{♢_{κ}}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{♢_{κ}} is defined as follows.

⟨W, v⟩ ⊧_{♢_{κ}} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Now, κ-times logic L_{κ-times} is L_{κ-times} =^{def} ⟨F_{♢_{κ}}, M_{♢_{κ}}, mng_{♢_{κ}}, ⊧_{♢_{κ}}⟩. We note that if κ = 2 then logic L_{2-times} is also called Twice logic and is denoted as T w. ◀

Exercises 2.2.10:

(1) Write up a self-contained definition of the logic L_{κ-times} without referring back to earlier texts.

(2) Prove that L_{0-times} is equivalent to L_{S} and that L_{1-times} is equivalent to S5. Prove that ♢_{2} is expressible in L_{D}. (What do you think of the other direction of expressing D in L_{n-times}, for some n ∈ ω?)

(3) Try to guess whether Ex’s2.2.3 (1), (4), (5) extend to L_{n-times} for finite n (that is, for κ = n ∈ ω). How about n = 0?? How about n = 1?

(4) (Probably too hard. May be ignored.) Try to guess how the logics introduced so far, especially the various L_{κ-times} logics for different cardinals κ, relate to each other in terms of expressive power. (Do not spend all your time on this!) Is the connective ♢ of S5 expressible in L_{2-times}?

(5) Prove that Ex’s.2.2.3 (1), (4), (5) generalize to L_{2-times}. (Hint: The same as given for L_{D} in (the hints of) Ex’s.2.2.8 (3), 2.2.6 (1).)

(6) Can you generalize Ex’s.2.2.3 (1), (4), (5) to L_{3-times}? If yes, how about L_{n-times}, for finite n? (Hint: Keep n elements from each equivalence class of ∼.)

(7) What do you think, does the method of Ex’s.2.2.6 (1), 2.2.8 (3) and 2.2.10 (5), (6) above generalize to L_{κ-times} when κ is infinite? (Hint: Look at the hint of Ex.2.2.14 below. Do not spend all your time with this exercise.)

(8) Think about the logic with extra-Boolean logical connectives ♢_{2} and ♢_{3}. Is it equivalent to L_{2-times} or to L_{3-times}? (Hint: No.) Is it decidable?

(9) Think about the logic L_{count} with extra-Boolean connectives {♢_{n} : n ∈ ω}. It can “count” up to any natural number. Is it decidable? (Hint: Yes.) ◀

So far the extra-Boolean connectives ♢, D, ♢_{κ} were all unary ones. Next we will see examples when the extra-Booleans are binary. DEFINITION 2.2.11 (L_{bin}):

The set of connectives of L_{bin} is {∧, ¬, ♦}, where ♦ is a new binary modality.

The set of formulas (denoted as F_{bin}) of L_{bin} is defined as that of propositional logic L_{S} together with the following clause:

φ, ψ ∈ F_{bin} ⟹ ♦(φ, ψ) ∈ F_{bin}.

Let M_{bin} =^{def} M_{S}. The definition of w ⊩_{v} φ is the same as in the propositional case but we also have the case of ♦:

w ⊩_{v} ♦(φ, ψ) ⟺^{def} (∃u, z ∈ W)[w ≠ u ≠ z ≠ w and u ⊩_{v} φ and z ⊩_{v} ψ] .

As usual, mng_{bin}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{bin} is defined as follows.

⟨W, v⟩ ⊧_{bin} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Now, let L_{bin} =^{def} ⟨F_{bin}, M_{bin}, mng_{bin}, ⊧_{bin}⟩. ◀

Exercises 2.2.12:

(1) Compare L_{bin} with the previous logics. E.g. show that ♢ and D are expressible in L_{bin}. Is ♢_{3} expressible in L_{bin}? (Hint: ♦(φ ∧ ♦(φ, φ)).)

(2) Try to guess whether Ex’s.2.2.3 (1), (4), (5) extend to L_{bin}. (Hint: The method of extending Ex’s.2.2.3 (1) to L_{D} should be adaptable to the present case, cf. hint of Ex’s.2.2.8 (3). So validity in L_{bin} should be decidable. To attack Ex’s.2.2.3 (5) in this case, recall the equivalence ≡ on formulas in the hint for Ex’s.2.2.3 (5). Check whether F_{bin}/≡ is still finite!) ◀

DEFINITION 2.2.13 (L_{more}):

The set of connectives of L_{more} is {∧, ¬, ♦_{more}}, where ♦_{more} is a new binary modality. The set of formulas (denoted as F_{more}) of L_{more} is defined as that of propositional

logic L_{S} together with the following clause:

φ, ψ ∈ F_{more} ⟹ ♦_{more}(φ, ψ) ∈ F_{more}.

Let M_{more} =^{def} M_{S}. The definition of w ⊩_{v} φ is the same as in the propositional case but we also have the case of ♦_{more}:

w ⊩_{v} ♦_{more}(φ, ψ) ⟺^{def} | {u ∈ W : u ⊩_{v} φ} | ≥ | {u ∈ W : u ⊩_{v} ψ} |.

As usual, mng_{more}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{more} is defined as follows.

⟨W, v⟩ ⊧_{more} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Now, L_{more} =^{def} ⟨F_{more}, M_{more}, mng_{more}, ⊧_{more}⟩. ◀

Exercises 2.2.14:

(1) Show that the connective ♢ of S5 is expressible in L_{more}.

(2) Compare L_{more} with the previous logics (concerning their expressive power).

(3) Try to guess whether Ex’s.2.2.3 (1) or (5) extend to L_{more}. (Hint: Recall the hint given for Ex’s.2.2.3 (5). Try to prove that for any fixed 𝔐, assuming that P is finite, the set F_{more}/≡ is still finite.)

(4) (If too hard, might be postponed to the end of this paper, but give it a few hours first, and then look at the detailed hints at the end of section 2.2.) Prove that Ex’s.2.2.3 (1) does extend to L_{more} (i.e. L_{more} is decidable). (Hint: If you followed the hints given for Ex’s.2.2.6 (1), 2.2.8 (3), etc. then you proved for those logics the so called finite model property (fmp). (“fmp” says that a formula is valid [in L] iff it is valid in all finite models [of L]. The cardinality of a model ⟨W, v⟩ is that of W.) Decide whether L_{more} has the fmp. You will see, it does not. Thus the hint given for Ex’s.2.2.6 (1), 2.2.8 (3), etc. has to be refined in order to make it applicable here. See the end of section 2.2 for a detailed hint.)

(5) Define ♢_{max} to be ♦(φ, True), where True abbreviates (φ ∨ ¬φ). Define L_{max} by replacing ♢_{κ} with ♢_{max} in L_{κ-times}. What are the basic properties of L_{max}? Write up an explicit definition for L_{max} without referring to L_{more}. Is ♢_{max} expressible in one of the logics in Defs.2.2.1–2.2.13 ? ◀

Beginning with Definition 2.2.15 below, we start discussing various Arrow Logics. The field of Arrow Logics grew out of application areas in Logic, Language and Computation, and plays an important rôle there, cf. e.g. van Benthem [Be91, Be92], and the proceedings of the Arrow Logic day at the conference “Logic at Work” (December 1992, Amsterdam [CCSOM of Univ. of Amsterdam]).

So far we strengthened L_{S} without modifying the class M_{S} of models. The mildest way of modifying M_{S} is to take a subclass (i.e. the models themselves do not change, only some of them are excluded). DEFINITION 2.2.15 (arrow logic L_{PAIR}):

The set of connectives of L_{PAIR} is {∧, ¬, ∘}, where ∘ is a binary connective.

The set of formulas (denoted as F_{PAIR}) of L_{PAIR} is defined as that of propositional logic L_{S} together with the following clause:

φ, ψ ∈ F_{PAIR} ⟹ φ ∘ ψ ∈ F_{PAIR}.

Let M_{PAIR} =^{def} {⟨W, v⟩ ∈ M_{S} : W ⊆ U × U for some set U}.

The definition of w ⊩_{v} φ is the same as in the propositional case but we also have the case of ∘:

⟨a, b⟩ ⊩_{v} φ ∘ ψ ⟺ ∃c[⟨a, c⟩, ⟨c, b⟩ ∈ W and ⟨a, c⟩ ⊩_{v} φ and ⟨c, b⟩ ⊩_{v} ψ] .

As usual, mng_{PAIR}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{PAIR} is defined as follows.

⟨W, v⟩ ⊧_{PAIR} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Now, arrow logic L_{PAIR} is L_{PAIR} =^{def} ⟨F_{PAIR}, M_{PAIR}, mng_{PAIR}, ⊧_{PAIR}⟩. ◀

Exercises 2.2.16:

(1) Write up a self-contained definition of the logic L_{PAIR} without referring back to earlier texts.

(2) (Important!) Try to guess whether Ex’s.2.2.3 (1), (4), (5) extend to L_{PAIR}. Guess separately (the answers need not be uniform). Concentrate first only on Ex’s.2.2.3 (1). This will be very hard but spend some considerable time with guessing each of the exercises. Do not spend all your time on this, but 8 hours is reasonable. Do not worry if you cannot prove anything in this connection, the insight gained by trying is enough. The solutions will be given at the end of section 2.2, but wait one week at least before reading them!!

(3) Assume that the set P of atomic formulas is finite. Is there a model 𝔐 of L_{PAIR} such that Th_{L_{PAIR}}(𝔐) is not even recursively enumerable? Note that this is a generalization of Ex’s.2.2.3 (5). (Why?) (Hint: A set X is called transitive if (∀y ∈ X) y ⊆ X. A set Y is called hereditarily finite if Y ⊆ X for some finite transitive set X. Let 𝔐 = ⟨W, v⟩ be defined as follows.

W =^{def} “all hereditarily finite sets”
P =^{def} {p_{0}, p_{1}, p_{2}}
v(p_{0}) =^{def} {⟨a, b⟩ ∈ W : a ∈ b}
v(p_{1}) =^{def} {⟨a, b⟩ ∈ W : b ∈ a}
v(p_{2}) =^{def} {⟨a, b⟩ ∈ W : a = b} .

Show first that many relations definable in the model 𝔚 = ⟨W, ∈⟩ of Finite Set Theory (using first-order logic) are also definable in 𝔐 using L_{PAIR}. Define first the relation {⟨∅, ∅⟩}. (Hint: p_{2} ∧ ¬(True ∘ p_{0}).) Then the relation {⟨X, Y ⟩ : Y ⊆ X ∈ W }. Next try to define the relations {⟨X, ∪X⟩ : X ∈ W }, and {⟨X, P(X)⟩ : X ∈ W }. Eventually you will have to use the well known fact that the set of first-order formulas involving only 3 variables (free or bound) and valid in 𝔚 is not recursively enumerable.

(This exercise is not easy if you are not experienced with first-order logic and Gödel’s incompleteness theorem, so you may postpone doing it after having spent about 7 hours with it.)

(4) Compare the answer to the previous exercise with the fact that Th(𝔐) is decidable for all the logics discussed so far. Observe the contrast! Try to find a reason for the sudden change of behaviour (of the logics we are looking at)!

(5) Try to guess the answer (yes or no) to Ex’s.2.2.3 (2), (3) when applied to L_{PAIR}. Is there e.g. a finite set Ax ⊆ F_{PAIR} such that Csq_{L_{PAIR}}(Ax) would not be decidable? (Do not spend all your time here. But spend a few hours.) ◀

DEFINITION 2.2.17 (arrow logic L_{REL}):

The set of connectives of L_{REL} is {∧, ¬, ∘}. Let F_{REL} =^{def} F_{PAIR}. Let M_{REL} =^{def} {⟨W, v⟩ ∈ M_{S} : W = U × U for some set U}. The definition of w ⊩_{v} φ is the same as in the case of L_{PAIR}. As usual, mng_{REL}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{REL}

is defined as follows.

⟨W, v⟩ ⊧_{REL} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Now, arrow logic L_{REL} is L_{REL} =^{def} ⟨F_{REL}, M_{REL}, mng_{REL}, ⊧_{REL}⟩. ◀

Exercises 2.2.18:

(1) The logics L_{REL} and L_{PAIR} are among the most important ones discussed in the whole material. So think about L_{REL} and compare it with the previous ones!

(2) Show that the connective ♢ of S5 is expressible in L_{REL}.

(Hint: ♢φ is (True ∘ φ) ∘ True.)

Show that “∘” is associative in L_{REL} (i.e.

⊧_{REL} [(φ_{1} ∘ φ_{2}) ∘ φ_{3}] ⟷ [φ_{1} ∘ (φ_{2} ∘ φ_{3})].

(Hence omitting brackets and writing “True ∘ φ ∘ True” [for ♢φ] is justified.)

(3) (Important!) Try to guess whether some of Ex’s.2.2.3 (1)–(5) generalizes to L_{REL} (give yes or no answers). (This is very hard, so concentrate on only one item for a while. Do not spend all your time, but spend 6–8 hours. Solutions will be at the end of section 2.2, but wait a few weeks before looking at them.)

(4) Try to prove that the set Th_{L_{REL}}(M_{REL}) of validities of L_{REL} is recursively enumerable. (Hint: To φ ∈ F_{REL} associate a first-order formula f(φ) such that

⊧_{REL} φ ⟺ ⊧ f(φ).

Then use the recursive enumerability of the validities of first-order logic (e.g. via Gödel’s completeness theorem). If this would be too hard, you may postpone it to the end of the section, but do not postpone it forever.) ◀ DEFINITION 2.2.19 (arrow logics L_{ARW0}, L_{ARROW}, L_{RA}):

The set of connectives of arrow logics L_{ARW0}, L_{ARROW}, L_{RA} is {∧, ¬, ∘,^{⌣}, Id}, where ∘ is a binary, ^{⌣} is a unary, and Id is a zero-ary modality.

• The set of formulas (denoted as F_{ARW0}) of L_{ARW0} is defined as that of propositional logic L_{S} together with the following clauses:

φ, ψ ∈ F_{ARW0} ⟹ (φ ∘ ψ), φ^{⌣} ∈ F_{ARW0}
Id ∈ F_{ARW0}

The models are those of propositional logic L_{S} enriched with three relations, called accessibility relations. That is,

M_{ARW0} =^{def} {⟨⟨W, v⟩, C_{1}, C_{2}, C_{3}⟩ : ⟨W, v⟩ ∈ M_{S}, C_{1} ⊆ W × W × W,
C_{2} ⊆ W × W, C_{3} ⊆ W }.

For propositional connectives ¬ and ∧ the definition of w ⊩_{v} φ is the same as in the propositional case. For the new connectives we have:

w ⊩_{v} (φ ∘ ψ) ⟺^{def} (∃w_{1}, w_{2} ∈ W)
(C_{1}(w, w_{1}, w_{2}) and w_{1} ⊩_{v} φ and w_{2} ⊩_{v} ψ)
w ⊩_{v} φ^{⌣} ⟺^{def} (∃w′ ∈ W)(C_{2}(w, w′) and w′ ⊩_{v} φ)
w ⊩_{v} Id ⟺^{def} C_{3}(w).

As usual, mng_{ARW0}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{ARW0} is defined as follows.

⟨W, v⟩ ⊧_{ARW0} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Then arrow logic L_{ARW0} is L_{ARW0} =^{def} ⟨F_{ARW0}, M_{ARW0}, mng_{ARW0}, ⊧_{ARW0}⟩.

• F_{ARROW} =^{def} F_{ARW0}. M_{ARROW} =^{def} M_{PAIR}.

For connectives ¬, ∧ and ∘ the definition of w ⊩_{v} φ is the same as in the case of L_{PAIR}. For the new connectives we have:

⟨a, b⟩ ⊩_{v} φ^{⌣}  ⟺^{def} [⟨b, a⟩ ∈ W and ⟨b, a⟩ ⊩_{v} φ],
⟨a, b⟩ ⊩_{v} Id ⟺^{def} a = b.

As usual, mng_{ARROW}(φ, ⟨W, v⟩) =^{def} {w ∈ W : w ⊩_{v} φ}, and the validity relation ⊧_{ARROW} is defined by

⟨W, v⟩ ⊧_{ARROW} φ ⟺^{def} (∀w ∈ W) w ⊩_{v} φ.

Arrow logic L_{ARROW} is defined by

L_{ARROW} =^{def} ⟨F_{ARROW}, M_{ARROW}, mng_{ARROW}, ⊧_{ARROW}⟩.

• F_{RA} =^{def} F_{ARROW}. M_{RA} =^{def} M_{REL}. The definitions of w ⊩_{v} φ, mng_{RA} and ⊧_{RA}

are the same as in the case of L_{ARROW}.

Arrow logic L_{RA} is L_{RA} =^{def} ⟨F_{RA}, M_{RA}, mng_{RA}, ⊧_{RA}⟩. L_{RA} is also called as the logic of relation algebras. ◀

Exercises 2.2.20:

(1) Define the arrow logics L_{ARW0}, L_{ARROW}, L_{RA} without referring back to earlier texts.

(2) Consider the fragment L_{ARW0}^{0} = ⟨F_{ARW0}^{0}, M_{ARW0}^{0}, mng_{ARW0}^{0} ⊧_{ARW0}^{0}⟩ of arrow logic L_{ARW0} defined above which differ from the original version only in that it does not contain the logical connectives^{⌣} and Id. Prove that L_{ARW0}^{0} is equivalent to L_{PAIR} in the sense that they have the same semantical consequence relation that is, for all Σ ∪ {φ} ⊆ F_{ARW0}^{0} = F_{PAIR}

Σ ⊧_{ARW0}^{0} φ ⟺ Σ ⊧_{PAIR} φ.

Prove that L_{ARW0} is not equivalent, in the above sense, to L_{ARROW}. ◀

DEFINITION 2.2.21 (first-order logic with n variables L_{n}):

Let V =^{def} {v_{0}, …, v_{n−1}} be a set, called the set of variables of L_{n}. Let the set P of atomic formulas of L_{n} be defined as P =^{def} {r_{i}(v_{0} … v_{n−1}) : i ∈ I} for some set I.

(i) The set F_{n} of formulas is the smallest set H satisfying • P ⊆ H

• (v_{i} = v_{j}) ∈ H for each i, j < n

• φ, ψ ∈ H, v_{i} ∈ V ⟹ (φ ∧ ψ), ¬φ, ∃v_{i}φ ∈ H. (ii) The class M_{n} of models of L_{n} is defined by

M_{n} =^{def} {⟨M, R_{i}⟩_{i∈I} : M is a non-empty set and for all i ∈ I, R_{i} ⊆ ^{n}M} .

If 𝔐 = ⟨M, R_{i}⟩_{i∈I} ∈ M_{n} then M is called the universe (or carrier) of 𝔐. (iii) Let 𝔐 = ⟨M, R_{i}⟩_{i∈I} ∈ M_{n}, q ∈ ^{n}M and φ ∈ F_{n}. We define the ternary relation

𝔐 ⊧ φ[q] by recursion on the complexity of φ as follows.

• 𝔐 ⊧ r_{i}(v_{0} … v_{n−1})[q] ⟺^{def} q ∈ R_{i} (i ∈ I)

• 𝔐 ⊧ (v_{i} = v_{j})[q] ⟺^{def} q_{i} = q_{j} (i, j < n)

• if ψ_{1}, ψ_{2} ∈ F_{n}, then

𝔐 ⊧ ¬ψ_{1}[q] ⟺^{def} not 𝔐 ⊧ ψ_{1}[q]
𝔐 ⊧ (ψ_{1} ∧ ψ_{2})[q] ⟺^{def} 𝔐 ⊧ ψ_{1}[q] and 𝔐 ⊧ ψ_{2}[q]
𝔐 ⊧ ∃v_{i}ψ_{1}[q] ⟺^{def} (∃q′ ∈ ^{n}M)(∀j < n)[j ≠ i ⇒
(q′_{j} = q_{j} and 𝔐 ⊧ ψ_{1}[q′])].

If 𝔐 ⊧ φ[q] then we say that the evaluation q satisfies φ in the model 𝔐. Now we define mng_{n} as follows.

mng_{n}(φ, 𝔐) =^{def} {q ∈ ^{n}M : 𝔐 ⊧ φ[q]}.

(iv) Validity is defined by

𝔐 ⊧_{n} φ ⟺^{def} (∀q ∈ ^{n}M) 𝔐 ⊧ φ[q].

First-order logic with n variables

L_{n} =^{def} ⟨F_{n}, M_{n}, mng_{n}, ⊧_{n}⟩

has been defined. ◀ Intuitive explanation: Our L_{n} might look somewhat unusual because we do not allow substitution of variables in atomic formulas r_{i}(v_{0} …). This does not restrict generality, because substitution is expressible by using quantifiers and equality. This is explained in more detail in Remark 2.2.24 (2) below.

Exercises 2.2.22:

(1) Write up a detailed definition of L_{n} as a modal logic. (Hint: Define the class of models by

M_{n} =^{def} {⟨W, v⟩ ∈ M_{S} : W = ^{n}U for some set U} .

The extra-Boolean connectives are “∃v_{i}” and “v_{i} = v_{j}” for i, j < n. Here (∃v_{i}) is a unary modality while (v_{i} = v_{j}) is a zero-ary modality.)

(2) Show that in some sense L_{1} is equivalent to modal logic S5. (In what sense? Try to define!)

(3) Show that in some sense L_{D} and L_{2-times} are comparable with L_{2}. Show that L_{D} and L_{2-times} are strictly weaker than L_{2}. ◀

Next we define first-order logic in a non-traditional form. Therefore, below the definition, we will give intuitive explanations for our present definition. DEFINITION 2.2.23 (first-order logic L_{FOL}, rank-free formulation):

Recall that ω is the set of natural numbers.

Let V =^{def} {v_{i} : i ∈ ω} be a set, called the set of variables of L_{FOL}. As before, let P be an arbitrary set, called the set of atomic formulas of L_{FOL}. (Now, we will think of atomic formulas as relation symbols, hence we will use the letter R for elements of P rather than p as in case of L_{S}.)

(i) The set F_{FOL} is the smallest set H satisfying • P ⊆ H

• (v_{i} = v_{j}) ∈ H for each i, j ∈ ω

• φ, ψ ∈ H, i ∈ ω ⟹ (φ ∧ ψ), ¬φ, ∃v_{i}φ ∈ H.

(ii) The class M_{FOL} of models of L_{FOL} is

M_{FOL} =^{def} { 𝔐 : 𝔐 = ⟨M, R^{𝔐}⟩_{R∈P} , M is a non-empty set and
for all R ∈ P, R^{𝔐} ⊆ ^{n}M for some n ∈ ω} .

If 𝔐 ∈ M_{F OL} then M and R^{𝔐} denote parts of 𝔐 determined by the convention ⟨M, R^{𝔐}⟩ = 𝔐.^{6}

(iii) Validity relation ⊧_{F OL}.

In L_{S5} the “basic semantical units” were the possible situations w ∈ W. In FOL the basic semantical units are the evaluations of individual variables into models 𝔐, where q ∈ ^{ω}M and q evaluates variables v_{i} as element q_{i} ∈ M in the model 𝔐. To follow model theoretic tradition, instead of 𝔐, q ⊩ φ we will write 𝔐 ⊧ φ[q] (though the former would be more in the line with our definitions of L_{S5} etc.).

Let 𝔐 = ⟨M, R^{𝔐}⟩_{R∈P} ∈ M_{FOL}, q ∈ ^{ω}M and φ ∈ F_{FOL}. We define the ternary relation “𝔐 ⊧ φ[q]” by recursion on the complexity of φ as follows:

• 𝔐 ⊧ R[q] ⟺^{def} ⟨q_{0}, …, q_{n−1}⟩ ∈ R^{𝔐} for some n ∈ ω (R ∈ P)

• 𝔐 ⊧ (v_{i} = v_{j})[q] ⟺^{def} q_{i} = q_{j} (i, j ∈ ω)

• if ψ_{1}, ψ_{2} ∈ F_{FOL}, then

𝔐 ⊧ ¬ψ_{1}[q] ⟺^{def} not 𝔐 ⊧ ψ_{1}[q]
𝔐 ⊧ (ψ_{1} ∧ ψ_{2})[q] ⟺^{def} 𝔐 ⊧ ψ_{1}[q] and 𝔐 ⊧ ψ_{2}[q]
𝔐 ⊧ ∃v_{i}ψ_{1}[q] ⟺^{def} (∃q′ ∈ ^{ω}M)(∀j ∈ ω)
[j ≠ i ⇒ (q′_{j} = q_{j} & 𝔐 ⊧ ψ_{1}[q′])].

If 𝔐 ⊧ φ[q] holds then we say that q satisfies φ in 𝔐.

Now we define mng_{FOL} as follows.

mng_{FOL}(φ, 𝔐) =^{def} {q ∈ ^{ω}M : 𝔐 ⊧ φ[q]}.

(iv) Validity is defined by

𝔐 ⊧_{FOL} φ ⟺^{def} (∀q ∈ ^{ω}M) 𝔐 ⊧ φ[q].

(v) First-order logic (in rank-free form) is

L_{FOL} =^{def} ⟨F_{FOL}, M_{FOL}, mng_{FOL}, ⊧_{FOL}⟩ . ◀

6That is, if 𝔐 is given, then M denotes the universe of 𝔐. Further, for R ∈ P, R^{𝔐} denotes the meaning of R in 𝔐.

For more on L_{FOL} see e.g. Henkin–Tarski [HT61], Simon [Si91], Venema [V92], Henkin–Monk–Tarski [HMT85, §4.3]. Intuitive explanations for L_{FOL}:

There are two kinds of explanations needed. Namely,

(i) Why does the definition go as it does? and

(ii) Why do we say that L_{FOL} is first-order logic? That is, what are the connections between L_{FOL} and the more traditional formulations of first-order logic?

We discuss (ii) in Remark 2.2.24 below. Let us first turn to (i).

Let R be a relation symbol, that is R ∈ P. Then instead of the traditional formula R(v_{0}, v_{1}, v_{2}, …) we simply write R. That is, we treat R as a shorthand for R(v_{0}, v_{1}, v_{2}, …).

So this is why R is an atomic formula. The next part of the definition which may need intuitive explanation is the definition of the satisfaction relation’s behaviour on R. That is, the definition of 𝔐 ⊧ R[k]. So let R^{𝔐} ⊆ ^{n}M be given. Recall that R abbreviates R(v_{0}, v_{1}, v_{2}, …) here. Clearly we want 𝔐 ⊧ R[k] to hold if in the traditional sense 𝔐 ⊧ R(v_{0}, v_{1}, v_{2}, …)[k] holds. But by the traditional definition this holds iff ⟨k_{0}, …, k_{n−1}⟩ ∈ R^{𝔐}. Which agrees with our definition. The rest of the definition of L_{FOL} coincides with the definition of the most traditional version of first-order logic. ◀

REMARK 2.2.24 (Connections between L_{FOL} and the more traditional form of first-order logic):

(1) The logic L_{FOL} is slightly more general than the more traditional forms of first-order logic in that here the logic does not tell us in advance which relation symbol has what rank (that is why it is called rank-free). This information is postponed slightly, because it is not considered to be purely logical. The information about the ranks of the relation symbols will be provided by the models, or equivalently, by the non-logical axioms of some theory. However, we can simulate the more traditional form of first-order logic in L_{FOL} as follows.

Any language (or similarity type) of traditional first-order logic is a theory of our L_{FOL}. Namely, such a language includes the rank ϱ(R) of each relation symbol R ∈ P. So, a traditional language is given by a pair ⟨P, ϱ⟩. To such a language we associate the following theory T_{ϱ} (given as a set of formulas):

T_{ϱ} =^{def} {∀v_{i}((∃v_{i}R) ↔ R) : R ∈ P and i ≥ ϱ(R)} .

The theory T_{ϱ} spells out for each R ∈ P that the rank of R is ϱ(R). After T_{ϱ} has been postulated, whenever one sees R as a formula, one can read it as an abbreviation of R(v_{0} … v_{ϱ(R)−1}). To any theory T it is usual to associate a “sublogic” of L_{FOL} as follows:

L_{T} =^{def} ⟨F_{FOL}, Mod(T), mng_{FOL}, ⊧_{FOL}⟩.

For our T_{ϱ}, the sublogic L_{T_{ϱ}} is strongly equivalent with the most traditional first-order logic of language ⟨P, ϱ⟩.^{7}

(2) The other feature of traditional first-order logic which might seem to be missing from L_{FOL} is substitution of individual variables, that is, L_{FOL} includes atomic formulas with a fixed order of variables only. The reason for this is that Tarski discovered in the 40’s that substitution can be expressed with quantification and equality. Namely, if we want to substitute v_{1} for v_{0} in formula φ then the resulting formula is equivalent to ∃v_{0}(v_{0} = v_{1} ∧ φ). E.g. R(v_{1}, v_{1}, v_{2}) is equivalent to

∃v_{0}(v_{0} = v_{1} ∧ R(v_{0}, v_{1}, v_{2})).

What happens if we want to interchange v_{0} and v_{1}, i.e. we want to express R(v_{1}, v_{0}, v_{2}). Then write

∃v_{3}∃v_{4}[v_{3} = v_{0} ∧ v_{4} = v_{1} ∧ ∃v_{0}∃v_{1}(v_{0} = v_{4} ∧ v_{1} = v_{3} ∧ R(v_{0}, v_{1}, v_{2}))].

Someone might object that before writing up the theory T_{ϱ} (cf. item (1) above) one cannot interchange variables. There are two answers: (i) This does not really matter if we want to simulate traditional first-order logic. (ii) This can be easily done by adding extra unary connectives p_{ij} (i, j ∈ ω) to those of L_{FOL}. The semantics of p_{ij} is given by

𝔐 ⊧ p_{ij}φ[q] ⟺^{def} 𝔐 ⊧ φ[⟨q_{0}, …, q_{i−1}, q_{j}, q_{i+1}, …, q_{j−1}, q_{i}, q_{j+1}, …⟩],

if i ≤ j, and similarly otherwise. Adding such connectives does not change the basic properties of the logic.

For more on the properties of L_{FOL} see e.g. the Appendix of Blok–Pigozzi [BP89], Andréka–Gergely–Németi [AGN77] and reference Henkin–Tarski [HT61] of [HMT85] Part I. ◀

Exercises 2.2.25:

(1) Write up a detailed definition of L_{FOL} as a multi-modal logic.

Hint: Define the modal models as

M_{m} =^{def} {⟨W, v⟩ ∈ M_{S} : W ⊆ ^{ω}U for some set U, and for each R ∈ P, (∃n ∈ ω)(∃R_{1} ⊆ ^{n}M)v(R) = {s ∈ ^{ω}U : ⟨s_{0}, …, s_{n}⟩ ∈ R_{1}}} .

The rest of the hint is in Ex.2.2.22(1).

(2) Take the multi-modal form of L_{FOL} obtained in (1) above. Consider the “modality” (∃v_{i}). Can you write down its meaning definition in the ⊩-style of modal logics, that is, the logics studied before L_{n} ?

7This equivalence is the strongest possible one. The models are practically the same, and the formulas are alphabetical variants of each other in the following sense. To each “traditional” formula ψ of ⟨P, ϱ⟩ there is φ ∈ F_{FOL} such that their meanings coincide in every model. (Same holds in the other direction:

for every φ ∈ F_{FOL} there is a “traditional” ψ, etc.)

Hint: Let s ∈ W. (Recall that W = ^{ω}U.) Then

s ⊩ ∃v_{i}φ iff (∃q ∈ W)∀j(j ≠ i ⇒ s_{i} = q_{i} and q ⊩ φ) .

What is the ⊩-style definition of the zero-ary modality (v_{i} = v_{j}) ?

(3) Consider the modal forms of L_{n} and L_{FOL}. Prove that D is expressible in L_{n}. Prove that ♢_{2} is expressible in L_{n} if n > 3. Is D expressible in L_{FOL} ? Is ♢_{2} expressible in L_{FOL} ?

(4) Prove that the following are expressible in L_{FOL} about its models

𝔐 = ⟨M, R^{𝔐}⟩_{R∈P} ∈ M_{FOL}.

(4.1) |M| > 1.

(4.2) |M| = 2.

(4.3) |M| > n for any fixed number n.

(4.4) |M| < n for any fixed number n.

(5) What part of (4) above carries over to L_{n} ?

(6) Prove that L_{1} is decidable. Do you think that L_{2} is decidable? Do you think that L_{FOL} is decidable??

(7) Do you think that the valid formulas of L_{FOL} are recursively enumerable?

Exercises 2.2.26:

(1) Write up a detailed definition of L_{FOL} as a modal logic. (Hint: See Ex.2.2.25 (1) above.)

(2) Prove that L_{FOL} is as expressive as the traditional form of first-order logic. Prove that traditional first-order logic with a language ⟨P, ρ⟩ is strongly equivalent with the sublogic L_{T_{ρ}} as described in Remark 2.2.24.

(3) Assume 𝔐 = ⟨M, R^{𝔐}⟩ ∈ M_{FOL} with R^{𝔐} ⊆ M × M. Express that R is a transitive relation. (This means that you are asked to write up a formula φ ∈ F_{FOL} such that for every ⟨M, R⟩ with R ⊆ M × M, if ⟨M, R⟩ ⊧ φ then R is transitive.)

Express that R is a partial ordering (transitive, reflexive and antisymmetric). Express that R is a dense ordering (density is the property ∀x, y(xRy ⇒

∃z(xRz and zRy)).)

Express that R is an equivalence relation.

(4) Think of L_{FOL} again as a multi-modal logic as in the previous list of exercises. Are there two models 𝔐, 𝔑 such that they are not distinguishable in L_{FOL} but they are distinguishable in any of L_{D}, L_{n-times} for n ∈ ω ? (Hint: no.) What is the answer for L_{κ-times} with some infinite κ (say κ > 2^{ω})?

Exercises 2.2.27:

(1) Let L_{i} = ⟨F_{i}, M_{i}, mng_{i}, ⊧_{i}⟩ with i ≤ 2 be two logics. Call L_{0} and L_{1} weakly equivalent iff

F_{0} = F_{1} and (∀Γ ⊆ F_{0})(∀φ ∈ F_{0})(Γ ⊧_{0} φ ⇔ Γ ⊧_{1} φ) .

Prove that the following logics are weakly equivalent: L_{S} and L_{S}^{0} from Ex.2.1.1.

(2) Let L_{i}, i ≤ 2 be as above. Assume that F_{i} ⊆ Z_{i} for some set of “symbols” Z_{i}. That is, we are assuming that the formulas are finite sets of symbols. For a function f : Z_{0} ⟶ Z_{1} define its natural extension f̃: Z_{0}^{∗} ⟶ Z_{1}^{∗} the usual way: f⟨a + 1, …, a_{n}⟩ = ⟨f(a_{1}), …, f(a_{n})⟩. Call L_{0} and L_{1} reasonably equivalent iff there is a function f : Z_{0} ⟶ Z_{1} such that f̃(F_{0}) = F_{1} and

(i) (∀Γ ∪ {φ} ⊆ F_{0})[Γ ⊧_{0} φ iff f̃(Γ) ⊧_{1} f̃(φ)],

(ii) (∀Γ ∪ {φ} ⊆ F_{1})[Γ ⊧_{1} φ iff f̃^{−1}(Γ) ⊧_{0} f̃^{−1}(φ)], and (iii) (∀φ, ψ ∈ F_{0})[f̃(φ) = f̃(ψ) ⇒ (φ ⊧_{0} ψ and ψ ⊧_{0} φ)].

Prove that any two weakly equivalent logics are reasonably equivalent.

(3) Consider propositional logic with logical connectives {∧, ∨, ¬} and another version of the same logic with {∧, →, false}. Clearly these two versions of propositional logic are equivalent in some natural sense. Prove that they are not equivalent in the sense of (1), (2) above. Try to broaden the scope of equivalence such that these two versions of L_{S} become equivalent.

(4) Let L_{i} be as in (1). Consider the existence of two “semantical” functions

m_{01} : M_{0} ⟶ (Subsets of M_{1}) and
m_{10} : M_{1} ⟶ (Subsets of M_{0}) .

Call L_{0} and L_{1} semantically equivalent iff F_{1} = F_{2} and there are m_{01}, m_{10} as above such that

(∀φ ∈ F_{0})(∀𝔐 ∈ M_{0})(∀𝔑 ∈ M_{1}) [𝔐 ⊧ φ ⇔ m_{01}(𝔐) ⊧ φ] and [𝔑 ⊧ φ ⇔ m_{10}(𝔑) ⊧ φ] .

Prove that L_{S} and L_{S}^{0} (in Ex.2.1.1) are strongly semantically equivalent.

(5) Combine the equivalences defined in (2) and (4) above. Call this combined concept semantical equivalence. Find logics which are semantically equivalent.

(6) Try to combine (5) and (3) above! ◀

∗ ∗ ∗

SUMMARY (of the logics defined so far):

L_{S}  propositional logic
S5  modal logic, where the accessibility relation is W × W for a set W
L_{D}  difference logic (or “some-other-time” logic)
Tw  twice logic
L_{κ-times} κ-times logic (κ is any cardinal)

L_{bin} L_{more}

L_{PAIR}  set of worlds is arbitrary W ⊆ U × U for some U, extra-Boolean is ∘
L_{REL}  set of worlds is U × U for some U, extra-Boolean is ∘
L_{ARROW} set of worlds is arbitrary W ⊆ U × U for some U, extra-Booleans are
∘, ^{⌣}, Id

L_{RA}  (logic of relation algebras) set of worlds is U × U, extra-Booleans are
∘, ^{⌣}, Id
L_{n}  first-order logic restricted to the first n variables (n ∈ ω)
L_{FOL}  (rank-free) first-order logic

DISTINGUISHED PROPERTIES to be checked for every logic L: (The reason for looking at these properties is that they distinguish first-order like logics from propositional like logics.) dec The set of all valid formulas of L is decidable. (Briefly: L is decidable.) r.e. The set of all valid formulas of L is recursively enumerable. (Briefly: L is r.e.) fmp L has the finite model property that is,

(∀φ ∈ F_{L})[⊧_{L} φ ⟺ (∀𝔐 ∈ M_{L})(𝔐 is finite^{8} ⇒ 𝔐 ⊧_{L} φ)].

Gip L has Gödel’s incompleteness property that is,

(∃φ ∈ F_{L})(∀T ⊆ F_{L})[(φ ∈ T and T is consistent) ⟹
⟹ Csq_{L}(T) is undecidable)].

clm We say that the distinction between set-models and class-models counts in L (L has clm for short) iff (roughly speaking)^{9} even in the case when the set P of atomic formulas of L is finite, we have

(∃ class-model 𝔐)[Th_{L}(𝔐) is not definable without parameters in our Set Theory].

unm Assuming again that the set P of atomic formulas of L is finite, there is some 𝔐 ∈ M_{L} such that Th_{L}(𝔐) is undecidable (unm abbreviates existence of \underline{un}decidable \underline{m}odel).

Exercise 2.2.32: Prove that if L is r.e. and L has the fmp the L is decidable. ◀ COMPARISON OF LOGICS w.r.t. the distinguished properties above: (An arrow points to the place where the property in question becomes true “moving from left to right”. Hence in principle it should always point to a gap between two logics.)

8𝔐 = ⟨W, v⟩ is called finite if W is a finite set.

9Recall that for fixed 𝔐, mng_{𝔐}(φ) was defined by recursion on the complexity of φ in case of each of our distinguished logics discussed so far. (This was so in L_{S}, …, in L_{n}, and also in L_{F OL} to mention only a few.) Saying that Th(𝔐) is undefinable implies that our recursive definition of mng_{𝔐} becomes incorrect as a definition if we permit 𝔐 to be a class model. Roughly, L has clm of Tarski’s Undefinability of Truth Theorem is applicable to L. For more on this property of logics see [ANSK, Appendix B].

|
| L_{3}
| |||
L_{S} S5 Tw . . . . . . L_{n-times} … L_{PAIR} L_{REL} | L_{RA} L_{n} L_{FOL}
|  (n > 3)
? ? |
| |
| |
| |
unm clm no fmp not dec Gip |
|
|

obviously obviously propositional first-order

Figure 2.2.1

Exercise 2.2.33: Check which claims represented on Figure 2.2.1 above were asked as an exercise in the text. Try to prove (and claim, if necessary) the missing ones too. ◀

∗ ∗ ∗

The following logics are of a different “flavor” than the ones seen so far. They include Lambek Calculus, some fragments of Linear Logic, Pratt’s Action Logic, Dynamic Logic, different kinds of semantics than seen so far. The main purpose of giving them is to indicate that the methods of algebraic logic are applicable almost to any unusual logic coming from completely different paradigms of logical or linguistic or computer science research areas, and are not restricted to the kinds of logics discussed so far. If the reader is already convinced, then he may safely skip Definitions 2.2.28–2.2.31.

Some further logics, which are even less similar to the ones discussed so far, are collected in Appendix A. It is advisable to look into Appendix A because our theorems apply to all the logics discussed there. The only reason why those logics are postponed to an appendix is that we did not want to postpone the main theorems too much. For example, infinite valued logics, relevant logics and partial logics are in Appendix A.

DEFINITION 2.2.28 (Lambek Calculus [slightly extended]): Recall the logic L_{RA} (Def.2.2.19). The connectives of Lambek calculus L_{LC} are {∧, ∘, \, /, →}. This defines the formulas F_{LC} of Lambek Calculus. Now,

L_{LC} =^{def} ⟨F_{LC}, M_{RA}, mng_{LC}, ⊧_{LC}⟩ ,

where for all φ, ψ ∈ F_{LC} and all 𝔐 ∈ M_{RA}

mng_{LC}(φ\ψ, 𝔐) =^{def} mng_{RA}(¬(φ^{⌣} ∘ ¬ψ), 𝔐),
mng_{LC}(φ/ψ, 𝔐) =^{def} mng_{RA}(¬(¬φ ∘ ψ^{⌣}), 𝔐),
mng_{LC}(φ → ψ, 𝔐) =^{def} mng_{RA}(¬φ ∨ ψ, 𝔐),

and ⊧_{LC} is defined analogously to ⊧_{RA}. ◀ REMARK 2.2.29: Original Lambek Calculus is only a fragment of L_{LC} because in the original case the use of “→” is restricted. (In any formula, “→” can be used only once, and it is the outer most connective.)

The methods of the present work yielded quite a few results for Lambek Calculus and for some further fragments of Linear Logic, cf. Andréka–Mikulás [AM93]. ◀

DEFINITION 2.2.30 (Language model for Lambek Calculus and other logics [e.g. arrow logic]):

(1) Notation: Recall that U^{∗} denotes the set of all finite sequences over the set U. A set X ⊆ U^{∗} is called a language (in the syntactic sense). Let X, Y ⊆ U^{∗}. Then X ∗ Y = {s^{∩}q : s ∈ X and q ∈ Y }, where s^{∩}q is the concatenation of s and q.

M_{L} =^{def} {⟨U, f⟩ : U is a set and f : P ⟶ U^{∗}} .

We write mng(φ) instead of mng_{L}(φ, ⟨U, f⟩).

mng(p_{i}) =^{def} f(p_{i}) for p_{i} ∈ P,
mng(φ ∧ ψ) =^{def} mng(φ) ∩ mng(ψ),
mng(φ ∘ ψ) =^{def} mng(φ) ∗ mng(ψ),
mng(φ → ψ) =^{def} [U^{∗} ∖ mng(φ)] ∪ mng(ψ),
mng(φ\ψ) =^{def} {q : (∀s ∈ mng(φ)) s^{∩}q ∈ mng(ψ)},
mng(φ/ψ) =^{def} {s : (∀q ∈ mng(ψ)) s^{∩}q ∈ mng(φ)} .

Now, ⊧_{L} is defined as before.

(2) Lambek calculus with language models is

L_{LCL} =^{def} ⟨F_{LC}, M_{L}, mng_{L}, ⊧_{L}⟩ .

This is quite a well investigated logic, and in some respects behaves slightly differently from L_{LC}.

Now we can extend the definition of mng_{L} to the connectives ¬, ^{⌣} and Id as follows:

mng(¬φ) =^{def} U^{∗}mng(φ),
mng(φ^{⌣}) =^{def} {⟨s_{n}, …, s_{1}⟩ : ⟨s_{1}, …, s_{n}⟩ ∈ mng(φ)},
mng(Id) =^{def} {⟨⟩},

where ⟨⟩ denotes the sequence of length 0.

(3) Extended Lambek calculus with language models: F_{LC}^{+} has all the Booleans as connectives in addition to F_{LC}, and the semantics described in (1) above.

L_{LCL}^{+} = ⟨F_{LC}^{+}, M_{L}, mng_{L}, ⊧_{L}⟩ .

(4) Arrow Logic with language models is

L_{ARROWL} = ⟨F_{ARROW}^{+}, M_{L}, mng_{L}, ⊧_{L}⟩ . ◀

DEFINITION 2.2.31 (Dynamic Arrow Logic): Recall the definition of L_{RA}. Add the unary connective ^{∗} sending φ to φ^{∗}. The set of formulas (denoted as F_{DL}) of Dynamic Arrow Logic is defined as that of L_{RA} together with the following clause:

φ ∈ F_{DL} ⟹ φ^{∗} ∈ F_{DL} .

The semantics of this connective is defined by

mng_{DL}(φ^{∗}, 𝔐) =^{def} “reflexive and transitive closure of the relation mng_{DL}(φ, 𝔐)”.

This defines ⊧^{∗} from ⊧_{RA}. Now, Dynamic Arrow Logic is

L_{DL} = ⟨F_{DL}, M_{RA}, mng_{DL}, ⊧^{∗}⟩ .

Pratt’s original dynamic logic can easily and naturally be interpreted into L_{DL}. For more on Dynamic Arrow Logic cf. e.g. van Benthem [Be92], Marx [Ma92]. ◀

Answers/solutions for important and hard exercises of section 2.2

Ex’s.2.2.16:

(2) L_{PAIR} is decidable.

There is a model 𝔐 ∈ M_{PAIR} such that Th_{L_{PAIR}}(𝔐) is not even recursively enumerable. See the hint for Ex’s.2.2.16 (3).

(5) A.Simon proved that for finite Ax, Csq_{L_{PAIR}}(Ax) is decidable. He proved that the logic L_{PAIR}+“♢ of S5” is still decidable; then, using ♢, Ax ⊧ φ is equivalent to validity of a single formula (see Simon [Si92/b]).

Ex’s.2.2.18:

(3) L_{REL} is undecidable. This hint is for the case you know that the word problem of semigroups [or equivalently, the quasi-equational theory of semigroups] is undecidable. Define a computable function f which to every quasi-equation q in the language of semigroups associates f(q) ∈ F_{REL} such that

⊧_{REL} f(q) ⟺ Semigroups ⊧ q.

Conclude that L_{REL} cannot be decidable because that would provide a decision algorithm for the quasi-equations of semigroups. There are other ways of handling this problem besides the “semigroup” one, cf. e.g. the important book Tarski–Givant [TG87].

There is a formula φ ∈ F_{REL} such that Csq_{L_{REL}}({φ}) is undecidable. Moreover, L_{REL} has the Gödel’s incompleteness property that is,

(∃φ ∈ F_{REL})(∀T ⊆ F_{REL})[(φ ∈ T and T is consistent) ⟹
⟹ Csq_{L_{REL}}(T) is undecidable)].

Observe the contrast between L_{PAIR} and L_{REL}!

(4) The others (Ex’s.2.2.3 (3)–(5) for L_{REL}) follow from the corresponding answers for Ex’s.2.2.16 above.

Ex’s.2.2.14 (4):

Here we give a very detailed hint for solving this exercise, i.e. for proving that L_{more} is decidable.

Let 𝔄 = ⟨A, ≤, +, O, I⟩ be a structure where ≤ is a binary relation on A, + is a partial binary operation on A (i.e. Dom(+) ⊆ A × A), I ⊆ A and O ∈ I. The diagram of 𝔄, in symbols Δ(𝔄), is defined as follows. Let a_{0}, …, a_{n} be a repetition-free enumeration of A ∖ I. Let x_{0}, …, x_{n} be variables. For any i, j ≤ n let

π(x_{i}, x_{j}) =^{def} \{ \begin{matrix}x_{i} + x_{j} = x_{k} if a_{i} + a_{j} = a_{k} in 𝔄 \\ x_{i} = x_{j}  if a_{i} + a_{j} is not defined in 𝔄, \end{matrix}
ϱ(x_{i}, x_{j}) =^{def} \{ \begin{matrix}x_{i} ≤ x_{j}  if a_{i} ≤ a_{j} in 𝔄 \\ x_{i} ≰ x_{j}  if a_{i} ≰ a_{j} in 𝔄, \end{matrix}
δ(x_{i}, x_{j}) =^{def} π(x_{i}, x_{j}) ∧ ϱ(x_{i}, x_{j}).
Δ(𝔄) =^{def} ∃x_{0} … x_{n}(⋀{δ(x_{i}, x_{j}) : i, j ≤ n}).

We note that Δ(𝔄) is a (first-order) formula containing only + and ≤, therefore it is decidable whether this formula is valid in standard arithmetic or not.

We say that 𝔄 is a cardinality structure iff the following hold for all a, b ∈ A: ≤ is a linear ordering on A; O is the smallest element, i.e. O ≤ a for every a ∈ A; I is an end segment, i.e. a ∈ I and a ≤ b imply b ∈ I; O + a = a + O = a, a + b = b if a ≤ b and b ∈ I; a + b ∈ I implies (a ∈ I or b ∈ I); + is commutative and associative in the sense that

if a + b exists then b + a exists and a + b = b + a;

a + b, (a + b) + c exist iff b + c, a + (b + c) exist and (a + b) + c = a + (b + c); ⟨N, ≤, +⟩ ⊧ Δ(𝔄).

We say that (𝔄, κ) is an abstract cardinality model, in symbols (𝔄, κ) ∈ ACMod, iff 𝔄 is a cardinality structure; κ : P(P) → A (where P is the set of atomic formulas of L_{more}); ∑⟨κ(H) : H ∈ H⟩ exists for all H ⊆ P(P), where ∑ refers to addition in 𝔄.

Now let (𝔄, κ) ∈ ACMod and χ ∈ F_{more}. We define σ(χ) ⊆ P(P) by induction on the complexity of the formula χ as follows.

σ(p) =^{def} {H ∈ P(P) : p ∈ H} if p ∈ P;

σ(φ ∧ ψ) =^{def} σ(φ) ∩ σ(ψ);

σ(¬φ) =^{def} P(P) ∖ σ(φ);

σ(♦(φ, ψ)) =^{def} \{ \begin{matrix}P(P)  if ∑⟨κ(H) : H ∈ σ(φ)⟩ ≥ ∑⟨κ(H) : H ∈ σ(ψ)⟩ \\ ∅  otherwise. \end{matrix}

(𝔄, κ) ⊧ φ ⟺^{def} σ(φ) = P(P).

Show that the following gives an algorithm for deciding validity of φ:

φ is valid in L_{more}

iff (𝔄, κ) ⊧ φ for all (𝔄, κ) ∈ ACMod such that |A| ≤ 2^{2^{|P |}}.

3. Bridge between the world of logics and the world of algebras

The algebraic counterpart of classical sentential logic L_{S} is the variety BA of Boolean algebras. Why is this so important? The answer lies in the general experience that it is usually much easier to solve a problem concerning L_{S} by translating it to BA, solving the algebraic problem, and then translating the result back to L_{S} (than solving it directly in L_{S}).

In this section we extend applicability of BA to L_{S} to applicability of algebra in general to logics in general. We will introduce a standard translation method from logic to algebra, which to each logic L associates a class of algebras Alg_{⊧}(L). (Of course, Alg_{⊧}(L_{S}) will be BA.) Further, this translation method will tell us how to find the algebraic question corresponding to a logical question. If the logical question is about L then its algebraic equivalent will be about Alg_{⊧}(L). For example, if we want to decide whether L has the proof theoretic property called Craig’s interpolation property, then it is sufficient to decide whether Alg_{⊧}(L) has the so called amalgamation property (for which there are powerful methods in the literature of algebra). If the logical question concerns connections between several logics, say between L_{1} and L_{2}, then the algebraic question will be about connections between Alg_{⊧}(L_{1}) and Alg_{⊧}(L_{2}). (The latter are quite often simpler, hence easier to investigate.)

3.1. Fine-tuning the framework

The definition of a logic in section 2.1 is very wide. Actually, it is too wide for proving interesting theorems about logics. Now we will define a subclass of logics which we will call nice logics. Our notion of a nice logic is wide enough to cover the logics mentioned in the previous section, moreover, it is broad enough to cover almost all logics investigated in the literature. (Certain quantifier logics might need a little reformulation for this, but that reformulation does not effect the essential aspects of the logic in question as we will see.) On the other hand, the class of nice logics is narrow enough for proving interesting theorems about them, that is, we will be able to establish typical logical facts that hold for most logics studied in the literature.

Before reading Def.3.1.1 below, it might be useful to contemplate the common features of the logics studied so far, e.g. L_{S}, S5, L_{ARW0}, L_{n} (cf. section 2.2).

In all the logics studied so far the biconditional “↔” is available as a derived connective. In condition (3) of Def.3.1.1 below new symbols “Δ_{0}”, …,“Δ_{n−1}” will occur, denoting derived connectives of the logic in question. Certainly, condition (3) is a weaker assumption than expressibility of “↔” (n = 1, “Δ_{0}”=“↔”), thus all theorems remain true for this simpler case.

We also note that the theorems of section 3.2 below (based on the next definition) can be proved in a more general setting (cf. [ANSK]). Here we do restrictions in order to make the methodology more transparent. The reader who would find the definition below too restrictive is asked to consult section 4 “Generalizations”, where several conditions are either eliminated or it is explained how to eliminate them, and references are given where the elimination is done.

DEFINITION 3.1.1 (nice logic, strongly nice logic, structural logic): Let L = ⟨F, M, mng, ⊧⟩ be a logic in the sense of Definition 2.1.3.

We say that L is a 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 some rank rank(c) ∈ ω. The set of all logical connectives of rank k is denoted by Cn_{k}(L).

There is a set P, called the set of atomic formulas (or parameters or propositional variables), such that F is the smallest set satisfying conditions (a–b) below.

(a) P ⊆ F,
(b) if c ∈ Cn_{k}(L) and φ_{1}, …, φ_{k} ∈ F then c(φ_{1}, …, φ_{k}) ∈ F.

The word-algebra generated by P using the logical connectives from Cn(L) as algebraic operations is denoted by 𝔉, that is, 𝔉 = ⟨F, c⟩_{c∈Cn(L)}. 𝔉 is called the formula algebra of L.

(2) The function mng_{𝔐} =^{def} ⟨mng(φ, 𝔐) : φ ∈ F ⟩ is a homomorphism from 𝔉, for every 𝔐 ∈ 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)(∀φ, ψ ∈ F)[mng_{𝔐}(φ) = mng_{𝔐}(ψ) ⟺ (∀i < n) 𝔐 ⊧ φΔ_{i}ψ]. (ii) (∀𝔐 ∈ M)(∀φ ∈ F)[𝔐 ⊧ φ ⟺ (∀j < m)(∀i < n) 𝔐 ⊧ ε_{j}(φ)Δ_{i}δ_{j}(φ)].

(By “derived” we mean that “ε_{j}”, “δ_{j}” and “Δ_{i}” are not necessarily members of Cn(L). They are only “built up” from elements of Cn(L). But we do not know from which elements of Cn(L) they are built up, or how. We do not care!)

(4) (∀ψ, φ_{0}, …, φ_{k} ∈ F)(∀p_{0}, …, p_{k} ∈ P)[⊧ ψ(\overline{p}) ⟹ ⊧ ψ(\overline{p}/\overline{φ})], where \overline{p} = ⟨p_{0}, …, p_{k}⟩, \overline{φ} = ⟨φ_{0}, …, φ_{k}⟩, and ψ(\overline{p}/\overline{φ}) denotes the formula that we get from ψ after simultaneously substituting φ_{i} for every occurrence of p_{i} (i ⩽ k) in ψ. We refer to this condition as ‘L has the substitution property’.

L is called strongly nice iff it is nice and satisfies condition (5) below.

(5) (∀s ∈ ^{P} F)(∀𝔐 ∈ M)(∃𝔑 ∈ M)(∀φ(p_{i_{0}}, …, p_{i_{k}}) ∈ F)

(+)  mng_{𝔑}(φ) = mng_{𝔐}(φ(p_{i_{0}}/s(p_{i_{0}}), …, p_{i_{k}}/s(p_{i_{k}}))) .

Let ŝ ∈ ^{F} F be the natural extension of s to 𝔉. Then (+) says mng_{𝔑}(φ) = mng_{𝔐}(ŝ(φ)). If this property holds, then we say that the logic ‘L has the semantical substitution property’ (the model 𝔑 is the substituted version of 𝔐 along substitution s).

Logics satisfying conditions (1), (2) and (5) above are called structural logics. ◀

Recall that if 𝔄 and 𝔅 are two similar algebras, then Hom(𝔄, 𝔅) denotes the set of all homomorphisms from 𝔄 into 𝔅 (cf. [Sa94]). REMARKS 3.1.2:

(i) An equivalent form of (+) above is the very natural condition

(∀h ∈ Hom(𝔉, 𝔉)) (∀𝔐 ∈ M)(∃𝔑 ∈ M) mng_{𝔑} = mng_{𝔐} ∘ h .

Since h is just a substitution, this form makes it explicit that 𝔑 is the hsubstituted version of 𝔐. Another equivalent version is the following.

(∀𝔐 ∈ M)(∀h ∈ Hom(𝔉, mng_{𝔐}(𝔉)))(∃𝔑 ∈ M) mng_{𝔑} = h.

(ii) Item (2) of Definition 3.1.1 above is a purely logical criterion. Namely, it is

Frége’s principle of compositionality. (iii) Conditions (1–3) of Def.3.1.1 above imply condition (⋆) of Def.2.1.3. (iv) A special case of condition (3) of Def.3.1.1 above is the case of m = 1, ε_{0}(φ) =

True, δ_{0}(φ) = φ. This simplification implies the following connection between ⊧ and mng:

(∀φ, ψ ∈ F)[⊧ φ and ⊧ ψ ⟹ (∀𝔐 ∈ M) mng_{𝔐}(φ) = mng_{𝔐}(ψ)].

This does not follow from the original condition.

(v) In the presence of (3) of Definition 3.1.1 above, semantical substitution property (5) implies substitution property (4). ◀

REMARK 3.1.3 (Connections with the Blok–Pigozzi approach): Here we mention only a small part of these connections.

The ⟨F_{L}, ⊧_{L}⟩ part^{10} of a strongly nice, consequence compact (see Def.3.2.10 below) logic L is always an algebraizable deductive system in the sense of Blok–Pigozzi [BP89] (which is an algebraizable 1-deductive system in [BP94]). The other way round, if ⟨F, ⊢⟩ is an algebraizable deductive system then L_{⊢}, as defined in Remark 2.1.2 above, is always a strongly nice consequence compact logic in our sense. Sructural logics and the connections between the two approaches are discussed in more detail in Font–Jansana [FJ94].

A small sample of references of the Blok–Pigozzi approach is [BP89], [BP94], [BP91], [Pi91], Czelakowski [Cz93], Font–Jansana [FJ93]. ◀

Exercises 3.1.4:

(1) (Important!) Show that all the logics introduced in Defs.2.2.1–2.2.21 above are strongly nice logics. It is especially important to do it for L_{n}!

(2) Show that L_{FOL} (cf. Def.2.2.23) is a nice logic. ◀ Exercise 3.1.5: Show logics where n = 1 but “Δ_{0}” is not our old biconditional “↔”. (E.g., in S5 we can also take □(Φ_{1} ↔ Φ_{2}) as Φ_{1}Δ_{0}Φ_{2}.) Show logics where n > 1. ◀

10Here ⊧_{L} denotes the semantical consequence relation induced by the validity relation of L.

For any class K of similar algebras, IK =^{def} {𝔐 : (∃𝔑 ∈ K) 𝔐 is isomorphic to 𝔑} (cf. [Sa94]). DEFINITION 3.1.6: (algebraic counterpart of a logic)

Let L = ⟨F, M, mng, ⊧⟩ be a logic satisfying conditions (1),(2) of Definition 3.1.1.

(i) Let K ⊆ M. Then for every φ, ψ ∈ F

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

Then ∼_{K} is an equivalence relation, which is a congruence on 𝔉 by condition (2) of Def.3.1.1. 𝔉/∼_{K} denotes the factor-algebra of 𝔉, factorized by ∼_{K}. Now,

Alg_{⊧}(L) =^{def} I {𝔉/∼_{K} : K ⊆ M} .

(ii)

Alg_{m}(L) =^{def} {mng_{𝔐}(𝔉) : 𝔐 ∈ M} ,

where mng_{𝔐} was defined in item (2) of Definition 3.1.1, and for any homomorphism h : 𝔄 ⟶ 𝔅, h(𝔄) is the homomorphic image of 𝔄 along h i.e., h(𝔄) is the smallest subalgebra of 𝔅 such that h : 𝔄 ⟶ h(𝔄) (cf. [Sa94]). ◀

REMARK 3.1.7: In the definition of Alg_{m}(L) above, it is important that Alg_{m}(L) is not an elementary class in the sense that it is not closed under isomorphisms. The reason for defining Alg_{m}(L) in such a way is that since Alg_{m}(L) is the class of algebraic counterparts of the models of L, we need these algebras as concrete algebras and replacing them with their isomophic copies would lead to loss of information (about semantic-model theoretic matters). See e.g. Thm.B10 in Appendix B about the algebraic characterization of the weak Beth definability property. ◀

FACT 3.1.8: Let L be a logic satisfying conditions (1–3(i)) of Def.3.1.1. Then

Alg_{⊧}(L) = I {𝔉/∼_{Mod_{L}(Γ)} : Γ ⊆ F } .

Proof: For every K ⊆ M, 𝔉/∼_{K}= 𝔉/∼_{Mod_{L}(T h_{L}(K))} holds (cf. Defs.2.1.5 and 2.1.6). ◀

Exercise 3.1.9: Show that for any logic L satisfying conditions (1),(2) of Def.3.1.1 • Alg_{m}(L) ⊆ Alg_{⊧}(L)

• SPAlg_{⊧}(L) = SPAlg_{m}(L). ◀

Exercise 3.1.10: Prove that (i) Alg_{m}(L_{S}) ⊆“class of all Boolean set algebras” (ii) Alg_{m}(S5) ⊆“class of all one-dimensional cylindric set algebras” ◀ THEOREM 3.1.11. For any logic L = ⟨F, M, mng, ⊧⟩ satisfying conditions (1),(2) of Definition 3.1.1

Alg_{⊧}(L) ⊆ SPAlg_{m}(L).

Proof: Let 𝔄 ∈ Alg_{⊧}(L) that is, let 𝔄 ≅ 𝔉/∼_{K} for some class K ⊆ M. Then there is a subset K′ ⊆ K such that 𝔉/∼_{K}= 𝔉/∼_{K′} (this holds because F is always a set). Now we can define an embedding h from 𝔉/∼_{K′} into P_{𝔐∈K′}mng_{𝔐}(𝔉) as follows. For each φ ∈ F

h (φ/∼_{K′}) =^{def} ⟨mng_{𝔐}(φ) : 𝔐 ∈ K′⟩.

∗ ∗ ∗

Next we turn to inference systems. Inference systems (usually denoted as ⊢) are syntactical devices serving to recapture (or at least to approximate) the semantical consequence relation of the logic L. The idea is the following. Suppose Σ⊧_{L}φ. This means that, in the logic L, the assumptions collected in Σ semantically imply the conclusion φ. (In any possible world 𝔐 of L that is, in any 𝔐 ∈ M_{L}, whenever Σ is valid in 𝔐, then also φ is valid in 𝔐.) Then we would like to be able to reproduce this relationship between Σ and φ by purely syntactical, “finitistic” means. That is, by applying some formal rules of inference (and some axioms of the logic L) we would like to be able to derive φ from Σ by using “paper and pencil” only. In particular, such a derivation will always be a finite string of symbols. If we can do this, that will be denoted by Σ ⊢ φ.

DEFINITION 3.1.12 (formula scheme):

Let L be a logic satisfying condition (1) of Def.3.1.1, with the set Cn(L) of logical connectives. Fix a countable set A = {A_{i} : i < ω}, called the set of formula variables. The set Fms_{L} of formula schemes of L is the smallest set satisfying conditions (a–b) below.

(a) A ⊆ Fms_{L},
(b) if c ∈ Cn_{k}(L) and Φ_{1}, …, Φ_{k} ∈ Fms_{L} then c(Φ_{1}, …, Φ_{k}) ∈ Fms_{L}.

An instance of a formula scheme is given by substituting formulas for the formula variables in it. ◀

DEFINITION 3.1.13 (Hilbert-style inference system):

Let L be a logic satisfying condition (1) of Def.3.1.1. An inference rule of L is a pair ⟨⟨B_{1}, …, B_{n}⟩, B_{0}⟩, where every B_{i} (i ⩽ n) is a formula scheme. This inference rule will be denoted by

\frac{B_{1}, …, B_{n}}{B_{0}} .

An instance of an inference rule is given by substituting formulas for the formula variables in the formula schemes occurring in the rule.

A Hilbert-style inference system (or calculus) for L is a finite set of formula schemes (called axiom schemes or axioms) together with a finite set of inference rules. ◀ DEFINITION 3.1.14 (derivability):

Let L be a logic satisfying condition (1) of Def.3.1.1 and let ⊢ be a Hilbert-style inference system for L. Assume Σ ∪ {φ} ⊆ F_{L}. We say that φ is ⊢-derivable (or ⊢- provable) from Σ iff there is a finite sequence ⟨φ_{1}, …, φ_{n}⟩ of formulas (an ⊢-proof of φ from Σ) such that φ_{n} is φ and for every 1 ⩽ i ⩽ n

• φ_{i} ∈ Σ or

• φ_{i} is an instance of an axiom scheme (an axiom for short) of ⊢ or

• there are j_{1}, ..., j_{k} < i, and there is an inference rule of ⊢ such that \frac{φ_{j_{1}} ,...,φ_{j_{k}}}{φ_{i}} is

an instance of this rule. We write Σ ⊢ φ if φ is ⊢-provable from Σ. (We will often identify an inference system ⊢ with the corresponding derivability relation.) ◀

DEFINITION 3.1.15 (complete and sound Hilbert-type inference system):

Let L be a logic satisfying condition (1) of Def.3.1.1 and let ⊢ be a Hilbert-type inference system for L. Then

• ⊢ is weakly complete for L iff

(∀φ ∈ F_{L}) (⊧_{L} φ ⟹ ⊢ φ) ;

• ⊢ is finitely complete for L iff

(∀Σ ⊆_{ω} F_{L})(∀φ ∈ F_{L}) (Σ ⊧_{L} φ ⟹ Σ ⊢ φ) ;

that is, we consider only finite Σ’s;

• ⊢ is strongly complete for L iff

(∀Σ ⊆ F_{L})(∀φ ∈ F_{L}) (Σ ⊧_{L} φ ⟹ Σ ⊢ φ) ;

• ⊢ is weakly sound for L iff

(∀φ ∈ F_{L}) (⊢ φ ⟹ ⊧_{L} φ) ;

• ⊢ is strongly sound for L iff

(∀Σ ⊆ F_{L})(∀φ ∈ F_{L}) (Σ ⊢ φ ⟹ Σ ⊧_{L} φ) . ◀

3.2. Algebraic characterizations of completeness and compactness properties via Alg_{m} and Alg_{⊧} (main theorems)

THEOREM 3.2.1.

(i) Let L = ⟨F, M, mng, ⊧_{L}⟩^{11} be a strongly nice logic. Then for any formulas φ_{0}, φ_{1}, …, φ_{k},

{φ_{1}, …, φ_{k}} ⊧_{L} φ_{0} ⟹ for each j < m

Alg_{m}(L) ⊧ ⋀{ε_{i}(φ_{s}) = δ_{i}(φ_{s}) : 1 ≤ s ≤ k, i < m} ⇒ (ε_{j}(φ_{0}) = δ_{j}(φ_{0})).

(ii) Let L be a logic satisfying conditions (1–3(i)) of Def.3.1.1. Then for any quasiequation q of form (τ_{1} = τ′_{1} ∧ ⋯ ∧ τ_{k} = τ′_{k} ⇒ τ_{0} = τ′_{0}),

Alg_{m}(L) ⊧ q ⟹ {τ_{s}Δ_{j}τ′_{s} : 1 ≤ s ≤ k, j < n} ⊧_{L} τ_{0}Δ_{i}τ′_{0} for each i < n.

Proof of (i): Assume p_{0}, …, p_{ℓ} are the only atomic formulas occurring in φ_{0}, …, φ_{k} and assume that

{φ_{1}(p_{0}, …, p_{ℓ}), …, φ_{k}(p_{0}, …, p_{ℓ})} ⊧_{L} φ_{0}(p_{0}, …, p_{ℓ}).

Let 𝔄 ∈ Alg_{m}(L). Then 𝔄 = mng_{𝔐}(𝔉) for some 𝔐 ∈ M. Let a ∈ ^{P} A be arbitrary. For every i ≤ ℓ we denote a_{i} =^{def} a(p_{i}). Clearly for every i ≤ ℓ a_{i} = mng_{𝔐}(γ_{i}) for some γ_{i} ∈ F. For every s ≤ k

φ_{s}[a_{0}, …, a_{ℓ}]^{𝔄} = φ_{s}[mng_{𝔐}(γ_{0}), …, mng_{𝔐}(γ_{ℓ})]^{𝔄} = mng_{𝔐}(φ_{s}(γ_{0}, …, γ_{ℓ})),

since mng_{𝔐} is a homomorphism by (2) of Def.3.1.1.

Assume that for every 1 ≤ s ≤ k and j < m, 𝔄 ⊧ (ε_{j}(φ_{s}) = δ_{j}(φ_{s}))[a].

⟺ mng_{𝔐}(ε_{j}(φ_{s}(γ_{0}, …, γ_{ℓ}))) = mng_{𝔐}(δ_{j}(φ_{s}(γ_{0}, …, γ_{ℓ}))) (1 ≤ s ≤ k, j < m)

⟹^{(by Def.3.1.1 (5))} (∃𝔑) mng_{𝔑}(ε_{j}(φ_{s})) = mng_{𝔑}(δ_{j}(φ_{s})) (1 ≤ s ≤ k, j < m)

⟺^{(by Def.3.1.1 (3))} 𝔑 ⊧_{L} φ_{s} (1 ≤ s ≤ k)

⟹^{(by our assumption)} 𝔑 ⊧_{L} φ_{0}

⟺^{(by Def.3.1.1 (3))} mng_{𝔑}(ε_{j}(φ_{0})) = mng_{𝔑}(δ_{j}(φ_{0})) (j < m)

⟹^{(by Def.3.1.1 (5))} mng_{𝔐}(ε_{j}(φ_{0}(γ_{0}, …, γ_{ℓ}))) = mng_{𝔐}(δ_{j}(φ_{0}(γ_{0}, …, γ_{ℓ}))) (j < m)

⟺ 𝔄 ⊧ (ε_{j}(φ_{0}) = δ_{j}(φ_{0}))[a], (j < m)

proving Thm.3.2.1 (i), since a was chosen arbitrarily.

11During the proofs of the main theorems we make a careful distinction between ⊧_{L} and ⊧, using the former symbol for the validity (and semantical consequence) relation of logic L and ⊧ for the usual first-order validity relation.

Proof of (ii): Assume that for every 𝔄 ∈ Alg_{m}(L) and for every valuation a ∈ ^{P} A

𝔄 ⊧ q[a].

Let 𝔐 ∈ M such that 𝔐 ⊧_{L} {τ_{s}Δ_{i}τ′_{s} : 1 ≤ s ≤ k, i < n}. Then by Def.3.1.1 (3)(i) mng_{𝔐}(τ_{s}) = mng_{𝔐}(τ′_{s}) for each 1 ≤ s ≤ k. Now let 𝔄 =^{def} mng_{𝔐}(𝔉) and let a ∈ ^{P} A be such that for each p ∈ P a(p) =^{def} mng_{𝔐}(p). Then

𝔄 ⊧ (τ_{1} = τ′_{1} ∧ ⋯ ∧ τ_{k} = τ′_{k})[a],

which implies by our assumption that 𝔄 ⊧ (τ_{0} = τ′_{0})[a]. This is the same as mng_{𝔐}(τ_{0}) = mng_{𝔐}(τ′_{0}), thus again by Definition 3.1.1 (3)(i), 𝔐 ⊧_{L} τ_{0}Δ_{i}τ′_{0} for each i < n, which proves Thm.3.2.1 (ii).

COROLLARY 3.2.2. Let L be a nice logic.

(i) For any formula φ,

⊧_{L} φ ⟹ Alg_{m}(L) ⊧ ε_{j}(φ) = δ_{j}(φ) for each j < m.

(ii) For any equation τ = τ′,

Alg_{m}(L) ⊧ τ = τ′ ⟹ ⊧_{L} τΔ_{i}τ′ for each i < n.

Proof: Item (ii) is a special case of item (ii) of Thm.3.2.1, but now we have to prove (i) for nice logics, cf. Def.3.1.1.

Assume ⊧_{L} φ(p_{0}, …, p_{ℓ}). Let 𝔄 ∈ Alg_{m}(L). Then 𝔄 = mng_{𝔐}(𝔉) for some 𝔐 ∈ M. Let a ∈ ^{P} A be arbitrary. We denote a_{0} =^{def} a(p_{0}), …, a_{ℓ} =^{def} a(p_{ℓ}). Clearly (∀s ≤ ℓ) (a_{s} = mng_{𝔐}(γ_{s}) for some γ_{s} ∈ F).

φ[a_{0}, …, a_{ℓ}]^{𝔄} = φ[mng_{𝔐}(γ_{0}), …, mng_{𝔐}(γ_{ℓ})]^{𝔄} = mng_{𝔐} (φ(γ_{0}, …, γ_{ℓ})) ,

since mng_{𝔐} is a homomorphism.

⊧_{L} φ(p_{0}, …, p_{ℓ}) implies, by Def.3.1.1 (4), that ⊧_{L} φ(γ_{0}, …, γ_{ℓ}). Thus by Def.3.1.1 (3), for each j < m

mng_{𝔐}(ε_{j}(φ(γ_{0}, …, γ_{ℓ}))) = mng_{𝔐}(δ_{j}(φ(γ_{0}, …, γ_{ℓ}))) .

But

mng_{𝔐}(ε_{j}(φ(γ_{0}, …, γ_{ℓ}))) = ε_{j}(φ)[a]^{𝔄} and
mng_{𝔐}(δ_{j}(φ(γ_{0}, …, γ_{ℓ}))) = δ_{j}(φ)[a]^{𝔄} (j < m).

Thus we have 𝔄 ⊧ (ε_{j}(φ) = δ_{j}(φ))[a] for each j < m, completing the proof since a was chosen arbitrarily.

In Theorem 3.2.3 below, we will give a sufficent and necessary condition for a strongly nice logic to have a finitely complete Hilbert-style inference system.

THEOREM 3.2.3. Assume L is a strongly nice logic and Cn(L) is finite^{12}. . Then

Alg_{m}(L) generates a finitely axiomatizable quasi-variety ⟺ (∃ Hilbert-style ⊢)(⊢ is finitely complete and strongly sound for L).

Proof of (⟹):

Notation Let Φ_{0}, Φ_{1}, … denote formula variables, τ_{0}, τ_{1}, … denote formula schemes, \overline{Φ} denote sequence of formula variables and \overline{x} denote sequence of variables. Let m and n (m, n ∈ ω) denote the number of ε_{j}’s and Δ_{i}’s, respectively. For any formula schemes τ, τ′, let τΔτ′ abbreviate the system τΔ_{0}τ′, …, τΔ_{n−1}τ′ of formula schemes.

Now assume that Ax is a finite set of quasi-equations axiomatizing the quasi-variety generated by Alg_{m}(L) and define a Hilbert-style inference system ⊢_{Ax} as follows:

Axiom schemes: Φ_{0}Δ_{i}Φ_{0} (i < n).

Inference rules: If [(τ_{1}(\overline{x}) = τ′_{1}(\overline{x}) ∧ ⋯ ∧ τ_{k}(\overline{x}) = τ′_{k}(\overline{x})) ⇒ τ_{0}(\overline{x}) = τ′_{0}(\overline{x})] ∈ Ax, then

\frac{τ_{1}(\overline{Φ})Δτ′_{1}(\overline{Φ}), …, τ_{k}(\overline{Φ})Δτ′_{k}(\overline{Φ})}{τ_{0}(\overline{Φ})Δ_{i}τ′_{0}(\overline{Φ})}

is a rule for each i < n. Other rules are:

(∀i < n) \frac{Φ_{0}ΔΦ_{1}, Φ_{1}ΔΦ_{2}}{Φ_{0}Δ_{i}Φ_{2}} ,

(∀i < n) \frac{Φ_{0}ΔΦ_{1}}{Φ_{1}Δ_{i}Φ_{0}} ,

(∀c ∈ Cn_{ℓ}(L))(∀i < n) \frac{Φ_{1}ΔΦ′_{1}, …, Φ_{ℓ}ΔΦ′_{ℓ}}{c(Φ_{1}, …, Φ_{ℓ})Δ_{i}c(Φ′_{1}, …, Φ′_{ℓ})},

\frac{ε_{0}(Φ_{0})Δδ_{0}(Φ_{0}), …, ε_{m−1}(Φ_{0})Δδ_{m−1}(Φ_{0})}{Φ_{0}},

(∀i < n)(∀j < m) \frac{Φ_{0}}{ε_{j}(Φ_{0})Δ_{i}δ_{j}(Φ_{0})} .

We will show that the inference system ⊢_{Ax} is finitely complete and strongly sound for L.

For any set Σ of formulas we define

ψ ∼_{Σ} ψ′ ⟺^{def} Σ ⊢_{Ax} {ψΔ_{i}ψ′ : i < n}.

Note that, by the definition of ⊢_{Ax} and by the definition of derivability (Def.3.1.14), ∼_{Σ} is a congruence relation on 𝔉 for any Σ.

12One can eliminate the assumption of Cn(L) being finite. Then the finitary character of a Hilbert-style inference system has to be ensured in a more subtle way. Also, “finitely axiomatizable quasi-variety”

must be replaced by “finite schema axiomatizable quasi-variety” in the second clause, cf. e.g. Monk [M69], Németi [N91].

Claim 3.2.3.1: For any Σ ⊆ F, (𝔉/∼_{Σ}) ⊧ Ax. Proof of Claim 3.2.3.1: Let q ∈ Ax and assume that q is of form

(τ_{1}(\overline{x}) = τ′_{1}(\overline{x}) ∧ ⋯ ∧ τ_{k}(\overline{x}) = τ′_{k}(\overline{x})) ⇒ τ_{0}(\overline{x}) = τ′_{0}(\overline{x}) .

Let 𝔄 =^{def} (𝔉/∼_{Σ}). We want to prove that, for every valuation a of the variables into 𝔄, 𝔄 ⊧ q[a].

So let a be an arbitrary valuation into 𝔄. Then (∀i ∈ ω) a(x_{i}) = φ_{i}/∼_{Σ} for some φ_{i} ∈ F. Assume that

𝔄 ⊧ τ_{1}[\overline{φ/∼_{Σ}}] = τ′_{1}[\overline{φ/∼_{Σ}}] ∧ ⋯ ∧ τ_{k}[\overline{φ/∼_{Σ}}] = τ′_{k}[\overline{φ/∼_{Σ}}].

Then

(τ_{1}(\overline{φ}))/∼_{Σ}= (τ′_{1}(\overline{φ}))/∼_{Σ}, …, (τ_{k}(\overline{φ}))/∼_{Σ}= (τ′_{k}(\overline{φ}))/∼_{Σ},

since ∼_{Σ} is a congruence on 𝔉. Then

τ_{1} (\overline{φ}) ∼_{Σ} τ′_{1} (\overline{φ}) , …, τ_{k} (\overline{φ}) ∼_{Σ} τ′_{k} (\overline{φ})

that is,

Σ ⊢_{Ax} \{τ_{j} (\overline{φ}) Δ_{i}τ′_{j} (\overline{φ}) : 1 ≤ j ≤ k, i < n\}

by the definition of ∼_{Σ}. In ⊢_{Ax}, we have the following rule for each i < n (corresponding to quasiequation q):

\frac{τ_{1}(\overline{Φ})Δτ′_{1}(\overline{Φ}), …, τ_{k}(\overline{Φ})Δτ′_{k}(\overline{Φ})}{τ_{0}(\overline{Φ})Δ_{i}τ′_{0}(\overline{Φ})} .

By these rules, we get that Σ ⊢_{Ax} τ_{0} (\overline{φ}) Δ_{i}τ′_{0} (\overline{φ}) for each i < n. Then τ_{0} (\overline{φ}) ∼_{Σ} τ′_{0} (\overline{φ}), whence (τ_{0} (\overline{φ}))/∼_{Σ}= (τ′_{0} (\overline{φ}))/∼_{Σ} that is, 𝔄 ⊧ τ_{0}[\overline{φ/∼_{Σ}}] = τ′_{0}[\overline{φ/ ∼_{Σ}}] which implies 𝔄 ⊧ (τ_{0}(\overline{x}) = τ′_{0}(\overline{x}))[a]. By this we proved Claim 3.2.3.1.

Now let Σ =^{def} {φ_{1}, …, φ_{k}} and assume Σ ⊧_{L} φ_{0}. Then, by Thm.3.2.1 (i),

Alg_{m}(L) ⊧ ⋀{ε_{i}(φ_{s}) = δ_{i}(φ_{s}) : 1 ≤ s ≤ k, i < m} ⇒ (ε_{j}(φ_{0}) = δ_{j}(φ_{0})) (j < m)

⟹ Ax ⊧ ⋀{ε_{i}(φ_{s}) = δ_{i}(φ_{s}) : 1 ≤ s ≤ k, i < m} ⇒ (ε_{j}(φ_{0}) = δ_{j}(φ_{0})) (j < m)

⟹^{(Claim 3.2.3.1)} (𝔉/∼_{Σ}) ⊧ ⋀{ε_{i}(φ_{s}) = δ_{i}(φ_{s}) : 1 ≤ s ≤ k, i < m} ⇒

⇒ (ε_{j}(φ_{0}) = δ_{j}(φ_{0})) (j < m)

⟹ [if ((∀i < m)(∀1 ≤ s ≤ k) ε_{i}(φ_{s}) ∼_{Σ} δ_{i}(φ_{s})) then (∀j < m) ε_{j}(φ_{0}) ∼_{Σ} δ_{j}(φ_{0})]

⟺ [if ((∀ℓ < n)(∀i < m)(∀1 ≤ s ≤ k) Σ ⊢_{Ax} ε_{i}(φ_{s})Δ_{ℓ}δ_{i}(φ_{s}))

then (∀ℓ < n)(∀j < m) Σ ⊢_{Ax} ε_{j}(φ_{0})Δ_{ℓ}δ_{j}(φ_{0})]. (•)

By the rules \frac{Φ_{0}}{ε_{i}(Φ_{0})Δ_{ℓ}δ_{i}(Φ_{0})} we have Σ ⊢_{Ax} ε_{i}(φ_{s})Δ_{ℓ}δ_{i}(φ_{s}) for every i < m, ℓ < n, 1 ≤ s ≤ k. Thus, by (•), Σ ⊢_{Ax} ε_{j}(φ_{0})Δ_{ℓ}δ_{j}(φ_{0}) holds for each ℓ < n, j < m. Now using the rule \frac{ε_{0}(Φ_{0})Δδ_{0}(Φ_{0}),...,ε_{m−1}(Φ_{0})Δδ_{m−1}(Φ_{0})}{Φ_{0}} we get Σ ⊢_{Ax} φ_{0}, proving the finite completeness of ⊢_{Ax}.

The strong soundness of ⊢_{Ax} can be proved by induction on the length of the ⊢_{Ax}- proof of φ_{0} from {φ_{1}, …, φ_{k}}. We only show one part of the induction step, namely the case when φ_{0} is ’obtained’ by one of the inference rules corresponding to a quasi-equation q ∈ Ax. Say q has the form

(τ_{1}(\overline{x}) = τ′_{1}(\overline{x}) ∧ ⋯ ∧ τ_{r}(\overline{x}) = τ′_{r}(\overline{x})) ⇒ τ_{0}(\overline{x}) = τ′_{0}(\overline{x}) ,

where \overline{x} = ⟨x_{1}, …, x_{z}⟩. Then a corresponding inference rule is

\frac{τ_{1}(\overline{Φ})Δτ′_{1}(\overline{Φ}), …, τ_{r}(\overline{Φ})Δτ′_{r}(\overline{Φ})}{τ_{0}(\overline{Φ})Δ_{i}τ′_{0}(\overline{Φ})} ,

for some i < n. Assume that φ_{0} is obtained with the help of this rule by substituting the members of the sequence \overline{γ} = ⟨γ_{1}, …, γ_{z}⟩ of formulas for the members of the sequence \overline{Φ} = ⟨Φ_{1}, …, Φ_{z}⟩ of formula variables, i.e. φ_{0} has the form τ_{0}(\overline{γ})Δ_{i}τ′_{0}(\overline{γ}).

Now fix a model 𝔐 and assume that

𝔐 ⊧_{L} τ_{1}(\overline{γ})Δτ′_{1}(\overline{γ}), …, 𝔐 ⊧_{L} τ_{r}(\overline{γ})Δτ′_{r}(\overline{γ}).

We have to show that 𝔐 ⊧_{L} τ_{0}(\overline{γ})Δ_{i}τ′_{0}(\overline{γ}).

Let 𝔄 =^{def} mng_{𝔐}(𝔉) ∈ Alg_{m}(L). and let a be a valuation of 𝔄 such that for every 1 ≤ v ≤ z a(x_{v}) =^{def} mng_{𝔐}(γ_{v}). Then by Definition 3.1.1 (3)(i)

(∀1 ≤ j ≤ r) mng_{𝔐}(τ_{j}(\overline{γ})) = mng_{𝔐}(τ′_{j}(\overline{γ}))
⟺ 𝔄 ⊧ (τ_{1}(\overline{x}) = τ′_{1}(\overline{x}) ∧ ⋯ ∧ τ_{r}(\overline{x}) = τ′_{r}(\overline{x}))[a]
(by Alg_{m}(L) ⊧ Ax) ⟹ 𝔄 ⊧ (τ_{0}(\overline{x}) = τ′_{0}(\overline{x}))[a]
(by Def.3.1.1 (3)(i)) ⟹ 𝔐 ⊧_{L} τ_{0}(\overline{γ})Δ_{i}τ′_{0}(\overline{γ}).

This completes the proof of direction “⟹” of Theorem 3.2.3.

Proof of (⟸): Let Φ_{1}, …, Φ_{z} denote formula variables, τ_{0}, τ_{1}, …, τ_{k} denote formula schemes, let \overline{Φ} =^{def} ⟨Φ_{1}, …, Φ_{z}⟩, and let \overline{x} =^{def} ⟨x_{1}, …, x_{z}⟩ be a sequence of variables. Assume that ⊢ is a finitely complete and strongly sound Hilbert-type inference system for the logic L, and define the finite set Ax of quasi-equations as follows:

(1) If τ_{0}(\overline{Φ}) is an axiom scheme of ⊢ then let “ε_{j}(τ_{0}(\overline{x})) = δ_{j}(τ_{0}(\overline{x}))” belong to Ax for each j < m.

(2) If \frac{τ_{1}(\overline{Φ}),...,τ_{k}(\overline{Φ})}{τ_{0}(\overline{Φ})} is an inference rule of ⊢ then let

“ ⋀\{ε_{i}(τ_{s}(\overline{x})) = δ_{i}(τ_{s}(\overline{x})) : 1 ≤ s ≤ k, i < m\} ⇒ ε_{j}(τ_{0}(\overline{x})) = δ_{j}(τ_{0}(\overline{x}))”

belong to Ax for each j < m.

(3) Let “ε_{j}(x_{0}Δ_{i}x_{0}) = δ_{j}(x_{0}Δ_{i}x_{0})” belong to Ax for each i < n, j < m.

(4) Let “⋀{ε_{j}(x_{0}Δ_{i}x_{1}) = δ_{j}(x_{0}Δ_{i}x_{1}) : j < m, i < n} ⇒ (x_{0} = x_{1})” belong to Ax.

We will show that Ax axiomatizes the quasi-variety generated by Alg_{m}(L).

Claim 3.2.3.2: Alg_{m}(L) ⊧ Ax. Proof of Claim 3.2.3.2: Quasi-equations of type (3) and (4) above obviously hold in Alg_{m}(L) by Definition 3.1.1 (3).

Now consider a quasi-equation of type (2). Let 𝔄 ∈ Alg_{m}(L) and let a be an arbitrary valuation of the variables into 𝔄. Let 𝔐 be such that 𝔄 = mng_{𝔐}(𝔉). Then for every i ∈ ω a(x_{i}) = mng_{𝔐}(φ_{i}) for some φ_{i} ∈ F. Assume that

𝔄 ⊧ ⋀\{ε_{i}(τ_{s}(\overline{x})) = δ_{i}(τ_{s}(\overline{x})) : 1 ≤ s ≤ k, i < m\}[a].

Then by Definition 3.1.1 (3)

(••)  𝔐 ⊧_{L} τ_{s}(x_{1}/φ_{1}, …, x_{z}/φ_{z}) (for each 1 ≤ s ≤ k).

But \frac{τ_{1}(\overline{Φ}),...,τ_{k}(\overline{Φ})}{τ_{0}(\overline{Φ})} is an inference rule of ⊢, therefore \{τ_{1}(\overline{φ}), …, τ_{k}(\overline{φ})\} ⊢ τ_{0}(\overline{φ}). This implies by the strong soundness of ⊢ that \{τ_{1}(\overline{φ}), …, τ_{k}(\overline{φ})\} ⊧_{L} τ_{0}(\overline{φ}). Now, by (••) above, 𝔐 ⊧ τ_{0}(\overline{φ}), hence again by Definition 3.1.1 (3), 𝔄 ⊧ (ε_{j}(τ_{0}(\overline{x})) = δ_{j}(τ_{0}(\overline{x})))[a] for each j < m, which was desired.

The case of equations of type (1) can be proved similarly.

Claim 3.2.3.3: For any formulas φ_{0}, φ_{1}, …, φ_{k},

{φ_{1}, …, φ_{k}} ⊢ φ_{0} ⟹

⟹ Ax ⊧ ⋀{ε_{i}(φ_{s}) = δ_{i}(φ_{s}) : 1 ≤ s ≤ k, i < m} ⇒ (ε_{j}(φ_{0}) = δ_{j}(φ_{0}))

for each j < m. Proof of Claim 3.2.3.3: It can be proved by induction on the length of the ⊢-proof of φ_{0} from {φ_{1}, …, φ_{k}}. We only show one part of the induction step, namely the case when φ_{0} is ’obtained’ by an inference rule \frac{τ_{1}(\overline{Φ}),...,τ_{r}(\overline{Φ})}{τ_{0}(\overline{Φ})}, where \overline{Φ} = ⟨Φ_{1}, …, Φ_{z}⟩. Then there are formulas γ_{1}, …, γ_{z} such that φ_{0} = τ_{0}(γ_{1}, …, γ_{z}) and for every 1 ≤ ℓ ≤ r \{φ_{1}, …, φ_{k}\} ⊢ τ_{ℓ}(\overline{γ}). Then by the induction hypothesis

Ax ⊧ ⋀{ε_{i}(φ_{s}) = δ_{i}(φ_{s}) : 1 ≤ s ≤ k, i < m} ⇒

⇒ ε_{j}(τ_{ℓ}(\overline{γ})) = δ_{j}(τ_{ℓ}(\overline{γ})) (for each j < m, 1 ≤ ℓ ≤ r). (♮)

By the definition of Ax

Ax ⊧ ⋀\{ε_{i}(τ_{ℓ}(\overline{x})) = δ_{i}(τ_{ℓ}(\overline{x})) : 1 ≤ ℓ ≤ r, i < m\} ⇒

⇒ ε_{j}(τ_{0}(\overline{x})) = δ_{j}(τ_{0}(\overline{x})) (for each j < m). (♮♮)

Let 𝔅 be an algebra with 𝔅 ⊧ Ax and let b be any valuation of the variables into B. Now we can define a valuation b′ with b′(x_{v}) =^{def} γ_{v}[b]^{𝔅} (1 ≤ v ≤ z). Then for every 0 ≤ ℓ ≤ r τ_{ℓ}(\overline{x})[b′]^{𝔅} = τ_{ℓ}(\overline{γ})[b]^{𝔅}. Thus, by (♮) and (♮♮),

𝔅 ⊧ ⋀\{ε_{i}(φ_{s}) = δ_{i}(φ_{s}) : 1 ≤ s ≤ k, i < m\} ⇒ (ε_{j}(τ_{0}(\overline{γ})) = δ_{j}(τ_{0}(\overline{γ})))[b]

for each j < m, which was desired.

Now we can prove that each quasi-equation which holds in Alg_{m}(L) is a consequence of Ax. Assume that

Alg_{m}(L) ⊧ (τ_{1} = τ′_{1} ∧ ⋯ ∧ τ_{k} = τ′_{k}) ⇒ τ_{0} = τ′_{0}.

⟹^{(Thm.3.2.1 (ii))} {τ_{s}Δ_{j}τ′_{s} : 1 ≤ s ≤ k, j < n} ⊧_{L} τ_{0}Δ_{i}τ′_{0} for each i < n

⟹^{(finite completeness)} {τ_{s}Δ_{j}τ′_{s} : 1 ≤ s ≤ k, j < n} ⊢ τ_{0}Δ_{i}τ′_{0} for each i < n

⟹^{(Claim 3.2.3.3)} Ax ⊧ ⋀{ε_{ℓ}(τ_{s}Δ_{j}τ′_{s}) = δ_{ℓ}(τ_{s}Δ_{j}τ′_{s}) : ℓ < m, 1 ≤ s ≤ k, j < n} ⇒

⇒ (ε_{p}(τ_{0}Δ_{i}τ′_{0}) = δ_{p}(τ_{0}Δ_{i}τ′_{0})) for all p < m, i < n.

But, since quasi-equations of type (3) and (4) belong to Ax, this implies to

Ax ⊧ (τ_{1} = τ′_{1} ∧ ⋯ ∧ τ_{k} = τ′_{k}) ⇒ τ_{0} = τ′_{0},

completing the proof of direction “⟸” of Theorem 3.2.3.

Having found the algebraic counterpart of “finitely complete”, let us try to characterize “weakly complete”. Since weak completeness is slightly weaker than finite completeness, we have to weaken the algebraic counterpart of finite completeness for characterizing weak completeness. This way we obtain condition (∗) below, where Eq_{L} and Qeq_{L} denote the set of all equations and the set of all quasi-equations, respectively, of the language of Alg_{m}(L) (cf. [Sa94]).

(∗) (∃Ax ⊆_{ω} Qeq_{L}) [(∀e ∈ Eq_{L}) (Alg_{m}(L) ⊧ e ⟹ Ax ⊧ e) & Alg_{m}(L) ⊧ Ax] .

That is, the equational theory of Alg_{m}(L) is finitely axiomatizable by quasi-equations valid in Alg_{m}(L).

THEOREM 3.2.4. Assume that L is nice and Cn(L) is finite^{13} . Then

(∗) ⟺ (∃ Hilbert-style ⊢)(⊢ is weakly complete and strongly sound for L) .

In particular, if the equational theory of Alg_{m}(L) is finitely axiomatizable, then L admits a weakly complete Hilbert-style inference system. Proof: It is similar to the proof of Theorem 3.2.3. The only important difference is that Theorem 3.2.4 already holds for nice logics. However, the only part of the proof of Theorem 3.2.3 which used the additional criterion for strong niceness (Definition 3.1.1 (5)) was Thm.3.2.1 (i). Here one has to use Cor.3.2.2 (i) instead.

13cf. the footnote of Theorem 3.2.3.

Exercise 3.2.5: Give weakly complete and sound calculi for the logics L_{S} and S5. (Hint: Use that the SP-closure of the Alg_{m}-image of these logics are finitely axiomatizable varieties, so (∗) is satisfied.) ◀

DEFINITION 3.2.6 (deduction theorem, deduction term):

Let L = ⟨F_{L}, M_{L}, mng_{L}, ⊧_{L}⟩ be a logic satisfying condition (1) of Def.3.1.1. We say that L has a deduction theorem, iff

(∃(Φ_{1}∇Φ_{2}) ∈ F ms_{L})) (∀Σ ⊆ F_{L})(∀φ, ψ ∈ F_{L}) (Σ ∪ {φ} ⊧_{L} ψ ⟺ Σ ⊧_{L} φ∇ψ) ,

where ”φ∇ψ” denotes an instance of scheme ”Φ_{1}∇Φ_{2}”. Such a ”Φ_{1}∇Φ_{2}” is called a deduction term for L. ◀

PROPOSITION 3.2.7. L_{S} and S5 have deduction terms.

Proof: It is not hard to show that ”Φ_{1} → Φ_{2}” and ”□Φ_{1} → □Φ_{2}” (where □ is the abbreviation of ¬♢¬) are suitable deduction terms for L_{S} and S5, respectively.

The following theorem states that for any nice logic the existence of a deduction term and that of a weakly complete Hilbert-style calculus provides a finitely complete inference system.

THEOREM 3.2.8. Assume L is alogic satisfying (1) of Def.3.1.1. Assume L has a deduction theorem, and there is some Hilbert-style inference system which is weakly complete and strongly sound for L. Then

(∃ Hilbert-style ⊢)(⊢ is finitely complete and strongly sound for L) .

First we note the following fact (its proof is straightforward by the assumptions on ∇).

Fact 3.2.9: The inference rule modus ponens w.r.t. ∇ (MP_{∇}) that is,

(MP_{∇})  \frac{Φ_{1}, Φ_{1}∇Φ_{2}}{Φ_{2}}

is strongly sound for L.

Proof of Theorem 3.2.8: Assume that there is some Hilbert-style inference system which is weakly complete and strongly sound for L. Let such an inference system be fixed and let us add (MP_{∇}) to it. We denote this (extended) inference system by ⊢.

To prove finite completeness, assume {φ_{0}, …, φ_{n}} ⊧ ψ. Then, applying the deduction theorem n + 1 times, we get:

{φ_{0}, …, φ_{n−1}} ⊧ (φ_{n}∇ψ)
{φ_{0}, …, φ_{n−2}} ⊧ (φ_{n−1}∇(φ_{n}∇ψ))

⋮

⊧ \underbrace{(φ_{0}∇(φ_{1}∇ … (φ_{n}∇ψ) …)}_{γ_{0}} .

Then ⊢ γ_{0} by weak completeness of ⊢. Then, using (MP_{∇}) n + 1 times, we get:

\{φ_{0}\} ⊢ \{φ_{0}, γ_{0}\} ⊢ \underbrace{φ_{1}∇(φ_{2}∇ … (φ_{n}∇ψ) …)}_{γ_{1}}
\{φ_{0}, φ_{1}\} ⊢ \{φ_{1}, γ_{1}\} ⊢ \underbrace{φ_{2}∇(φ_{2}∇ … (φ_{n}∇ψ) …)}_{γ_{2}}

⋮  ⋮
{φ_{0}, φ_{1}, …, φ_{n}} ⊢ {φ_{n}, γ_{n}} ⊢ ψ , where γ_{n} = (φ_{n}∇ψ).

Thus we received the following ⊢-proof of ψ from {φ_{0}, …, φ_{n}}:

⟨γ_{0}, φ_{0}, γ_{1}, φ_{1}, γ_{2}, φ_{2}, …, γ_{n}φ_{n}, ψ⟩ ,

which proves Theorem 3.2.8.

DEFINITION 3.2.10 (compactness of a logic):

Let L = ⟨F_{L}, M_{L}, mng_{L}, ⊧_{L}⟩ be a logic. We say that

(i) L is satisfiability compact (sat. compact for short), if

(∀Γ ⊆ F_{L})[(∀Σ ⊆_{ω} Γ) (Σ has a model) ⟹ (Γ has a model)] , and

(ii) L is consequence compact (cons. compact), if for every Γ ∪ {φ} ⊆ F_{L}

Γ ⊧_{L} φ ⟹ (∃Σ ⊆_{ω} Γ) Σ ⊧_{L} φ. ◀

Exercise 3.2.11: Prove that even for nice logics we have (1) sat. compact ≠⇒ cons. compact;

(2) sat. compact ⇍= cons. compact.

(Hint for (1): Let the logical connectives be Δ (binary), and True, k_{0}, …, k_{n}, … all zero-ary. A model 𝔐 is a function 𝔐 : {True, p_{i}, k_{i} : i ∈ ω} → {0, 1}. mng_{𝔐}(True) = 1 for every 𝔐 and meaning of Δ is the standard meaning of the biconditional ↔. Exclude those models from M in which (∀ i > 0) 𝔐(k_{i}) = 1 but 𝔐(k_{0}) = 0. [This logic is not strongly nice!] Observe that for 𝔐 = {True, p_{i}, k_{i} : i ∈ ω} × {1} we have 𝔐 ⊧_{L} F_{L}. Hence sat. completeness trivially holds.)

(Hint for (2): Let L have True and Δ as the only logical connectives. Exclude the models 𝔐 with 𝔐 ⊧_{L} F_{L}. Then sat. completeness fails (we have infinitely many propositional variables). Show that cons. completeness remains true.) ◀

Exercise 3.2.12: Find natural conditions under which “⟹” and/or “⟸” of Exercise 3.2.11 above hold.

(1) We say that L has weak false if (∃φ ∈ F_{L}) such that (∀𝔐 ∈ M_{L}) 𝔐 |̸=_{L} φ. Show that under this assumption

cons. compact ⟹ sat. compact.

(2) We say that L has negation if

(∀φ ∈ F_{L})(∃ψ ∈ F_{L})(∀𝔐 ∈ M_{L})[𝔐 ⊧_{L} ψ ⟺ 𝔐 |̸=_{L} φ] .

Show that under this assumption

sat. compact ⟹ cons. compact.

(3) Try to find weaker sufficient conditions.

(4) Show that for nice logics

L has weak false ⟺ L has negation.

For more information about the two notions of compactness, see [ANSK]. ◀

∗ ∗ ∗

Recall that in Definition 3.1.1 (and also in the logics studied so far), there was a parameter P, which was the set of atomic formulas. The choice of P influenced what the set F of formulas would be. Thus in fact, our old definition of a logic yields a family

⟨⟨F^{P} , M^{P} , mng^{P} , ⊧^{P} ⟩ : P is a set⟩

of logics.

DEFINITION 3.2.13 (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 sense of Def.2.1.3.

L is called a nice [strongly nice, structural] general logic iff conditions (1–4) below hold for L.

(1) L^{P} is a nice [strongly nice, structural] logic (cf. Def.3.1.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} (j < m) and Δ_{i} (i < n) are the same for any logic L^{P} (cf. Def.3.1.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 𝔉^{P} onto 𝔉^{Q} extending f;

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

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

(4) For all sets P ⊆ Q,

{mng_{𝔐}^{P} : 𝔐 ∈ M^{P} } = {(mng_{𝔐}^{Q}) ↾ F^{P} : 𝔐 ∈ M^{Q}} .

(Intuitively, condition (4) says that L^{P} is the “natural” restriction of L^{Q}.) ◀

REMARK 3.2.14: We note that if L is a nice general logic then L has the following property. For all sets P ⊆ Q,

{{φ ∈ F^{P} : 𝔐 ⊧^{P} φ} : 𝔐 ∈ M^{P} } = {{φ ∈ F^{P} : 𝔑 ⊧^{Q} φ} : 𝔑 ∈ M^{Q}} .

Moreover, for all Γ ∪ {φ} ⊆ F^{P},

Γ ⊧^{P} φ ⟺ Γ ⊧^{Q} φ.

However, (5) below does not automatically hold for all strongly nice logics.

(5) For each P ⊆ Q there is a “reduct-function” r : M^{Q} ⟶ M^{P} with Rng(r) = M^{P} such that

(∀𝔐 ∈ M^{Q})(∀φ ∈ F^{P})[(𝔐 ⊧^{Q} φ ⟺ r(𝔐) ⊧^{P} φ) and mng_{𝔐}^{Q}(φ) = mng_{r(𝔐)}^{P}(φ)] .

We will not assume and use condition (5), but it can be useful for investigations of the Beth definability properties (and related issues) which are (partially) treated in Appendix B. ◀

DEFINITION 3.2.15 (algebraic counterpart of a general logic):

Let L = ⟨L^{P} : P is a set⟩ be a nice or structural general logic. Then

Alg_{⊧}(L) =^{def} ⋃ {Alg_{⊧}(L^{P}) : P is a set} ,
Alg_{m}(L) =^{def} ⋃ {Alg_{m}(L^{P}) : P is a set}

(cf. Def.3.1.6). ◀ Exercise 3.2.16: Prove that

(i) Alg_{m}(L_{S}) =“class of all Boolean set algebras”

(ii) Alg_{m}(L_{S5}) =“class of all one-dimensional cylindric set algebras”

(cf. Defs.2.2.1 and 2.2.4). (Hint: The part “⊆” will be easy. If you would encounter cardinality difficulties in the other direction, e.g. a Boolean algebra 𝔄 with |A| too big, then choose the set P of atomic formulas to be bigger than |A|.) ◀

THEOREM 3.2.17. For structural general logics

Alg_{⊧}(L) = SPAlg_{m}(L).

Proof: First we not that, by Thm.3.1.11, Alg_{⊧}(L^{P}) ⊆ SPAlg_{m}(L^{P}) for any set P, thus Alg_{⊧}(L) ⊆ SPAlg_{m}(L) holds.

To prove SPAlg_{m}(L) ⊆ Alg_{⊧}(L) we need Claims 3.2.17.1 and 3.2.17.2 below.

Claim 3.2.17.1: For any sets P, Q, algebra 𝔄 ∈ Alg_{m}(L^{Q}) and homomorphism h : 𝔉^{P} → 𝔄,

(∃𝔑 ∈ M^{P})(∀φ ∈ F^{P}) h(φ) = mng_{𝔑}^{P}(φ).

Proof of Claim 3.2.17.1: Let 𝔐 ∈ M^{Q} be such that 𝔄 = mng_{𝔐}^{Q}. Then

(∗)  (∀p ∈ P)(∃φ_{p} ∈ F^{Q}) h(p) = mng_{𝔐}^{Q}(φ_{p}).

Because of condition (3) of Def.3.2.13 without loss of generality we can assume that either P ⊆ Q or Q ⊆ P hold.

1^{st} case : Q ⊆ P

Then, by (4) of Def.3.2.13,

(∗∗)  (∃𝔐′ ∈ M^{P})(∀p ∈ P) mng_{𝔐′}^{P}(φ_{p}) = mng_{𝔐}^{Q}(φ_{p}) = h(p).

Let s : P → F^{P} be defined by s(p) =^{def} φ_{p}, for any p ∈ P. Then, by (5) of Def.3.1.1,

(∗ ∗ ∗)  (∃𝔑 ∈ M^{P})(∀p ∈ P) mng_{𝔑}^{P}(p) = mng_{𝔐′}^{P}(φ_{p}).

Now (∗), (∗∗) and (∗ ∗ ∗) together imply that (∀p ∈ P) h(p) = mng_{𝔑}^{P}(p).

2^{nd} case : P ⊆ Q

Let s : Q → F^{Q} be defined by

s(p) =^{def} \{ \begin{matrix}φ_{p}, if p ∈ P \\ any element of F^{Q}, else. \end{matrix}

Then, by (5) of Def.3.1.1,

(†)  (∃𝔐′ ∈ M^{Q})(∀p ∈ P) mng_{𝔐′}^{Q}(p) = mng_{𝔐}^{Q}(φ_{p}).

By (4) of Def.3.2.13,

(††)  (∃𝔑 ∈ M^{P})(∀p ∈ P) mng_{𝔑}^{P}(p) = mng_{𝔐′}^{Q}(p).

Then, by (∗), (†) and (††), (∀p ∈ P) mng_{𝔑}^{P}(p) = h(p) holds again.

Claim 3.2.17.2: Let 𝔄 ∈ SPAlg_{m}(L) and let h : 𝔉^{P} ↠ 𝔄 be a surjective homomorphism for some set P. Then

(∃K ⊆ M^{P}) (ker(h) =∼_{K} that is, 𝔄 ≅ 𝔉^{P} /∼_{K}).

Proof of Claim 3.2.17.2: Let 𝔄 ∈ SPAlg_{m}(L). Then there are some sets I and Q_{i} (i ∈ I) and 𝔄_{i} ∈ Alg_{m}(L^{Q_{i}}) such that 𝔄 ⊆ P_{i∈I}𝔄_{i}. For each i ∈ I let π_{i} denote the projection function into 𝔄_{i}. Then, by Claim 3.2.17.1, (∀i ∈ I)(∃𝔑_{i} ∈ M^{P})(∀p ∈ P) (π_{i} ∘ h)(p) = mng_{𝔑_{i}}^{P}(p). Let K =^{def} {𝔑_{i} : i ∈ I}. Then it is easy to check that for any φ, ψ ∈ F^{P},

h(φ) = h(ψ) iff φ ∼_{K} ψ

that is, 𝔄 ≅ 𝔉^{P} /∼_{K}.

Now, to prove SPAlg_{m}(L) ⊆ Alg_{⊧}(L), assume 𝔄 ∈ SPAlg_{m}(L). Let h : 𝔉^{A} ↠ 𝔄 be the usual extension of the identity map of A to a homomorphism. Then, by Claim 3.2.17.2, (∃K ⊆ M^{A}) 𝔄 ≅ 𝔉^{A}/ ∼_{K} that is, 𝔄 ∈ Alg_{⊧}(L), completing the proof of Theorem 3.2.17.

DEFINITION 3.2.18 (compactness of a general logic):

A general logic L = ⟨L^{P} : P is a set⟩ is satisfiability (consequence) compact if for each set P the logic L^{P} is satisfiability (consequence) compact. ◀

Recall that for an arbitrary class K of algebras,

UpK =^{def} I {P_{i∈I}𝔄_{i}/F : F is an ultrafilter over the set I, and (∀i ∈ I) 𝔄_{i} ∈ K} .

We say that K is Up-closed if UpK ⊆ K, in other words, K is Up-closed if it is closed under taking ultraproducts (cf. [Sa94]).

Our next theorem gives a sufficent condition for sat. compactness of a strongly nice general logic.

THEOREM 3.2.19. Let L be a strongly nice general logic. Then

(Alg_{⊧}(L) is Up-closed) ⟹ (L is sat. compact) .

Proof: We let L = ⟨L^{P} : P is a set⟩ We give a proof for the case of P = ω that is, for the compactness of L^{ω} = ⟨F^{ω}, M^{ω}, mng^{ω}, ⊧^{ω}⟩. For other sets the proof is similar and is left to the reader. Assume Γ ⊆ F^{ω} and

(∀Σ ⊆_{ω} Γ) Σ has a model .

Then we may assume that Γ is countable, say Γ = {φ_{0}, φ_{1}, …, φ_{n}, … }_{n∈ω} and

(∀k ∈ ω)(∃𝔐_{k} ∈ M^{ω}) 𝔐_{k} ⊧^{ω} {φ_{0}, …, φ_{k}} .

Let such 𝔐_{k}’s be fixed. Let 𝔄_{k} =^{def} mng_{𝔐_{k}}^{ω}(𝔉^{ω}) ∈ Alg_{m}(L). Then 𝔄_{k} ∈ Alg_{⊧}(L) also holds (by Ex.3.1.9). Let mng_{k} =^{def} mng_{𝔐_{k}}^{ω} ↾ ω. Since ω is the set of atomic formulas of L^{ω}, the function mng_{k} : ω ⟶ A_{k} is a valuation of the (propositional) variables into 𝔄_{k}. Let F be a non-principal ultrafilter over ω, and let 𝔄 =^{def} P_{k∈ω}𝔄_{k}/F denote the ultraproduct of algebras 𝔄_{k} w.r.t. F. We define the function v : ω ⟶ A as follows:

v(i) =^{def} ⟨mng_{k}(i) : k ∈ ω⟩/F .

See Figure 3.2.1 below.

ω
mng_{0}  mng_{k}  v
𝔄_{0}  …  𝔄_{k}  …  ⟹_{lim} 𝔄

Figure 3.2.1

By assumption, 𝔐_{k} ⊧^{ω} φ_{i} for every i ≤ k. Thus, for every i ≤ k ∈ ω, we have the following:

𝔐_{k} ⊧^{ω} φ_{i}

⇕ by Definition 3.1.1 (3)(ii)

𝔐_{k} ⊧^{ω} ε_{j}(φ_{i})Δ_{ℓ}δ_{j}(φ_{i}) for each j < m, ℓ < n

⇕ by Definition 3.1.1 (3)(i)

mng_{𝔐_{k}}^{ω}(ε_{j}(φ_{i})) = mng_{𝔐_{k}}^{ω}(δ_{j}(φ_{i})) for each j < m

⇕

𝔄_{k} ⊧ (ε_{j}(φ_{i}) = δ_{j}(φ_{i}))[mng_{k}] for each j < m.

We derived that (∀k ∈ ω)(∀i ≤ k) 𝔄_{k} ⊧ ⋀_{j<m}(ε_{j}(φ_{i}) = δ_{j}(φ_{i}))[mng_{k}], i.e. for every i ∈ ω, {k ∈ ω : 𝔄_{k} ⊧ ⋀_{j<m}(ε_{j}(φ_{i}) = δ_{j}(φ_{i}))[mng_{k}]} ∈ F. Using Łos’s theorem (cf. [Sa94]), we have that

(∀i ∈ ω) 𝔄 ⊧ ⋀_{j<m}(ε_{j}(φ_{i}) = δ_{j}(φ_{i}))[v] .

Since by our assumption Alg_{⊧}(L) is Up-closed, 𝔄 ∈ Alg_{⊧}(L). Thus, Def.3.2.13 (3), (∃ set P ⊇ ω) (∃K ⊆ M^{P}) 𝔄 ≅ 𝔉^{P} / ∼_{K}. Let iso denote this isomorphism. Let 𝔅 =^{def} 𝔉^{P} /∼_{K}, and let w =^{def} iso ∘ v. Then

(∀i ∈ ω) 𝔅 ⊧ ⋀_{j<m}(ε_{j}(φ_{i}) = δ_{j}(φ_{i}))[w]

that is,

(∀i ∈ ω)(∀j < m) ε_{j}(φ_{i})[w(p_{i_{0}}), …, w(p_{i_{z}})]^{𝔅} = δ_{j}(φ_{i})[w(p_{i_{0}}), …, w(p_{i_{z}})]^{𝔅},

where all the atomic formulas (elements of ω) occurring in φ_{i} are among {p_{i_{0}}, …, p_{i_{z}}}. Let s : P ⟶ F^{P} be such that for all p ∈ ω s(p) is an element of the congruence class w(p). For every i ∈ ω, let φ̂_{i} ∈ F^{P} be φ_{i}(p_{i_{0}}/s(p_{i_{0}}), …, p_{i_{z}}/s(p_{i_{z}})). Then for every i ∈ ω, j < m we have,

ε_{j}(φ_{i})[s(p_{i_{0}})/∼_{K}, …, s(p_{i_{z}})/∼_{K}]^{𝔅} = δ_{j}(φ_{i})[s(p_{i_{0}})/∼_{K}, …, s(p_{i_{z}})/∼_{K}]^{𝔅}
⇓ (∼_{K} is a congruence on 𝔉^{P})
ε_{j}(φ_{i}(s(p_{i_{0}}), …, s(p_{i_{z}})))/∼_{K} = δ_{j}(φ_{i}(s(p_{i_{0}}), …, s(p_{i_{z}})))/∼_{K}
⇕
(†)  ε_{j}(φ̂_{i}) ∼_{K} δ_{j}(φ̂_{i}).

We have that (∀𝔐 ∈ K)(∀i ∈ ω)(∀j < m)

mng_{𝔐}^{P}(ε_{j}(φ̂_{i})) = mng_{𝔐}^{P}(δ_{j}(φ̂_{i})).

Let 𝔐 be any model belonging to K. Then, by (5) of Def.3.1.1, (∃𝔑′ ∈ M^{P}) (∀i ∈ ω) (∀j < m)

mng_{𝔑′}^{P}(ε_{j}(φ_{i})) = mng_{𝔐}^{P}(ε_{j}(φ̂_{i})) = mng_{𝔐}^{P}(δ_{j}(φ̂_{i})) = mng_{𝔑′}^{P}(δ_{j}(φ_{i})).

Since for each i ∈ ω, φ_{i} belongs to F^{ω}, by (3) of Def.3.2.13,

(∃𝔑 ∈ M^{ω})(∀i ∈ ω)(∀j < m) mng_{𝔑}^{ω}(ε_{j}(φ_{i})) = mng_{𝔑}^{ω}(δ_{j}(φ_{i})).

Then, by (3) of Definition 3.1.1,

(∀i ∈ ω) 𝔑 ⊧^{ω} φ_{i},

which proves Theorem 3.2.19.

Our next theorem states that the condition of Theorem 3.2.19 above is sufficient and also necessary for cons. compactness, and so for strong completeness (cf. Theorem 3.2.21 below).

THEOREM 3.2.20. (cf. [ANSK] Thm.2.8) Assume L is a strongly nice general logic. Then

(Alg_{⊧}(L) is Up-closed) ⟺ (L is cons. compact) .

Proof of (⟹): One can push through the proof of Thm.3.2.19 for this case, as follows. Now we want to prove {φ_{i} : i ∈ ω} |̸=^{ω} ψ from the assumption {φ_{0}, …, φ_{k}} |̸=^{ω} ψ for each k ∈ ω. Change 𝔐_{k} in the above proof such that 𝔐_{k} ⊧^{ω} {φ_{0}, …, φ_{k}} and 𝔐_{k} |̸=^{ω} ψ. Drag this “|̸=^{ω} ψ” part through the whole argument in exactly the same style as “⊧^{ω} φ_{k}” was treated in the original proof. Then in line (†) of the proof above we have

(∀i ∈ ω)(∀j < m)  ε_{j}(φ̂_{i}) ∼_{K} δ_{j}(φ̂_{i}) and
(‡)  (∃j < m)  ε_{j}(ψ̂) ≁_{K} δ_{j}(ψ̂).

Now we cannot choose an arbitrary 𝔐 ∈ K but we can infer that there exists some 𝔐 ∈ K such that (∀i ∈ ω) (∀j < m)

mng_{𝔐}^{P}(ε_{j}(φ̂_{i})) = mng_{𝔐}^{P}(δ_{j}(φ̂_{i}))

and (∃j < m)

mng_{𝔐}^{P}(ε_{j}(ψ̂)) ≠ mng_{𝔐}^{P}(δ_{j}(ψ̂)).

Thus, again by (5) of Def. 3.1.1 and by (3) of Def.3.2.13, there is an 𝔑 ∈ M^{ω} with 𝔑 ⊧^{ω} {φ_{i} : i ∈ ω} and 𝔑 |̸=^{ω} ψ, as was desired.

Proof of (⟸): Fix any set I and assume that for each i ∈ I, 𝔄_{i} ∈ Alg_{⊧}(L).

We let 𝔓 =^{def} P_{i∈I}𝔄_{i}. For each X ⊆ I define the congruence R_{X} of 𝔓 as follows.

R_{X} =^{def} {(a, b) ∈ P × P : a ↾ X = b ↾ X} .

Then for each X ⊆ I, 𝔓/R_{X} ≅ P_{i∈X}𝔄_{i} obviously holds. Therefore

𝔓/R_{X} ∈ PAlg_{⊧}(L) ⊆^{Thm.3.1.11} PSPAlg_{m}(L) ⊆ SPAlg_{m}(L)

(cf. e.g. [Sa94] for PSP ⊆ SP). Let h : 𝔉^{P} ↠ 𝔓 be the natural extension of the identity map on P to a homomorphism and let g_{X} : 𝔓 ↠ 𝔓/R_{X} be the quotient map corresponding to R_{X}. Then, by Claim 3.2.17.2, for each X ⊆ I there is some class K_{X} ⊆ M^{P} such that ker(g_{X} ∘ h) =∼_{K_{X}} that is,

(∗)  (∀φ, ψ ∈ F^{P}) [(h(φ), h(ψ)) ∈ R_{X} ⟺ φ ∼_{K_{X}} ψ].

Moreover, an inspection of the proof of Claim 3.2.17.2 shows, that

(∗∗)  X ⊆ Y ⊆ I ⟹ K_{X} ⊆ K_{Y} .

For each X ⊆ I, let Γ_{X} =^{def} T h(K_{X}). Recall (cf. Fact 3.1.8) that ∼_{K_{X}} =∼_{Mod(Γ_{X})} holds.

Claim 3.2.20.1: Let F be any filter on I and let Γ =^{def} ⋃ {Γ_{X} : X ∈ F}. Then for every φ, ψ ∈ F^{P}

φ ∼_{Mod(Γ)} ψ ⟺ (∃X ∈ F) φ ∼_{Mod(Γ_{X})} ψ.

Proof of Claim 3.2.20.1: First, assume that (∃X ∈ F) φ ∼_{Mod(Γ_{X})} ψ. Then, since Γ_{X} ⊆ Γ, φ ∼_{Mod(Γ)} ψ obviously holds.

On the other hand, assume φ ∼_{Mod(Γ)} ψ. Then, by (3) of Def.3.1.1, (∀i < n) Γ ⊧^{P} φΔ_{i}ψ. Then, by the cons. compactness of L^{P}, for each i < n there is some Σ_{i} ⊆_{ω} Γ with Σ_{i} ⊧^{P} φΔ_{i}ψ. Then there is some Σ ⊆_{ω} Γ such that for each i < n Σ ⊧^{P} φΔ_{i}ψ. Say, Σ = {χ_{0}, …, χ_{z−1}}. Since Σ ⊆ Γ, (∀j < z)(∃X_{j} ∈ F) χ_{j} ∈ Γ_{X_{j}}. Let

X =^{def} ⋂{X_{j} : j < z}. Then X ∈ F, since F is a filter. Now Σ ⊆ Γ_{X_{0}} ∪ ⋯ ∪ Γ_{X_{z−1}} ⊆ Γ_{X} holds by (∗∗) above, thus for each i < n, Γ_{X} ⊧^{P} φΔ_{i}ψ, which implies φ ∼_{Mod(Γ_{X})} ψ.

Now we want to prove that 𝔓/F ∈ Alg_{⊧}(L). We show that 𝔓/F ≅ 𝔉^{P} /∼_{Mod(Γ)} (cf. Claim 3.2.20.1 above for the definition of Γ). That is,

(∀φ, ψ ∈ F^{P}) [h(φ) ∼_{F} h(ψ) ⟺ φ ∼_{Mod(Γ)} ψ]

holds. Indeed,

h(φ) ∼_{F} h(ψ)

⟺ (∃X ∈ F) (h(φ), h(ψ)) ∈ R_{X}

⟺^{(∗)} (∃X ∈ F) φ ∼_{Mod(Γ_{X})} ψ

⟺^{Cl.3.2.20.1} φ ∼_{Mod(Γ)} ψ,

which completes the proof of Theorem 3.2.20. We note that we proved that Alg_{⊧}(L) is closed under taking arbitrary reduced products (not only ultraproducts).

THEOREM 3.2.21:

Assume L = ⟨L^{P} : P is a set⟩ is a strongly nice general logic. Then

Alg_{⊧}(L) is a finitely axiomatizable quasi-variety ⟺

(∃ Hilbert-style ⊢)(∀ set P)(⊢ is strongly complete and strongly sound for L^{P}). Proof: To prove Theorem 3.2.21 we need the following lemma. Lemma 3.2.21.1: For every infinite set P and for every quasi-equation q

Alg_{m}(L^{P}) ⊧ q ⟹ Alg_{m}(L) ⊧ q.

Proof of Lemma 3.2.21.1: Fix an infinite set P and a quasi-equation q such that Alg_{m}(L^{P}) ⊧ q. Let 𝔄 ∈ Alg_{m}(L^{Q}) for some set Q. Then there is some 𝔐 ∈ M^{Q} with 𝔄 = mng_{𝔐}^{Q}(𝔉^{Q}). By (3) of Def.3.2.13, without loss of generality we can assume that either P ⊆ Q or Q ⊆ P hold.

First assume that Q ⊆ P. Then, by (4) of Def.3.2.13, (∃𝔑 ∈ M^{P}) mng_{𝔑}^{P} ↾ 𝔉^{Q} = mng_{𝔐}^{Q}. Then 𝔄 ⊆ mng_{𝔑}^{P}(𝔉^{P}) ∈ Alg_{m}(L^{P}), thus 𝔄 ⊧ q, since quasi-equations are preserved under taking subalgebras.

Now let Q ⊇ P and assume that 𝔄 |̸= q[k] for some evaluation k of the variables. Say, let k(x_{i}) =^{def} mng_{𝔐}^{Q}(γ_{i})) (1 ≤ i ≤ n), assuming that x_{1}, …, x_{n} are the only variables occurring free in q. Assume that the atomic formulas occurring in the formulas γ_{1}, …, γ_{n} are among p_{i_{1}}, …, p_{i_{m}} and let s be the following substitution:

(∀1 ≤ j ≤ m) s(p_{j}) =^{def} p_{i_{j}}.

Then, by (5) of Definition 3.1.1,

(∃𝔑 ∈ M^{Q})(∀1 ≤ i ≤ n) mng_{𝔐}^{Q}(γ_{i}) = mng_{𝔑}^{Q}(γ_{i}(p_{i_{1}}/p_{1}, …, p_{i_{m}}/p_{m})).

By (4) of Definition 3.2.13, (∃𝔑′ ∈ M^{P}) mng_{𝔑}^{Q} ↾ 𝔉^{P} = mng_{𝔑′}^{P}. Now, let 𝔅 =^{def} mng_{𝔑′}^{P} and let k′(x_{i}) =^{def} mng_{𝔑′}^{P}(γ_{i}(p_{1}, …, p_{m})). Then 𝔄 |̸= q[k] implies 𝔅 |̸= q[k′], which contradicts to 𝔅 ∈ Alg_{m}(L^{P}).

Proof of (⟹) of Theorem 3.2.21: Assume that Ax is a finite set of quasi-equations axiomatizing Alg_{⊧}(L). Since Alg_{⊧}(L) = SPAlg_{m}(L) (cf. Theorem 3.2.17), by Lemma 3.2.21.1 above, Ax also axiomatizes the quasi-variety generated by Alg_{m}(L^{P}) for each infinite set P. Thus, by Theorem 3.2.3, for each infinite P there is a finitely complete and strongly sound Hilbert-style inference system ⊢ for L^{P}. Moreover, checking the proof of Theorem 3.2.3 one can observe that the same inference system ⊢ works for all infinite sets P.

We show that for any set Q, ⊢ is strongly complete for L^{Q}. Assume that for some Γ ∪ {φ} ⊆ F^{Q} Γ ⊧^{Q} φ. Then there is some infinite set P such that Γ ∪ {φ} ⊆ F^{P} and Γ ⊧^{P} φ (cf. Remark 3.2.14 above). Since quasi-varieties are Up-closed, L^{P} is cons. compact by Theorem 3.2.20. Therefore there is a finite subset Σ of Γ such that Σ ⊧^{P} φ. Thus, by finite completeness Σ ⊢ φ, which implies Γ ⊢ φ by the definition of derivability (Def.3.1.14).

Proof of (⟸) of Theorem 3.2.21: If ⊢ is strongly complete then it is also finitely complete. Thus, by Theorem 3.2.3, the quasi-variety generated by Alg_{m}(L^{P}) is finitely axiomatizable for each set P.

On the other hand, strong completeness implies cons. compactness, as follows. Assume that for some P, Γ∪{φ} ⊆ F^{P} Γ ⊧^{P} φ. Then Γ ⊢ φ, which implies by Definition 3.1.14 that there is a finite subset Σ of Γ such that Σ ⊢ φ. Then, by strong soundness, Σ ⊧^{P} φ. Now, by Theorem 3.2.20, Alg_{⊧}(L) is Up-closed. But by Theorem 3.2.17, it is also closed under S and P, thus it is a quasi-variety (cf. “quasi-variety characterization” in [Sa94]). This and the fact that the quasi-varieties generated by Alg_{m}(L^{P}) are finitely axiomatizable (with the same set Ax of quasi-equations, as the proof of Theorem 3.2.3 shows) imply that Alg_{⊧}(L) is a finitely axiomatizable quasi-variety.

Exercise 3.2.22: Show that L_{S} and S5 have strongly complete and sound Hilbertstyle inference systems. Give such calculi. (Hint: Use that the corresponding classes of algebras (Alg_{m}(L_{S}) = BA and Alg_{m}(L_{S5}) = Cs_{1}) generate finitely axiomatizable varieties.) ◀

In all the above we investigated only some logical properties, e.g. completeness and compactness. However, the literature contains similar theorems for a very large number of further logical properties. Such are e.g. Craig’s interpolation property, the various definability properties (e.g. Beth’s), the property of having a deduction theorem, the property of admitting Gabbay-style inference systems, to mention only a few. Some of these are discussed in Appendix B below.

4. Generalizations

First we relax the assumption on our logic having derived connectives “ε_{j}”, “δ_{j}” (j < m) (cf. Def.3.1.1). We will omit condition (3)(ii) from the definition of a nice logic obtaining the notion of a semi-nice logic.

DEFINITION 4.1 ((strongly) semi-nice (general) logic): Let L = ⟨F, M, mng, ⊧⟩ be a logic in the sense of Def.2.1.3. Then

(i) L is said to be semi-nice if it satisfies conditions (1), (2), (3)(i), (4) of Def.3.1.1. (ii) L is said to be strongly semi-nice if L is semi-nice and it also satisfies condition

(5) of Def.3.1.1. (iii) A (strongly) semi-nice general logic is obtained by replacing “nice logic” with

“semi-nice logic” in condition (1) of Def.3.2.13 (i.e. by doing the natural change in the definition of a (strongly) nice general logic). ◀

Semi-nice logics, even without condition (4) of Def.3.1.1, were investigated in [ANSK] but investigation of the ⊧ relation was restricted to the case of one Δ_{i} and to formulas of the form (φΔ_{0}ψ). Below we indicate how to extend investigation to all formulas, i.e. how to extend the theory described in the present work to semi-nice logics.

To algebraize (in a reversible way) these more general logics, we add a new unary operation symbol “c” to (the language of) our algebras. So the new version Alg_{i}^{+}(L) of Alg_{i}(L) (i ∈ {⊧, m}) will consist of algebras which have an extra operation “C” not available in Alg_{i}(L). However, in order to make our approach work, we have to permit “c” to be a partial operation. This means that for certain elements of our algebras “c” may not be defined. (A classical example of a partial operation is inversion x → x^{−1} in the field of real numbers. Zero has no inverse, so ^{−1} is undefined at argument 0.) Universal algebra for partial algebras (i.e. algebras with partial operations) is well defined, cf. e.g. Burmeister [Bu86], Andréka–Németi [AN76]. Therefore generalizing our previous theorems to the new algebras causes no real difficulty. Those readers who would prefer avoiding partial algebras are asked to consult Remark 4.3 below. It is shown there how to eliminate the partial operation symbol “c”.

DEFINITION 4.2 (Alg_{⊧}^{+}(L), Alg_{m}^{+}(L)): Let L = ⟨F, M, mng, ⊧⟩ be a logic. Assume L satisfies conditions (1), (2) of Def.3.1.1.

Let K ⊆ M. Then we define the partial function c_{K} : F → F in the following way. For any φ ∈ F,

if K ⊧ φ then c_{K}(φ) is defined and c_{K}(φ) = φ; while
if K |̸= φ then c_{K}(φ) is undefined.

Clearly, ⟨𝔉, c_{K}⟩ is a partial algebra for every K ⊆ M. The equivalence relation ∼_{K} (defined in Def.3.1.6) is a congruence not only on 𝔉 but also on ⟨𝔉, c_{K}⟩ (c_{K} was defined in a way to ensure this). Now,

Alg_{⊧}^{+}(L) =^{def} I {⟨𝔉, c_{K}⟩/∼_{K} : K ⊆ M} .

Let us turn to defining Alg_{m}^{+}(L). First we define a new partial function c on the algebra 𝔄(𝔐) =^{def} mng_{𝔐}(𝔉) as follows. For every φ ∈ F,

c(mng_{𝔐}(φ)) =^{def} mng_{𝔐}(φ) if 𝔐 ⊧ φ; else
c(mng_{𝔐}(φ)) is undefined.

The new partial algebra 𝔄^{+}(𝔐) associated to 𝔐 is

𝔄^{+}(𝔐) =^{def} ⟨𝔄(𝔐), c⟩.

Now

Alg_{m}^{+}(L) =^{def} {𝔄^{+}(𝔐) : 𝔐 ∈ M} . ◀

As we mentioned, universal algebra for partial algebras is well developed (cf. op cit). For completeness we recall those notions which are most needed. Since any partial algebra ⟨𝔄, c⟩ is a model in the model theoretic sense (consider “c” as a binary relation), the model theoretic operations like direct products (P), ultraproducts (Up), reduced products (P^{r}) need not de defined. Subalgebras are submodels closed under “c”, i.e. to each element x of our subalgebra, if c is defined on x then c(x) is also in our subalgebra.

Let τ be a term, 𝔄 a partial algebra and k ∈ ^{ω}A an evaluation of the variables. Then, τ is said to be defined at evaluation k (in 𝔄) iff every subterm of τ is defined at k.^{14}

Now, 𝔄 ⊧ (τ = σ)[k] (i.e. evaluation k satisfies the equation τ = σ) iff both τ and σ are defined at evaluation k and their values coincide.

With this we defined the satisfaction for atomic formulas (i.e. equations) of the language of partial algebras. The logical connectives are interpreted the usual way, hence satisfaction (and thus validity) is defined for all formulas of partial algebras. In particular, quasi-equations (τ_{1} = σ_{1} ∧ ⋯ ∧ τ_{n} = σ_{n}) → τ_{0} = σ_{0} are defined and interpreted in the usual way. A class K is said to be a quasi-variety iff it is definable by a set of quasi-equations. It is a variety iff it is definable by equations. The usual theorems carry over, e.g.

K is a quasi-variety iff K = SPUp K = SP^{r} K.

For more cf. [Bu86], [AN76].

With the above in mind, it seems reasonable to repeat for semi-nice logics and Alg_{i}^{+}(L)(i ∈ {⊧, m}) what we did in section 3 for nice logics and Alg_{i}(L)(i ∈ {⊧, m}).

We note that Blok and Pigozzi (cf. [BP89], [BP94] and the references therein) have strong results in this direction (in perhaps a slightly different formulation). Before turning to generalizing section 3 to the present more general setting, we should mention an equivalent form of what we are doing.

14Variables are always defined and c(τ) is defined if [τ is defined and c is defined at the value of τ].

REMARK 4.3: If the reader would like to avoid using partial algebras, then the following equivalent more natural approach works. Instead of “c” we add a new unary predicate “T (x)” (T for truth). Imitating the definition of “c_{K}”, we let T_{K} =^{def} {φ ∈ F : K ⊧ φ} for any K ⊆ M. Similarly, the algebraic counterpart of a model 𝔐 looks like ⟨𝔄, T ⟩, where 𝔄 ∈ Alg_{m}(L) and T ⊆ A such that

(∀φ ∈ F)(𝔐 ⊧ φ ⟺ mng_{𝔐}(φ) ∈ T );

holds for T.

This approach is practically equivalent to the one using “c” instead of “T ”. Further, this is very-very closely related to what is called “matrix semantics” in Blok–Pigozzi [BP89], [BP94], Czelakowski [Cz82] and in the papers quoted in these works. In these papers there are several strong results about the presently outlined approach. ◀

Now, many of the results proved for nice logics so far, can be pushed through for semi-nice logics (with Alg_{⊧}^{+}, Alg_{m}^{+} in place of Alg_{⊧}, Alg_{m}).

For example, the proof of

(Alg_{⊧}^{+}(L) is Up-closed) ⟹ (L is sat. compact)

(cf. Thm.3.2.19) should go through with the natural modifications for semi-nice logics.

For some of the results the formulation of the result needs a minor modification. E.g. the algebraic equation corresponding to logical formula φ is now c(φ) = φ (instead of ε_{j}(φ) = δ_{j}(φ) for all j < m). But again we have

⊧_{L} φ ⟺ Alg_{m}^{+}(L) ⊧ c(φ) = φ

(cf. Thm.3.2.1).

Exercises 4.4:

(1) Replace the definition of the validity relation f ⊧_{∞} φ of logic L_{∞} (cf. Def.2.2.28)

by

f ⊧′_{∞} φ ⟺^{def} mn_{f}(φ) > 0.9

and show that the resulting logic is not nice but semi-nice.

(2) Push through the proof of Thm.3.2.19 for strongly semi-nice general logics.

(3) Check what is needed for the other direction, i.e. for Thm.3.2.20 to go through.

(4) Repeat the proof of Fact 3.1.8 in the new (semi-nice) setting.

(5) Look at the major theorems in section 3.2 one by one and check if their proofs can be pushed through in the new setting. Where it does not seem to go through, check whether some change in the formulation of the result permits you to push the proof through.

(6) Try to find out whether we could use a total operation instead of our partial one “c”. E.g. try to define c_{K}(φ) = φ if K ⊧ φ else (φΔ_{0}φ) (assume that only Δ_{0} is available as “special” connective). Now our algebra is not partial! Can this approach work? Show that the validity relation ⊧ can be recovered from the new total “c”, so the coding is faithful. But do the results go through? Check them! Show that Ex.3.1.9 fails. Show that Thm.3.2.3 does not want to go through even with modifications. ◀

∗ ∗ ∗

If we want to drop condition (3) of the definition of nice logic (Def.3.1.1) altogether, then a possibility is to restrict the validity relation ⊧ to sequents (φ ⇒ ψ) of formulas (instead of having it for all formulas). Here “⇒” is not a logical connective, but rather a metalevel symbol. If φ, ψ ∈ F then (φ ⇒ ψ) is a sequent (sequents are not formulas). Further,

𝔐 ⊧ (φ ⇒ ψ) iff mng_{𝔐}(φ) ⊆ mng_{𝔐}(ψ).

This approach is applicable to more logics, hence more kinds of algebras show up in Alg_{i}(L) (i ∈ {⊧, m}). However, similarly to the way we had to introduce “c” above to code validity in a model, now we have to introduce a pre-ordering “≤” on our algebras to code “⇒”. However, this is not needed if we restrict the validity relation ⊧ a little bit more, namely to pairs {(φ ⇒ ψ), (ψ ⇒ φ)} of sequents. Then we do not need new symbols like “≤” in our algebras. This approach is investigated e.g. in [ANSK] to quite some extent. See also investigations on k-deductive systems in Blok–Pigozzi [BP94]. For a general method using sequents see Guzman–Verdu [GV82], Font–Verdu [FV91].

We could also try to drop conditions (4), (5) of Def.3.1.1, i.e. permutability of atomic formulas. This would enable us to treat traditional first-order logic more comfortably (with less preparation to do). This can be done, the only thing needed is the universal algebraic concept of a free algebra over some defining relations. The details are available in [ANSK].

Appendix A: New kinds of logics

In this appendix we collect a few logics which are of a different “flavor” than the ones listed in section 2.2. The main purpose of these examples is showing that the present Algebraic Logic framework is suitable for handling all sorts of unusual logics coming from completely different paradigms of logical or linguistic or computer science research areas. DEFINITION A1 (infinite valued logic L_{∞}):

Let P be any set, the set of atomic formulas of L_{∞}. The logical connectives of L_{∞} are ∧, ¬, ∨ and →. The set F_{∞} of formulas is defined the usual way. Recall that P ⊆ F_{∞} is the set of atomic formulas.

M_{∞} =^{def} {f : (f : P → [0, 1])} ,

where [0, 1] denotes the usual interval of real numbers.

Let f ∈ M_{∞}. First we define mn_{f}(φ):

mn_{f}(p) =^{def} f(p) for p ∈ P
mn_{f}(φ ∧ ψ) =^{def} min {mn_{f}(φ), mn_{f}(ψ)}
mn_{f}(¬φ) =^{def} 1 − mn_{f}(φ)
mn_{f}(φ ∨ ψ) =^{def} max {mn_{f}(φ), mn_{f}(ψ)}
mn_{f}(φ → ψ) =^{def} \{ \begin{matrix}1,  if mn_{f}(φ) ≤ mn_{f}(ψ) \\ 1 − (mn_{f}(φ) − mn_{f}(ψ)), else. \end{matrix}

For any f ∈ M_{∞}, φ ∈ F_{∞},

mng_{∞}(φ, f) =^{def} {x ∈ [0, 1] : x ≤ mn_{f}(φ)};
f ⊧_{∞} φ ⟺^{def} mng_{f}(φ) = [0, 1].

With this the logic

L_{∞} =^{def} ⟨F_{∞}, M_{∞}, mng_{∞}, ⊧_{∞}⟩

is defined. ◀

Even in intuitionistic logic we have ⊧ ¬(φ ∧ ¬φ). However, in L_{∞} this is not so, the truth value of (φ∧¬φ) can be as high as 1/2. So in a sense, L_{∞} tolerates contradictions (and by a cheap joke, we could call it “dialectical” because of this, but we will not do so). Also (φ ↔ ¬φ) can be valid in some of our models. This again cannot happen even in intuitionistic logic. Further, mn_{f}(φ) ≥ 1/2 is expressible as (¬φ → φ), hence if we would want to have a new validity relation ⊧_{1}, where f ⊧_{1} φ iff mn_{f}(φ) ≥ 1/2, then we can express this new ⊧_{1} by f ⊧_{1} φ iff mng_{∞}(¬φ → φ) = mng_{∞}(φ → φ). We do not look into this new ⊧_{1} any more, we only use it as an example of definability of ⊧_{1} from mng without identifying truth with a greatest meaning or even with a single meaning.

L_{∞} is strongly nice since we can define ε_{0}(φ) =^{def} (φ → φ), δ_{0}(φ) =^{def} φ and (φΔ_{0}ψ) =^{def} (φ → ψ) ∧ (ψ → φ).

REMARK A2: If we omit ∧ from the connectives then we will need Δ_{0} =^{def} “ → ” and Δ_{1} =^{def} “ ← ”. If we replaced f ⊧_{∞} φ ⇔ mn_{f}(φ) = 1 by f ⊧_{∞} φ ⇔ mn_{f}(φ) > 0.9 then we would loose niceness. However, our logic would still remain semi-nice as described in section 4. ◀

Exercises A3:

(1) Try to define logics similar to L_{∞} but perhaps with more intuitive appeal to you.

(2) Prove that the intuitionistic tautology (φ ∧ (φ → ψ)) → ψ is not valid in L_{∞}. Change the semantics in order to make this valid.

(3) Show that L_{∞} is strongly nice.

(4) Obtain a new logic L_{ℚ} from L_{∞} by executing the following modifications in the definition. Replace [0,1] with the set ℚ of rational numbers everywhere. Define mn_{f}(¬φ) =^{def} −mn_{f}(φ). Redefine the meaning of “→” as follows:

mn_{f}(φ → ψ) =^{def} mn_{f}(ψ) − mn_{f}(φ) ,

and let mng_{ℚ}(φ, f) =^{def} {x ∈ ℚ : x ≤ mn_{f}(φ)}. Change the definition of f ⊧_{∞} φ to the following:

f ⊧_{ℚ} φ ⟺^{def} 0 ∈ mng_{∥}(φ, f) .

The rest remains unchanged. (4.1) Investigate the logic L_{ℚ}! Compare it with L_{∞}. (4.2) Prove that mng_{ℚ}(¬φ ∨ ψ, f) ≠ mng_{ℚ}(φ → ψ, f), for some model f. Prove that

⊧_{ℚ} (p_{1} ∨ ¬p_{1}). (4.3) Prove that ⊭_{ℚ} p_{0} → (p_{1} ∨¬p_{1}). (This property is aimed at by relevance logic, the

idea being, roughly, that the formulas p_{0} and (p_{1} ∨ ¬p_{1}) have no common atomic formulas, hence they are not relevant to each other, so they cannot “relevantly imply” each other.)

(4.4) Prove that ⊧_{ℚ} (φ → φ). (4.5) Prove that ⊧_{ℚ} φ iff (∀f ∈ M_{ℚ}) mng_{ℚ}(φ, f) = mng_{ℚ}((φ → φ) ∨ φ, f). ◀

DEFINITION A4 (Relevance Logic L_{r}): We obtain a new logic L_{r} from L_{∞} by executing the following modifications in the definition. Replace [0, 1] with the set ℚ of rational numbers everywhere. Define mn_{f}(¬φ) =^{def} −mn_{f}(φ). Redefine the meaning of “→” as follows:

mn_{f}(φ → ψ) =^{def} \{ \begin{matrix}max\{−mn_{f}(φ), mn_{f}(ψ)\}, if mn_{f}(φ) ≤ mn_{f}(ψ) \\ min\{mn_{f}(φ), −mn_{f}(ψ)\}, else. \end{matrix}

The rest is exactly as in Ex.A3 (4).

Now, Relevance Logic is

L_{r} = ⟨F_{r}, M_{r}, mng_{r}, ⊧_{r}⟩ . ◀

We note that logic L_{r} is also called R-Mingle (RM) in the literature.

Exercises A5:

(1) Compare L_{r}, L_{ℚ} and L_{∞}! Compare them with L_{S}. What are the most striking differences?

(2) Prove that ⊧_{r} (φ → φ), and ⊧_{r} (φ ∨ ¬φ).

(3) Prove that ⊭_{r} (p_{0} → (p_{1} ∨ ¬p_{1})). Compare with what we said about Relevance Logic in Ex.A3 (4)!

(4) Prove that (⊧_{r} φ) ⟺ [mng_{ℚ}(φ, f) = mng_{ℚ}(φ → φ, f), for all f ∈ M_{ℚ}].

(5) Check what happens if we replace ℚ with ℤ (the set of integers) or with the interval [−n, n] for some n ∈ ω.

(6) Prove that in L_{r} we have

[f ⊧ φ and f ⊧ ψ] ≠⇒ mng_{r}(φ, f) = mng_{r}(ψ, f).

Compare with Def.2.1.3!

(7) Prove that ⊧_{r} (φ → ψ) → (¬φ ∨ ψ) but ⊭_{r} (¬φ ∨ ψ) → (φ → ψ).

(8) Compare the {∧, ∨, ¬}-fragment of L_{r} with that of L_{S}! (Prove e.g. that for φ of this fragment, (⊧_{r} φ ⇒⊧_{S} φ))…. Go on comparing!)

Next we define Partial Logics (L_{P}). Partial logics are designed to express the fact that in certain situations, certain statements may be meaningless. For example, the statement “the integer 2 is of pink color” may be meaningless in certain situations. If φ is meaningless then so is ¬φ. Also, according to the Copenhagen interpretation of quantum mechanics, in certain situations certain statements are meaningless, e.g. asking for the exact location of a particle in a situation where the particle has only a probability distribution of locations is meaningless. DEFINITION A6 (Partial Logic, L_{P}): Connectives of L_{P} are: ∧, ∨, ¬, N, where the new kind of formula N(φ) intends to express that φ is either meaningless or false (“It is not the case that φ” or perhaps “It is not the fact that φ”). (N is a very strong negation.)

• The set of formulas F_{P} is obtained from F_{S} by adding the new unary connective N.

• The class M_{P} of models is

M_{P} =^{def} {f : f ∈ ^{P} {0, 1, 2}} .

Here 0, 1, 2 are intended to denote the truthvalues “false”, “true” and “undefined”, respectively.

• If 2 ∉ {mng_{P} (φ, f), mng_{P} (ψ, f)}, then mng_{P} of (φ ∧ ψ), (φ ∨ ψ), ¬φ is defined as in the case of L_{S}. Else (if 2 is one of the meanings) then mng_{P} of (φ ∧ ψ), (φ ∨ ψ), ¬φ is 2 (so all three are the same and they all are 2).

mng_{P} (Nφ, f) =^{def} \{ \begin{matrix}0, if mng_{P} (φ, f) = 1 \\ 1, otherwise. \end{matrix}

f ⊧_{P} iff mng_{P} (φ, f) = 1 .

With this, L_{P} = ⟨F_{P} , M_{P} , mng_{P} , ⊧_{P} ⟩ is defined. ◀ L_{P} above is a quite important logic. It was introduced by Prior and was further

investigated by I. Ruzsa (cf. e.g. [Ru91]).

Exercises A7:

(1) Prove that L_{P} is a nice logic. (Hint: Use ε_{0}(φ) =^{def} N(φ ∧ ¬φ), δ_{0}(φ) =^{def} φ. Then use φΔ_{0}ψ =^{def} N¬(φ ↔ ψ) ∧ (u(φ) ↔ u(ψ)), where u(φ) ⟺^{def} N(φ) ∧ N(¬φ). Here u(φ) means that φ is undefined [or meaningless]).

(2) Try to characterize Alg_{⊧}(L_{P}) and Alg_{m}(L_{P}). How many non-isomorphic algebras are there in Alg_{m}(L_{P}) ?

(3) Try to invent the partial version of our more sophisticated logics, e.g. of L_{S5} (or the others). (Warning: This might take too much time, because there are too many logics. So try one or two [if you are interested] and then try to develop an “intuition” that you probably could do the rest.) ◀

Appendix B: Further equivalence results

In this appendix we give the algebraic characterization of further logical properties, such as decidability of the validity problem, various Beth’s definability properties, Craig’s weak interpolation property.

First recall that a logic is called decidable iff the set of its validities is a decidable subset of the set of all formulas (cf. Def.2.1.7).

THEOREM B1. Assume that L is a nice logic. Then (i) L is decidable ⟺ the equational theory of Alg_{⊧}(L) is decidable. (ii) The validities of L are recursively enumerable ⟺ the equational theory of

Alg_{⊧}(L) is recursively enumerable.

Proof: It is a straightforward corollary of Cor.3.2.2 above.

Next we turn to the algebraic characterization of some definability properties. Beth definability properties of logics were defined e.g. in Sain [Sa88] and in Barwise–Feferman [BF85]. Here we give the definitions in the framework of the present paper. The proofs of Theorems B6 and B10 below can be found in Németi [N82]. DEFINITION B2 (implicit definition, explicit definition):

Let L = ⟨L^{P} : P is a set⟩ be a structural general logic. Let P ⫋ Q be sets with F^{P} ≠ ∅, and let R =^{def} Q\P. A set Σ ⊆ F^{Q} of formulas defines R implicitly in Q iff

(∀𝔐, 𝔑 ∈ Mod^{Q}(Σ))[mng_{𝔐}^{Q} ↾ F^{P} = mng_{𝔑}^{Q} ↾ F^{P} ⟹ mng_{𝔐}^{Q} = mng_{𝔑}^{Q}].

Σ defines R explicitly in Q iff

(∀r ∈ R)(∃φ_{r} ∈ F^{P})(∀𝔐 ∈ Mod^{Q}(Σ)) mng_{𝔐}^{Q}(r) = mng_{𝔐}^{Q}(φ_{r}). ◀

DEFINITION B3 ((strong) Beth definability property):

Let L be a structural general logic. L has the (strong) Beth definability property iff for all P, Q, R and Σ as in Def.B2 above

(Σ defines R implicitly in Q ⟹ Σ defines R explicitly in Q). ◀

DEFINITION B4 (patchwork property of models):

Let L be a structural general logic. L has the patchwork property of models iff

(∀sets P, Q)(∀𝔐 ∈ M^{P})(∀𝔑 ∈ M^{Q})

[F^{P ∩Q} ≠ ∅ and mng_{𝔐}^{P} ↾ F^{P ∩Q} = mng_{𝔑}^{Q} ↾ F^{P ∩Q} ⟹

⟹ (∃𝔓 ∈ M^{P ∪Q})(mng_{𝔓}^{P ∪Q} ↾ F^{P} = mng_{𝔐}^{P} and mng_{𝔓}^{P ∪Q} ↾ F^{Q} = mng_{𝔑}^{Q}). ◀ DEFINITION B5 (morphism, epimorphism):

Let K be a class of algebras. By a morphism of K we understand a triple ⟨𝔄, h, 𝔅⟩, where 𝔄, 𝔅 ∈ K and h : 𝔄 → 𝔅 is a homomorphism.

A morphism ⟨𝔄, h, 𝔅⟩ is an epimorphism of K iff for every ℭ ∈ K and every pair f : 𝔅 → ℭ, k : 𝔅 → ℭ of homomorphisms we have f ∘ h = k ∘ h ⟶ f = k). ◀

Typical examples of epimorphisms are the surjections. But for certain choices of K there are epimorphisms of K which are not surjective. Such is the case e.g. when K is the class of distributive lattices.

THEOREM B6 ([N82], [ANS84, sec.II.2]). Let L be a structural general logic which has the patchwork property of models. Then

L has the (strong) Beth definability property ⟺ all the epimorphisms of Alg_{⊧}(L) are surjective.

The proof is in [N82]. A less general version of thie theorem is proved in [HMT85, Thm.5.6.10].

DEFINITION B7 (strong implicit definition):

Let L be a structural general logic. Let P, Q, R and Σ be as in Def.B2 above. Σ defines R implicitly in Q in a strong sense iff

Σ defines R implicitly in Q and

(∀𝔐 ∈ Mod^{P} (Σ ∩ F^{P}))(∃𝔑 ∈ Mod^{Q}(Σ)) mng_{𝔑}^{Q} ↾ F^{P} = mng_{𝔐}^{P}. ◀ .

DEFINITION B8 (weak Beth definability property):

Let L be a structural general logic. L has the weak Beth definability property iff for all P, Q, R and Σ as in Def.B2 above

(Σ defines R implicitly in Q in a strong sense ⟹ Σ defines R explicitly in Q). ◀

DEFINITION B9 (K-extensible):

Let K_{0} ⊆ K be two classes of algebras. Let ⟨𝔄, h, 𝔅⟩ be a morphism of K. h is said to be K_{0}-extensible iff for every algebra ℭ ∈ K_{0} and every homomorphism f : 𝔄 → ℭ there exists some 𝔑 ∈ K_{0} and g : 𝔅 → 𝔑 such that ℭ ⊆ 𝔑 and g ∘ h = f. ◀

It is important to emphasize that ℭ is a concrete subalgebra of 𝔑 and not only is embeddable into 𝔑.

THEOREM B10. Let L be a structural general logic which has the patchwork property of models. Then

L has the weak Beth definability property ⟺ every Alg_{m}(L)-extensible epimorphism of Alg_{⊧}(L) is surjective.

In the formulation of Thm.B10 above, it was important that Alg_{m}(L) is not an elementary class in the sense that it is not closed under isomorphisms, since the definition of K-extensibility strongly differentiates isomorphic algebras.

Finally, we characterize a kind of Craig’s interpolation property. DEFINITION B11 (weak interpolation property):

Let L = ⟨F, M, mng, ⊧⟩ be a nice logic. For each formula φ ∈ F let atf(φ) denote the set of atomic formulas occurring in φ. Then L has the weak interpolation property iff

(∀φ, ψ ∈ F)[{φ} ⊧ ψ ⇒ (∃χ ∈ F)(atf(χ) = atf(φ) ∩ atf(ψ)
and{φ} ⊧ χ and {χ} ⊧ ψ)]. ◀

Recall that for any class K of algebras IK denotes the class of all isomorphic copies of members of K.

DEFINITION B12 (amalgamation property):

Let K be a class of algebras. We say that K has the amalgamation property iff for any 𝔄, 𝔅, ℭ ∈ IK with 𝔅 ⊇ 𝔄 ⊆ ℭ, there are 𝔑 ∈ K and injective homomorphisms (embeddings) f : 𝔅 ↣ 𝔑, h : ℭ ↣ 𝔑 such that f ↿ A = h ↿ A. ◀ THEOREM B13 (Czelakowski). Let L be a strongly nice and consequence compact logic. Assume that usual conjuction “∧” is in Cn(L). Assume that L has a deduction theorem. Then L has the weak interpolation property ⟺ Alg_{⊧}(L) has the amalgamation property.

Proof: It can be found in Czelakowski [Cz82], cf. Thm.3 therein.

Open problems:

(1) Are all the conditions of the above theorem needed? Try to characterize weak interpolation property with fewer assumptions on the logic.

(2) What is the logical counterpart of the algebraic property that “Alg_{⊧}(L) has the strong amalgamation property” (i.e. we also require f(B ∖ A) ∩ h(C ∖ A) = ∅ in Def.B12 above)?

REFERENCES 71

References

[ABNPS] Andréka,H., Blok,W.J., Németi,I., Pigozzi,D.L. and Sain,I., Abstract Algebraic Logic, In preparation.

[ABN81] Andréka,H., Burmeister,P. and Németi,I., Quasi-varieties of Partial Algebras – a Unifying Approach Towards a Two-Valued Model Theory for Partial Algebras, Studia Sci.Math.Hungar. 16 (1981), 325–372.

[AGN77] Andréka,H., Gergely,T. and Németi,I., On universal algebraic construction of logics, Studia Logica 36 (1977), 9–47.

[AM93] Andréka,H. and Mikulás,Sz., Lambek Calculus and its Relational Semantics: Completeness and Incompleteness, Journal of Logic, Language and Information (JoLLI) 3 (1994), 1–37.

[AMN91] Andréka,H., Monk,J.D. and Németi,I. (ed.s), “Algebraic Logic,” (Proc. Conf. Budapest 1988) Colloq. Math. Soc. J. Bolyai Vol 54,, North Holland, Amsterdam, 1991, pp. v+746 pp.

[AN76] Andréka,H. and Németi,I., Generalization of variety and quasi-variety concepts to partial algebras through category theory, Dissertationes Mathematicae (Rozprawy Math.) PWN Polish Scientific Publisher, Warsaw, Poland Vol CCIV (1982), 1–56.

[AN80] Andréka,H. and Németi,I., Does SP K ⊇ PS K imply the axiom of choice?, Comment. Math. Univ. Carolinae 21 (1980), 699–706.

[ANS84] Andréka,H., Németi,I. and Sain,I., Abstract model theoretic approach to Algebraic Logic, Preprint, Math. Inst. Budapest (1984), 70pp..

[ANSK] Andréka,H., Németi,I., Sain,I. and Kurucz,Á., General Algebraic Logic, “In: Proceedings of Logic Colloquium’92,” (L. Csirmaz, D.M.Gabbay eds.), to appear.

[AH91] Anellis,I.H. and Houser,N., The nineteenth century roots of universal algebra and algebraic logic: A critical-bibliographical guide for the contemporary logician, in [AMN91], 1–36.

[BF85] Barwise, J. and Feferman, S. (ed.s), “Model-Theoretic Logics,” Springer Verlag, Berlin, 1985.

[Be91] van Benthem,J., “Language in Action (Categories, Lambdas and Dynamic Logic),” North Holland, Amsterdam, 1991.

[Be92] van Benthem,J., A Note on Dynamic Arrow Logic, “In: Logic and Information Flow,” (J. van Eick, A.Visser eds.), The MIT Press, Cambridge, Massachusetts — London, England, 1994.

[BP89] Blok,W.J. and Pigozzi,D.L., Algebraizable logics, Memoirs Amer. Math. Soc. 77,396 (1989), vi+78 p.

[BP91] Blok,W.J. and Pigozzi,D.L., Local Deduction Theorems in Algebraic Logic, in [AMN91], 75–109.

[BP94] Blok,W.J. and Pigozzi,D.L., Abstract Algebraic Logic, (this volume).

[Bu86] Burmeister,P., “A model theoretic oriented approach to partial algebras,” Akademie Verlag, Berlin, 1986.

[BS81] Burris,S. and Sankappanavar,H.P., “A course in universal algebra,” (Graduate Texts in Mathematics), Springer-Verlag, New York, 1981.

[CGHO] del Cerro,L.F., Gabbay,D.M., Herzig,A. and Ohlbach,H.J., Overview on the Current State of Translation Methods for Non-classical Logics, Preprint, Imperial College (1993), 4pp.

[Cz82] Czelakowski,J., Logical matrices and the amalgamation property, Studia Logica XLI No 4 (1982), 329–342.

[Cz93] Czelakowski,J., Logic, algebras and consequence operators, Preprint, (1993), 79 pp.

[FJ93] Font,J.M. and Jansana,R., A general algebraic semantics for deductive systems, Preprint, Univ. of Barcelona (1993).

[FJ94] Font,J.M. and Jansana,R., Connections between two approaches, (this volume).

[FV91] Font,J.M. and Verdu,V., On some non-algebraizable logic, in [AMN91], 183–189.

[GV82] Guzman,F. and Verdu,V., On two Gentzen logifications of the variety of semilattices, Preprint, Univ. of Barcelona (1982).

[HMT85] Henkin,L., Monk,J.D. and Tarski,A., “Cylindric Algebras,” Part I and Part II, North Holland, Amsterdam, 1971 and 1985.

[Ma91] Maddux,R., The Origin of Relation Algebras in the Development and Axiomatization of the Calculus of Relations, Studia Logica Vol L, No 3/4 (1991), 421–456 pp.

[Ma92] Marx,M., Dynamic Arrow Logic with Pairs, In: Proceedings of Logic at Work Conference, Amsterdam, 1992 Dec, CCSOM of Univ. of Amsterdam (Eds.: M.Masuch and L.Pólos), to appear.

72 REFERENCES

[M69] Monk,J.D., Nonfinitizability of classes of representable algebras, J. of Symbolic Logic 34 (1969), 331–343.

[M76] Monk,J.D., “Mathematical Logic,” Springer-Verlag, 1976.

[N82] Németi,I., Surjectiveness of epimorphisms is equivalent to Beth definability property in general algebraic logic, Mathematical Institute Budapest, Preprint (1982), 26pp.

[N91] Németi,I., Algebraization of quantifier logics, an introductory overview, Studia Logica Vol 50, No 3/4 (a special issue devoted to Algebraic Logic, eds.: W. J. Blok and D. L. Pigozzi) (1991), 485-570. (Strongly updated and expanded [e.g. with proofs] version is available from author.)

[NS77] Németi,I. and Sain,I., Cone-implicational subcategories and some Birkhoff-type theorems, “In: Universal Algebras,” (Proc. Conf. Esztergom Hungary 1977), Colloq. Math. Soc. J. Bolyai — North Holland, 1981, pp. 535–578.

[Pi91] Pigozzi,D.L., Fregean Algebraic Logic, in [AMN91], 475–502.

[P89] “Possible worlds in Humanities, Arts and Sciences,” W.de Gruyer, Berlin–New York, 1989,, pp. 450 pp.

[Ro91] Roorda,D., Resource Logics. Proof-Theoretical Investigations, Ph.D. Dissertation, Institute for Logic, Language and Computation, Univ. of Amsterdam (1991).

[Ru91] Ruzsa,I., Intensional logic revisited, Published by the author (1991).

[S73] Sain,I., Category theoretical investigations in order to generalize identities and quasi-identities, Master’s Thesis (in Hungarian) (1973).

[S80/a] Sain,I., Dogmas on Language, Manuscript (in Hungarian) (1980). [S80/b] Sain,I., Cognition, Learning, (Rats and) Logic, Manuscript (in Hungarian) (1980).

[Sa83] Sain,I., Successor axioms for time increase the program verifying power of full computational induction, Math. Inst. Budapest, Preprint. No.23/1983.

[Sa86] Sain,I., Is “Some-Other-Time” sometimes better than “Sometime” in proving partial correctness of programs?, Studia Logica Vol XLVII, No 3 (1988), 279–301.

[Sa88] Sain,I., Beth’s and Craig’s properties via epimorphisms and amalgamation in algebraic logic, “In: Algebraic logic and universal algebra in computer science,” (Proc. Conf. Ames USA, 1988, Bergman,C.H., Maddux,R.D. and Pigozzi,D.L. eds.), Springer Lecture Notes in Computer Science Vol 425, 1990, pp. 209–226.

[Sa94] Sain,I., Universal algebraic basics for algebraic logic, (this volume).

[Se70] Segerberg,K., “Somewhere else” and “Some other time”, in: Wright and Wrong — Mini essays in honor of Georg Henrik von Wright, Published with support from Stiftersens vid Abo Akademi Forskningsinstitut, 61–64.

[Si91] Simon,A., Finite Schema Completeness for Typeless Logic and Representable Cylindric Algebras, in [AMN91], 665–670.

[Si92/a] Simon,A., What the Finitization Problem is Not, In: ‘Algebraic methods in logic and in computer science’, Banach Center publications, vol 28, Inst. of Math. Polish Acad. of Sci., Warsawa (1993).

[Si92/b] Simon,A., Arrow Logic Does Not Have Deduction Theorem, In: Proceedings of Logic at Work Conference, Amsterdam, 1992 Dec, CCSOM of Univ. of Amsterdam (Eds.: M.Masuch and L.Pólos), to appear.

[TG87] Tarski,A. and Givant,S., “A formalization of set theory without variables,” AMS Colloquium publications Vol 41, Providence, Rhode Island, 1987.

[V92] Venema,Y., Many-Dimensional Modal Logic, Ph.D. Dissertation, Institute for Logic, Language and Computation, Univ. of Amsterdam (1992).