A Fixpoint Approach to Second-Order

Quantifier Elimination with Applications to Correspondence Theory

Andreas Nonnengart and Andrzej Szałas

MPI–I–95–2-007 March 1995 Author’s Address

Andreas Nonnengart Max-Planck-Institut für Informatik Im Stadtwald 66123 Saarbrücken, Germany nonnenga@mpi-sb.mpg.de

Andrzej Szałas Institute of Informatics University of Warsaw ul. Banacha 2, 02-097 Warsaw, Poland szalas@mimuw.edu.pl

Acknowledgements

Supported in part by the KBN grant 3 P406 019 06 and the German Ministry for Research and Technology (Bundesministerium für Forschung und Technologie) under grant ITS 9102.

Abstract

This paper is about automated techniques for (modal logic) correspondence theory. The theory we deal with concerns the problem of finding fixpoint characterizations of modal axiom schemata. Given a modal schema and a semantics based method of translating modal formulae into classical ones, we try to derive automatically a fixpoint formula characterizing precisely the class of frames validating this schema. The technique we consider can, in many cases, be easily applied without any computer support.

Although we mainly concentrate on Kripke semantics, our fixpoint approach is much more general, as it is based on the elimination of second-order quantifiers from formulae. Thus it can be applied in second-order theorem proving as well. We show some application examples for the method which may serve as new, automated proofs of the respective correspondences.

Keywords

Correspondence Theory, Fixpoint Calculus, Modal Logics, Quantifier Elimination, Second-order Logic, Semantics based Translation

1 Introduction

The development of possible world semantics in the late fifties and the early sixties opened the area of the so-called Correspondence Theory, i.e. the discovery of strict connections between Hilbert style axioms and properties of the accessibility relation between worlds. For instance it was shown that the modal logic T-axiom □Φ ⊃ Φ is valid in a modal frame with accessibility relation ℜ if and only if ℜ is reflexive. Many such correspondences have been discovered since then and it became of major interest in this area to develop methods which allow to find such correspondences and which provide a formal basis for doing so. (As a main sourcebook to this see [20]). Until recently, all of these methods were based on more or less abstract model theoretic considerations and it can hardly be imagined that these can be automated. In the last couple of years, however, major steps have been taken towards an automated approach of finding modal logic correspondences. For example we can find algorithms for an automatic synthesis of correspondence axioms expressed in classical logic in [5, 14, 17, 18] where the algorithm of [17, 18] is further developed in [4]. All these approaches are incomplete. On the other hand, we know that the problem we deal with is totally undecidable (not even arithmetical - cf. [20]). Some of these algorithms (the ones presented in [4, 14, 17, 18]) always stop, while that of [5], called SCAN, sometimes loops. However, when SCAN loops, it is often possible to observe certain patterns which, put together, provide us with a correspondence axiom described in infinitary logic. This method is similar to Ackermann’s general method of second-order quantifier elimination given in [1], which works fine in general but, unfortunately, is difficult to use and hard to apply for it deals with infinitary logic.

With the approach proposed in this paper we try to avoid these problems if possible, i.e. we want to get answers to correspondence problems for which SCAN loops and the general Ackermann technique results in an infinite formula. Evidently, infinite formulae are problematic for any automated approach and therefore these have to be finitely encoded somehow. We do so by allowing fixpoint operators within formulae. We thus deal with a formalism which still has a nice proof theory (cf. [8, 15, 16]) and polynomial time model checking over finite domains (cf. [7]).

The paper is organized as follows: Section 2 contains the basic principles behind modal logics, their semantics based (relational) translation into first-order predicate logic, and earlier secondorder quantifier elimination techniques. Moreover, we briefly describe the major features of the fixpoint calculus and that just as far as they are necessary in order to be able to understand our main theorem given in Section 3. In Section 4 we apply this technique to a number of examples, including interesting modal logic axiom schemata which could not be solved with the automated approaches known so far. A final summary then concludes the paper.

2 Preliminaries

2.1 Notation

In what follows Φ and Ψ are meta-variables representing formulae, ∧, ∨, ⊃ and ≡ stand for conjunction, disjunction, implication and equivalence respectively. The negation is denoted by \overline{Φ}; x̄ and ȳ stand for tuples of variables. By ⊤ and ⊥ we shall denote the truth values true and false, respectively. Predicates and predicate variables are denoted by P, Q, . . .. The modal operators are denoted by □_{i} and ◇_{i}, where i ∈ I for some index set I. By A ← B we denote the substitution of expression A by expression B.

2.2 The SCAN algorithm

The SCAN algorithm (short for “Synthesizing Correspondence Axioms for Normal modal logics”) is a method to eliminate second-order quantifiers in order to find first-order equivalents if these exist. The main idea behind this algorithm is as follows: suppose there is the (secondorder) formula Φ = ∃P Ψ where Ψ is a first-order subformula and we want to find a first-order equivalent to Φ. Then transform Ψ into clause normal form (i.e. negation normal form and standard skolemization) and perform all possible constraint resolution and constraint factorization steps that are possible between P -literals. By a constraint resolution step it is meant to perform a resolution step even if the corresponding arguments are not unifiable. This means that residual inequalities have to be added to the resolvents sometimes. So, for example, a constraint resolution step between the two unit clauses P (a) and \overline{P (b)} results in the (constraint) resolvent a ≠ b (and similarly for constraint factorization steps). Very often this process terminates since after all possible constraint inference steps are performed with some literal P (α) in a clause C this very clause can be eliminated by purity deletion. Thus, after termination, the algorithm ends up with a set of clauses not containing any P -literal. A further necessary step in this approach is to deskolemize the clause set, i.e. all function symbols which were actually introduced by the skolemization during the clause form transformation have to be “back-translated” into existential quantifiers and if this succeeds we end up with a first-order formula which is equivalent to the second-order formula given as input.

Example 2.1 Consider the following simple formula

∀P [(∀x P (x) ⊃ Q(x)) ⊃ ∀x \overline{P (x)}] (1)

which states that every subset of the set Q is empty. Evidently this is equivalent to Q being empty and SCAN indeed has no problems with it. (Note that this formula has a universal secondorder quantifier; it therefore has to be negated beforehand in order to be able to apply the SCAN algorithm. This evidently does not affect the whole procedure for the final result can be negated once again.) Hence we first negate the input formula, getting ∃P [(∀x P (x) ⊃ Q(x)) ∧ ∃x P (x)] and try to find a first-order equivalent for this one. Transformation into clause normal form results in

\begin{matrix}\overline{P (x)}, Q(x) \\ P (a) \end{matrix}

and the task is now to produce all possible constraint resolvents from this clause set. As a matter of fact, this is trivial because only one resolution step is at all possible. This step results in the resolvent Q(a) and since all possible steps between P -literals have been performed now the clauses containing P -literals can be eliminated leaving the unit clause Q(a) as the only remaining clause. Recall that the constant a had been introduced by skolemization. It therefore has to be back-translated into an existential quantifier and after doing so we end up with ∃x Q(x). We thus have that ∃P [(∀x P (x) ⊃ Q(x)) ∧ ∃x P (x)] is equivalent to ∃x Q(x) and therefore

∀P [(∀x P (x) ⊃ Q(x)) ⊃ ∀x \overline{P (x)}] ≡ ∀x \overline{Q(x)}

SCAN has no problems with this example. Nevertheless, already a tiny change lets SCAN run into an infinite loop as can be seen as follows: consider the formula

∀P [(∀x P (x) ⊃ ∃y P (y) ∧ Q(x)) ⊃ ∀x \overline{P (x)}] (2)

which tells us just the same as the formula (1); it only contains some superfluous ballast given by the ∃y P (y). Now, after transforming the negation of (2) into clause normal form we get:

\overline{P (x)}, P (f(x))
\overline{P (x)}, Q(x)
P (a)

SCAN now attempts to perform all possible constraint resolution steps between P -literals. However, the first and third of these three clauses allow to derive infinitly many unit P -clauses. SCAN tries to produce all of them and therefore never terminates.

However, if we take a look at the (infinitly many) resolvents produced by SCAN we can find a fairly nice pattern of resolvents, namely the unit clauses Q(f^{n}(a)) and P (f^{n}(a)) with n ≥ 0. Thus, if SCAN were able to find such clause schemata it would be sufficient to find a first-order equivalent to ∃a∃f Q(f^{n}(a)) and, not too surprising, this can be found in ∃a Q(a) just as expected.

Unfortunately, SCAN is not able to derive such clause schemata and therefore the final steps of the above example cannot be automated yet. We therefore concentrate on another approach on second-order variable elimination, namely the one presented in [18, 4].

2.3 The Ackermann Lemma

Note that the method we propose extends known approaches, in particular the one based on the lemma of Ackermann (cf. [17, 18]). This lemma is a part of the Ackermann’s general method given in [1]. It is interesting, as the result is always first-order. We therefore start with a formulation of this lemma.

We say that a formula Φ is positive w.r.t. a predicate P iff P appears under no negation sign in Φ (in the negation normal form). Dually, we say that Φ is negative w.r.t. P iff all occurrences of P have the form \overline{P} and \overline{P} appears under no negation sign in Φ. The following lemma was proved by Ackermann in [1].

Lemma 2.2 Let P be a predicate variable and Φ(x̄), Ψ(P) be formulae without second-order quantification. Let Ψ(P) be positive w.r.t. P and let Φ contain no occurrences of P at all. Then the following equivalences hold:

∃P ∀x̄[P (x̄) ∨ Φ(x̄, z̄)] ∧ Ψ(P ← \overline{P}) ≡ Ψ(P ← Φ(x̄, z̄)) (3)

∃P ∀x̄[\overline{P} (x̄) ∨ Φ(x̄, z̄)] ∧ Ψ(P) ≡ Ψ(P ← Φ(x̄, z̄)) (4)

where in the righthand formulae the arguments x̄ of Φ are to be substituted by the respective actual arguments of P (renaming the bound variables whenever necessary).

The syntactic form required in Lemma 2.2 is usually not given initially and we are therefore forced to apply some well-known equivalence preserving transformations of classical logic in order to obtain this form. The following one was found particularly useful in [1]:

P (x̄) ≡ ∀ȳ (P (ȳ) ∨ x̄ ≠ ȳ). (5)

This technique was substantially strengthened in [4] by applying the following equivalence:

P (\overline{x_{1}}) ∨ P (\overline{x_{2}}) ∨ ⋯ ∨ P (\overline{x_{n}}) ≡ ∃z̄ [(z̄ = \overline{x_{1}} ∨ z̄ = \overline{x_{2}} ∨ ⋯ ∨ z̄ = \overline{x_{n}}) ∧ P (z̄)] (6)

Other quite well-known transformation techniques turn out to be useful as well as there are e.g. the transformation into conjunctive normal form and the following second-order skolemization that preserves equivalence of formulae and allows to eliminate existential quantifiers (similar formulation can be found e.g. in [19]):

∀x̄∃yΦ(x̄, y, …) ≡ ∃f∀x̄Φ(x̄, y ← f(x̄), …). (7)

One of the main restrictions in Lemma 2.2 is that it does not allow clauses which contain both, positive and negative occurrences of the predicate symbol to be eliminated. In order to overcome this difficulty we prove Theorem 3.1, which shows how to deal with such a situation. We thus substantially extend the approach based on the Ackermann lemma. On the other hand, Lemma 2.2, if applicable, gives as a result a first-order formula, while our theorem gives as a result a fixpoint formula. It is therefore recommended to try the application of Lemma 2.2 first and if it fails try to apply Theorem 3.1.

2.4 Fixpoint calculus

Let L_{I} be the classical first-order logic. In order to define the fixpoint calculus L_{F} we extend L_{I} by allowing the least fixpoint operator μP.Φ(P), where Φ is positive w.r.t. P, and abbreviate a formula of the form \overline{μ\overline{P} .\overline{Φ}(\overline{P})} by νP.Φ(P). It is sometimes convenient to distinguish the individual variables that are bound by the fixpoint operators μ and ν from other variables. We write μ.P (x̄) and ν.P (x̄) to indicate that the tuple x̄ of variables is bound by a fixpoint operator. Example 2.3 explains the rôle of fixpoint operators and the variables bound by μ and ν.

Let us now recall some useful well-known facts. The formulation we give is adapted to the particular problems we deal with. In particular, the partial order we consider is the following:

• the carrier is the set of formulae of L_{F}/_{≡}, where we do not distinguish between logically equivalent formulae (formally the carrier is the quotient set L_{F}/_{≡}; in order to simplify the considerations the equivalence classes and formulae are identified)

• the formulae are ordered by implication, i.e. Φ is less or equal to Ψ iff Φ ⊃ Ψ is a tautology.

Note that fixpoint operators are also formulae. Thus the partial order we consider is complete. Every formula Φ(P) which is positive w.r.t. P is monotone and therefore we have by the Knaster & Tarski fixpoint theorem that the fixpoints we consider are well defined. Moreover, the fixpoints have the following nice characterization:

μP.Φ(P) ≡ ⋁_{β∈α} Φ^{β}(⊥) (8)

for an ordinal α (the least such ordinal is called the closure ordinal for Φ(P)).

Note that μP (x̄).Φ(P) is the least (w.r.t. the partial order defined above) formula Ψ(x̄) such that

Ψ(x̄) ≡ Φ(P ← Ψ(x̄)).

We illustrate the introduced notions by the following example:

Example 2.3 Consider μP (x).Φ(P), where Φ(P (x)) ≡ [x = y ∨ ∃z (R(x, z) ∧ P (z))]. Then the formula Φ(P (x)) is positive w.r.t. P. Moreover, it is possible to show that the respective closure ordinal is ω (see e.g. the proof of Theorem 3.1). Thus, according to (8),

μP (x). [x = y ∨ ∃z (R(x, z) ∧ P (z))] ≡ [Φ(P)]^{ω}(⊥) ≡ ⋁_{i∈ω}[Φ(P)]^{i}(⊥)

where

Φ^{0}(⊥) ≡ ⊥
Φ^{1}(⊥) ≡ [x = y ∨ ∃z (R(x, z) ∧ P (z))]^{1}(⊥)
≡ x = y ∨ ∃z (R(x, z) ∧ Φ^{0}(⊥))
≡ x = y
Φ^{2}(⊥) ≡ Φ(Φ^{1}(⊥))
≡ Φ(x = y)
≡ x = y ∨ ∃z (R(x, z) ∧ z = y)
≡ x = y ∨ R(x, y)
Φ^{3}(⊥) ≡ Φ(Φ^{2}(⊥))
≡ Φ(x = y ∨ R(x, y))
≡ x = y ∨ ∃z (R(x, z) ∧ (z = y ∨ R(z, y)))
≡ x = y ∨ R(x, y) ∨ ∃z (R(x, z) ∧ R(z, y))
…

Thus Φ^{i}(⊥) ≡ ⋁_{j<i} R^{j}(x, y) and therefore μP (x).Φ(P) describes the reflexive and ω-transitive closure of the relation R.

2.5 Modal Logics

Since we are mainly interested in the fixpoint characterization of modal logics, a short introduction to modal logics seems adequate. Evidently, this cannot be done here in every detail. The reader not experienced with modal logics is referred to [6] and [3].

It should be emphasized here that, for the sake of simplicity, we make the following restrictions:

• we consider one-argument modalities only

• we consider Kripke semantics only

• we do not consider first-order versions of modal logics

• we consider only normal modal logics.

However, the extension of our approach to cover the case of many-argument modalities as well as first-order quantifiers is straightforward. The method is even applicable to other kinds of semantics as well.

We consider (propositional multi-) modal logic with modalities {□_{i}}_{i∈I}, where I is an enumerable set. Let V be a set of propositional variables. The set of formulae F is then defined as the least set such that

• V ⊂ F

• Φ, Ψ ∈ F implies that \overline{Φ}, Φ ∨ Ψ, Φ ∧ Ψ ∈ F and for each i ∈ I, □_{i}Φ ∈ F.

The dual modalities ◇_{i} and the boolean connectives ⊃, ≡ are defined as usual.

The semantics for modal logics is given by the Kripke semantics. A Kripke frame (frame, in short) is a pair ⟨W, {ℜ_{i}}_{i∈I}⟩, where

• W is any non-empty set, called the set of worlds

• {ℜ_{i}}_{i∈I} is a set of binary relations defined on W, called the accessibility relations.

By a Kripke model we shall mean any triple ⟨K, w, v⟩, where

• K = ⟨W, {ℜ_{i}}_{i∈I}⟩ is a Kripke frame

• w ∈ W is a distinguished element of W, called the actual world

• v : V × W ⟶ {⊤, ⊥} is a mapping associating a truth value to a given propositional variable in a given world.

The satisfiability relation ⊧ is defined as follows:

• K, w, v ⊧ p iff v(p, w) = ⊤, where p ∈ V is a propositional variable

• K, w, v ⊧ \overline{Φ} iff not K, w, v ⊧ Φ

• K, w, v ⊧ Φ ∨ Ψ iff K, w, v ⊧ Φ or K, w, v ⊧ Ψ

• K, w, v ⊧ Φ ∧ Ψ iff K, w, v ⊧ Φ and K, w, v ⊧ Ψ

• K, w, v ⊧ □_{i}Φ iff for any w′ such that ℜ_{i}(w, w′), we have K, w′, v ⊧ Φ.

2.6 Semantics Based Translation

The semantics based translation we consider (sometimes called relational translation) goes back at least to Moore (see [9, 10, 11, 12]) and consists mainly of a direct translation of the Kripke semantics for modal logics into first-order predicate logic. I.e. the domain under consideration is the set of worlds, the actual world is represented by a special world constant (or variable) and the accessibility relations ℜ_{i} by the binary predicate symbols R_{i}. Finally, for each propositional variable p a unary predicate symbol P is introduced which accepts a world (the actual world) as its only argument and is supposed to be evaluated to true if and only if the associated propositional variable is evaluated to true in the world given by the interpretation of the argument. Translation from modal logic formulae into predicate logic is then defined as follows:

\begin{aligned}⌈p⌉_{x} & = & P (x) \\ ⌈□_{i}Φ⌉_{x} & = & ∀y R_{i}(x, y) ⊃ ⌈Φ⌉_{y} \\ ⌈◇_{i}Φ⌉_{x} & = & ∃y R_{i}(x, y) ∧ ⌈Φ⌉_{y} \end{aligned}

where the translation for the classical connectives is obtained by the usual homomorphic extension to the above. Note that we sometimes use the modal operator symbol as the index of the corresponding accessibility relation symbol (e.g. R_{□} for the accessibility relation of the □-operator).

This relational translation is sound and complete for the modal logic K. If we are interested in other modal logics, say S4, we have to add the correspondence axioms which characterize the modal logic under consideration (reflexivity and transitivity of R in case of S4). Thus the Correspondence Theory can be viewed as a discipline of finding such correspondence axioms.

We won’t go into any further detail what the basics of the relational translation is concerned. Instead we provide with a small table of examples and encourage the reader to have a look at [3, 6, 9, 10, 11, 12] where this and other translation techniques are described in more detail.

Modal formula Translated formula (with actual world x)

□p ⊃ p  [∀y R_{□}(x, y) ⊃ P (y)] ⊃ P (x)
□p ⊃ □□p  [∀y R_{□}(x, y) ⊃ P (y)] ⊃ [∀y (R_{□}(x, y) ⊃ ∀z(R_{□}(y, z) ⊃ P (z)))]
p ⊃ □◇p  P (x) ⊃ [∀y R_{□}(x, y) ⊃ ∃z (R_{□}(y, z) ∧ P (z))]
□(p ⊃ ◯p) ⊃ (p ⊃ □p) [∀y (R_{□}(x, y) ⊃ (P (y) ⊃ ∀z (R_{◯}(y, z) ⊃ P (z))))] ⊃
[P (x) ⊃ ∀u (R_{□}(x, u) ⊃ P (u))]

Note that the above translation can easily be extended to the case of modal schemata, using second-order quantification as follows (cf. also [20]).

Modal schema Translated schema

□p  ∀P ∀x∀y R_{□}(x, y) ⊃ P (y)
◇p  ∀P ∀x∃y R_{□}(x, y) ∧ P (y)

The following table illustrates the translation of modal schemata.

Modal schema Translated schema

□p ⊃ p  ∀P ∀x(∀y R_{□}(x, y) ⊃ P (y)) ⊃ P (x)
□p ⊃ □□p  ∀P ∀x(∀y R_{□}(x, y) ⊃ P (y)) ⊃ ∀y(R_{□}(x, y) ⊃ ∀z(R_{□}(y, z) ⊃ P (z)))
p ⊃ □◇p  ∀P ∀x P (x) ⊃ (∀y R_{□}(x, y) ⊃ ∃z(R_{□}(y, z) ∧ P (z)))
□(p ⊃ ◯p) ⊃ (p ⊃ □p) ∀P ∀x[∀y(R_{□}(x, y) ⊃ (P (y) ⊃ ∀z(R_{◯}(y, z) ⊃ P (z))))] ⊃
[P (x) ⊃ ∀u(R_{□}(x, u) ⊃ P (u))]

However, the above formulae are fairly useless from the point of view of automated theorem proving, as the set of second-order tautologies even with one second-order quantification is, in general, totally undecidable. In order to put our translation into good use, we should therefore try to eliminate the second-order quantifications and find some suitable, less complex conditions on R that could serve as a basis for modal logic theorem proving.

Note that the elimination technique we consider preserves logical equivalence of formulae. This means that the resulting formula is equivalent over all interpretations. Thus, whenever one considers semantics of modal logics which is based on some interpreted formalism (like neighbourhood semantics), one has to work in some theory that approximates the formalism. However, we shall not consider the question of interpreted formalisms in this paper.

3 The Main Theorem

As mentioned earlier our aim is to find first-order correspondences for modal schemata. To this end we consider the relational translation approach described in the previous section (which results in second-order formulae) and apply our main theorem in order to obtain an equivalent first-order formula. This section is now meant to formulate and prove the main theorem that serves as a basis of the proposed approach.

Theorem 3.1 Assume that all occurrences of the predicate symbol P in the formula Ψ bind only variables^{1}.

• if Φ and Ψ are negative w.r.t. P then the closure ordinal for Φ(\overline{P}) is less than or equal to ω, and

∃P ∀ȳ [P (ȳ) ∨ Φ(\overline{P})] ∧ [Ψ(\overline{P})] ≡ Ψ[\overline{P} ← ν\overline{P (ȳ)}.Φ(\overline{P})] (9)

• if Φ and Ψ are positive w.r.t. P then the closure ordinal for Φ(P) is less than or equal to ω, and

∃P ∀ȳ[\overline{P (ȳ)} ∨ Φ(P)] ∧ [Ψ(P)] ≡ Ψ[P ← νP (ȳ).Φ(P)] (10)

where the above substitutions exchange the variables bound by fixpoint operators by the corresponding actual variables of the substituted predicate^{2}.

Proof Let us prove the first part of the theorem, concerning equivalence (9) (the proof of (10) is then obvious).

We start by showing that the closure ordinal for Φ(\overline{P}) is less or equal to ω. It suffices to prove that

Φ(\overline{P} ← ⋁_{i∈ω} Φ^{i}(\overline{P} ← ⊥)) ≡ ⋁_{i∈ω} Φ(\overline{P} ← Φ^{i}(\overline{P} ← ⊥)). (11)

Without loss of generality we assume that Φ is in prenex and conjunctive normal form. By applying equivalences (5) and (6) one can transform this formula equivalently to the form

Q_{1} … Q_{k}∀z̄[(\overline{P (z̄)} ∨ Φ_{1}) ∧ … ∧ (\overline{P (z̄)} ∨ Φ_{r}) ∧ Φ′), (12)

where Q_{1}, …, Q_{k} are first-order quantifiers and Φ_{1}, …, Φ_{r}, Φ′ are clauses containing no occurrences of \overline{P}. Formula (12) is equivalent to Q_{1} … Q_{k}∀z̄[(\overline{P (z̄)} ∨ (Φ_{1} ∧ … ∧ Φ_{r})) ∧ Φ′]. Next one can eliminate first-order existential quantifiers by applying equivalence (7). The formula takes the form ∃f̄∀ū∀z̄[(\overline{P (z̄)} ∨ (Φ_{1} ∧ … ∧ Φ_{r})) ∧ Φ′], where f̄ is a tuple of Skolem functions. One can now exchange the order of universal quantifiers and move ∀ū inside. The resulting formula, equivalent to Φ, is of the form

1Evidently, by applying the equivalence (5), every formula Ψ can easily be transformed to the required form.

2Observe that the assumption that P ’s in Ψ bind only variables is necessary here.

∃f̄∀z̄[(\overline{P (z̄)} ∨ (∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀ūΦ′]. (13)

The following equivalences show that (11) holds:

Φ(\overline{P} ← ⋁_{i∈ω} Φ^{i}(\overline{P} ← ⊥)) ≡ (by (13))
∃f̄∀z̄[(⋁_{i∈ω} Φ^{i}(\overline{P} ← ⊥) ∨ (∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀ūΦ′] ≡
∃f̄[∀z̄(⋁_{i∈ω} Φ^{i}(\overline{P} ← ⊥) ∨ (∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀z̄∀ūΦ′] ≡
(since ⋁_{i∈ω} Φ^{i}(\overline{P} ← ⊥) does not contain free occurrences of z̄)
∃f̄[(⋁_{i∈ω} Φ^{i}(\overline{P} ← ⊥) ∨ ∀z̄(∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀z̄∀ūΦ′] ≡
∃f̄[⋁_{i∈ω}(Φ^{i}(\overline{P} ← ⊥) ∨ ∀z̄(∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀z̄∀ūΦ′] ≡
∃f̄⋁_{i∈ω}[(Φ^{i}(\overline{P} ← ⊥) ∨ ∀z̄(∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀z̄∀ūΦ′] ≡
⋁_{i∈ω} ∃f̄[(Φ^{i}(\overline{P} ← ⊥) ∨ ∀z̄(∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀z̄∀ūΦ′] ≡
⋁_{i∈ω} ∃f̄∀z̄[(Φ^{i}(\overline{P} ← ⊥) ∨ (∀ūΦ_{1} ∧ … ∧ ∀ūΦ_{r})) ∧ ∀ūΦ′] ≡
⋁_{i∈ω} Φ(\overline{P} ← Φ^{i}(\overline{P} ← ⊥)).

Let us now show that equivalence (9) holds. (⊃) Assume that ∃P ∀ȳ[P (ȳ) ∨ Φ(\overline{P})] ∧ [Ψ(\overline{P})]. Let P be such that the formula

∀ȳ[P (ȳ) ∨ Φ(\overline{P})] ∧ [Ψ(\overline{P})] (14)

is satisfied. Observe that the first conjunct of formula (14) can be rewritten as ∀ȳ[\overline{P (ȳ)} ⊃ Φ(\overline{P})]. By assumption, Φ is negative w.r.t. P, thus positive (and monotone) w.r.t. \overline{P}. Obviously, \overline{P (ȳ)} ⊃ ⊤. By monotonicity of Φ, Φ(\overline{P (ȳ)}) ⊃ Φ(⊤), thus by the first conjunct of formula (14), \overline{P (ȳ)} ⊃ Φ(⊤). By induction one can show that for any i ∈ ω, we have that \overline{P (ȳ)} ⊃ Φ^{i}(⊤). Thus also \overline{P (ȳ)} ⊃ ν\overline{P (ȳ)}.Φ(P̄).

By assumption, P occurs only negatively in Ψ. Thus Ψ is positive (and monotone) w.r.t. \overline{P}. By the second conjunct of our formula (14), Ψ(\overline{P (ȳ)}). This, together with the monotonicity of Ψ implies

Ψ[\overline{P} ← ν\overline{P (ȳ)}.Φ(\overline{P})].

(⊂) Assume that Ψ[\overline{P} ← ν\overline{P (ȳ)}.Φ(\overline{P})]. In order to show that ∃P ∀ȳ[P (ȳ) ∨ Φ(\overline{P})] ∧ [Ψ(\overline{P})] we define \overline{P (ȳ)} to be ν\overline{P (ȳ)}.Φ(\overline{P}), i.e.

P (ȳ) ≡ μP (ȳ).\overline{Φ}(P). (15)

By (15) we have that P (ȳ) is a fixpoint of \overline{Φ}(P), i.e. P (ȳ) ≡ \overline{Φ}(P). Thus

∃P ∀ȳ [P (ȳ) ∨ Φ(\overline{P})] ∧ [Ψ(\overline{P})]

is equivalent to

∃P ∀ȳ [\overline{Φ}(P) ∨ Φ(\overline{P})] ∧ [Ψ(\overline{P})],

i.e. to ∃P [Ψ(\overline{P})], which holds by our assumption.

In order to transform formulae into the form required in Theorem 3.1 we apply well-known tautologies of the classical logic, in particular (5), (6) and (7) of Section 2.3.

4 Applications

Now let us come to some application examples of our approach. The strategy is always essentially the same for all of the examples. I.e. first the problem has to be transformed into the form ∃P Φ where P is a predicate symbol (the one we try to eliminate) and Φ is a first-order formula. Modal schemata are not initially of this form. We therefore have to translate the schema with the help of the relational translation approach and to negate its result (the translation results in a universal second-order quantification). After that the formula has to be transformed into the form required for the main theorem to be applicable. This application then results in a fixpoint formula which has to be negated again. Finally some simplification transformations are performed if possible and we are done.

Example 4.1 Let us first have another look at Example 2.1 where SCAN ran into a loop, i.e. consider again the formula (2)

∀P [(∀x P (x) ⊃ ∃y P (y) ∧ Q(x)) ⊃ ∀x \overline{P (x)}].

Negated and transformed into the form required in Theorem 3.1 —

∃x∃P ∀y (\overline{P (y)} ∨ ∃z P (z) ∧ Q(y)) ∧ P (x) After application of Theorem 3.1 —

∃x νP (x).[∃z P (z) ∧ Q(x)], i.e. ∃x νP (x).[∃z P (z)] ∧ Q(x) Simplified^{3} — ∃x Q(x) Unnegated — ∀x \overline{Q(x)}.

The following example illustrates the use of Theorem 3.1 in case of the second-order induction axiom.

Example 4.2 Consider the second-order induction, where S(x, y) means that y is a successor of x:

∀P [P (0) ∧ ∀xy ((P (x) ∧ S(x, y)) ⊃ P (y))] ⊃ ∀z P (z) (16)

Let us now transform the formula into the form required in Theorem 3.1 and then apply the theorem:

Negated —

∃P [P (0) ∧ ∀xy((P (x) ∧ S(x, y)) ⊃ P (y))] ∧ ∃z\overline{P (z)} Transformed into the conjunctive normal form —

∃z∃P ∀y[(y ≠ 0 ∨ P (y)) ∧ ∀x(\overline{P (x)} ∨ \overline{S(x, y)} ∨ P (y))] ∧ \overline{P (z)} Transformed into the form required in Theorem 3.1 —

∃z∃P ∀y[P (y) ∨ (y ≠ 0 ∧ ∀x(\overline{S(x, y)} ∨ \overline{P (x)}))] ∧ \overline{P (z)} After application of Theorem 3.1 —

∃z ν\overline{P (z)}.(z ≠ 0 ∧ ∀x[\overline{S(x, z)} ∨ \overline{P (x)})] Unnegated —

∀z μP (z).[z = 0 ∨ ∃x(S(x, z) ∧ P (x))].

3Using the equivalence νP (x).[∃z P (z)] ≡ ⊤

By Theorem 3.1 we have that the above formula is equivalent to the following infinite disjunction:

∀z ⋁_{i∈ω}[z = 0 ∨ ∃x(S(x, z) ∧ P (x))]^{i}(⊥).

Denote by Φ(Ψ(z)) the formula z = 0 ∨ ∃x(S(x, z) ∧ Ψ(x)). Now

Φ^{0}(⊥) ≡ ⊥ Φ^{1}(⊥) ≡ [z = 0 ∨ ∃x(S(x, z) ∧ ⊥)] ≡ [z = 0 ∨ ⊥] ≡ [z = 0] Φ^{2}(⊥) ≡ Φ(Φ^{1}(⊥)) ≡ [z = 0 ∨ ∃x(S(x, z) ∧ x = 0)] ≡ [z = 0 ∨ S(0, z)] Φ^{3}(⊥) ≡ Φ(Φ^{2}(⊥)) ≡ [z = 0 ∨ ∃x(S(x, z) ∧ (x = 0 ∨ S(0, x)))] ≡

[z = 0 ∨ S(0, z) ∨ S^{2}(0, z)] ... Φ^{i}(⊥) ≡ [z = 0 ∨ S(0, z) ∨ ... ∨ S^{i−1}(0, z)].

Thus, by a simple calculation we obtain the well-known, but not trivial fact that the second-order induction (16) is equivalent to

∀z ⋁_{i∈ω}[S^{i}(0, z)],

i.e. “every natural number is obtained from 0 by a finite number of applications of the successor relation”. In fact, the other Peano axioms say that the successor relation is a function, etc.

Example 4.3 Assume that R is transitive and consider the formula

∀P [(∀x \overline{P (x)}) ∨ (∀y P (y)) ∨ ∃xy (P (x) ∧ R(x, y) ∧ \overline{P (y)})]. (17)

Note that formula (17) has a first-order equivalent over transitive frames. However SCAN loops and the method based on the Ackermann lemma fails with (17) given as an input. Hence let us apply Theorem 3.1.

Negated — ∃P [(∃x P (x)) ∧ (∃y \overline{P (y)}) ∧ ∀xy (\overline{P (x)} ∨ \overline{R(x, y)} ∨ P (y))] Transformed into an equivalent form —

∃xy∃P [∀w (P (w) ∨ ∀u(\overline{P (u)} ∨ \overline{R(u, w)})) ∧ ∀w (P (w) ∨ x ≠ w) ∧ \overline{P (y)}] Transformed into the form required in Theorem 3.1 —

∃xy∃P [∀w (P (w) ∨ (x ≠ w ∧ ∀u (\overline{R(u, w)} ∨ \overline{P (u)})))] ∧ \overline{P (y)} After application of Theorem 3.1 —

∃xy ν\overline{P (y)}.[x ≠ y ∧ ∀u (\overline{R(u, y)} ∨ \overline{P (u)})] Unnegated — ∀xy μP (y).[x = y ∨ ∃u (R(u, y) ∧ P (u))].

Denote by Φ(P (y)) the formula x = y ∨ ∃u (R(u, y) ∧ P (u)). Then

Φ^{0}(⊥) ≡ ⊥ Φ^{1}(⊥) ≡ x = y ∨ ∃u(R(u, y) ∧ ⊥) ≡ x = y Φ^{2}(⊥) ≡ Φ(Φ^{1}(⊥)) ≡ x = y ∨ ∃u(R(u, y) ∧ x = u) ≡ x = y ∨ R(x, y) Φ^{3}(⊥) ≡ Φ(Φ^{2}(⊥)) ≡ x = y ∨ ∃u(R(u, y) ∧ (x = u ∨ R(x, u))) ≡

x = y ∨ R(x, y) ∨ ∃u(R(u, y) ∧ R(x, u))

Evidently, ∃u (R(u, y) ∧ R(x, u)) together with the transitivity of R implies R(x, y). It therefore follows that

Φ^{3}(⊥) ≡ x = y ∨ R(x, y) ≡ Φ^{2}(⊥)

Thus Φ^{i}(⊥) ≡ x = y ∨ R(x, y) forall i ≥ 2 and therefore we have (under the assumption that R is transitive) that formula (17) is equivalent to ∀x, y (x = y ∨ R(x, y)) i.e. it represents the reflexive closure of R.

So far we considered merely some general second-order quantification elimination problems. Let us now show some correspondence-theoretical applications of Theorem 3.1.

Example 4.4 Consider the Löb Axiom

□(□P ⊃ P) ⊃ □P (18)

Translated —

∀P ∀x [∀y (R(x, y) ⊃ ∀z (R(y, z) ⊃ P (z)) ⊃ P (y))] ⊃ ∀u (R(x, u) ⊃ P (u)) After negation and elimination of ⊃ —

∃P ∃x [∀y (\overline{R(x, y)} ∨ ∃z (R(y, z) ∧ \overline{P (z)} ∨ P (y)))] ∧ ∃u (R(x, u) ∧ \overline{P (u)}) Transformed into the form required in Theorem 3.1 —

∃x∃P [∀y (P (y) ∨ \overline{R(x, y)} ∨ ∃z (R(y, z) ∧ \overline{P (z)}))] ∧ ∃u (R(x, u) ∧ \overline{P (u)}) After application of Theorem 3.1 —

∃xu R(x, u) ∧ ν\overline{P (u)}.[\overline{R(x, u)} ∨ ∃z (R(u, z) ∧ \overline{P (z)})] Unnegated —

∀xu R(x, u) ⊃ μP (u).[R(x, u) ∧ ∀z (R(u, z) ⊃ P (z))]

Denote by Φ(Ψ(u)) the formula R(x, u) ∧ ∀z (R(u, z) ⊃ Ψ(z)). Now

Φ^{0}(⊥) ≡ ⊥

Φ^{1}(⊥) ≡ R(x, u) ∧ ∀z \overline{R(u, z)}

Φ^{2}(⊥) ≡ Φ(Φ(⊥)) ≡ Φ(R(x, u) ∧ ∀z \overline{R(u, z)}) ≡ R(x, u) ∧ ∀z (R(u, z) ⊃ (R(x, z) ∧ ∀z_{1} \overline{R(z, z_{1})})))

Φ^{3}(⊥) ≡ Φ(Φ^{2}(⊥)) ≡ Φ(R(x, u) ∧ ∀z (R(u, z) ⊃ (R(x, z) ∧ ∀z_{1} \overline{R(z, z_{1}))} ≡ R(x, u) ∧ ∀z (R(u, z) ⊃ R(x, z) ∧ ∀z_{2} (R(z, z_{2}) ⊃ (R(x, z_{2}) ∧ ∀z_{1} \overline{R(z_{2}, z_{1})})))

...

Thus the Löb axiom (18) is equivalent to

∀xu R(x, u) ⊃ ⋁_{i∈ω} Φ^{i}(⊥),

which expresses that the relation R is transitive and reverse well-founded. Transitivity of R can be seen by “unrolling” the fixpoint two times and the reverse well-foundedness of R then follows from the simplification of ∀xu R(x, u) ⊃ μP (u).[R(x, u) ∧ ∀z (R(u, z) ⊃ P (z))] to ∀xu R(x, u) ⊃ μP (u).[∀z R(u, z) ⊃ P (z)] under the transitivity assumption.

Next we consider a modal schema which is not validated by any frame. It is interesting in so far as SCAN is again not able prove this fact. Similarly, the application of Lemma 2.2 is not possible here.

Example 4.5 Consider the axiom schema

□(□P ⊃ P) ⊃ P (19)

Translated —

∀P ∀x [∀y(R(x, y) ⊃ (∀z (R(y, z) ⊃ P (z)) ⊃ P (y))) ⊃ P (x)] Negated and transformed into the form required in Theorem 3.1 —

∃x∃P ∀y [P (y) ∨ \overline{R(x, y)} ∨ ∃z (R(y, z) ∧ \overline{P (z)})] ∧ \overline{P (x)} After application of Theorem 3.1 —

∃x ν\overline{P (x)}.[\overline{R(x, x)} ∨ ∃z (R(x, z) ∧ \overline{P (z)})] Unnegated —

∀x μP (x).[R(x, x) ∧ ∀z (\overline{R(x, z)} ∨ P (z))].

Denote by Φ(P (x)) the formula R(x, x) ∧ ∀z (\overline{R(x, z)} ∨ P (z)). Now

Φ^{0}(⊥) ≡ ⊥ Φ^{1}(⊥) ≡ R(x, x) ∧ ∀z \overline{R(x, z)} ≡ ⊥

Thus Φ^{i}(⊥) ≡ ⊥ for all i, hence the schema (19) is equivalent to ⊥, i.e. no frame validates this schema.

Example 4.6 Consider the following axiom schema:

□(P ⊃ ◇P) ⊃ (◇P ⊃ □◇P) (20)

which is sometimes called the modified Löb Axiom (see [20])^{4}.

Translated — ∀P ∀x [∀y (R(x, y) ⊃ (P (y) ⊃ ∃z (R(y, z) ∧ P (z)))] ⊃ [∃u (R(x, u) ∧ P (u)) ⊃ ∀v (R(x, v) ⊃ ∃w (R(v, w) ∧ P (w)))]

Negated — ∃x ∃P [∀y (R(x, y) ⊃ (P (y) ⊃ ∃z (R(y, z) ∧ P (z)))] ∧ ∃u (R(x, u) ∧ P (u)) ∧ ∃v (R(x, v) ∧ ∀w (\overline{R(v, w)} ∨ \overline{P (w)}))

Transformed into an equivalent form — ∃xuv ∃P [∀y (\overline{R(x, y)} ∨ \overline{P (y)} ∨ ∃z (R(y, z) ∧ P (z))) ∧ (R(x, u) ∧ P (u)) ∧ (R(x, v) ∧ ∀w (\overline{R(v, w)} ∨ \overline{P (w)}))]

Transformed into the form required in Theorem 3.1 — ∃xuv ∃P ∀y [\overline{P (y)} ∨ (\overline{R(v, y)} ∧ (\overline{R(x, y)} ∨ ∃z (R(y, z) ∧ P (z))))] ∧ [R(x, u) ∧ P (u) ∧ R(x, v)]

After application of Theorem 3.1 —

∃xuv R(x, u) ∧ R(x, v) ∧ νP (u).[\overline{R(v, u)} ∧ (\overline{R(x, u)} ∨ ∃z (R(u, z) ∧ P (z)))] Unnegated —

∀xuv R(x, u) ∧ R(x, v) ⊃ μ\overline{P (u)}.[R(v, u) ∨ (R(x, u) ∧ ∀z (R(u, z) ⊃ \overline{P (z)}))] It is still not easy to provide with a nice intuition about this property. Its strong relation to the Löb axiom is pretty evident, however. As Arthur Prior mentions in [13], it allows to prove Dummet’s axiom of discreteness under the Diodorian Modality. Also it serves as a schema for the tense logic definability of the natural numbers under the <-relation (see [20]).

4In a temporal interpretation this schema is often examined in its equivalent form (◇P ∧ ◇□\overline{P}) ⊃ ◇(P ∧ □\overline{P}), i.e. if P has not yet stopped being true but will do so eventually then there will be a final moment of P ’s truth.

Example 4.7 Consider the temporal logic formula

□(p ⊃ ◯p) ⊃ (p ⊃ □p). (21)

where □ should be interpreted as always or henceforth and ◯ as at the next moment of time.

Translated — ∀P ∀x [∀y (R_{□}(x, y) ⊃ (P (y) ⊃ ∀z (R_{◯}(y, z) ⊃ P (z))))] ⊃ [P (x) ⊃ ∀u (R_{□}(x, u) ⊃ P (u))]

Negated — ∃x ∃P [∀y (R_{□}(x, y) ⊃ (P (y) ⊃ ∀z (R_{◯}(y, z) ⊃ P (z))))] ∧ [P (x) ∧ ∃u (R_{□}(x, u) ∧ \overline{P (u)})]

Transformed into the conjunctive normal form — ∃xu ∃P ∀y, z (P (z) ∨ \overline{R_{□}(x, y)} ∨ \overline{R_{◯}(y, z)} ∨ \overline{P (y)}) ∧ ∀z (P (z) ∨ x ≠ z) ∧ R_{□}(x, u) ∧ \overline{P (u)}

Transformed into the form required in the Theorem 3.1 —

∃xu ∃P ∀z [P (z) ∨ (x ≠ z ∧ ∀y (\overline{R_{□}(x, y)} ∨ \overline{R_{◯}(y, z)} ∨ \overline{P (y)})] ∧ R_{□}(x, u) ∧ \overline{P (u)} After application of Theorem 3.1 —

∃xu R_{□}(x, u) ∧ ν\overline{P (u)}.(x ≠ u ∧ ∀y (\overline{R_{□}(x, y)} ∨ \overline{R_{◯}(y, u)} ∨ \overline{P (y)})] Unnegated — ∀x, u R_{□}(x, u) ⊃ μP (u).(x = u ∨ ∃y (R_{□}(x, y) ∧ R_{◯}(y, u) ∧ P (y)).

Thus formula (21) is equivalent to the following one:

∀xu R_{□}(x, u) ⊃ [x = u ∨ ⋁_{i∈ω} ∃y_{0} … y_{i}(R_{◯}(x, y_{0}) ∧ … ∧ R_{◯}(y_{i−1}, y_{i}) ∧ R_{◯}(y_{i}, u))],

or to the even simpler looking

∀xu R_{□}(x, u) ⊃ ⋁_{i∈ω} R_{◯}^{i}(x, u)

i.e. (21) states that R_{□} is contained in the reflexive and ω-transitive closure of R_{◯}, a property which is not expressible by means of classical logic but expressible by means of fixpoint logic.

5 Conclusions

In this paper we presented an automated technique of eliminating second-order quantifiers from formulae. The technique we consider substantially extends known approaches. The resulting formulae are in general first-order or fixpoint formulae that are relatively easy to handle and to understand.

Although we mainly concentrated on the modal correspondence theory, our fixpoint approach is much more general. In particular it can be applied in the following important areas:

• modal and second-order theorem proving, since fixpoint calculus have a nice proof theory (cf. [8, 15, 16]). The Park rule

Ψ(I) ⊃ I ⊢ μP.Ψ(P) ⊃ I

and its ν-formulation

I ⊃ Ψ(I) ⊢ I ⊃ νP.Ψ(P)

are particularly useful here, since the formulae that result from application of Theorem 3.1 are monotone w.r.t. predicates substituted by fixpoint formulae

• modal and second-order model checking over finite domains, since model checking in this case can be done in polynomial time (cf. [7]), while second-order model checking over finite domains is NP-complete (by Fagin’s theorem [7])

• mechanizing commonsense reasoning, e.g. based on circumscription (recall, that circumscription introduces second-order quantification).

It is worth emphasizing here that the formulae of the form required in Theorem 3.1 are, in general, not reducible to first-order formulae. E.g. the second-order induction considered in Example 4.2 has no first-order equivalent. Similarly, most of the modal schemata considered in this paper are not first-order definable. Thus the extension of classical logic by fixpoint formulae seems to be, in a sense, minimal.

Also it should be mentioned that this approach does not always lead to either a first-order formula or some fixpoint formula. Recall that it is sometimes necessary to apply an equivalence preserving skolemization in order to be able to transform the input formula into the form required for our main theorem. Such a skolemization evidently introduces a quantification over functions and therefore the final result might not be a first-order formula even if the generated fixpoint itself causes no further problems. A typical example for such a case is the so called McKinsey Axiom □◇Φ ⊃ ◇□Φ for which neither a first-order equivalent nor a fixpoint formula exists which characterizes its frames. However, it is often possible to simplify such a quantification over functions such that the final result is again of first-order.

References

[1] W. Ackermann: Untersuchungen über das Eliminationsproblem der mathematischen Logik, Mathematische Annalen, 110 (1935), 390–413.

[2] R. A. Bull, K. Segerberg: Basic Modal Logic, in: Handbook of Philosophical Logic, Vol. 2 (D. Gabbay and F. Guenthner, eds.), D. Reidel Pub. Co. (1984), 1–88.

[3] B. Chellas: Modal Logic: An Introduction, Cambridge University Press (1980).

[4] P. Doherty, W. Łukaszewicz & A. Szałas: Computing Circumscription Revisited: A Reduction Algorithm (1994), Technical Report, Linköping University, IDA, LiTh-IDA-R-94-42, Sweden.

[5] D. Gabbay & H. J. Ohlbach: Quantifier elimination in second–order predicate logic, in: Proceedings of the KR’92, Principles of Knowledge Representation and Reasoning, Morgan Kaufmann (1992), 425–436.

[6] G. E. Hughes & M. J. Cresswell: An Introduction to Modal Logic, Routledge (1989).

[7] N. Immerman: Descriptive and Computational Complexity, in: Proceedings of Symposia in Applied Mathematics 38 (1989), 75–91.

[8] D. Kozen: Results on the Propositional μ-calculus, Theoretical Computer Science 27 (1983), 333–354.

[9] R. Moore: Reasoning About Knowledge and Action, PhD Thesis, MIT, Cambridge (1980).

[10] A. Nonnengart: First-Order Modal Logic Theorem Proving and Functional Simulation, in: Proceedings of the IJCAI’93, Morgan Kaufmann (1993), 80–85.

[11] A. Nonnengart: How to Use Modalities and Sorts in Prolog, in: Proceedings of the JELIA’94, LNAI 838, Springer Verlag (1994), 365–378.

[12] H. J. Ohlbach: Semantics-Based Translation Methods for Modal Logics, Journal of Logic and Computation, 5 (1991), 691–746.

[13] A. Prior: Past, Present and Future, Clarendon Press, Oxford (1967).

[14] H. Simmons: The Monotonous Elimination of Predicate Variables, Journal of Logic and Computation, 4 (1994), 23–68.

[15] A. Szałas: On Strictly Arithmetical Completeness in Logics of Programs, Theoretical Computer Science 79 (1991), 341–355.

[16] A. Szałas: Axiomatizing Fixpoint Logics, Information Processing Letters, 41 (1992), 175– 180.

[17] A. Szałas: On the Correspondence Between Modal and Classical Logic: an Automated Approach, Journal of Logic and Computation, 3 (1993), 605–620.

[18] A. Szałas: On an Automated Translation of Modal Proof Rules into Formulas of the Classical Logic, Journal of Applied Non-Classical Logics, 4 (1994), 119–128.

[19] J. van Benthem: Modal Logic and Classical Logic, Bibliopolis, Napoli (1983).

[20] J. van Benthem: Correspondence Theory, in: Handbook of Philosophical Logic, Vol. 2 (D. Gabbay and F. Guenthner, eds.), D. Reidel Pub. Co. (1984), 167–247.