MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Synthesizing Semantics for Extensions of Propositional Logic

Hans Jürgen Ohlbach

MPI–I–94–225 June 94

[figure: I N F O R M A T I K]

Im Stadtwald D 66123 Saarbrücken

Germany Author’s Address

Hans Jürgen Ohlbach Max–Planck–Institut für Informatik Im Stadtwald D-66123 Saarbrücken F. R. Germany email: ohlbach@mpi-sb.mpg.de

Acknowledgements

I would like to thank Dov Gabbay as well as my colleagues Andreas Nonnengart and Renate Schmidt for very fruitful discussions.

This work was supported by the ESPRIT project 6471 MEDLAR and by the BMFT funded project LOGO (ITS 9102).

Abstract

Given a Hilbert style specification of a propositional extension of standard propositional logic, it is shown how the basic model theoretic semantics can be obtained from the axioms by syntactic transformations. The transformations are designed in such a way that they eliminate certain derived theorems from the Hilbert axiomatization by turning them into tautologies.

The following transformations are considered. Elimination of the reflexivity and transitivity of a binary consequence relation yields the basic possible worlds framework. Elimination of the congruence properties of the connectives yields weak neighbourhood semantics. Elimination of certain monotonicity properties yields a stronger neighbourhood semantics. Elimination of certain closure properties yields relational possible worlds semantics for the connectives.

Propositional logic as basis of the specification allows to turn those parts which are not eliminated into second–order predicate logic (PL2) formulae. In many cases these formulae can be simplified to an equivalent first–order predicate logic (PL1) formula which describes the corresponding frame property. All transformations work for arbitrary n-place connectives. The steps can be fully automated by means of PL1 theorem provers and quantifier elimination algorithms. The meta theory guarantees that all transformation steps are sound and complete. As a by–product, translations into multi–modal logic are developed.

Key Words: Logic, Transformations, Semantics

Contents

1 Introduction 3

2 Transformation Operations 6 2.1 K-Transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Quantifier Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

3 A Test Example 10

4 The Transformations 11 4.1 Reflexivity and Transitivity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 4.2 Congruence Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

4.2.1 Sets as Neighbourhoods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2.2 Binary Neighbourhood Relations . . . . . . . . . . . . . . . . . . . . . . . . 15

4.3 Monotonicity Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 4.4 Transformations Based on Stone’s Representation Theorem . . . . . . . . . . . . . 18 4.5 Closure Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.6 Binary Accessibility Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.7 Truth Value Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

5 The Semantics Generation Procedure 27

6 Summary 28

A Appendix: Proofs for the Test Example 31

1 Introduction

Logics can be defined in various ways. The most abstract way is by means of a Hilbert system. A Hilbert system is a kind of grammar. It specifies how to enumerate all formulae to be considered as theorems. For encoding vague notions, like “knows”, “believes” and “wants”, a Hilbert style axiomatization is usually the method of choice because in Hilbert systems their properties can be expressed in a very abstract and intuitive way. Proving theorems in Hilbert systems, however, is extremely inefficient. It involves enumerating the theorems until the formula under consideration is eventually obtained. (Lemma A.2, for example, gives a good impression what theorem proving from Hilbert axioms means.)

One reason for developing an alternative to Hilbert systems is the desire to get more efficient calculi. Another reason is to understand the logic better by bringing properties to the surface which are sometimes very deeply hidden. Who, besides Łukasiewics, would for example guess that the Hilbert axiom

(p → q) → r) → ((r → p) → (s → p))  (1)
together with the rule:  from p and p → q infer q  (2)

specify the implicational fragment of propositional logic [Łuk70, p. 295]? An alternative way to describe a logic is by mapping the syntactic constructs to a (hopefully) simple and well understood mathematical structure, a Boolean algebra or more generally, a structure, i.e. a set with relations and functions defined over this set. The mapping must include an interpreter or a satisfiability relation for evaluating the truth value of a given formula in the structure. Typical examples for this semantical description of a logic are Tarski’s set theoretic semantics for predicate logic or Kripke’s possible worlds semantics for modal logic [Kri59, Kri63].

The usual way the correlations between the axiomatic description and the semantics are presented is: the axioms and the semantics are defined and soundness and completeness are proved. Soundness and completeness guarantee that a formula is a theorem in the axiomatic description if and only if it is a valid formula in the semantics. Finding an appropriate semantic structure, however, is nontrivial and requires experience and intuition. The purpose of this paper is to overcome this problem and to show how the process of finding a semantics can be automated to a large extend. The long–term goal of this work is the development of a logic engineering workbench where application oriented logics can be specified on a very abstract level and the investigation of the so defined logic can be left to the computer.

As examples for semantics of a logic consider the different versions of the semantics of modal logic. Common to all of them is the possible worlds framework as basic semantic structure. Each possible world determines the interpretation of the propositional variables and the classical connectives in the usual way. The interpretation of formulae with non–classical operators is defined in terms of relations or functions connecting the worlds. The weakest semantics for modal logic is the (weak) neighbourhood semantics (also called minimal model semantics [Che80]). Each world has sets of worlds as ‘neighbourhoods’. A formula □p is true in a world w iff the truth set of p, i.e. the set of worlds where p is true, is among w’s neighbourhoods. This semantics satisfies the ME rule, p ⇔ q implies □p ⇔ □q, but no stronger axiom or rule. In strong neighbourhood semantics, □p is true in a world w iff one of w’s neighbourhoods is a subset of p’s truth set. Strong neighbourhood semantics satisfies a monotonicity property: p ⇒ q implies □p ⇒ □q. The next stage is the well known Kripke semantics with a binary accessibility relation. But this is not the end of the story. For example, modal logic S5 has a semantics in terms of an accessibility relation with the extra condition that the accessibility condition is an equivalence relation. This condition guarantees that the S5 axioms hold. An alternative semantics for S5 has the truth condition for the □–operator: □p is true in a world iff p is true everywhere. In this semantics without accessibility relation, all S5 axioms are tautologies.

Each version of the semantics consists of two parts. The basic semantics contains just the definition of the primitive notions, neighbourhood relations or accessibility relations for example, and the satisfiability relation. The possible worlds together with the relations and functions operating on them are usually called frames.

The second part of the full specification of the semantics restricts the class of semantic structures by imposing constraints on the frames (so called frame conditions) and sometimes by restricting the assignment of truth values to the propositional variables. Modal logic T, for example is characterized by restricting the class of frames to those with reflexive accessibility relations. Intuitionistic logic as another example has a restriction on the assignment of propositional variables: if p is true in a world w then it remains true in all words accessible from w.

Each part of the semantics validates a certain part of the Hilbert axioms. The basic semantics of normal modal logic with binary accessibility relation for example validates the K-axiom □(p ⇒ q) ⇒ (□p ⇒ □q) and the Necessitation rule: from p infer □p. The reflexivity condition on the accessibility relation validates the axiom □p ⇒ p. Obviously, there is a hierarchy of semantics. A semantics S_{1} is stronger than a semantics S_{2} if the basic part of S_{1} validates more axioms than the basic part of S_{2}. A semantics is optimal for a Hilbert system if all axioms are validated in the basic part and no extra conditions are needed.

The questions we address in this paper are: where do these semantic notions, possible worlds, neighbourhoods, accessibility relations, satisfiability relations etc. come from? Is their invention really a creative act, or is there a systematic way to obtain them directly from the Hilbert axioms? The second question is, can one compute the frame conditions, i.e. the restrictions on a given semantic structure corresponding to Hilbert axioms with an automatic procedure? To answer these questions I proceed as indicated in the following picture.

[figure: HS; P L1(HS); Transformation; Υ(P L1(HS)); Transformation; rules Υ; semantics definitions; of the connectives; = frame conditions; =]

We begin with an arbitrary Hilbert system HS. Using first–order predicate logic as meta logic, the first step is to encode HS in PL1. In the PL1 axiomatization P L1(HS), the logical connectives are encoded as function symbols and formulae are encoded as terms. The propositional variables in Hilbert axioms are placeholders for arbitrary formulae. Therefore they become universally quantified variables in P L1(HS). Actually we need a PL1 axiomatization of the Hilbert system in terms of a binary consequence relation ⊢^{2}. p ⊢^{2} q means q is derivable from p^{1}.

The key observation underlying my approach for systematically finding a semantics comes from automated theorem proving. In order to prove a conjecture from assumptions, one need not perform the proof directly, but we can transform assumptions and conjectures and prove the transformed conjectures from the transformed assumption, provided the transformation Υ guarantees

assumption ⇒ conjecture iff Υ(assumption) ⇒ Υ(conjecture).  (3)

The working hypothesis of this paper is therefore

The semantics of an axiomatically defined logic is the result of a carefully designed transformation of predicate logic formulae. The transformation rules represent the interpretation function and the non–tautologous transformed Hilbert axioms are the frame conditions.

An optimal transformation turns all axioms into tautologies. In this case, proving a theorem φ from HS reduces to proving Υ(φ) without any additional assumptions. The guideline for finding a good transformation is therefore the intention to turn axioms into tautologies, or to make them in some other way redundant.

1If the Hilbert system is originally specified with a unary ‘provability’ predicate ⊢^{1}, the deduction theorem p ⊢^{2} q iff ⊢^{1} (p → q) can be used to translate it into the formulation with a binary consequence relation. This, however, excludes axiomatizations in terms of the provability predicate where the top–level connectives of the formulae are not some sort of implication.

Ideally one would like to have a procedure T rans Gen which, given a formula φ as input, computes a transformation Υ_{φ} with property (3) such that Υ_{φ}(φ) = true. If P L1(HS) consists of the formulae φ_{1}, …, φ_{n} one would compute Υ_{φ_{1}} = T rans Gen(φ_{1}), get φ′_{i} = Υ_{φ_{1}}(φ_{i}) for i = 2, …, n, compute Υ_{φ′_{2}} = T rans Gen(φ′_{2}), apply it to φ′_{3}, …, φ′_{n} and repeat the process until all axioms are turned into tautologies. And, in fact, in [OGP94], we sketch such a procedure T rans Gen. Unfortunately this idea does not work in general. The reason is that Υ may produce an infinite conjunction of formulae, and then the process does not terminate. But even if this method worked, it would not be very satisfactory because we do not want any transformation, but a transformation that gives some insight into the structure of the logic. I therefore propose an approach which is restricted to a certain class of logics, but gives better results for them. The idea is to develop transformations for very concrete formulae or formula schemas. For each given Hilbert system, we then check which of the formulae out of our database of formulae with known transformations is a theorem. That means we decompose

P L1(HS) ⇔ φ_{1} ∧ … ∧ φ_{k} ∧ rest

and for the φ_{i} we develop transformations once and for all. The transformations for φ_{1} ∧ … ∧ φ_{k} specify the basic semantics and the transformation of the rest gives the frame conditions. The properties φ_{i} investigated in this paper are the n–place connective versions of the following four properties of a one–place □–operator, formulated with a binary consequence relation ⊢^{2}.

φ_{1} = reflexivity and transitivity of ⊢^{2}
φ_{2} = p ⊢^{2} q ∧ q ⊢^{2} b ⇒ □p ⊢^{2} □q  (ME rule)
φ_{3} = p ⊢^{2} q ⇒ □p ⊢^{2} □q  (monotonicity)
φ_{4} = w ⊢^{2} □p ∧ w ⊢^{2} □q ⇒ w ⊢^{2} □(p ∧ q). (closure property)

These properties are of a very basic nature. They hold in many logics. The transformations we have developed for φ_{1} to φ_{4} reconstruct the well known semantic structures. φ_{1} gives rise to the basic possible worlds framework and the satisfiability relation. Elimination of φ_{2} reconstructs weak neighbourhood semantics, elimination of φ_{3} reconstructs strong neighbourhood semantics, and finally, φ_{4} is responsible for the usual accessibility relation.

Although in this paper, only these four properties are investigated, the technique for finding the transformations is not restricted to these cases. Following our recipe, it should not be too difficult to extend the results to other properties.

Since the transformations for φ_{1} to φ_{4} are sound and complete (property (3)), each given Hilbert system for which some of the φ_{i} have been proved can be transformed, and we are guaranteed that a transformed theorem follows from the transformed Hilbert system if and only if it follows from the original system. This gives us a general soundness and completeness result for the whole class of logics with these properties φ_{i}. Proving the φ_{i} from a given Hilbert system is usually nontrivial. But fortunately it is a pure PL1 theorem proving problem which can be solved with an automated theorem prover.

As we shall see, the result of the transformation of a Hilbert system is an axiomatization of the corresponding frame properties. A considerable simplification of the axioms describing the frame properties is possible if a propositional logic is part of the axiomatization. The Lindenbaum algebra of a propositional logic is a Boolean algebra, which, by Stone’s representation theorem, is isomorphic to a field of sets. This property can be exploited to turn formula variables, which in the PL1 formulation are ordinary variables ranging over some domain, into set variables ranging over the powerset of the set of ‘worlds’. Each such set can be correlated with a formula which is valid exactly at this set. Thus, ordinary variables become formula variables. By this transformation the Hilbert axioms which do not become tautologies become second–order predicate logic formulae. In many cases, however, these PL2 formulae are equivalent to PL1 formulae describing properties of the neighbourhood or accessibility relations. Thus, we have a two-step transformation. The first step translates the original Hilbert axiom into a PL1 formula. The original formula variables are ordinary PL1 variables. The transition to PL2 turns these variables into predicate variables. In the second step the predicate variables are completely eliminated by a quantifier elimination procedure and an equivalent PL1 formula is computed – if there is one. This formula specifies a frame property. That means the correspondence problem [vB84], i.e. the problem of finding for a given Hilbert axiom a corresponding property at the semantic level, reduces to the problem of finding for a PL2 formula an equivalent PL1 formula. This problem can in many cases be solved with a quantifier elimination algorithm. The algorithm we have developed for this purpose [GO92a] is briefly described in Section 2.2.

PL2 formulae without PL1 equivalents specify so–called incomplete logics. Since the transition to PL2 formulae which turns ordinary variables into predicate variables is not mandatory, we still have a way to deal with these incomplete systems.

The transformation techniques are described in the next section. Section 4 is the main section of the paper. The particular transformations are introduced for arbitrary n-place connectives and soundness and completeness is proved. In order to illustrate the various aspects of the method and to demonstrate that the investigation of a concrete Hilbert system can be automated, we use a very complicated test example. For proving the key lemmas for this test example we used the Otter theorem prover. All proofs are listed in the Appendix.

Warning!

In this paper we use predicate logic as meta logic for the ‘object logic’ we want to investigate. Therefore there are two kinds of semantics involved. The standard semantics of predicate logic is needed when we talk about the general mechanisms and verify our methododology. The semantics of the object logic, on the other hand, is the result of the transformations of the Hilbert system. This should not be mixed up.

2 Transformation Operations

The transformations needed to synthesize the semantics follow essentially the same few schemas, K-transformations [OGP94] and quantifier elimination [GO92a]. A short overview of both is given in this section.

2.1 K-Transformations

To illustrate the basic idea of K-transformations^{2}, suppose we have some set Φ of axioms which, among other things, axiomatize a reflexive and transitive relation R, i.e.

∀x R(x, x)  (4)
∀x, y, z R(x, y) ∧ R(y, z) ⇒ R(x, z)  (5)

are either contained in Φ or derivable from Φ, and we want to get rid of the reflexivity and transitivity of R.

In order to show that a formula C is entailed by Φ, one usually tries to refute Φ ∧ ¬C. Before the refutation is actually started, every transformation on Φ ∧ ¬C which preserves satisfiability and unsatisfiability is allowed. Skolemization of existential quantifiers is a typical example of a routinely applied transformation which preserves satisfiability and unsatisfiability, but not logical equivalences.

The translation we propose for eliminating reflexivity and transitivity of R exploits that these two properties together imply

∀x, y R(x, y) ⇔ (∀w R(w, x) ⇒ R(w, y)).  (6)

To see this, suppose R(x, y) and R(w, x) hold. By transitivity, R(w, y) also holds, i.e. the “⇒”–part is shown. For the “⇐”–part, take w = x and use the reflexivity of R to derive R(x, y).

2‘K-transformation’ is short for ‘Killer transformation’. These transformations ‘kill’ certain properties from axiomatizations.

Since (6) is entailed by Φ, we could add it to Φ ∧ ¬C without loosing satisfiability or unsatisfiability. However, instead of (6), we add

∀x, y R(x, y) ⇔ (∀w R′(w, x) ⇒ R′(w, y))  (7)

to Φ ∧ ¬C where R′ is a new predicate symbol. Clearly, if Φ ∧ ¬C is satisfiable then Φ ∧ ¬C ∧ (7) is also satisfiable: the interpretation of R′ can be chosen to be the same as the interpretation of R. In this case (7) is equivalent to (6), which follows from Φ. Thus, (7) is also true in the extended interpretation. On the other hand, if Φ ∧ ¬C ∧ (7) is satisfiable then certainly Φ ∧ ¬C is satisfiable as well.

But now we have a definition of R in terms of R′ where R′ is an uninterpreted new predicate symbol. In the next step, (7) is used as a rewrite rule from left to right, replacing all occurrences of R in Φ ∧ ¬C by the formula with R′. We obtain the transformed formula Φ′ ∧ ¬C′ ∧ (7) with R′ in place of R. This is a terminating equivalence preserving transformation.

What happens to the reflexivity and transitivity of R? ∀x R(x, x) becomes ∀x ∀w R′(w, x) ⇒ R′(w, x) which is a tautology (by the reflexivity of “⇒”). The transitivity (5) becomes ∀x, y, z (∀w R′(w, x) ⇒ R′(w, y)) ∧ (∀w R′(w, y) ⇒ R′(w, z)) ⇒ (∀w R′(w, x) ⇒ R′(w, z)) which is also a tautology (by the transitivity of ⇒). Thus, R′ need neither be reflexive nor transitive.

Nothing would have been gained if the definition (7) of R, could not be removed afterwards. That means we have to show that Φ′ ∧ ¬C′ ∧ (7) is satisfiable if and only if Φ′ ∧ ¬C′ is satisfiable. Since Φ′ ∧ ¬C′ does not contain R any more, we can always find an interpretation for R, using (7) as definition. Therefore each model for Φ′ ∧ ¬C′ can be extended to a model for Φ′ ∧ ¬C′ ∧ (7). Thus, (7) can be eliminated. Φ′ ∧ ¬C′ is the final result of our transformation.

A small example illustrates how this works. Suppose, besides transitivity of R we have the facts

R(a, b) ∧ R(b, c) ∧ R(c, d)

From this, R(a, d) can be derived. The transformed formulae are:

∀w R′(w, a) ⇒ R′(w, b)
∀w R′(w, b) ⇒ R′(w, c)
∀w R′(w, c) ⇒ R′(w, d).

The negated and transformed theorem is ¬∀w R′(w, a) ⇒ R′(w, d) which is normalized to R′(e, a) ∧ ¬R′(e, d) where e is a Skolem constant. The transformed formulae can now be refuted without transitivity of R′^{3}.

What has actually happened is that the role of the reflexivity and transitivity of R has been taken over by the reflexivity and transitivity of the implication connective. Many other examples of K-transformations are of a similar kind. The built in properties of predicate logic take over the role of special properties of non–logical symbols.

The General Transformation Procedure

The general procedure for transforming formulae Φ in a consistent way, i.e. without loosing satisfiability or unsatisfiability, consists of the following sequence of steps

extension  transformation  elimination
Φ  →  Φ ∧ transformer  →  Φ′ ∧ transformer  →  Φ′

where ‘transformer’ is a formula of the kind

Left ⇔ Right.  (8)

(7) is an example for (8). The ‘extension’ step involves finding the transformer. In general this is still a creative step. In [OGP94], however, we describe methods for automating this step to a certain extend. The actual transformation is done in the ‘transformation’ step. In the simplest case the transformation strategy is just definitional replacement where (8) is used as rewrite rule form left to right. It can, however, also be a much more complex combination of rewriting, inferencing and deleting formulae. In the elimination step we delete the transformer. Since removing formulae can turn unsatisfiable formula sets into satisfiable sets, this is also a nontrivial step which has to be justified. To ensure that the transformation is satisfiability preserving, which is sufficient to do theorem proving by refutation, the following lemmas have to be proved.

3In [OGP94] we optimize the transformation for reflexivity and transitivity. If reflexivity is kept and R is not renamed, then only the positive R–literals need to be transformed. For the purposes of this paper, however, this optimization is irrelevant.

Definition 2.1 (Transformation Lemmas) The extension lemma proves that satisfiability of Φ implies satisfiability of Φ ∧ transformer. The transformation lemma proves that Φ ∧ transformer is satisfiable if and only if Φ′ ∧ transformer is satisfiable, where Φ′ is the transformed version of Φ. The elimination lemma proves that satisfiability of Φ′ implies satisfiability of Φ′ ∧ transformer. <

Lemma 2.2 (Faithfulness) A K-transformation for which the extension lemma, the transformation lemma, and the elimination lemma have been proved, preserves satisfiability and unsatisfiability. We call this a faithful transformation. It is sound and complete. <

There are standard cases of transformations which occur quite frequently. For these cases we can prove some of the lemmas once and for all. In an actual case, it has only to be checked whether the transformer is one of these standard types.

Definition 2.3 (Renamed Transformer) A transformer Left ⇔ Right is called a renamed transformer for a formula Φ iff there is a formula Left ⇔ Right_{0} entailed by Φ and Right is obtained from Right_{0} by renaming constant, function, predicate symbols and sorts with new symbols not occurring in Φ. Different occurrences of the same symbol in Right_{0} may be renamed differently. Left ⇔ Right_{0} is called the basis of the transformer. <

Lemma 2.4 (Extension Lemma for Renamed Transformers) The extension lemma (Def. 2.1) holds for renamed transformers. <

The proof of the extension lemma for this type of transformers amounts to proving that the basis Left ⇔ Right_{0} follows from Φ. This is a standard theorem proving task which can be done with automated theorem provers.

The transformer (7) for the elimination of reflexivity and transitivity is an example for a renamed transformer. The proof of Left ⇔ Right_{0}, i.e. (6) is trivial in this case.

As we have seen in the example with reflexivity and transitivity, the renamed predicate R′ need not be reflexive or transitive any more. An important observation is, however, that we can assume that the renamed symbols have some or all properties of the original symbols. The proof showing that there is an interpretation for (7) just interpreted R′ like R, and therefore R′ has R’s properties in this interpretation. Thus, we are free to add suitable axioms for R′ without changing satisfiability or unsatisfiability.

In the class of transformers specified in the next definition, the transformation process itself is reduced to a simple rewriting operation.

Definition 2.5 (Rewriting Transformers) A transformer ∀x_{1}, …, x_{n} R(x_{1}, …, x_{n}) ⇔ Right where R does not occur in Right, is called a rewriting transformer. The transformation strategy for rewriting transformers is just definitional replacement, i.e. all occurrences R(s_{1}, …, s_{n}) are replaced with the corresponding instances of Right. <

Lemma 2.6 (Transformation Lemmas for Rewriting Transformers) The transformation lemma and the elimination lemma (Def. 2.1) hold for rewriting transformers.

<

Renamed rewriting transformers are the simplest transformers of all. The only thing which has to be proved for this class of transformers is that the basis Left ⇔ Right_{0} for the transformer follows from Φ. The transformer (7) turns out to be of this simple type.

The next class of transformers is of a more general nature. It allows us to exploit completeness results for special inference strategies, as for example ordered resolution. (24) is an example for a transformer of this kind.

Definition 2.7 (Saturation Transformers) A transformer Left ⇔ Right is called a saturation transformer for the formula Φ if there is a refutation complete deduction strategy and it can be shown that according to this strategy only finitely many inferences between the transformer itself and the formulae in Φ are possible. Φ is transformed by drawing all inferences between the transformer and Φ, this strategy allows. Redundant formulae which are no longer necessary for finding a contradiction are removed. <

Lemma 2.8 (Transformation Lemmas for Saturation Transformers) The transformation lemma and the elimination lemma (Def. 2.1) hold for saturation transformers.

<

The formula Φ which is transformed usually consists of the two parts, the assumption and the negated onjecture. At the time of the development of the K-transformation, usually only the assumption is known. Therefore the transformation lemma has to be proved for all potential conjectures. Alternatively one can specify the class of admissible conjectures for which the Ktransformation works.

2.2 Quantifier Elimination

In [GO92a] we have developed an algorithm which can compute for second–order formulae of the kind ∃P_{1}, …, P_{k} Φ where Φ is a first–order formula, an equivalent first–order formula — if there is one. Since ∀P_{1}, …, P_{k} Φ ⇔ ¬∃P_{1}, …, P_{k} ¬Φ, this algorithm can also be applied to universally quantified predicate variables. Related methods can also be found in [Ack35a, Ack35b, Ack54, Sza92, BGW92, Sim94].

The definition of the algorithm is:

Definition 2.9 (The SCAN Algorithm) Input to SCAN is a formula α = ∃P_{1}, …, P_{n} Φ with predicate variables P_{1}, …, P_{n} and an arbitrary first–order formula Φ. Output of the SCAN — if it terminates — is a formula φ_{α} which is logically equivalent to α, but not containing the predicate variables P_{1}, …, P_{n}. SCAN performs the following three steps:

1. Φ is transformed into clause form.

2. All C–resolvents and C–factors with the predicate variables P_{1}, …, P_{n} have to be generated. C–resolution (‘C’ for constraint) is defined as follows:

P (s_{1}, …, s_{n}) ∨ C  P (…) and ¬P (…)
¬P (t_{1}, …, t_{n}) ∨ D  are the resolution literals
C ∨ D ∨ s_{1} ≠ t_{1} ∨ … ∨ s_{n} ≠ t_{n}

and the C-factorization rule is defined analogously:

\frac{P (s_{1}, …, s_{n}) ∨ P (t_{1}, …, t_{n}) ∨ C}{P (s_{1}, …, s_{n}) ∨ C ∨ s_{1} ≠ t_{1} ∨ … ∨ s_{n} ≠ t_{n}.} .

Notice that only C-resolutions between different clauses are allowed (no self resolution). A C-resolution or C-factorization can be optimized by destructively resolving literals x ≠ t where the variable x does not occur in t with the reflexivity equation. C–resolution and C–factorization takes into account that second–order quantifiers may well impose conditions on the interpretations which must be formulated in terms of equations and inequations.

As soon as all resolvents and factors between a particular literal and the rest of the clause set have been generated (the literal is ‘resolved away’), the clause containing this literal must be deleted (purity deletion). If all clauses are deleted this way, this means that α is a tautology.

All equivalence preserving simplifications may be applied freely. If an empty clause is generated, this means that α is contradictory.

3. If the previous step terminates and there are still clauses left then reverse the Skolemization. <

The SCAN algorithm is correct in the sense that its result is logically equivalent to the input formula. It cannot be complete, i.e. there may be second–order formulae which have a first–order equivalent, but SCAN cannot find it. An algorithm which is complete in this sense cannot exists, otherwise the theory of arithmetic would be enumerable.

The points where SCAN can fail to compute a first–order equivalent for α are (i) the resolution does not terminate and (ii) reversing Skolemization is not possible. In the second case there is a (again second–order) solution with existentially quantified Skolem functions.

3 A Test Example

For illustrating the various transformation steps, we use a test example. It is a propositional logic extended with two more operators. The first one is a binary connective ⇝ as an example for a non–classical implication operator. ⇝ is axiomatized with a variant (12) of the Łukasiewics axiom (1) and its own version of Modus Ponens (13) below, both formulated with the binary consequence relation.

Since, by the deduction theorem, the binary consequence relation corresponds to the propositional implication →, (12) is not precisely the Łukasiewics axiom. The difference is that the top–level connective definitely is the propositional implication. For the connective ⇝ we pretend for the moment not to know anything besides the axioms. The result of our analysis should of course be that this connective is in fact also propositional implication.

The second connective in our test example is the modal □–operator. The □–operator is axiomatized with the K-axiom and the Necessitation rule. Thus, we should be able to reproduce standard relational possible worlds semantics. To make things more interesting, however, the K-axiom is not formulated with the known propositional implication →, but with the new connective ⇝. The semantics of the □–operator therefore depends on the semantics of the ⇝–connective.

Example 3.1 (Our Main Test Example) We use the following seven formulae as our test example. The first three formulae axiomatize propositional logic. They are not important. Any other axiomatization of propositional logic would do as well. The next two axioms formalize our “new” connective ⇝. We pretend not to know anything more about it. The last two formulae axiomatize the modal □–operator. (14) is a formulation of the Necessitation rule ‘⊢^{1}P implies ⊢^{1}□P ’ in terms of the binary consequence relation.

(15) is a version of the K-axiom, formulated with the ‘unknown’ connective ⇝.

∀p, q, r, s  ((p → q) → r) ⊢^{2} ((r → p) → (s → p))  (9)
∀p, q, r, s  p ⊢^{2} q ∧ (p → q) ⊢^{2} (r → s) ⇒ r ⊢^{2} s  (10)
∀p  ⊥ ⊢^{2} p  (11)
∀p, q, r, s  ((p ⇝ q) ⇝ r) ⊢^{2} ((r ⇝ p) ⇝ (s ⇝ p))  (12)
∀p, q, r, s  p ⊢^{2} q ∧ (p ⇝ q) ⊢^{2} (r ⇝ s) ⇒ r ⊢^{2} s  (13)
∀p  (∀q q ⊢^{2} p) ⇒ (∀q q ⊢^{2} □p)  (14)
∀p, q  □(p ⇝ q) ⊢^{2} (□p ⇝ □q).  (15)

<

In the sequel let A_{1} be the initial Hilbert system for the logic L we want to investigate. The set consisting of (9) to (15) is an example for A_{1}. The □–operator as part of the test example shows the correspondence between the techniques developed in this paper and the well known facts about modal logic. The generalization of the semantics construction from a one–place operator like □ to an non–classical n-place operator is illustrated with the binary ⇝ connective. I recommend the reader to follow this example carefully and in particular to compare the development of the semantics for the □–operator with the standard methods you can find in the literature, for example in [Che80].

We use a many–sorted version of PL1 [Wal87] and we assume that the variables which are to be understood as formula variables are of sort F (for Formula). In most cases we use the letters p, q, r, s for formula variables without explicitly annotating them with the sort symbol F.

4 The Transformations

In this section, which is the main section of the paper, the transformation process is described. The transformations are designed to eliminate properties of A_{1}, or more precisely, absorb these properties into the properties of our meta logic, predicate logic. First we eliminate the reflexivity and transitivity of ⊢^{2}. This transformation introduces the basic possible worlds framework and the satisfiability relation. In the second and third step, the congruence properties and the monotonicity properties of the connectives are eliminated. This gives rise to so–called neighbourhood semantics. Finally in the last step certain closure properties are eliminated and we reconstruct possible worlds semantics with n + 1–ary accessibility relations for n–place connectives.

4.1 Reflexivity and Transitivity

To start with, we want to eliminate reflexivity and transitivity of the consequence relation ⊢^{2}. The method for eliminating reflexivity and transitivity has been explained in Section 2.1. The transformer is ∀p, q p ⊢^{2} q ⇔ (∀w w ⊧^{L} p ⇒ w ⊧^{L} q). But we can go a step further and introduce a new sort W for the variable w. The first one of our sequence of transformers is therefore for all p, q:

T_{1}:  p ⊢^{2} q ⇔ (∀w:W w ⊧^{L} p ⇒ w ⊧^{L} q)  (16)

which is still a renamed rewriting transformer and therefore sound and complete.

We want to interpret the sort W as the set of ‘worlds’ in a possible worlds semantics and the predicate ⊧^{L} as the satisfiability relation. The intended reading for (16) is therefore really ‘q is entailed by p iff q is true in all worlds satisfying p’. But for the moment (16) is still to be understood as an ordinary predicate logic formula.

Completeness of T_{1} gives us our first completeness lemma.

Lemma 4.1 (Completeness Lemma for Possible Worlds) If A_{1} implies reflexivity and transitivity of ⊢^{2} then for every formula φ: A_{1} entails φ iff A_{2} =^{def}T_{1}(A_{1}) entails T_{1}(φ). <

Notation: Frequently we will use the following notation: Instead of w ⊧^{L} p we write w ∈ |p|. Syntactically, this is just an abbreviation. It allows us to abbreviate formulae ‘∀w w ⊧^{L} p ⇒ w ⊧^{L} q’ by ‘|p| ⊆ |q|’ and formulae ‘∀w w ⊧^{L} p ⇔ w ⊧^{L} q’ by ‘|p| = |q|’. Semantically, however, this |...| notation has a particular meaning. |...| can be understood as a function mapping domain elements to sets: |p| =^{def} {w | (w, ℑ(p)) ∈ ℑ(⊧^{L})} where ℑ is any predicate logic interpretation. On the level of predicate logic semantics, defined by some ℑ, expressions like w ∈ |p| and |p| ⊆ |q| and |p| = |q| are to be understood literally. As we shall see in Subsection 4.4, under certain circumstances, ⊧^{L} can be interpreted as membership relation. In this case this abbreviating notation is equivalent to the original notation.

The methods discussed in this paper work for arbitrary n–place connectives. To simplify notation we therefore use p⃗ as an abbreviation for p_{1}, …, p_{n} where n is the arity of the connectives under consideration.

As proved in Lemma A.1 and A.2 in the Appendix, the consequence relation in our test example (3.1) is in fact reflexive and transitive ands therefore the transformer T_{1} is applicable. If we apply the transformer T_{1} to the last four axioms of our test example, we obtain

∀p, q, r, s  ∀w:W w ⊧^{L} ((p ⇝ q) ⇝ r) ⇒ w ⊧^{L} ((r ⇝ p) ⇝ (s ⇝ p))
∀p, q, r, s  (∀w:W w ⊧^{L} p ⇒ w ⊧^{L} q) ∧ (∀w:W w ⊧^{L} p ⇝ q ⇒ w ⊧^{L} r ⇝ s)
⇒ (∀w:W w ⊧^{L} r ⇒ w ⊧^{L} s)
∀p  (∀q ∀w:W w ⊧^{L} q ⇒ w ⊧^{L} p) ⇒ (∀q ∀w:W w ⊧^{L} q ⇒ w ⊧^{L} □p)
∀p, q  ∀w:W w ⊧^{L} □(p ⇝ q)) ⇒ w ⊧^{L} (□p ⇝ □q).

Obviously these formulae are no tautologies. Therefore we have to go on and find stronger transformations.

4.2 Congruence Properties

After having eliminated reflexivity and transitivity of ⊢^{2}, we now attack certain congruence properties. As we shall see, eliminating these properties on the syntactic side introduces neighbourhood semantics (also called minimal model semantics [Che80]) on the semantic side.

Assumption: In the sequel we assume that ⊢^{2} is the only predicate symbol occurring in A_{1}. In this case only literals w ⊧ t where w is a variable occur in A_{2}. Furthermore, we assume that all formula variables in A_{1} are universally quantified.

The congruence properties we want to eliminate are

∀p⃗, q⃗ ⋀_{i}(p_{i} ⊢^{2} q_{i} ∧ q_{i} ⊢^{2} p_{i}) ⇒ f(p⃗) ⊢^{2} f(q⃗).  (17)

For verifying (17) from A_{1}, it can be split into individual lemmas for each argument position.

∀p, q (p ⊢^{2} q ∧ q ⊢^{2} p) ⇒ ∀s⃗, s′f(s⃗, p, s′) ⊢^{2} f(s⃗, q, s′).  (18)

The instances of (18) for our test example are

∀p, q (p ⊢^{2} q ∧ q ⊢^{2} p) ⇒ ∀s p ⇝ s ⊢^{2} q ⇝ s)  (19)
∀p, q (p ⊢^{2} q ∧ q ⊢^{2} p) ⇒ ∀s s ⇝ p ⊢^{2} s ⇝ q  (20)
∀p, q (p ⊢^{2} q ∧ q ⊢^{2} p) ⇒ □p ⊢^{2} □q.  (21)

The proofs for these formulae are also listed in the Appendix (Lemmas A.3, A.4, A.5). The congruence property (21) for the □–operator corresponds to the well known ME rule, ⊢^{1}(P ⇔ Q) implies ⊢^{1}(□P ⇔ □Q), which is the only rule required for classical modal systems.

The transformer T_{1} translates the congruence properties (17) for the connectives f into

∀p⃗, q⃗ ⋀_{i}(∀w:W w ⊧^{L} p_{i} ⇔ w ⊧^{L} q_{i}) ⇒ (∀w:W w ⊧^{L} f(p⃗) ⇒ w. ⊧^{L} f(q⃗))  (22)

A straightforward proof from this yields for all p⃗, w:

w ⊧^{L} f(p⃗) ⇔ ∃x⃗:W w ⊧^{L} f(x⃗) ∧ ⋀_{i} ∀v:W v ⊧^{L} x_{i} ⇔ v ⊧^{L} p_{i}  (23)

as the basis for the next K-transformation, a renamed transformer (Def. 2.3), which is, for all p⃗, w:

T_{2}:  w ⊧^{L} f(p⃗) ⇔ ∃x⃗:S N_{f}(w, x⃗) ∧ ⋀_{i} ∀v:W R_{f}^{i}(x_{i}, v) ⇔ v ⊧^{L} p_{i}.  (24)

Here we take advantage of the fact that different occurrences of a predicate may well be renamed differently in a renamed transformer. The ‘w ⊧^{L} f(x⃗)’ occurrence is renamed to N_{f}(w.x⃗) and the ‘v ⊧^{L} x_{i}’ occurrence is renamed to R_{f}^{i}(x_{i}, v). This is the fist place where we introduced relations between worlds as new semantic structures. It is easy to check that T_{2} in fact turns the congruence properties (22) into tautologies.

The instances of (24) for our test example are:

w ⊧^{L} (p ⇝ q) ⇔ ∃x, y:S N_{⇝} (w, x, y) ∧ (∀v:W R_{⇝}^{1} (x, v) ⇔ v ⊧^{L} p) ∧
(∀v:W R_{⇝}^{2} (y, v) ⇔ v ⊧^{L} q)  (25)
w ⊧ □p ⇔ ∃x:S N_{□} (w, x) ∧ (∀v:W R_{□} (x, v) ⇔ v ⊧^{L} p).  (26)

Lemma 4.2 (Soundness and Completeness of the Transformer T_{2}) If A_{2} implies the congruence properties (22) for all functions f and as transformation strategy, rewriting with T_{2} until all occurrences of the connectives disappear, is chosen, then the extension, the transformation and the elimination lemmas (Def. 2.1) hold.

Proof : \underline{Extension Lemma:} This lemma holds because the sort symbol S can be interpreted like W, N_{f}(w, x⃗) can be interpreted as w ⊧^{L} f(w, x⃗), R_{f}^{i}(x_{i}, v) can be interpreted as v ⊧^{L} x_{i} and then (24) is true in the extended model because (23) is. \underline{Transformation Lemma:} Unfortunately the transformer T_{2} is no longer a simple definition for a predicate. The left hand side is of the form w ⊧^{L} f(p⃗), where w and the p_{i} are variables. Since, by the first transformer T_{1}, all literals in A_{2} are of the form v ⊧^{L} f(s⃗) where v is a variable and the s_{i} are terms, the transformers can also be applied as rewrite rules. Due to the structure of the transformers’ right hand sides, each rewrite step eliminates one occurrence of a connective at a time. Furthermore, because there is a transformer for every connective f, eventually all occurrences of the connectives are eliminated. We end up with formulae A_{3} containing only literals with the N_{f} and R_{f}^{i} predicates with variables as their arguments, and literals v ⊧^{L} p_{i} where the p_{i} are the original variables. So far, this is an equivalence transformation which does not affect the models at all. \underline{Elimination Lemma:} Although there are further inferences possible between the transformers and A_{3}, we can delete the transformers now without changing the satisfiability or unsatisfiability. The argument is proof theoretic. We show that there is a complete inference strategy which does not allow to draw any further inferences with the transformers in this particular case. The completeness of the strategy then guarantees that the transformers are useless. The strategy we use is ordered resolution with elimination of redundant clauses [BG90]. Ordered resolution requires the definition of an ordering on literals. Only resolvents between the biggest literals in a clause need to be generated and we still have a complete procedure. The redundancy criterion, Bachmair and Ganzinger [BG90] have shown to be complete is: inferences are redundant if the inferred clause follows from smaller (in the given ordering) clauses. If we choose the ordering such that literals with the connectives f are bigger than the other literals, we immediately see that no resolvents with literals at the right hand side of the transformers are generated. These literals are smaller than the literal at the left hand side. But there are still resolutions possible between the literals w ⊧^{L} f(p⃗) from the left hand sides of the transformers and literals v ⊧^{L} p in A_{3}, where p is a variable. We have assumed that these variables are of the basic domain sort F (for ‘Formula’). That means, there are quantifications ∀p:F . . .. It is well known that sorts can be written as one–place predicates. Instead of ∀p:F …, one writes ∀p F (p) ⇒ . . .. Now we assume this syntactic form for A_{3} and extend the ordering by requiring that literals F (f(...)) are bigger than any other literals. Since the first rewrite step eliminates all occurrences of connectives in A_{3}, there are of course no literals of the form F (f(…)) in A_{3}, but only literals of the form F (p). Each resolution between w ⊧^{L} f(p⃗) and v ⊧^{L} p now instantiates p to f(…). That means, the resolvent contains literals F (f(…)) and is therefore bigger than the parent clauses. This resolvent is redundant and needs not be generated. Thus, we find that all resolvents with the transformers are redundant, which finally licenses their deletion. <

Soundness and completeness of T_{2} together with Lemma 4.1 gives us the second completeness lemma.

Lemma 4.3 (Completeness Lemma for Neighbourhood Relations) If A_{1} implies reflexivity and transitivity of ⊢^{2} and the congruence properties (17) for all connectives then for every formula φ: A_{1} entails φ iff A_{3} =^{def} T_{2}(T_{1}(A_{1})) entails T_{2}(T_{1}(φ)). <

4.2.1 Sets as Neighbourhoods

The transformer (24) is not yet recognizable as neighbourhood semantics we are familiar with from textbooks. The next transformation therefore combines the relations N and R^{i} into one neighbourhood relation N′ with sets as arguments. To this end we define a K-transformation Q by

∃x⃗:S N_{f}(w, x⃗) ∧ ⋀_{i}(∀v:W R_{f}^{i}(x_{i}, v) ⇔ φ(v, p_{i}))
⇔  (27)
∃X⃗ N′_{f}(w, X⃗) ∧ ⋀_{i}(∀v:W v ∈ X_{i} ⇔ φ(v, p_{i}))

where φ(v, p_{i}) is any formula containing v and p_{i} as free variables and ∈ is the membership relation.

Lemma 4.4 (Soundness and Completeness of Q) If A_{1} implies reflexivity and transitivity of ⊢^{2} together with the congruence properties (17) for all connectives, and the transformation strategy to be applied to A_{3} is rewriting inside–out using Q as rewrite rule from left to right, then the transformation lemmas hold for Q.

Proof : \underline{Extension Lemma:} The extension Lemma 2.4 for Q can be proved by defining the N′_{f} according to

N′_{f}(w, X⃗) ⇔ ∃x⃗ N_{f}(w, x⃗) ∧ ⋀_{i}(∀v x_{i} ∈ X_{i} ⇔ R_{f}^{i}(x_{i}, v))

The sets X_{i} are just the set of R_{f}^{i}–accessible points from some N_{f}–accessible point as the figure below illustrates for a single neighbourhood set.

[figure: R_{f}^{1}; v_{1}; v_{2}; v_{3}; φ(v_{1}, p_{i}); …; N′_{f}; X_{1}; …; φ(v_{3}, p_{i}); φ(v_{2}, p_{i}); w; N_{f}; x]

This definition of N′_{f} entails the transformer (27). \underline{Transformation Lemma:} Since the transformer T_{2} generates formulae with exactly the structure of the left hand side of (27), the transformation strategy can simply be rewriting, starting with the innermost occurrences of the pattern. All instances of the left hand side are replaced by the corresponding instances of the right hand side. This is an equivalence preserving transformation. It eliminates the predicates N_{f} and R_{f}^{i} completely.

\underline{Elimination Lemma:} In order to prove the elimination lemma we interpret N_{f} as N′_{f} and R_{f}^{i} as membership relation. This makes (27) a valid formula. <

The composition of the two transformers T_{2} (24) and Q (27) is

T_{3}:  w ⊧^{L} f(p⃗) ⇔ ∃X⃗ N′_{f}(w, X⃗) ∧ ⋀_{i} X_{i} = |p_{i}|  (28)

where X_{i} = |p_{i}| is an abbreviation for ∀v v ∈ X_{i} ⇔ v ⊧^{L} p_{i}.

The instances of (28) for ⇝ and □ in our test example are:

w ⊧^{L} (p ⇝ q) ⇔ ∃X, Y N′_{⇝} (w, X, Y) ∧ X = |p| ∧ Y = |q|  (29)
w ⊧^{L} □p ⇔ ∃X N′_{□} (w, X) ∧ X = |p|.  (30)

In (30) we recognize the standard definition of neighbourhood semantics for the modal □–operator.

(29) is the generalization of neighbourhood semantics to an implication like connective. Soundness and completeness of T_{3} together with Lemma 4.3 yields the next completeness result.

Lemma 4.5 (Completeness Lemma for Sets as Neighbourhoods) If A_{1} implies reflexivity and transitivity of ⊢^{2} and the congruence properties (17) for all connectives then for every formula φ: A_{1} entails φ iff A_{4} =^{def} T_{3}(T_{1}(A_{1})) entails T_{3}(T_{1}(φ)). <

4.2.2 Binary Neighbourhood Relations

The transformer Q is only a structural modification, more or less syntactic sugar. An alternative to Q is the transformer P. It reduces the n-ary neighbourhood relation to a binary relation and it breaks the equivalence into two implications. P is defined for all p⃗ and w as

∃x⃗:S N_{f}(w, x⃗) ∧ ⋀_{i} ∀v:W R_{f}^{i}(x_{i}, v) ⇔ φ_{i}(v, p_{i})
⇔  (31)
∃x:S′K_{f}(w, x) ∧ ⋀_{i}(∀v:W R_{f}^{i+}(x_{i}, v) ⇒ φ_{i}(v, p_{i})) ∧ (∀v:W R_{f}^{i−}(x_{i}, v) ⇒ ¬φ_{i}(v, p_{i})).

Lemma 4.6 (Soundness and Completeness of P) If (i) A_{1} implies that ⊢^{2} is reflexive and transitive and (ii) A_{1} implies the congruence properties (17) for all connectives and (iii) the transformation strategy to be applied to A_{3} is inside–out rewriting, using P as rewrite rule from left to right, then the transformation lemmas hold for P.

Proof : \underline{Extension Lemma:} To prove the extension lemma we have to define for a given interpretation ℑ an extension ℑ′ with an interpretation for the new sort S′ and the new relations K_{f} and R_{f}^{i+} such that (31) is true. For the new sort S′ we define ℑ(S′) =^{def} ℑ(W)^{n}, i.e. the set of n-tuples of worlds. For K we define (w, (x⃗)) ∈ ℑ′(K) iff (w, x⃗) ∈ ℑ(N_{f}). Finally ((x⃗), v) ∈ ℑ′(R_{f}^{i+}) iff (x_{i}, v) ∈ ℑ(R_{f}^{i}) and ((x⃗), v) ∈ ℑ′(R_{f}^{i−}) iff (x_{i}, v) ∉ ℑ(R_{f}^{i}). It is easy to show that these definitions satisfy (31). \underline{Transformation Lemma:} The transformation strategy is definitional replacement, which is an equivalence transformation. In T_{2}(T_{1}(A_{1})) the formulae all have the structure of the left hand side of (31). These formulae can be replaced by the corresponding instances of the right hand side. Equivalence transformations preserve models. \underline{Elimination Lemma:} To exhibit the elimination lemma we define for a given interpretation ℑ of the transformed system an extension ℑ′ with an interpretation for the old sort S and the old relations N and R_{f}^{i} such that (31) again becomes true. We define ℑ′(S) =^{def} 2^{ℑ(W)}, ℑ′(R_{f}^{i})=^{def} ∋ and (w, X⃗) ∈ ℑ′(N_{f}) iff X_{i} ⊇ R_{f}^{i+}(x) and X_{i} ∩ R_{f}^{i−}(x) = ∅ for some x ∈ ℑ(S′), where R_{f}^{i+}(x) =^{def} {y | (x, y) ∈ ℑ(R_{f}^{i+})}. That means, the elements of ℑ′(S) are sets of worlds and the neighbourhoods of w are all the supersets of R_{f}^{i+}–accessible worlds which do not intersect with the set of R_{f}^{i−}–accessible worlds. To show that this interpretation satisfies (31), first suppose the right hand side of (31) is true for some w and p⃗. That means there is some x with R_{f}^{i+}(x) ⊆ |p_{i}| and R_{f}^{i−}(x) ⊆ |p_{i}|^{c}, where |p_{i}| =^{def}{v | φ(v, p_{i}) is true in ℑ′}, and |p_{i}|^{c} is the complement of |p_{i}|. According to the construction of ℑ′(N_{f}), for all supersets X_{i} of |p_{i}| which do not intersect with |p_{i}|^{c}, N_{f}(w, X⃗) holds. In particular this is true for X_{i} = |p_{i}| and therefore the left hand side of (31) is also true. Now assume the left hand side of (31) holds, i.e. there is some X⃗ with N_{f}(w, X⃗) and X_{i} = |p_{i}|. From the construction of ℑ′(N_{f}) we know there is some x with K_{f}(w, x) and R_{f}^{i+}(x) ⊆ X_{i} and X_{i} ∩ R_{f}^{i−}(x) = ∅. Therefore R_{f}^{i−}(x) ⊆ |p_{i}|^{c} and thus the right hand side of (31) is also true. < Composing the transformers T_{2} and P yields the new transformer B_{1} (for ‘Binary’). For all w and p⃗:

w ⊧^{L} f(p⃗) ⇔ ∃x:S′ K_{f}(w, x) ∧ ⋀_{i}(∀v:W R_{f}^{i+}(x_{i}, v) ⇒ v ⊧^{L} p_{i}) ∧ (∀v:W R_{f}^{i−}(x_{i}, v) ⇒ ¬v ⊧^{L} p_{i}). (32)

As before, soundness and completeness of P together with Lemma 4.3 yields a further completeness result.

Lemma 4.7 (Completeness Lemma for the B_{1} Transformation) If A_{1} implies reflexivity and transitivity of ⊢^{2} and the congruence properties (17) for all connectives then for every formula φ: A_{1} entails φ iff B_{1}(T_{1}(A_{1})) entails B_{1}(T_{1}(φ)). <

The transformation B_{1} (32) is identical with a transformation of a multi–modal logic formula ⟨K_{f}⟩(⋀_{i}([R_{f}^{i+}]p_{i} ∧ [R_{f}^{i+}]¬p_{i})) using the transformer T_{6}, defined in (58) below, for a corresponding number of normal unary modal operators. That means, there is a translation

π_{1}(f(p⃗)) = ⟨K⟩(⋀_{i}([R_{f}^{i+}]π_{1}(p_{i}) ∧ [R_{f}^{i+}]¬π_{1}(p_{i})))  (33)

from the given logic L into a normal multi–modal logic. ⟨...⟩ is the parameterized ◇–operator and [...] is the parameterized □–operator. This translation is further investigated in Section 4.6.

4.3 Monotonicity Properties

The congruence properties (17) can be strengthened in many cases to monotonicity properties:

upward monotonicity:  ∀p, q p ⊢^{2} q ⇒ ∀s⃗, s′f(s⃗, p, s′) ⊢^{2} f(s⃗, q, s′)  (34)
downward monotonicity:  ∀p, q p ⊢^{2} q ⇒ ∀s⃗, s′f(s⃗, q, s′) ⊢^{2} f(s⃗, p, s′).  (35)

For example, for our test set the implication connective ⇝ is downward monotonic in the first argument and upward monotonic in the second argument and the □–operator is upward monotonic. This means,

p ⊢^{2} q ⇒ ∀s (s ⇝ p) ⊢^{2} (s ⇝ q)  (36)
p ⊢^{2} q ⇒ ∀s (q ⇝ s) ⊢^{2} (p ⇝ s)  (37)
p ⊢^{2} q ⇒ □p ⊢^{2} □q  (38)

follow from A_{1}. ((38) is the so–called MN rule.). (36) is proved in Lemma A.6, (37) is proved in Lemma A.7, and (38) is proved in Lemma A.8.

The monotonicity properties (34) and (35) are translated by T_{1} into

upward monotonicity:

(∀w:W w ⊧^{L} p ⇒ w ⊧^{L} q) ⇒ ∀s⃗, s′ ∀w:W w ⊧^{L} f(s⃗, p, s′) ⇒ w ⊧^{L} f(s⃗, q, s′)  (39)

downward monotonicity:

(∀w:W w ⊧^{L} p ⇒ w ⊧^{L} q) ⇒ ∀s⃗, s′ ∀w:W w ⊧^{L} f(s⃗, q, s′) ⇒ w ⊧^{L} f(s⃗, p, s′).  (40)

If f(p⃗, q⃗) is downward monotonic in the first arguments p⃗ and upward monotonic in the last arguments q⃗ (we shall assume this ordering of the argument positions from now on) one can prove from these two formulae for all p⃗, q⃗, w

w ⊧^{L} f(p⃗, q⃗) ⇔ ∀x⃗ ⋀_{i}(∀v:W v ⊧^{L} x_{i} ⇒ v ⊧^{L} p_{i}) ⇒ ∃y⃗ ⋀_{j}(∀v:W v ⊧^{L} y_{j} ⇒ v ⊧^{L} q_{j}) ∧ w ⊧^{L} f(x⃗, y⃗).

The proof is given in Lemma A.9 of the Appendix. This equivalence can be used as the basis for a more stronger K-transformation than T_{2}. The new transformer T_{4} is

w ⊧^{L} f(p⃗, q⃗) ⇔ ∀x⃗:S ⋀_{i}(∀v:W R_{f}^{i}(x_{i}, v) ⇒ v ⊧^{L} p_{i}) ⇒
∃y⃗:S ⋀_{j}(∀v:W R_{f}^{j}(y_{j}, v) ⇒ v ⊧^{L} q_{j}) ∧ N_{f}(w, x⃗, y⃗).  (41)

The soundness and completeness proof for this transformer is identical to the proof for T_{2} (Lemma 4.2). The instances of (41) for our test connectives are

w ⊧^{L} (p ⇝ q) ⇔ ∀x:S (∀v:W R_{⇝}^{1} (x, v) ⇒ v ⊧^{L} p) ⇒
∃y:S (∀v:W R_{⇝}^{2} (y, v) ⇒ v ⊧^{L} q) ∧ N_{⇝} (w, x, y)
w ⊧^{L} □q  ⇔ ∃y:S (∀v:W R_{□} (y, v) ⇒ v ⊧^{L} q) ∧ N_{□} (w, y).

Just as we derived variations of the neighbourhood relation for the congruence properties, we can derive the corresponding variations of the neighbourhood relation for the monotonicity properties. The variant with sets as arguments of the neighbourhood relation which corresponds to T_{3} is

T_{5}:  w ⊧^{L} f(p⃗, q⃗) ⇔ ∀X⃗ X⃗ ⊆ |p⃗| ⇒ ∃Y⃗ Y⃗ ⊆ |q⃗| ∧ N′_{f}(w, X⃗, Y⃗).  (42)

A version with binary neighbourhood relation which corresponds to B_{1} seems not possible in general. Only for connectives which are either upward monotonic or downward monotonic in all their arguments, a corresponding transformation is possible. For the upward monotonic version the K-transformation

∃y⃗:S ⋀_{i}(∀v:W R_{f}^{i}(y_{i}, v) ⇒ φ(v, q_{i})) ∧ N_{f}(w, y⃗) ⇔

∃y:S′K_{f}(w, y) ∧ ⋀_{i}(∀v:W R_{f}^{′i}(y, v) ⇒ φ(v, q_{i}))

is sounds and complete. This is because the n arguments y⃗ of N_{f} can be replaced with the one argument y of K_{f} by interpreting y as the n–tuple of the values assigend to y⃗ and by interpreting the R_{f}^{′i}–relations as projection functions which extract the i^{th} component of this n–tuple. Combined with T_{4} (41), we obtain a transformer

B_{2}^{+}: w ⊧^{L} f(p⃗) ⇔ ∃y:S′K_{f}(w, y) ∧ ⋀_{i}(∀v:W R_{f}^{′i}(y, v) ⇒ v ⊧^{L} q_{i})

which in turn gives rise to a translation

π_{2}^{+}(f(p⃗)) = ⟨K_{f}⟩(⋀_{i}[R_{f}^{′i}]π_{2}^{+}(p_{i}))  (43)

into a multi–modal logic. For the downward monotonic version the K-transformation is

∀y⃗:S ⋀_{i}(∀v:W R_{f}^{i}(x_{i}, v) ⇒ φ_{i}(v, p_{i})) ⇒ N_{f}(w, y⃗) ⇔

∀y:S′K_{f}(w, y) ⇒ ⋁_{i}(∃v:W R_{f}^{′i}(y, v) ∧ ¬φ_{i}(v, p_{i})).

The right hand side of the equivalence is the contrapositive of the left hand side. K_{f}(w, y) is interpreted this time as ¬N_{f}(w, y⃗). Again y represents the n-tuple y⃗. Combined with T_{4}, we obtain a transformer

B_{2}^{−}:  w ⊧^{L} f(p⃗) ⇔ ∀y:S′ K_{f}(w, y) ⇒ ⋁_{i}(∃v:W R_{f}^{′i}(y, v) ∧ ¬v ⊧^{L} p_{i})  (44)

which this time gives rise to a translation

π_{2}^{−}(f(p⃗)) = [K_{f}](⋁_{i} ⟨R_{f}^{′i}⟩¬π_{2}^{−}(p_{i}))

into a multi–modal logic. Finally, we obtain the completeness lemma

Lemma 4.8 (Completeness Lemma for the Monotonic Case) If (i) A_{1} implies that ⊢^{2} is reflexive and transitive, and (ii) A_{1} implies the congruence properties (17) for all connectives and the monotonicity properties for some connectives then for every formula φ: A_{1} entails φ iff A entails φ′, where A and φ′ are transformed by the strongest transformers, i.e. the transformers for monotonicity if possible, otherwise the transformer for the congruence relations. They can be mixed arbitrarily. <

4.4 Transformations Based on Stone’s Representation Theorem

The transformations we consider in this section correspond to the transition from neighbourhood semantics to standard relational Kripke semantics in modal logic. Unfortunately this transition requires the relatively strong assumption that the logic defined by A_{1} is an extension of standard propositional logic. For propositional logic it is known that its Lindenbaum algebra is a Boolean algebra, and Boolean algebras are isomorphic to fields of sets. As we shall see, this enables us to take quantifications ∀p … w ⊧^{L} p … as quantifications over sets ∀p … w ∈ p … or their characteristic predicates ∀p … p(w) … respectively. With this assumption a semantics in the usual way is obtained and many properties of the system can be simplified considerably.

Lemma 4.9 (Congruence Relation) If A_{1} entails the reflexivity and transitivity of ⊧^{L} and the congruence properties (17) hold for all connectives f then the relation p ≈ q =^{def} (A_{1} entails (p ⊢^{2} q ∧ q ⊢^{2} p)), is a congruence relation on L–terms.

Proof : ≈ is reflexive and transitive because ⊢^{2} is. It is symmetric by definition. It is a congruence relation because we assumed that the congruence properties of ⊢^{2} hold for all connectives. <

For a term s let [s] be its ≈–congruence class. L_{|≈} =^{def} {[s] | s is an L–term} is called the Lindenbaum algebra of L. If L contains propositional logic, its Lindenbaum algebra is a Boolean algebra.

Definition 4.10 (Transition to PL2) The transformation S replaces all occurrences of literals of the form w ⊧^{L} p, where p is a variable or constant symbol with a literal p(w). Quantifications ∀p … w⊧^{L} p … are turned into quantifications of the form ∀p … p(w) … and likewise for existential quantifications. <

Theorem 4.11 (Soundness and Completeness of S) If

1. A_{1} contains an axiomatization of standard propositional logic (this implies that ⊧^{L} is reflexive and transitive),

2. A_{1} entails the congruence properties (17) for all connectives f,

3. T ≠ T_{1} is any of the sound and complete transformations defined above and

4. φ is a formula with ⊢^{2} as the only predicate and whose conjunctive normal form contains at least one positive literal in each conjunct (we say φ is positive)

then, A_{1} entails φ iff S(T (T_{1}(A_{1}))) entails S(T (T_{1}(φ))).

Proof : \underline{Case 1:} A_{1} entails ∀p, q p ⊢^{2} q. Since at least one literal of φ’s conjunctive normal form is positive, i.e. it has the form s ⊢^{2} t, φ is obviously true, given A_{1}. By the previous completeness theorems, T (T_{1}(A_{1})) entails α =^{def} ∀p, q, w w ⊧^{L} p ⇒ w ⊧^{L} q, i.e. T (T_{1}(A_{1})) ⇔ T (T_{1}(A_{1})) ∧ α. Since S(α) = (∀p, q, w p(w) ⇒ q(w)) and this is a contradiction, S(T (T_{1}(A_{1}))) entails everything, in particular it entails φ. \underline{Case 2:} A_{1} is consistent with β =^{def} ∃p, q ¬(p ⊢^{2} q). Thus, A_{1} entails φ iff A_{1} ∧ β entails φ and A_{1} ∧ ¬β entails φ. The latter case is actually already considered in case 1. Therefore, w.l.o.g. we can assume that A_{1} entails β. By the completeness theorems for T we have, A_{1} entails φ iff T (T_{1}(A_{1})) entails T (T_{1}(φ)). Let A′ =^{def} T (T_{1}(A_{1})) and φ′ =^{def}T (T_{1}(φ)). We need to show, A′ entails φ′ iff S(A′) entails S(φ′). By assumption 1 and Lemma 4.9, {[p] | p is an L-term} is a Boolean algebra. We have

p ≈ q iff A_{1} entails p ⊢^{2} q ∧ q ⊢^{2} p
iff A_{2} entails ∀w:W w ⊧^{L} p ⇔ w ⊧^{L} q
iff in every interpretation ℑ of A_{2}: |p| = |q|
where |p| = {w | (w, ℑ(p)) ∈ ℑ(⊧^{L})}.

Thus, q ∈ [p] iff for every interpretation ℑ of A′, |p| = |q|. Hence, {|p| | p ∈ domain(ℑ)} is a Boolean algebra for every interpretation of A′. By Stone’s representation theorem [Sto36], every Boolean algebra is isomorphic to a field of sets. Therefore {|p| | p ∈ domain(ℑ)} is isomorphic to the powerset of some base set. Because of the assumption β the Boolean algebra contains at least two elements, the base set of the corresponding powerset is therefore not empty. Since the transformations S(A′) and S(φ′) affect only literals of the form … ⊧^{L} p, where p is a variable or constant symbol, and p occurs only as the second argument of the ⊧^{L} –predicate, there is an isomorphism between the interpretations of A′ and S(A′). By structural induction on the formulae it can be shown that this isomorphism guarantees that A′ and S(A′) entail the same theorems. <

Notice that S can turn a consistent axiomatization into an inconsistent axiomatization when A_{1} entails ∀p, q p ⊢^{2} q. This is usually an undesired phenomenon. Therefore one should check whether this formula is entailed by A_{1} or not. A model generation program like John Slaney’s FINDER can do this automatically [PS90].

There is a weaker version S′ of S. S′ replaces literals w ⊧^{L} p with w ∈ p. Since the formula ∀p, q ∀w w ∈ p ⇒ w ∈ q is consistent, whereas ∀p, q ∀w p(w) ⇒ q(w) is inconsistent, there is a slight difference between S′ and S. If A_{1} does not entail ∀p, q p ⊢^{2} q, however, these two are equivalent. In the following we shall make this assumption and use S′ and S both interchangeably.

p ⊢^{2} q is transformed by T_{1} into ∀w w ⊧^{L} p ⇒ w ⊧^{L} q, and this in turn is transformed by S′ into ∀w w ∈ p ⇒ w ∈ q which means p ⊆ q. Thus, from now on the ⊢^{2}–relation can be interpreted as subset relation. As further consequences, we need no longer the notations w ∈ |p| and |p| = |q| etc. for atomic p’s and q’s.

The |...|–function is no longer necessary. w ∈ |p| becomes w ∈ p and |p| = |q| becomes p = q, where p and q now denote sets. This allows considerable simplifications. For example, the formula T_{3}(f(p⃗)) = ∃X⃗ N′_{f}(w, X⃗) ∧ ⋀_{i} X_{i} = |p_{i}| simplifies to just N′_{f}(w, p⃗).

Example 4.12 (for Transformations with S) As a first example, suppose A_{1} contains γ =^{def} ∀p □p ⊢^{2} ¬p where ¬ is classical negation and (w ⊧ ¬p) ⇔ ¬(w ⊧ p) has been verified already.

\begin{aligned}γ′ & =^{def} & T_{3}(T_{1}(γ)) = ∀p, w (∃XN′_{□} (w, X) ∧ X = |p|) ⇒ ¬w ∈ |p|. \\ S′(γ′) & = & ∀p, w N′_{□} (w, p) ⇒ w ∉ p. \\ γ′′ & =^{def} & T_{5}(T_{1}(γ)) = ∀p, w (∃XX ⊆ |p| ∧ N′_{□} (w, X)) ⇒ ¬w ∈ |p|. \\ S(γ′′)) & = & ∀p, w (∃X(∀v v ∈ X ⇒ p(v)) ∧ N′_{□} (w, X)) ⇒ ¬p(w). \end{aligned}

This last formula is a PL2 formula which is equivalent to the PL1 formula ∀w, X ¬N′_{□} (w, X) (try the SCAN algorithm on it). Thus, under the monotonicity assumption of □ (we used T_{3}), □p ⊢^{2} ¬p enforces that no world has any neighbourhood at all, not even the empty set.

As a second example, we take the monotonicity properties (34) and (35). The composition of the transformers T_{1}, T_{3} and S translates these two formulae into:

upward monotonicity:  ∀p, q p ⊆ q ⇒ ∀s⃗, s′∀w:W N′_{f}(w, s⃗, p, s′) ⇒ N′_{f}(w, s⃗, q, s′) (45)
downward monotonicity:  ∀p, q p ⊆ q ⇒ ∀s⃗, s′∀w:W N′_{f}(w, s⃗, q, s′) ⇒ N′_{f}(w, s⃗, p, s′). (46)

Since p and q are variables, we could use again the simpler notation N(w, p) instead of ∃X N(w, X) ∧ X = |p| which these transformers initially produce. Upward monotonicity thus enforces for the neighbourhood relation closedness under supersets, and downward monotonicity enforces closedness under subsets. <

4.5 Closure Properties

In modal logic, relational possible worlds semantics can be obtained from neighbourhood semantics if the neighbourhood structure is closed under supersets and intersections. We generalize this result now for arbitrary connectives. The key formula which must hold in order to strengthen neighbourhood semantics to relational semantics in modal logic is (□q_{1} ∧ □q_{2}) ⇒ □(q_{1} ∧ q_{2}). A slightly weaker property which can be formulated without the ∧ –connective and which is sufficient for this purpose is

∀q_{1}, q_{2}, w w ⊢^{2} □q_{1} ∧ w ⊢^{2} □q_{2} ⇒ ∃s s ⊢^{2} q_{1} ∧ s ⊢^{2} q_{2} ∧ w ⊢^{2} □s.  (47)

The s replaces q_{1} ∧ q_{2} or something stronger respectively.

In line with the previous sections where we tried to find transformations eliminating particular properties of the consequence relation and connectives f, the properties we want to eliminate now, are for each upward monotonic argument position of f (to simplify notation we assume this is the last argument position):

∀p⃗, q_{1}, q_{2}, w w ⊢^{2} f(p⃗, q_{1}) ∧ w ⊢^{2} f(p⃗, q_{2}) ⇒ ∃s s ⊢^{2} q_{1} ∧ s ⊢^{2} q_{2} ∧ w ⊢^{2} f(p⃗, s)  (48)

and for each downward monotonic argument position of f (to simplify notation we assume this is the first argument position):

∀p_{1}, p_{2}, q⃗, w w ⊢^{2} f(p_{1}, q⃗′) ∧ w ⊢^{2} f(p_{2}, q⃗) ⇒ ∃s p_{1} ⊢^{2} s ∧ p_{2} ⊢^{2} s ∧ w ⊢^{2} f(s, q⃗).  (49)

The instance of (48) for the □–operator is (47). The instance of (48) for the ⇝–connective is (50) and the instance of (49) for the ⇝–connective is (51) below.

∀p, q_{1}, q_{2}, w w ⊢^{2} (p ⇝ q_{1}) ∧ w ⊢^{2} (p ⇝ q_{2}) ⇒ ∃s s ⊢^{2} q_{1} ∧ s ⊢^{2} q_{2} ∧ w ⊢^{2} (p ⇝ s)  (50)
∀p_{1}, p_{2}, q, w w ⊢^{2} (p_{1} ⇝ q) ∧ w ⊢^{2} (p_{2} ⇝ q) ⇒ ∃s p_{1} ⊢^{2} s ∧ p_{2} ⊢^{2} s ∧ w ⊢^{2} (s ⇝ q).  (51)

(50) is proved in Lemma A.10. (51) is proved in Lemma A.11 and (47) is proved in Lemma A.12 in the Appendix.

Induction on natural numbers shows that from the closure properties (48) and (49) the stronger versions with finite premises

∀q_{1}, …, q_{m}, p⃗, w (⋀_{i=1}^{m} w ⊢^{2} f(p⃗, q_{i})) ⇒ ∃s (⋀_{i=1}^{m} s ⊢^{2} q_{i}) ∧ w ⊢^{2} f(p⃗, s)  (52)
∀p_{1}, …, p_{m}, q⃗, w (⋀_{i=1}^{m} w ⊢^{2} f(p_{i}, q⃗)) ⇒ ∃s (⋀_{i=1}^{m} p_{i} ⊢^{2} s) ∧ w ⊢^{2} f(s, q⃗)  (53)

follow.

Lemma 4.13 (Finite Closure Properties of the Neighbourhood Relation) If A_{1} is an extension of propositional logic then the closure formula (52) for the k^{th} argument together with the upward monotonicity for the same argument implies closedness under finite intersections of the corresponding argument position in the neighbourhood relation. Conversely,

(53) and downward monotonicity implies closedness under finite unions.

Proof : We prove the first part. The proof for closedness under unions is analogous. Since the q_{i} and p_{i} are variables in (52), the composition of the transformers T_{1}, T_{3} and S, applied to (52) yields a formula which is equivalent to

∀q_{1}, …, q_{m}, p⃗, w ⋀_{i=1}^{m} N′_{f}(w, p⃗, q_{i}) ⇒ ∃s (⋀_{i=1}^{m} s ⊆ q_{i}) ∧ N′_{f}(w, p⃗, s).

This in turn is equivalent to

∀q_{1}, …, q_{m}, p⃗, w ⋀_{i=1}^{m} N′_{f}(w, p⃗, q_{i}) ⇒ ∃s s ⊆ ⋂_{i=1}^{m} q_{i} ∧ N′_{f}(w, p⃗, s)

and since the monotonicity formulae imply that the neighbourhood relation is closed under supersets in the ‘s-argument’ (see Example 4.12), we obtain

∀q_{1}, …, q_{m}, p⃗, w ⋀_{i=1}^{m} N′_{f}(w, p⃗, q_{i}) ⇒ N′_{f}(w, p⃗, ⋂_{i=1}^{m} q_{i}),

i.e. closedness under finite intersections. A similar transformation of (53) yields

∀p_{1}, …, p_{m}, q⃗, w ⋀_{i=1}^{m} N′_{f}(w, p_{i}, q⃗) ⇒ N′_{f}(w, ⋃_{i=1}^{m} p_{i}, q⃗).

i.e. closedness under finite unions. <

Unfortunately closedness under finite unions and intersections is not sufficient for our next transformation step. We need closedness under arbitrary intersections and unions respectively. As the lemma below shows, this can be assumed in fact, provided A_{1} consists of definite Horn clauses.

Lemma 4.14 ((52) for m = ∞) If A_{1} consists of definite Horn clauses (they have exactly one positive literal), and (52) holds for all finite m, and φ is a finite formula, then A_{1} entails φ iff A_{1} ∧ δ entails φ, where δ is (52) for m = ∞.

Proof : The ‘if’–direction is trivial. For the ‘only–if’–direction suppose A_{1} ∧ δ entails φ. It suffices to show that φ is true in all Herbrand interpretations of A_{1}. Since A_{1} consists of definite Horn clauses, this can be reduced further. It is sufficient to show that φ holds in the unique minimal Herbrand interpretation ℑ_{0}, which is the intersection of all Herbrand interpretations of A_{1}. We now construct an extension of ℑ_{0} as a model for A_{1} ∧ δ. Let A_{0} =^{def} A_{1}. For i > 0, we construct ℑ_{i} and A_{i} as follows. For each term w and set {p_{1}, …, p_{∞}} of terms for which the premise of δ holds in ℑ_{i−1}, but the conclusion does not hold, we create a new constant symbol s and add the corresponding conclusion literals of δ to A_{i−1}. A_{i} is the result of this extension. ℑ_{i} is the minimal Herbrand interpretation of A_{i}. ℑ_{i} is a superset of ℑ_{i−1}. Now let A =^{def} ⋃ A_{i} and ℑ =^{def} ⋃ ℑ_{i}. A consists of A_{1} and infinitely many additional unit clauses. ℑ is the minimal Herbrand model of A and by construction, ℑ satisfies (52). Therefore A entails δ. Since A also contains A_{1}, A entails φ. Because of the compactness of PL1, a finite subset of A′ of A already entails φ. Suppose A′ contains some of the additional unit clauses s ⊢^{2} q_{i} or w ⊢^{2} f(p⃗, s) for some of the newly created constant symbols s. Since A_{1} implies (52) for all finite m, there is also a term s′ such that s′ ⊢^{2} q_{i} and w ⊢^{2} f(p⃗, s′) is entailed by A_{1}. s does not occur in φ. Therefore the clauses with s can be replaced with the corresponding clauses with s′. In other words, a subset A′ of A_{1} is sufficient to derive φ, and that’s what we set out to show. <

Analogously we can show that (53) for m = ∞ can be assumed either. As a corollary of the above lemma and the Lemma 4.13 we get:

Corollary 4.15 (Closure Properties of the Neighbourhood Relation) If A_{1} satisfies all the conditions of Theorem 4.11 and additionally A_{1} consists of definite Horn clauses and (48) holds for the upward monotonic argument positions and (49) holds for the downward monotonic argument positions of f then closedness under arbitrary intersections, and closedness under arbitrary unions, respectively, holds:

\begin{matrix}(⋀_{i∈I} N′_{f}(w, X⃗, Y_{i})) ⇒ N′_{f}(w, X⃗, ⋂_{i∈I} Y_{i}) \\ (⋀_{i∈I} N′_{f}(w, X_{i}, Y⃗)) ⇒ N′_{f}(w, ⋃_{i∈I} X_{i}, Y⃗). \end{matrix}

<

Unfortunately for the proof we used that A_{1} consists of definite Horn clauses. It is not clear whether this is an artefact of the proof technique or whether this is necessary in general.

Lemma 4.16 (Accessibility Relation) If the neighbourhoud relation N′ is serial for at least one argument position, for example ∀w, X⃗ ∃Y N′(w, X⃗, Y) holds, and N′ is closed under subsets and union in the first group of arguments and closed under supersets and intersections in the last group of arguments in the sense of Corollary 4.15, then there exists a relation R on worlds with

N′(w, X⃗, Y⃗) ⇔ ∀x⃗, y⃗ R(w, x⃗, y⃗) ⇒ (⋀_{i} x_{i} ∈ X_{i}) ⇒ (⋁_{j} y_{j} ∈ Y_{j}).  (54)

Proof : For the first part of the proof we assume the serial argument position of N′ is one where N′ is upward monotonic and hence closed under intersections. W.l.o.g. let this be the last argument position. We split N′s arguments into N′(w, x⃗, y′, y) where x⃗ denotes the downward monotonic argument positions and all others are upward monotonic. All but the last argument position may be empty. y⃗ abbreviates ‘y′, y’. For a world w and sets X⃗, Y⃗′ we define the intersection of all neighbourhoods:

⊓ (w, X⃗, Y⃗′) =^{def} ⋂_{Y} N′(w, X⃗, Y⃗′, Y).  (55)

Since N′ is serial, the range of the intersection is not empty. Closedness under intersections for the downward monotonic argument positions means for all w, X⃗, Y⃗′

N′(w, X⃗, Y⃗′, ⊓(w, X⃗, Y⃗′)).  (56)

Notice that, (56) is false if N′ is not serial. In this case ⊓(w, X⃗, Y⃗′) is the set of all worlds, but this is not neccessarily a neighbourhood. The accessibility relation R is now defined as

R(w, x⃗, y⃗) ⇔ y ∈ ⊓(w, {x⃗}, {y′}^{c}).  (57)

Recall {y}^{c} denotes the complement of the set {y}. \underline{⇒ part of (54)}. Suppose N′(w, X⃗, Y⃗′, Y) is true and ∀x⃗, y⃗ R(w, x⃗, y′, y) ⇒ (⋀_{i} x_{i} ∈ X_{i}) ⇒ (⋁_{j} y_{j} ∈ Y′_{j} ∨ y ∈ Y) is false. That means the following facts are assumed for some w, X⃗, Y⃗′, Y, a⃗, b⃗′, b

(a) N′(w, X⃗, Y⃗′, Y)

(b) R(w, a⃗, b⃗′, b)

(c) a_{i} ∈ X_{i} for the downward monotonic arguments

(d) b_{i} ∉ Y′_{i} for the first upward monotonic arguments

(e) b ∉ Y for the last upward monotonic argument

≻ (f) b ∈ ⊓(w, {a⃗}, {b⃗′}^{c}) (b) and (57) ≻ (g) N′({a⃗}, {b⃗′}^{c}, ⊓(w, {a⃗}, {b⃗′}^{c}) (f) and (56)

(h) N′({a⃗}, Y⃗′, Y) (a), (c) and downward monotonicity

(i) Y⃗′ ⊆ {b⃗′}^{c} from (d) ≻ (j) N′({a⃗}, {b⃗′}^{c}, Y) (h), (i) and upward monotonicity

(k) ⊓(w, {a⃗}, {b⃗′}^{c}) ⊆ Y (g), (j) and (55) ≻ contradiction with (e) and (f).

≻  The ⇒ part of (54) holds.  ‘≻ ’ denotes ‘this implies’.

\underline{⇐ part of (54)}. Suppose ∀x⃗, y′, y R(w, x⃗, y′, y) ⇒ (⋀_{i} x_{i} ∈ X_{i}) ⇒ (⋁_{j} y′_{j} ∈ Y′_{j} ∨ y ∈ Y) is true. ≻ ∀x⃗, y′, y y ∈ ⊓(w, {x⃗}, {y′}^{c}) ⇒ (y ∈ Y ∨ ¬(⋀_{i} x_{i} ∈ X_{i}) ∨ ⋁_{j} y′_{j} ∈ Y′_{j})) (57) ≻ ∀x⃗, y′ ((⋀_{i} x_{i} ∈ X_{i}) ∧ (⋀_{j} y′_{j} ∉ Y′_{j})) ⇒ ⊓ (w, {x⃗}, {y⃗}^{′c}) ⊆ Y (logic and set theory) ≻ ∀x⃗, y′ ((⋀_{i} x_{i} ∈ X_{i}) ∧ (⋀_{j} y′_{j} ∉ Y′_{j})) ⇒ N′(w, {x⃗}, {y′}^{c}, Y) (56) and (upward monotonicity) ≻ ∀y′ (⋀_{j} y′_{j} ∉ Y′_{j}) ⇒ N′(w, X⃗, {y′}^{c}, Y) (closedness under unions) ≻ N′(w, X⃗, Y⃗′, Y) (closedness under intersections) ≻ The ⇐ part of (54) holds.

If the argument position where N′ is serial is not upward monotonic, but downward monotonic, there is a proof for the lemma which is just dual to the proof given above. Instead of intersections, use the union of all neighbourhoods. Therefore we do not give the proof here. <

Seriality of the neighbourhood relation is one of the conditions in the previous lemma. The next lemma shows how this can be proved by alternatively proving an appropriate lemma from A_{1}.

Lemma 4.17 (Seriality of the Neighbourhood Relation) If A_{1} satisfies the conditions of Theorem 4.11 and the formula ∀w ∀p⃗ ∃q w ⊢^{2} f(p⃗, q) is provable from A_{1} then the neighbourhood relation is serial in the last argument. Proof : Since p and q are variables, this formula can be translated directly into ∀w ∀p⃗ ∃q N′_{f}(w, p⃗, q).

<

Seriality for other argument positions are proved analogously. For our test connectives we prove ∀w, p ∃q w ⊢^{2} p ⇝ q in Lemma A.13 and ∀w∃q w ⊢^{2} □q in Lemma A.14.

Now we are ready to define a transformer that eliminates the closure properties.

Lemma 4.18 (Transformer for Closure Properties) If A_{1} satisfies the conditions of Theorem 4.11 and Lemmas 4.13 and 4.17 for some connective f then the following transformer

T_{6}:  w ⊧^{L} f(p⃗, q⃗) ⇔ ∀x⃗, y⃗ R_{f}(w, x⃗, y⃗) ⇒ (⋀_{i} x_{i} ⊧^{L} p_{i}) ⇒ (⋁_{j} y_{j} ⊧^{L} q_{j})  (58)

is sound and complete for A_{2}.

Proof : \underline{Extension Lemma}: Soundness and completeness of the transformer T_{3} implies that there is an extension of a model for A_{2} which satisfies (28): w ⊧^{L} f(p⃗) ⇔ ∃X⃗ N′_{f}(w, X⃗) ∧ ⋀_{i} X_{i} = |p_{i}|. In this model w ⊧^{L} f(p⃗) ⇔ N′_{f}(w, |p⃗|) holds. But according to Lemma 4.16, N′_{f}(w, |p⃗|) is equivalent to the right hand side of (58). The other lemmas are proved as in Lemma (4.2). <

The instances of T_{6} for our test connectives are:

w ⊧^{L} (p ⇝ q) ⇔ ∀x, y R_{⇝} (w, x, y) ⇒ (x ⊧^{L} p ⇒ y ⊧^{L} q)  (59)
w ⊧^{L} □q ⇔ ∀y R_{□} (w, y) ⇒ y ⊧^{L} q  (60)

and we recongize the standard relational semantics for the □–operator. If we had axiomatized the □–operator with the classical implication connective → instead of ⇝, then the transformer (60) together with T_{1} would turn the two axioms (14) and (15) for the □–operator into tautologies and we had found an optimal semantics for □. In order to obtain this result also for our axiomatization, we need to show that ⇝ is equivalent to →. Therefore we continue the investigation of the ⇝– connective in In Section 4.7.

For ∧ –like connectives, the seriality condition cannot be proved, because ∀w, p ∃q w ⊢^{2}(p ∧ q) is certainly not a theorem. In this case there is no semantics in terms of the accessibility relation as above. Usually, however, ∧ –like connectives are defined connectives. If it is for example defined as (p&q) ⇔ ¬(p ⇝ ¬q) then the semantics for ⇝ can be used to define the semantics for &:

w ⊧^{L} (p&q) ⇔ ∃x, y R_{⇝} (w, x, y) ∧ x ⊧^{L} p ∧ y ⊧^{L} q

Theorem 4.19 (Soundness and Completeness of the Transformation) If A_{1} satisfies all the conditions of 4.18 and φ is a positive formula (see 4.11) then A_{1} entails φ iff T (T_{1}(A_{1})) entails T (T_{1}(φ)) where T is the strongest admissible transformer. <

4.6 Binary Accessibility Relations

As we have seen in Lemma 4.18, n–place connectives correspond to n+1–ary accessibility relations. It is well known that m–place relations can be decomposed into m + 1 binary relations. This trick can be used to find a translation into normal multi–modal systems. To this end we define a further K-transformation. For all p⃗, q⃗, w:

∀x⃗, y⃗:W R(w, x⃗, y⃗) ⇒ ((⋀_{i} φ_{i}(x_{i}, p_{i})) ⇒ (⋁_{j} φ_{j}(y_{j}, q_{j})) ⇔  (61)

∀z:S′ K(w, z) ⇒ ((⋀_{i} ∃x_{i}:W R_{i}(z, x_{i}) ∧ φ_{i}(x_{i}, p_{i})) ⇒

(⋁_{j} ∀y_{j}:W R_{j}(z, y_{j}) ⇒ φ_{j}(y_{j}, q_{j})).

Lemma 4.20 (Soundness and Completeness of (61)) The transformation lemmas hold for the K-transformation (61), if we use as transformation strategy inside–out rewriting, applying (61) from left to right on formulae which are the result of a transformation using T_{6}.

Proof : \underline{Extension Lemma:} We have to show that every interpretation ℑ for the accessibility relation R can be extended to an interpretation ℑ′ satisfying (61). We interpret the sort S′ as the set of n–tuples of worlds and the predicates R_{k} as the k^{th} projection function for these n–tuples. This interpretation satisfies (61). \underline{Transformation Lemma:} The results of a transformation with T_{6} are just formulae with the same structure as (61)’s left hand side. Therefore the transformation is an equivalence transformation. \underline{Elimination Lemma:} We have to show that every interpretation ℑ for the transformed system can be extended to an interpretation ℑ′ satisfying (61). We define R as follows

R(w, x⃗, y⃗) ⇔ ∃z K(w, z) ∧ ⋀_{i} R_{i}(z, x_{i}) ∧ ⋀_{j} R_{j}(z, x_{j}).

This implies ∀x⃗, y⃗ R(w, x⃗, y⃗) ⇒ ((⋀_{i} φ_{i}(x_{i}, p_{i})) ⇒ (⋁_{j} φ_{j}(y_{j}, q_{j})) ⇔ ∀x⃗, y⃗ (∃z K(w, z) ∧ ⋀_{i} R_{i}(z, x_{i}) ∧ ⋀_{j} R_{j}(z, x_{j})) ⇒ ((⋀_{i} φ_{i}(x_{i}, p_{i})) ⇒ (⋁_{j} φ_{j}(y_{j}, q_{j})) ⇔ ∀z K(w, z) ⇒ x⃗, y⃗ ⋀_{i} R_{i}(z, x_{i}) ∧ ⋀_{j} R_{j}(z, x_{j})) ⇒ ((⋀_{i} φ_{i}(x_{i}, p_{i})) ⇒ (⋁_{j} φ_{j}(y_{j}, q_{j})) ⇔ ∀z K(w, z) ⇒ (⋁_{i} ∀x_{i} ¬R_{i}(z, x_{i}) ∨ φ_{i}(x_{i}, p_{i})) ∨ (⋁_{j} ¬R_{j}(z, x_{j}) ∨ φ_{j}(y_{j}, q_{j})) ⇔ ∀z K(w, z) ⇒ ((⋀_{i} ∃x_{i} R_{i}(z, x_{i}) ∧ φ_{i}(x_{i}, p_{i})) ⇒ (⋁_{j} ∀y_{j} R_{j}(z, y_{j}) ⇒ φ_{j}(y_{j}, q_{j})). <

The composition of T_{6} with the transformer (61) is

B_{3}  w ⊧^{L} f(p⃗, q⃗) ⇔ ∀z:S′ K(w, z) ⇒ ((⋀_{i} ∃x_{i}:W R_{i}(z, x_{i}) ∧ φ_{i}(x_{i}, p_{i})) ⇒
(⋁_{j} ∀y_{j}:W R_{j}(z, y_{j}) ⇒ φ_{j}(y_{j}, q_{j})).  (62)

This in turn corresponds to a translation function π_{3} which maps n-place connectives to modal operators:

π_{3}(f(p⃗, q⃗)) = [K]((⋀_{i} ⟨R_{i}⟩π_{3}(p_{i})) ⇒ ⋁_{j}[R_{j}]π_{3}(q_{j})).  (63)

At different places we have defined translations π_{i} into the language of multi–modal logic. But there is a very subtle point to be discussed here. The transformers B_{1}, B_{2}^{+}, B_{2}^{−} and B_{3} introduce a new sort S′. That means the worlds are split into two different kinds, worlds of sort W and worlds of sort S′. The outermost quantification of T_{1}(φ), however, quantifies over the sort W. Therefore the frame conditions specified by φ don’t hold for all worlds, but only for the worlds of sort W.

To see what this means, suppose as an example, φ = □p⊢^{2}p. Let us assume strong neighbourhood semantics. Quantifier elimination of S(B_{2}^{+}(T_{1}(φ))) yields ∀w:W ∀v:S′ K(w, v) ⇒ R(v, w). This is the frame property corresponding to φ. Now consider φ′ =^{def} π_{2}^{+}(φ) = ⟨K⟩[R]p ⊢^{2} p. Quantifier elimination of S(T_{6}(T_{1}(φ′))) yields ∀w, v:W K(w, v) ⇒ R(v, w). That means, if we interpret the formula φ′ as a normal axiom schema in normal multi modal logic, we get frame conditions for all worlds whereas the original schema φ specified a frame condition only for certain worlds. Thus, the target system for the π_{i} is not standard multi modal logic, but a refined version with some more structure.

The additional structure in the semantics is the separation into two different sets of worlds. The accessibility relations K lead from the W –type worlds to the S′–type worlds and vice versa for the R–relations. The additional structure on the syntactic side is an invariant on the nesting sequence of the modal operators. All translations π_{i} yield K–type operators followed by R–type operators which are again followed by K–type operators etc. Formulae like [K][K] … or [R][R] … do not occur. Therefore we can classify the formulae as K–type formula if the top–level operators are K–type connectives operating on R–type formulae. Analogously, R–type formulae have top–level operators of R–type operating on K–type formulae. Pure classical propositional formulae fall into both sets. K–type formulae are to be interpreted only at W –type worlds and R–type formulae are to be interpreted at S′–type worlds.

I omit giving a formal definition because I think the structure is simple. What is important, however, is that the axiomatization of this logic with K-axiom and Necessitation rules for each of these operators needs to be modified also. For the K–type operators, K-axiom and Necessitation rule are defined only for R–type formulae, and vice versa for the R–type operators. For example, the p’s and q’s in the K-axiom [K](p ⇒ q) ⊢ ([K]p ⇒ [K]q) for the K–type operator must be R– type formulae, otherwise the syntactic structure does not match the semantics. Let us call this logic a separated multi modal logic.

Exploiting soundness and completeness of T_{6} we can now prove soundness and completeness of these translations into separated multi–modal logic.

Theorem 4.21 (Translation into Multi–Modal Logic: Soundness and Completeness) The translations π_{1}, π_{2}^{+}, π_{2}^{−} and π_{3} (defined in (33), (43), (44) and (63)) to the separated multi modal logic are sound and complete.

Proof : Let T′_{6} be the instance of T_{6} for the appropriate number of parameterized modal operators. For K–type operators, T′_{6} quantifies over worlds of sort W and for R–type operators, T′_{6} quantifies over worlds of sort S. By the definition of the π_{i}, π_{1} ∘ T_{1} ∘ T′_{6} = T_{1} ∘ B_{1}, holds π_{2}^{+} ∘ T_{1} ∘ T′_{6} = T_{1} ∘ B_{2}^{+},holds π_{2}^{−} ∘ T_{1} ∘ T′_{6} = T_{1} ∘ B_{2}^{−} holds and also π_{3} ∘ T_{1} ∘ T′_{6} = T_{1} ∘ B_{3} holds, where ∘ denotes composition. Let (π, B) be one of these four pairs of transformers. If K is the set of K-axioms and N is the set of Necessitation rules for the different modal operators then soundness and completeness (s&c) of the transformers B and T′_{6} allow us to prove

A_{1} ⇒ φ

iff B(T_{1}(A_{1})) ⇒ B(T_{1}(φ))  (s&c) of T_{1} and B
iff T′_{6}(T_{1}(π(A_{1}))) ⇒ T′_{6}(T_{1}(π(φ)))  above equations
iff T′_{6}(T_{1}(K) ∧ T_{1}(N) ∧ T_{1}(π(A_{1}))) ⇒ T′_{6}(T_{1}(π(φ))) T′_{6}(T_{1}(K) ∧ T_{1}(N)) = true
iff T_{1}(K) ∧ T_{1}(N) ∧ T_{1}(π(A_{1})) ⇒ T_{1}(π(φ))  (s&c) of T′_{6}
iff K ∧ N ∧ π(A_{1}) ⇒ π(φ)  (s&c) of T_{1}.
<

Usually the direct B–transformations using binary accessibility relations is sufficient, and we need not take a detour via multi modal logic. Therefore I have not investigated the difference between this kind of separated multi modal logic, introduced above and the standard multi modal logic. I conjecture that there is no significant difference as long as the syntactic invariant of the nested K–type and R–type formulae is guaranteed. Direct translations for modal logic with neighbourhood semantics into normal bi- or tri-modal logic respectively have been investigated by Olivier Gasquet and Andreas Herzig [GH93a, GH93b]. It turnes out that it is extremely complicated to extend the frame properties from the worlds of sort W to all worlds. There is no general scheme and each frame property has to be treated individually.

4.7 Truth Value Semantics

For a connective f with a semantics defined in terms of the accessibility relation we can prove that f is actually a classical connective by proving that the accessibility relation collapses to a point relation.

A point relation is one where general reflexivity ∀x R(x, …, x) holds and all arguments of R ‘collapse’ in the following sense: ∀x⃗ R(x⃗) ⇒ ⋀_{i,j} x_{i} = x_{j} holds.

For our test connective ⇝ we can actually prove these properties. In order to illustrate how the translation, quantifier elimination and theorem proving techniques work together, we list all the details. First, the two axioms (12) and (13), namely

\begin{matrix}∀p, q, r, s & ((p ⇝ q) ⇝ r) ⊢^{2} ((r ⇝ p) ⇝ (s ⇝ p)) \\ ∀p, q, r, s & p ⊢^{2} q ∧ (p ⇝ q) ⊢^{2} (r ⇝ s) ⇒ r ⊢^{2} s, \end{matrix}

can be translated with a composition of the transformers T_{1},T_{6} and S. This is simple rewriting. The results are: ∀w (∀u, v R(w, u, v) ⇒ ((∀x, y R(u, x, y) ⇒ (p(x) ⇒ q(y))) ⇒ r(v)))

⇒ (∀a, b R(w, a, b) ⇒ ((∀x, y R(a, x, y) ⇒ (r(x) ⇒ p(y))) ⇒ (∀c, d R(b, c, d) ⇒ (s(c) ⇒ p(d))))) and ((∀w p(w) ⇒ q(w)) ∧ (∀w (∀u, v (R(w, u, v) ⇒ p(u) ⇒ q(v))) ⇒ (∀u, v R(w, u, v) ⇒ (r(u) ⇒ s(v)))))

⇒ (∀w r(w) ⇒ s(w)).

All predicates except R are universally quantified. To simplify the formulae we apply the quantifier elimination algorithm SCAN. First we negate the formulae in order to get existentential quantifications. The negation is clausified, all existentially quantified predicates are resolved away, the quantifiers are reconstructed and the formula is negated again. Lets start with the first formula. Its negation is ∃w (∀u, v R(w, u, v) ⇒ ((∀x, y R(u, x, y) ⇒ (p(x) ⇒ q(y))) ⇒ r(v)))

∧ (∃a, b R(w, a, b) ∧ (∀x, y R(a, x, y) ⇒ (r(x) ⇒ p(y))) ∧ (∃c, d R(b, c, d) ∧ s(c) ∧ ¬p(d))).

The clause form is

C_{1} ¬R(w, u, v), R(u, f(u, v), g(u, v)), r(v) C_{2} ¬R(w, u, v), p(f(u, v)), r(v) C_{3} ¬R(w, u, v), ¬q(g(u, v)), r(v) C_{4} R(w, a, b) C_{5} ¬R(a, x, y), ¬r(x), p(y)

C_{6} R(b, c, d) C_{7} s(c) u, v, x, y are variables. C_{8} ¬p(d) all other symbols are Skolem constants or functions.

The result of resolving p, q, r, s away is

C′_{1} ¬R(w, u, v), R(u, f(u, v), g(u, v)), ¬R(a, v, d) C′_{2} ¬R(w, u, v), f(u, v) ≠ d, ¬R(a, v, d) C_{4} R(w, a, b) C_{6} R(b, c, d).

The quantifier prefix is reconstructed. f and g become existentially quantified variables again. The resulting formula is

∃w, a, b, c, d ∀u, v ∃x, y R(w, a, b) ∧ R(b, c, d) ∧ (¬R(w, u, v) ∨ ¬R(a, v, d) ∨ (R(u, x, y) ∧ x ≠ d) To obtain the final result, this formula is negated.

∀w, a, b, c, d (R(w, a, b) ∧ R(b, c, d)) ⇒ ∃u, v R(w, u, v) ∧ R(a, v, d) ∧ ∀x, y R(u, x, y) ⇒ x = d.

(64)

That means in relational possible worlds semantics the Łukasiewics axiom (12) corresponds to the property (64) of the accessibility relation. Now lets turn to the second formula. Its negation is ((∀w p(w) ⇒ q(w)) ∧ ∀w (∀u, v R(w, u, v) ⇒ (p(u) ⇒ q(v))) ⇒ (∀u, v R(w, u, v) ⇒ (r(u) ⇒ s(v))))

∧ (∃w r(w) ∧ ¬s(w)). The clause form is

C_{1} ¬p(w), q(w) C_{2} R(w, f(w), g(w)), ¬R(w, x, y), ¬r(x), s(y) C_{3} p(f(w)), ¬R(w, x, y), ¬r(x), s(y) C_{4} ¬q(g(w)), ¬R(w, x, y), ¬r(x), s(y) C_{5} r(a) w, x, y are variables. C_{6} ¬s(a) f, g, a are Skolem symbols.

The result of resolving p, q, r, s away is

C′_{2} R(w, f(w), g(w)), ¬R(w, a, a) C′_{3} f(w) ≠ g(w), ¬R(w, a, a).

The quantifier prefix is reconstructed. f and g become existentially quantified variables. The resulting formula is ∃a ∀w ∃u, v ¬R(w, a, a) ∨ (R(w, u, v) ∧ u = v). Negating this formula, we obtain the final result

∀a ∃w R(w, a, a) ∧ ∀u, v R(w, u, v) ⇒ u = v.  (65)

That means in relational possible worlds semantics our version of Modus Ponens (13) corresponds to the property (65) of the accessibility relation.

From the two translated axioms (64) and (65), the three lemmas ∀x R(x, x, x) and ∀w, u, v R(w, u, v) ⇒ w = u and ∀w, u, v R(w, u, v) ⇒ u = v follow, which shows that R collapses to a point relation. The proofs were found with the Otter theorem prover. They are listed in A.15 in the Appendix. The transformer

w ⊧^{L} (p ⇝ q) ⇔ ∀x, y R_{⇝} (w, x, y) ⇒ (x ⊧^{L} p ⇒ y ⊧^{L} q) now simplifies to

w ⊧^{L} (p ⇝ q) ⇔ (w ⊧^{L} p ⇒ w ⊧^{L} q) which proves the equivalence between ⇝ and ⇒.

5 The Semantics Generation Procedure

We collect the results of the previous section and define a procedure for developing the semantics for the given non–classical operators.

We start with an arbitrary formula set A_{1} containing the ⊢^{2}–predicate. Naturally A_{1} should be consistent, otherwise the following steps have no meaning.

\underline{Step 1} Prove that ⊢^{2} is reflexive and transitive.

\underline{Step 2} Prove the congruence properties, (17) for all connectives. If there are connectives where this is not possible, the logic is outside the scope of the current theory. If the congruence properties hold for all connectives and ⊢^{2} is the only predicate in A_{1}, and all formula variables are universally quantified then any of the transformers T_{2} (24), T_{3} (28) or B_{1} (32) defines a sound and complete semantics.

\underline{Step 3} Try proving for each connective f the monotonicity properties (34) and (35) from A_{1}. In this step we determine for each argument position of f, whether it is upward or downward monotonic. We assume that each argument position is monotonic. If some but not all argument positions are monotonic, or one argument position is both upward and downward monotonic, there is a straightforward extension of our theory which can deal with this (we leave it to the reader to show this).

The actual semantics is now determined by one of the transformers T_{4} (41), T_{5}(42), B_{2}^{+} (43) or B_{2}^{−} (44) respectively, for each monotonic connective, and one of the previous transformers for the non–monotonic connectives. All can be mixed freely.

\underline{Step 4} Check whether A_{1} contains an axiomatization of standard propositional logic. Find a model for A_{1} ∧ (∃p, q ¬(p ⊢^{2} q)) to ensure that the next transformations do not produce inconsistencies. If both conditions are fulfilled, one can simplify the previously transformed axioms A by applying the transformer S which replaces literals v ⊧^{L} p in A with p(v) and trying the quantifier elimination algorithm on these PL2 formulae. Notice that this is an optional simplification step. If the quantifier elimination algorithm does not compute an equivalent first–order formula, then the original translated first–order formula A is the final result of the transformation. In this way we can also deal with so–called incomplete systems.

\underline{Step 5} If the conditions of the previous step are fulfilled and A_{1} consists of definite Horn clauses only, then check for the closure properties. For the connectives which are either upward or downward monotonic for each argument position, try proving (48) for each upward monotonic argument position and (49) for each downward monotonic argument position. If this is successful then the transformer T_{6} (58) yields the classical relational possible worlds semantics. Translate A_{1} again using the strongest possible transformer for each connective. As in the previous step, these translated axioms can be simplified using the transformer S and quantifier elimination.

Notice that this step and the corresponding completeness proof subsumes the Sahlquist technique frequently used in modal logic to get frame properties from Hilbert axioms [Sah75, vB83].

\underline{Step 6} For connectives with relational semantics (the previous step was successful) try proving that the accessibility relation collapses to a point relation (see Section 4.7). If this is provable then the connective has a standard truth value semantics.

The completeness lemmas guarantee that a (positive) theorem can be proved from the original Hilbert axioms A_{1} if and only if the translated theorem can be proved from the resulting translated axiom system.

6 Summary

I have presented an alternative way for developing model theoretic semantics from an axiomatic specification of non–classical propositional logics. The semantics is represented as syntactic transformation rules. These transformation rules are derived from particular theorems of the original system and they translate these theorems into tautologies. Reflexivity and transitivity of a binary consequence relation yields the basic possible worlds framework. The congruence properties of the connectives yield weak neighbourhood semantics. The monotonicity properties yield a stronger neighbourhood semantics. The closure properties yield relational possible worlds semantics for the connectives.

Propositional logic as basis of the specification allows us to turn those parts which are not eliminated into second–order predicate logic formulae. In many cases these formulae can be simplified to a first–order predicate logic formula which describes the corresponding frame property. As a consequence, the correspondence problem reduces to a quantifier elimination problem which can be solved with a quantifier elimination algorithm like SCAN. All transformations preserve satisfiability and unsatisfiability. This is sufficient for the soundness and completeness of the generated semantics.

Sometimes there are alternative transformations for the same property. For example the transformations which produce neighbourhood semantics may define a neighbourhood relation between worlds or a neighbourhood relation between a world and sets of worlds. Moreover, one can define transformations which produce for n–place connectives only binary accessibility relations. We have shown how these transformation can be turned into a translation from the original logic into multi–modal logic.

With PL1 theorem provers, quantifier elimination algorithms and model finders, all steps of the transformation process can be automated.

This work can be extended in various directions. For example, one can try to find transformations for other properties than the ones considered in this paper. The starting point for our method were the congruence properties of the connectives. There are, however, quite interesting and useful connectives which do not have the congruence properties and for which our method does not work. An example is Fagin and Halpern’s awareness operator [FH88].

In order to apply Stone’s representation theorem we need to have a propositional logic as basis. It should be investigated whether some of the representation theorems for weaker structures than Boolean algebras can be exploited to investigate extensions of intuitionistic or relevance logics. Of particular interest are of course logics with quantifiers. It is not clear how quantifiers fit into our framework.

Although in this paper we investigated only specifications of logics, the ideas and techniques used are independent of this particular application. There might be other areas where similar manipulations of logical specifications also yield interesting results. In particular, the area of representation theorems for algebraic systems is related to this work. For example Jónsson and Tarski’s representation theorem for Boolean algebras with operators [JT51, JT52] gives an alternative completeness theorem for relational possible worlds semantics. Transferring the ideas and methods developed in this paper to algebraic logic and to general algebra seems promising.

References

[Ack35a] Wilhelm Ackermann. Untersuchung über das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110:390–413, 1935.

[Ack35b] Wilhelm Ackermann. Zum Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 111:61–63, 1935.

[Ack54] Wilhelm Ackermann. Solvable Cases of the Decision Problem. North–Holland Pu. Co., 1954.

[BG90] Leo Bachmair and Harald Ganzinger. On restrictions of ordered paramodulation with simplification. In CADE-10: 10th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, pages 427–441, Kaiserslautern, FRG, 1990. Springer-Verlag. Copy filed.

[BGW92] Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Theorem proving for hierarchic first-order theories. In G. Levi and H. Kirchner, editors, Algebraic and Logic Programming, Third International Conference, pages 420–434. Springer-Verlag, LNCS 632, September 1992.

[Che80] B. F. Chellas. Modal Logic: An Introduction. Cambridge University Press, Cambridge, 1980.

[FH88] Ronald Fagin and Joseph Halpern. Belief, awareness, and limited reasoning. Artificial Intelligence, 34:39–76, 1988.

[GH93a] Olivier Gasquet and Andreas Herzig. Translating inaccessible worlds logic into bimodal logic. In Michael Clarke, Rudolf Kruse, and Serafín Moral, editors, Symbolic and Quantitative Approaches to Reasoning and Uncertainty, Proceedings of ECSQARU ’93, Granada, Spain, Nov. 1993, volume 747 of LNCS, pages 145–150, Granada, Spain, 8–10 November 1993.

[GH93b] Olivier Gasquet and Andreas Herzig. Translating non-normal modal logics into normal modal logics. In I. J. Jones and M. Sergot, editors, Proc. of International Workshop on Deontic Logic in Computer Science (DEON–94), TANO, Oslo, December 1993.

[GO92a] Dov M. Gabbay and Hans Jürgen Ohlbach. Quantifier elimination in second–order predicate logic. South African Computer Journal, 7:35–43, July 1992. also published in [GO92b].

[GO92b] Dov M. Gabbay and Hans Jürgen Ohlbach. Quantifier elimination in second–order predicate logic. In Bernhard Nebel, Charles Rich, and William Swartout, editors, Principles of Knowledge Representation and Reasoning (KR92), pages 425–435. Morgan Kaufmann, 1992. also published as a technical report MPI-I-92-231 of the Max-Planck-Institut für Informatik, Saarbrücken and in the South African Computer Journal, 1992.

[JT51] B. Jónsson and A. Tarski. Boolean algebras with operators, Part I. American Journal of Mathematics, 73:891–939, 1951.

[JT52] B. Jónsson and A. Tarski. Boolean algebras with operators, Part II. American Journal of Mathematics, 74:127–162, 1952.

[Kri59] S. A. Kripke. A completeness theorem in modal logic. Journal of Symbolic Logic, 24:1– 14, 1959.

[Kri63] S. A. Kripke. Semantical analysis of modal logic i, normal propositional calculi. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 9:67–96, 1963.

[Łuk70] J. Łukasiewicz. Selected Works. North Holland, 1970. Edited by L. Borkowski.

[McC89] William W. McCune. OTTER User’s Guide. Mathematical and Computer Science Devision, Argonne National Laboratory, april 1989.

[McC90] William McCune. Otter 2.0. In Mark Stickel, editor, Proc. of 10^{th} Internation Conference on Automated Deduction, LNAI 449, pages 663–664. Springer Verlag, 1990.

[OGP94] Hans Jürgen Ohlbach, Dov Gabbay, and David Plaisted. Killer transformations. Technical Report MPI-I-94-226, Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1994. To be published in Proc. of the 1993 Workshop on Proof Theory in Modal Logic, Hamburg.

[PS90] P. Pritchard and J. Slaney. Computing models of propositional logics. In 10th International Conference on Automated Deduction, CADE-10, LNCS 449, page 685. Springer Verlag, 1990.

[Sah75] H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logics. In S. Kanger, editor, Proceedings of the 3rd Scandinavian Logic Symposium, 1973, pages 110–143, Amsterdam, 1975. North Holland.

[Sim94] Harold Simmons. The monotonous elimination of predicate variables. Journal of Logic and Computation, 4(1), 1994.

[Sto36] M. H. Stone. The theory of representations for boolean algebras. Transactions of American Mathematical Society, 40:37–111, 1936.

[Sza92] Andrzej Szałas. On correspondence between modal and classical logic: Automated approach. Technical Report MPI–I–92–209, Max-Planck-Institut für Informatik, Saarbrücken, March 1992.

[vB83] Johan van Benthem. The Logic of Time. Reidel, Kluwer Academic Publishers, Dordrecht, 1983.

[vB84] Johan van Benthem. Correspondence theory. In Gabbay Dov M and Franz Guenthner, editors, Handbook of Philosophical Logic, Vol. II, Extensions of Classical Logic, Synthese Library Vo. 165, pages 167–248. D. Reidel Publishing Company, Dordrecht, 1984.

[Wal87] Christoph Walther. A Many-Sorted Calculus Based on Resolution and Paramodulation. Research Notes in Artificial Intelligence. Pitman Ltd., London, 1987.

A Appendix: Proofs for the Test Example

We list the proofs for the key lemmas needed Section 4 for jusitfying the application of the transformations. All proofs were found by the theorem prover Otter [McC89, McC90]. The proofs of the lemmas below are almost the original output listings of Otter. Only the superfluous information has been deleted and the layout has been changed slightly. I used Otter Version 2.2xa on a Solburn machine with SuperSparc processors. Some of the proofs required several hours of CPU time, and the program generated up to 70 million clauses. Otter is a refutational theorem prover. Therefore the theorem to be proved is negated and the systems tries to find the empty clause F, the basic contradiction. ‘|’ is Otter’s symbol for disjunction. x != y means x ≠ y. All other symbols are self explanatory.

In most cases I used hyperresolution as inference rule. Except for the weighting limit, which limits the size of the derived clauses, no other control parameter was changed from its default value. For some of the proofs the weighting limit turned out to be crucial. No proof could be found for other weighting limits. During the proof search, however, there was no interaction with the system. In most cases all formulae were put into the set of support (sos) list. This is necessary because hyperresolution is not complete together with the sos strategy.

In the protocols below, d is used for the binary consequence relation ⊢^{2}, i is the implication connective and b stands for the □–operator. x,y,z,u,v,w are variable symbols.

Lemma A.1 (Reflexivity of ⊢^{2}) From the axioms (12) and (13) we prove that the consequence relation is reflexive.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
% negated theorem.
-(all p d(p,p)).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3  -d(c1,c1).
----> UNIT CONFLICT at   1.58 sec ----> 380 [379,3] F.
---------------- PROOF ----------------
  4 [2,1,1]     d(i(i(i(x,y),i(z,y)),i(y,u)),i(v,i(y,u))).
  5 [4,2,4]     d(x,i(i(y,z),i(z,i(y,z)))).
  8 [5,2,1]     d(i(i(i(x,y),i(y,i(x,y))),z),i(u,z)).
 16 [8,2,1]     d(x,i(i(i(y,i(z,y)),z),i(u,z))).
 21 [16,2,1]    d(i(i(i(i(x,i(y,x)),y),i(z,y)),u),i(v,u)).
253 [21,2,4]    d(x,i(i(y,z),i(u,i(y,z)))).
259 [253,2,253] d(i(x,y),i(z,i(x,y))).
288 [259,2,1]   d(i(i(x,i(y,z)),y),i(u,y)).
310 [288,2,1]   d(i(i(x,y),i(z,i(y,u))),i(v,i(z,i(y,u)))).
369 [310,2,259] d(x,i(y,i(z,z))).
376 [369,2,369] d(x,i(y,y)).
379 [376,2,376] d(x,x).
380 [379,3]     F.

<

Lemma A.2 (Transitivity of ⊢^{2}) From the axioms (12) and (13) we prove the transitivity of the consequence relation.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).

all p d(p,p).
% negated theorem.
-(all p q r (d(p,q)&d(q,r)->d(p,r))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4   d(c3,c2).
5   d(c2,c1).
6  -d(c3,c1).
----> UNIT CONFLICT at 3612.46 sec ----> 41345 [41344,6] F.
---------------- PROOF ----------------
  7 [2,3,1]         d(i(i(x,y),x),i(z,x)).
  9 [7,2,7]         d(x,i(y,y)).
 10 [7,2,1]         d(i(i(x,y),i(y,z)),i(u,i(y,z))).
 11 [9,2,1]         d(i(i(x,x),y),i(z,y)).
 20 [10,2,1]        d(i(i(x,i(y,z)),i(u,y)),i(v,i(u,y))).
 30 [20,2,1]        d(x,i(i(i(i(y,z),u),z),i(y,z))).
 31 [20,2,1]        d(i(i(x,i(y,z)),i(u,i(z,v))),i(w,i(u,i(z,v)))).
 32 [30,2,30]       d(i(i(i(x,y),z),y),i(x,y)).
 34 [32,2,20]       d(x,i(y,i(z,y))).
 35 [32,2,7]        d(x,i(y,x)).
 37 [32,2,1]        d(i(i(x,y),i(i(x,y),z)),i(u,i(i(x,y),z))).
 47 [35,2,5]        d(x,i(c2,c1)).
 48 [35,2,4]        d(x,i(c3,c2)).
 50 [35,2,1]        d(i(i(x,i(y,z)),y),i(u,y)).
 51 [47,2,35]       d(x,i(y,i(c2,c1))).
 52 [47,2,1]        d(i(i(c2,c1),x),i(y,x)).
 53 [48,2,35]       d(x,i(y,i(c3,c2))).
 54 [48,2,1]        d(i(i(c3,c2),x),i(y,x)).
 56 [34,2,1]        d(i(i(x,i(y,x)),z),i(u,z)).
 58 [51,2,1]        d(i(i(x,i(c2,c1)),y),i(z,y)).
 60 [53,2,1]        d(i(i(x,i(c3,c2)),y),i(z,y)).
267 [37,2,60]       d(x,i(i(i(y,i(c3,c2)),z),z)).
268 [37,2,58]       d(x,i(i(i(y,i(c2,c1)),z),z)).
269 [37,2,56]       d(x,i(i(i(y,i(z,y)),u),u)).
270 [37,2,54]       d(x,i(i(i(c3,c2),y),y)).
271 [37,2,52]       d(x,i(i(i(c2,c1),y),y)).
272 [37,2,50]       d(x,i(i(i(y,i(z,u)),z),z)).
284 [37,2,11]       d(x,i(i(i(y,y),z),z)).
287 [37,2,7]        d(x,i(i(i(y,z),y),y)).
294 [270,2,270]     d(i(i(c3,c2),x),x).
297 [271,2,294]     d(i(i(c2,c1),x),x).
300 [284,2,297]     d(i(i(x,x),y),y).
303 [287,2,300]     d(i(i(x,y),x),x).
306 [303,2,1]       d(i(x,i(x,y)),i(z,i(x,y))).
307 [267,2,303]     d(i(i(x,i(c3,c2)),y),y).
311 [268,2,307]     d(i(i(x,i(c2,c1)),y),y).
315 [269,2,311]     d(i(i(x,i(y,x)),z),z).
319 [272,2,315]     d(i(i(x,i(y,z)),y),y).
323 [319,2,1]       d(i(x,i(y,i(x,z))),i(u,i(y,i(x,z)))).
339 [306,2,306]     d(x,i(i(y,i(y,z)),i(y,z))).
342 [339,2,339]     d(i(x,i(x,y)),i(x,y)).
364 [342,2,10]      d(i(i(x,y),i(y,z)),i(y,z)).
371 [364,2,1]       d(i(i(x,y),i(z,x)),i(u,i(z,x))).
458 [371,2,32]      d(x,i(y,i(z,x))).
605 [323,2,1]       d(x,i(i(y,z),i(i(i(z,u),y),z))).
609 [605,2,605]     d(i(x,y),i(i(i(y,z),x),y)).

  622 [609,2,458]     d(i(i(i(x,i(y,z)),u),z),i(x,i(y,z))).
  674 [609,2,54]      d(i(i(i(x,y),z),i(i(c3,c2),y)),i(x,y)).
  676 [609,2,50]      d(i(i(i(x,y),z),i(i(u,i(y,v)),y)),i(x,y)).
  690 [609,2,7]       d(i(i(i(x,y),z),i(i(y,u),y)),i(x,y)).
 3887 [31,2,1]        d(x,i(i(i(y,z),u),i(z,u))).
 3899 [3887,2,3887]   d(i(i(x,y),z),i(y,z)).
 3908 [3899,2,1]      d(x,i(i(x,y),i(z,y))).
 4217 [3908,2,3899]   d(x,i(i(i(y,x),z),i(u,z))).
 4225 [3908,2,609]    d(i(i(i(i(x,y),i(z,y)),u),x),i(i(x,y),i(z,y))).
 4229 [3908,2,1]      d(i(i(i(i(x,y),z),i(u,z)),x),i(v,x)).
 4604 [4217,2,1]      d(i(i(i(i(x,i(y,z)),u),i(v,u)),y),i(w,y)).
 5104 [4229,2,342]    d(i(i(i(i(x,y),z),i(u,z)),x),x).
 5118 [5104,2,676]    d(i(i(i(i(x,i(i(y,z),u)),i(y,z)),v),z),i(y,z)).
 6337 [4604,2,342]    d(i(i(i(i(x,i(y,z)),u),i(v,u)),y),y).
 6354 [6337,2,674]    d(i(i(x,i(i(i(c3,c2),i(y,z)),u)),z),i(y,z)).
16572 [4225,2,6354]   d(i(i(x,y),z),i(i(i(c3,c2),i(x,y)),z)).
18364 [16572,2,1]     d(i(i(c3,c2),i(i(x,y),z)),i(i(z,x),i(u,x))).
39219 [5118,2,690]    d(i(i(x,i(i(i(y,z),y),u)),i(i(y,z),y)),y).
39255 [39219,2,4225]  d(i(x,y),i(i(i(x,z),x),y)).
40733 [39255,2,5]     d(i(i(c2,x),c2),c1).
40751 [39255,2,18364] d(i(c2,i(c3,x)),i(y,i(c3,x))).
40917 [40733,2,622]   d(c2,i(x,c1)).
41296 [40751,2,40917] d(x,i(c3,c1)).
41344 [41296,2,41296] d(c3,c1).
41345 [41344,6]       F.

<

Lemma A.3 (First Congruence Lemma for ⇝) From the axioms (12) and (13) we prove the first congruence lemma (19) for ⇝:

∀p, q (p ⊢^{2} q ∧ q ⊢^{2} p) ⇒ ∀s p ⇝ s ⊢^{2} q ⇝ s).

As lemmas we use reflexivity and transitivity of ⊢^{2}.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
% negated theorem.
-(all p q (d(p,q)&d(q,p)-> (all s d(i(p,s),i(q,s))))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5   d(c3,c2).
6   d(c2,c3).
7  -d(i(c3,c1),i(c2,c1)).
----> UNIT CONFLICT at 886.29 sec ----> 35208 [35207,7] F.
---------------- PROOF ----------------
    9 [2,3,1]       d(i(i(x,y),x),i(z,x)).
   11 [9,4,1]       d(i(i(x,y),i(z,x)),i(u,i(z,x))).
   13 [9,2,9]       d(x,i(y,y)).
   16 [13,2,1]      d(i(i(x,x),y),i(z,y)).
   18 [16,4,1]      d(i(i(x,y),x),i(z,i(u,x))).
   31 [18,2,9]      d(x,i(y,i(z,y))).
   34 [31,2,31]     d(x,i(y,x)).
   37 [34,4,6]      d(c2,i(x,c3)).

   40 [34,4,1]      d(x,i(i(x,y),i(z,y))).
   43 [34,2,5]      d(x,i(c3,c2)).
   47 [37,4,1]      d(c2,i(i(c3,x),i(y,x))).
   55 [43,2,1]      d(i(i(c3,c2),x),i(y,x)).
  770 [11,2,40]     d(x,i(i(i(i(y,z),u),z),i(y,z))).
 2355 [770,2,770]   d(i(i(i(x,y),z),y),i(x,y)).
 2421 [2355,4,55]   d(i(i(i(i(c3,c2),x),y),x),i(z,x)).
 2468 [2421,2,9]    d(x,i(i(i(c3,c2),y),y)).
 2479 [2468,2,2468] d(i(i(c3,c2),x),x).
 2519 [2479,4,11]   d(i(i(x,y),i(z,x)),i(z,x)).
 2520 [2479,4,9]    d(i(i(x,y),x),x).
 2845 [2520,4,47]   d(i(i(c2,x),c2),i(i(c3,y),i(z,y))).
35207 [2845,2,2519] d(i(c3,x),i(c2,x)).
35208 [35207,7]     F.

<

Lemma A.4 (Second Congruence Lemma for ⇝) From the axioms (12) and (13) we prove the second congruence lemma (20) for ⇝:

∀p, q (p ⊢^{2} q ∧ q ⊢^{2} p) ⇒ ∀s s ⇝ p ⊢^{2} s ⇝ p).

As lemmas we use again reflexivity and transitivity of ⊢^{2}.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
% negated theorem.
-(all p q (d(p,q)&d(q,p)-> (all s d(i(s,p),i(s,q))))).
end_of_list.
-------> sos clausifies to:
1     d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2    -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3     d(x9,x9).
4    -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5     d(c3,c2).
6     d(c2,c3).
7    -d(i(c1,c3),i(c1,c2)).
----> UNIT CONFLICT at 10394.18 sec ----> 126271 [126270,7] F.
---------------- PROOF ----------------
     9 [2,3,1]          d(i(i(x,y),x),i(z,x)).
    11 [9,4,1]          d(i(i(x,y),i(z,x)),i(u,i(z,x))).
    13 [9,2,9]          d(x,i(y,y)).
    16 [13,2,1]         d(i(i(x,x),y),i(z,y)).
    18 [16,4,1]         d(i(i(x,y),x),i(z,i(u,x))).
    31 [18,2,9]         d(x,i(y,i(z,y))).
    34 [31,2,31]        d(x,i(y,x)).
    38 [34,4,5]         d(c3,i(x,c2)).
    40 [34,4,1]         d(x,i(i(x,y),i(z,y))).
    43 [34,2,5]         d(x,i(c3,c2)).
    45 [34,2,1]         d(i(i(x,i(y,z)),y),i(u,y)).
    51 [38,2,34]        d(x,i(c3,i(y,c2))).
    55 [43,2,1]         d(i(i(c3,c2),x),i(y,x)).
    83 [51,2,1]         d(i(i(c3,i(x,c2)),y),i(z,y)).
   327 [11,2,40]        d(x,i(i(i(i(y,z),u),z),i(y,z))).
   450 [327,2,327]      d(i(i(i(x,y),z),y),i(x,y)).
   498 [450,4,55]       d(i(i(i(i(c3,c2),x),y),x),i(z,x)).
   528 [498,2,9]        d(x,i(i(i(c3,c2),y),y)).
   534 [528,2,528]      d(i(i(c3,c2),x),x).

   564 [534,4,83]       d(i(i(c3,i(x,c2)),y),y).
   568 [534,4,45]       d(i(i(x,i(y,z)),y),y).
   574 [534,4,9]        d(i(i(x,y),x),x).
   829 [574,4,450]      d(i(i(i(i(x,y),x),z),x),x).
   905 [574,2,1]        d(i(x,i(x,y)),i(z,i(x,y))).
  5733 [905,4,829]      d(i(x,i(x,y)),i(x,y)).
  6649 [5733,4,1]       d(i(i(x,y),z),i(i(z,x),x)).
 16808 [6649,4,564]     d(i(i(i(x,c2),y),c3),i(x,c2)).
 16814 [6649,4,1]       d(i(i(x,y),z),i(i(x,z),i(u,z))).
 16845 [6649,2,568]     d(i(x,i(y,i(x,z))),i(y,i(x,z))).
124104 [16845,2,16814]  d(i(x,y),i(i(i(x,z),y),y)).
126270 [124104,4,16808] d(i(x,c3),i(x,c2)).
126271 [126270,7]       F.

<

Lemma A.5 (Congruence Lemma for □) From the axioms (12) to (15) we prove the congruence lemma (21) for □:

∀p, q (p ⊢^{2} q ∧ q ⊢^{2} p) ⇒ □p ⊢^{2} □q.

Reflexivity and transitivity of ⊢^{2} are again used as lemmas.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
all p ((all x d(x,p))-> (all x d(x,b(p)))).
all p q d(b(i(p,q)),i(b(p),b(q))).
% negated theorem.
-(all p q (d(p,q)&d(q,p)->d(b(p),b(q)))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5  -d(f1(x13),x13)|d(x,b(x13)).
6   d(b(i(x14,x15)),i(b(x14),b(x15))).
7   d(c2,c1).
8   d(c1,c2).
9  -d(b(c2),b(c1)).
----> UNIT CONFLICT at   0.71 sec ----> 209 [208,9] F.
 11 [2,3,1]     d(i(i(x,y),x),i(z,x)).
 15 [11,2,11]   d(x,i(y,y)).
 19 [15,2,1]    d(i(i(x,x),y),i(z,y)).
 27 [19,4,1]    d(i(i(x,y),x),i(z,i(u,x))).
 90 [27,2,11]   d(x,i(y,i(z,y))).
 94 [90,2,90]   d(x,i(y,x)).
103 [94,2,8]    d(x,i(c1,c2)).
104 [94,2,7]    d(x,i(c2,c1)).
114 [103,5]     d(x,b(i(c1,c2))).
117 [104,5]     d(x,b(i(c2,c1))).
122 [114,4,6]   d(x,i(b(c1),b(c2))).
126 [117,4,6]   d(x,i(b(c2),b(c1))).
197 [122,2,122] d(b(c1),b(c2)).
208 [126,2,197] d(b(c2),b(c1)).
209 [208,9]     F.

<

Lemma A.6 (Upwards Monotonicity Lemma for ⇝) From the axioms (12) and (13) we prove the upward monotonicity lemma for ⇝ (36):

p ⊢^{2} q ⇒ ∀s (s ⇝ p) ⊢^{2} (s ⇝ q).

Reflexivity and transitivity of ⊢^{2} are again used as lemmas.

set(hyper_res).
assign(max_weight,13).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
% negated theorem.
-(all p q (d(p,q)-> (all s d(i(s,p),i(s,q))))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5   d(c3,c2).
6  -d(i(c1,c3),i(c1,c2)).
----> UNIT CONFLICT at 1041.75 sec ----> 54166 [54165,6] F.
    8 [2,3,1]        d(i(i(x,y),x),i(z,x)).
   10 [8,4,1]        d(i(i(x,y),i(z,x)),i(u,i(z,x))).
   12 [8,2,8]        d(x,i(y,y)).
   15 [12,2,1]       d(i(i(x,x),y),i(z,y)).
   17 [15,4,1]       d(i(i(x,y),x),i(z,i(u,x))).
   30 [17,2,8]       d(x,i(y,i(z,y))).
   33 [30,2,30]      d(x,i(y,x)).
   36 [33,4,5]       d(c3,i(x,c2)).
   38 [33,4,1]       d(x,i(i(x,y),i(z,y))).
   40 [33,2,5]       d(x,i(c3,c2)).
   42 [33,2,1]       d(i(i(x,i(y,z)),y),i(u,y)).
   45 [36,2,33]      d(x,i(c3,i(y,c2))).
   47 [40,2,1]       d(i(i(c3,c2),x),i(y,x)).
   71 [45,2,1]       d(i(i(c3,i(x,c2)),y),i(z,y)).
  345 [10,2,38]      d(x,i(i(i(i(y,z),u),z),i(y,z))).
  491 [345,2,345]    d(i(i(i(x,y),z),y),i(x,y)).
  528 [491,4,47]     d(i(i(i(i(c3,c2),x),y),x),i(z,x)).
  563 [528,2,8]      d(x,i(i(i(c3,c2),y),y)).
  573 [563,2,563]    d(i(i(c3,c2),x),x).
  592 [573,4,71]     d(i(i(c3,i(x,c2)),y),y).
  594 [573,4,42]     d(i(i(x,i(y,z)),y),y).
  600 [573,4,8]      d(i(i(x,y),x),x).
  714 [600,4,491]    d(i(i(i(i(x,y),x),z),x),x).
  775 [600,2,1]      d(i(x,i(x,y)),i(z,i(x,y))).
 3013 [775,4,714]    d(i(x,i(x,y)),i(x,y)).
 3642 [3013,4,1]     d(i(i(x,y),z),i(i(z,x),x)).
 7874 [3642,4,592]   d(i(i(i(x,c2),y),c3),i(x,c2)).
 7882 [3642,4,1]     d(i(i(x,y),z),i(i(x,z),i(u,z))).
 7900 [3642,2,594]   d(i(x,i(y,i(x,z))),i(y,i(x,z))).
53109 [7900,2,7882]  d(i(x,y),i(i(i(x,z),y),y)).
54165 [53109,4,7874] d(i(x,c3),i(x,c2)).
54166 [54165,6]      F.

<

Lemma A.7 (Downwards Monotonicity Lemma for ⇝) From the axioms (12) and (13) we prove the downward monotonicity lemma for ⇝ (37):

p ⊢^{2} q ⇒ ∀s (q ⇝ s) ⊢^{2} (p ⇝ s).

As lemmas we use again reflexivity and transitivity of ⊢^{2}.

set(hyper_res).
assign(max_weight,13).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s)))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
% negated theorem.
-(all p q (d(p,q)-> (all s d(i(q,s),i(p,s))))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5   d(c3,c2).
6  -d(i(c2,c1),i(c3,c1)).
----> UNIT CONFLICT at  82.77 sec ----> 11511 [11510,6] F.
    8 [2,3,1]     d(i(i(x,y),x),i(z,x)).
   10 [8,4,1]     d(i(i(x,y),i(z,x)),i(u,i(z,x))).
   12 [8,2,8]     d(x,i(y,y)).
   15 [12,2,1]    d(i(i(x,x),y),i(z,y)).
   17 [15,4,1]    d(i(i(x,y),x),i(z,i(u,x))).
   30 [17,2,8]    d(x,i(y,i(z,y))).
   33 [30,2,30]   d(x,i(y,x)).
   36 [33,4,5]    d(c3,i(x,c2)).
   38 [33,4,1]    d(x,i(i(x,y),i(z,y))).
   40 [33,2,5]    d(x,i(c3,c2)).
   44 [36,4,1]    d(c3,i(i(c2,x),i(y,x))).
   47 [40,2,1]    d(i(i(c3,c2),x),i(y,x)).
  345 [10,2,38]   d(x,i(i(i(i(y,z),u),z),i(y,z))).
  491 [345,2,345] d(i(i(i(x,y),z),y),i(x,y)).
  528 [491,4,47]  d(i(i(i(i(c3,c2),x),y),x),i(z,x)).
  563 [528,2,8]   d(x,i(i(i(c3,c2),y),y)).
  573 [563,2,563] d(i(i(c3,c2),x),x).
  599 [573,4,10]  d(i(i(x,y),i(z,x)),i(z,x)).
  600 [573,4,8]   d(i(i(x,y),x),x).
  750 [600,4,44]  d(i(i(c3,x),c3),i(i(c2,y),i(z,y))).
11510 [750,2,599] d(i(c2,x),i(c3,x)).
11511 [11510,6]   F.

<

Lemma A.8 (Upwards Monotonicity Lemma for □) From the axioms (12) to (15) we prove the upward monotonicity lemma for □ (38):

p ⊢^{2} q ⇒ □p ⊢^{2} □q.

Reflexivity and transitivity of ⊢^{2} are used as lemmas.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
all p ((all x d(x,p))-> (all x d(x,b(p)))).
all p q d(b(i(p,q)),i(b(p),b(q))).
% negated theorem.

-(all p q (d(p,q)->d(b(p),b(q)))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5  -d(f1(x13),x13)|d(x,b(x13)).
6   d(b(i(x14,x15)),i(b(x14),b(x15))).
7   d(c2,c1).
8  -d(b(c2),b(c1)).
----> UNIT CONFLICT at   0.54 sec ----> 170 [169,8] F.
 10 [2,3,1]     d(i(i(x,y),x),i(z,x)).
 14 [10,2,10]   d(x,i(y,y)).
 18 [14,2,1]    d(i(i(x,x),y),i(z,y)).
 26 [18,4,1]    d(i(i(x,y),x),i(z,i(u,x))).
 89 [26,2,10]   d(x,i(y,i(z,y))).
 93 [89,2,89]   d(x,i(y,x)).
101 [93,2,7]    d(x,i(c2,c1)).
108 [101,5]     d(x,b(i(c2,c1))).
113 [108,4,6]   d(x,i(b(c2),b(c1))).
169 [113,2,113] d(b(c2),b(c1)).
170 [169,8]     F.

<

Lemma A.9 (Basis for Transformer T_{4}) From the monotonicity properties (40) and (39) we prove

w ⊧^{L} f(p⃗, q⃗) ⇔ ∀x⃗ ⋀_{i}(∀v:W v ⊧^{L} x_{i} ⇒ v ⊧^{L} p_{i}) ⇒ ∃y⃗ ⋀_{j}(∀v:W v ⊧^{L} y_{j} ⇒ v ⊧^{L} q_{j}) ∧ w ⊧^{L} f(x⃗, y⃗). It is sufficient to prove it for two arguments of f, the first one being downward monotonic and the second one being upward monotonic. ‘m(w,p)’ means w ⊧^{L} p. This time we use binary resolution and the set of support strategy.

set(binary_res).
set(factor).
formula_list(usable).
all p q ((all w (m(w,p)->m(w,q)))-> (all r w (m(w,f(r,p))->m(w,f(r,q))))).
all p q ((all w (m(w,p)->m(w,q)))-> (all r w (m(w,f(q,r))->m(w,f(p,r))))).
end_of_list.
-------> usable clausifies to:
 1   m(f1(x1,x2),x1)| -m(w,f(x3,x1))|m(w,f(x3,x2)).
 2  -m(f1(x1,x2),x2)| -m(w,f(x3,x1))|m(w,f(x3,x2)).
 3   m(f2(x4,x5),x4)| -m(w,f(x5,x6))|m(w,f(x4,x6)).
 4  -m(f2(x4,x5),x5)| -m(w,f(x5,x6))|m(w,f(x4,x6)).
formula_list(sos).
% negated theorem.
-(all p q w (m(w,f(p,q)) <->
   (all x ((all v (m(v,x)->m(v,p))) ->
     (exists y ((all v (m(v,y)->m(v,q))) & m(w,f(x,y)))))))).
end_of_list.
-------> sos clausifies to:
 5   m(c2,f(c4,c3))|m(f3(x),x)| -m(v,f4(x))|m(v,c3).
 6   m(c2,f(c4,c3))|m(f3(x),x)|m(c2,f(x,f4(x))).
 7   m(c2,f(c4,c3))| -m(f3(x),c4)| -m(v,f4(x))|m(v,c3).
 8   m(c2,f(c4,c3))| -m(f3(x),c4)|m(c2,f(x,f4(x))).
 9  -m(c2,f(c4,c3))| -m(x7,c1)|m(x7,c4).
10  -m(c2,f(c4,c3))|m(f5(y),y)| -m(c2,f(c1,y)).
11  -m(c2,f(c4,c3))| -m(f5(y),c3)| -m(c2,f(c1,y)).
----> UNIT CONFLICT at  10.65 sec ----> 1090 [1089,164] F.
---------------- PROOF ----------------

  47 [11,10]   -m(c2,f(c4,c3))| -m(c2,f(c1,c3)).
  60 [47,4]    -m(c2,f(c4,c3))| -m(f2(c1,x),x)| -m(c2,f(x,c3)).
  61 [47,3]    -m(c2,f(c4,c3))|m(f2(c1,x),c1)| -m(c2,f(x,c3)).
  66 [60]      -m(c2,f(c4,c3))| -m(f2(c1,c4),c4).
  67 [61]      -m(c2,f(c4,c3))|m(f2(c1,c4),c1).
  80 [66,9]    -m(c2,f(c4,c3))| -m(f2(c1,c4),c1).
  90 [80,67]   -m(c2,f(c4,c3)).
  93 [90,2]    -m(f1(x,c3),c3)| -m(c2,f(c4,x)).
  94 [90,1]     m(f1(x,c3),x)| -m(c2,f(c4,x)).
 119 [6,90]     m(f3(x),x)|m(c2,f(x,f4(x))).
 144 [8,90]    -m(f3(x),c4)|m(c2,f(x,f4(x))).
 156 [144,119]  m(c2,f(c4,f4(c4))).
 163 [156,94]   m(f1(f4(c4),c3),f4(c4)).
 164 [156,93]  -m(f1(f4(c4),c3),c3).
 455 [5,90]     m(f3(x),x)| -m(y,f4(x))|m(y,c3).
 546 [455,163]  m(f3(c4),c4)|m(f1(f4(c4),c3),c3).
 616 [546,164]  m(f3(c4),c4).
 844 [7,90]    -m(f3(x),c4)| -m(y,f4(x))|m(y,c3).
 968 [844,616] -m(x,f4(c4))|m(x,c3).
1089 [968,163]  m(f1(f4(c4),c3),c3).
1090 [1089,164] F.

<

Lemma A.10 (Intersection Closure Lemma for ⇝) From (11) to (13) we prove the closure lemma (50) for ⇝:

∀p, q, r, w w ⊢^{2} (r ⇝ p) ∧ w ⊢^{2} (r ⇝ q) ⇒ ∃s s ⊢^{2} p ∧ s ⊢^{2} q ∧ w ⊢^{2} (r ⇝ s).

Reflexivity and transitivity of ⊢^{2} and the monotonicity properties for ⇝ are used as lemmas.

set(hyper_res).
assign(max_weight,13).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
all p d(bot,p).
all p q (d(q,p)-> (all s d(i(s,q),i(s,p)))).
all p q (d(p,q)-> (all s d(i(q,s),i(p,s)))).
% negated theorem.
-(all p q r w (d(w,i(r,p))&d(w,i(r,q))->
   (exists s (d(s,p)&d(s,q)&d(w,i(r,s)))))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5   d(bot,x13).
6  -d(x14,x15)|d(i(x16,x14),i(x16,x15)).
7  -d(x17,x18)|d(i(x18,x19),i(x17,x19)).
8   d(c1,i(c2,c4)).
9   d(c1,i(c2,c3)).
10  -d(x20,c4)| -d(x20,c3)| -d(c1,i(c2,x20)).
-----> EMPTY CLAUSE at 4234.45 sec ----> 8834 [8482,10,8384,5493] F.
---------------- PROOF ----------------
  13 [6,5]         d(i(x,bot),i(x,y)).
  14 [13,6]        d(i(x,i(y,bot)),i(x,i(y,z))).
  17 [7,13]        d(i(i(x,y),z),i(i(x,bot),z)).
  22 [7,5]         d(i(x,y),i(bot,y)).

  25 [22,4,13]     d(i(x,bot),i(bot,y)).
  93 [17,4,13]     d(i(i(x,y),bot),i(i(x,bot),z)).
 129 [1,4,17]      d(i(i(x,y),z),i(i(z,bot),i(u,x))).
 148 [2,25,1]      d(i(i(bot,x),y),i(z,y)).
 150 [2,13,1]      d(i(i(x,y),x),i(z,x)).
 151 [148,7]       d(i(i(x,y),z),i(i(i(bot,u),y),z)).
 161 [148,4,1]     d(i(i(x,y),bot),i(z,i(u,x))).
 169 [150,4,93]    d(i(i(x,y),bot),i(z,x)).
 226 [161,2,150]   d(x,i(y,i(z,y))).
 235 [226,2,226]   d(x,i(y,x)).
 237 [235,6]       d(i(x,y),i(x,i(z,y))).
 266 [235,4,1]     d(x,i(i(x,y),i(z,y))).
 381 [237,7]       d(i(i(x,i(y,z)),u),i(i(x,z),u)).
 800 [151,2,150]   d(x,i(i(i(bot,y),z),z)).
 813 [800,2,800]   d(i(i(bot,x),y),y).
 816 [813,6]       d(i(x,i(i(bot,y),z)),i(x,z)).
 848 [813,4,169]   d(i(i(x,y),bot),x).
 852 [813,4,150]   d(i(i(x,y),x),x).
 914 [848,7]       d(i(x,y),i(i(i(x,z),bot),y)).
 954 [852,7]       d(i(x,y),i(i(i(x,z),x),y)).
 964 [852,4,129]   d(i(i(x,y),i(z,x)),i(z,x)).
1340 [816,4,266]   d(x,i(i(x,y),y)).
1353 [816,4,129]   d(i(i(x,y),z),i(i(z,bot),x)).
1361 [816,4,1]     d(i(i(x,y),z),i(i(z,x),x)).
2816 [914,4,1340]  d(x,i(i(i(i(x,y),z),bot),y)).
3735 [954,4,9]     d(c1,i(i(i(c2,x),c2),c3)).
3736 [954,4,8]     d(c1,i(i(i(c2,x),c2),c4)).
3901 [964,4,954]   d(i(x,i(y,i(x,z))),i(y,i(x,z))).
3911 [964,4,14]    d(i(i(x,y),i(z,bot)),i(z,x)).
4150 [1361,4,3736] d(c1,i(i(c4,i(c2,x)),i(c2,x))).
4151 [1361,4,3735] d(c1,i(i(c3,i(c2,x)),i(c2,x))).
5493 [3911,4,2816] d(x,i(y,i(i(x,i(y,bot)),z))).
6675 [381,4,4151]  d(c1,i(i(c3,x),i(c2,x))).
6676 [381,4,4150]  d(c1,i(i(c4,x),i(c2,x))).
6754 [6675,4,237]  d(c1,i(i(c3,x),i(y,i(c2,x)))).
6781 [6676,4,237]  d(c1,i(i(c4,x),i(y,i(c2,x)))).
7782 [3901,2,6781] d(i(c4,x),i(c1,i(c2,x))).
7783 [3901,2,6754] d(i(c3,x),i(c1,i(c2,x))).
8384 [7782,2,1353] d(i(i(c1,i(c2,x)),bot),c4).
8482 [7783,2,1353] d(i(i(c1,i(c2,x)),bot),c3).
8834 [8482,10,8384,5493] F.

<

Lemma A.11 (Union Closure Lemma for ⇝) From (11) to (13) we prove the closure lemma (51) for ⇝.

∀p, q, r, w w ⊢^{2} (p ⇝ r) ∧ w ⊢^{2} (q ⇝ r) ⇒ ∃s p ⊢^{2} s ∧ q ⊢^{2} s ∧ w ⊢^{2} (s ⇝ r).

As lemmas we use reflexivity and transitivity of ⊢^{2} and the monotonicity properties for ⇝.

set(hyper_res).
assign(max_weight,13).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
all p q (d(q,p)-> (all s d(i(s,q),i(s,p)))).
all p q (d(p,q)-> (all s d(i(q,s),i(p,s)))).
% negated theorem.
-(all p q r x (d(x,i(p,r))&d(x,i(q,r))->

    (exists s (d(p,s)&d(q,s)&d(x,i(s,r)))))).
end_of_list.
-------> sos clausifies to:
1  d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3  d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5  -d(x13,x14)|d(i(x15,x13),i(x15,x14)).
6  -d(x16,x17)|d(i(x17,x18),i(x16,x18)).
7  d(c1,i(c4,c2)).
8  d(c1,i(c3,c2)).
9  -d(c4,x19)| -d(c3,x19)| -d(c1,i(x19,c2)).
-----> EMPTY CLAUSE at  15.92 sec ----> 819 [726,9,728,727] F.
---------------- PROOF ----------------
 16 [6,8]       d(i(i(c3,c2),x),i(c1,x)).
 17 [6,7]       d(i(i(c4,c2),x),i(c1,x)).
 26 [1,4,17]    d(i(i(c2,x),c4),i(c1,i(y,c2))).
 27 [1,4,16]    d(i(i(c2,x),c3),i(c1,i(y,c2))).
 32 [2,3,1]     d(i(i(x,y),x),i(z,x)).
 33 [32,6]      d(i(i(x,y),z),i(i(i(y,u),y),z)).
 38 [32,4,27]   d(i(i(c3,x),c3),i(c1,i(y,c2))).
 39 [32,4,26]   d(i(i(c4,x),c4),i(c1,i(y,c2))).
 45 [32,2,32]   d(x,i(y,y)).
 47 [45,6]      d(i(i(x,x),y),i(z,y)).
 61 [47,4,1]    d(i(i(x,y),x),i(z,i(u,x))).
 93 [61,2,32]   d(x,i(y,i(z,y))).
 98 [93,2,93]   d(x,i(y,x)).
112 [98,4,39]   d(c4,i(c1,i(x,c2))).
113 [98,4,38]   d(c3,i(c1,i(x,c2))).
114 [98,4,1]    d(x,i(i(x,y),i(z,y))).
467 [33,2,32]   d(x,i(i(i(y,z),y),y)).
479 [467,2,467] d(i(i(x,y),x),x).
480 [479,6]     d(i(x,y),i(i(i(x,z),x),y)).
681 [480,4,479] d(i(x,i(x,y)),i(x,y)).
726 [681,4,114] d(x,i(i(x,y),y)).
727 [681,4,113] d(c3,i(c1,c2)).
728 [681,4,112] d(c4,i(c1,c2)).
819 [726,9,728,727] F.

<

Lemma A.12 (Closure Lemma (47) for □) From (11) to (15) we prove the closure lemma (47) for □.

∀p, q, w w ⊢^{2} □p ∧ w ⊢^{2} □q ⇒ ∃s s ⊢^{2} p ∧ s ⊢^{2} q ∧ w ⊢^{2} □s.

Reflexivity and transitivity of ⊢^{2} and the monotonicity properties for ⇝ and □ are used as lemmas.

set(hyper_res).
assign(max_weight,13).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
all p d(bot,p).
all p q (d(p,q)-> (all s d(i(s,p),i(s,q)))).
all p q (d(p,q)-> (all s d(i(q,s),i(p,s)))).
all p ((all x d(x,p))-> (all x d(x,b(p)))).
all p q d(b(i(p,q)),i(b(p),b(q))).
all p q (d(p,q)->d(b(p),b(q))).
% negated theorem.

-(all p q w (d(w,b(p))&d(w,b(q))-> (exists s (d(s,p)&d(s,q)&d(w,b(s)))))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5   d(bot,x13).
6  -d(x14,x15)|d(i(x16,x14),i(x16,x15)).
7  -d(x17,x18)|d(i(x18,x19),i(x17,x19)).
8  -d(f1(x20),x20)|d(x,b(x20)).
9   d(b(i(x21,x22)),i(b(x21),b(x22))).
10  -d(x23,x24)|d(b(x23),b(x24)).
11   d(c1,b(c3)).
12   d(c1,b(c2)).
13  -d(x25,c3)| -d(x25,c2)| -d(c1,b(x25)).
-----> EMPTY CLAUSE at 14759.62 sec ----> 11001 [11000,13,7739,7383] F.
---------------- PROOF ----------------
  33 [6,5]          d(i(x,bot),i(x,y)).
  45 [7,33]         d(i(i(x,y),z),i(i(x,bot),z)).
  56 [7,12]         d(i(b(c2),x),i(c1,x)).
  58 [7,5]          d(i(x,y),i(bot,y)).
  62 [58,4,33]      d(i(x,bot),i(bot,y)).
 134 [9,4,56]       d(b(i(c2,x)),i(c1,b(x))).
 158 [134,6]        d(i(x,b(i(c2,y))),i(x,i(c1,b(y)))).
 266 [45,4,33]      d(i(i(x,y),bot),i(i(x,bot),z)).
 579 [1,4,45]       d(i(i(x,y),z),i(i(z,bot),i(u,x))).
 617 [2,62,1]       d(i(i(bot,x),y),i(z,y)).
 621 [2,33,1]       d(i(i(x,y),x),i(z,x)).
 623 [617,7]        d(i(i(x,y),z),i(i(i(bot,u),y),z)).
 639 [617,4,1]      d(i(i(x,y),bot),i(z,i(u,x))).
 690 [621,4,266]    d(i(i(x,y),bot),i(z,x)).
 711 [621,2,621]    d(x,i(y,y)).
 715 [711,7]        d(i(i(x,x),y),i(z,y)).
 830 [715,4,33]     d(i(i(x,x),bot),i(y,z)).
1171 [639,2,621]    d(x,i(y,i(z,y))).
1198 [1171,2,1171]  d(x,i(y,x)).
1365 [1198,4,1]     d(x,i(i(x,y),i(z,y))).
1450 [1198,2,1]     d(i(i(x,i(y,z)),y),i(u,y)).
1879 [1365,4,45]    d(x,i(i(x,bot),i(y,z))).
3472 [623,2,621]    d(x,i(i(i(bot,y),z),z)).
3494 [3472,2,3472]  d(i(i(bot,x),y),y).
3498 [3494,6]       d(i(x,i(i(bot,y),z)),i(x,z)).
3590 [3494,4,1450]  d(i(i(x,i(y,z)),y),y).
3623 [3494,4,830]   d(i(i(x,x),bot),y).
3646 [3494,4,690]   d(i(i(x,y),bot),x).
3662 [3494,4,621]   d(i(i(x,y),x),x).
3698 [3623,6]       d(i(x,i(i(y,y),bot)),i(x,z)).
3775 [3646,7]       d(i(x,y),i(i(i(x,z),bot),y)).
3776 [3646,6]       d(i(x,i(i(y,z),bot)),i(x,y)).
5420 [3498,4,1879]  d(x,i(i(x,bot),y)).
5434 [3498,4,1365]  d(x,i(i(x,y),y)).
5438 [3498,4,579]   d(i(i(x,y),z),i(i(z,bot),x)).
5471 [5420,7]       d(i(i(i(x,bot),y),z),i(x,z)).
5768 [5434,10]      d(b(x),b(i(i(x,y),y))).
6822 [5768,4,11]    d(c1,b(i(i(c3,x),x))).
7383 [3698,4,3590]  d(i(i(x,i(y,z)),i(i(u,u),bot)),y).
7455 [3775,10]      d(b(i(x,y)),b(i(i(i(x,z),bot),y))).
7480 [3775,4,3662]  d(i(x,i(x,y)),i(x,y)).

 7513 [7480,4,158]   d(i(c1,b(i(c2,x))),i(c1,b(x))).
 7739 [3776,4,3662]  d(i(i(x,y),i(i(x,z),bot)),x).
 8290 [5438,10]      d(b(i(i(x,y),z)),b(i(i(z,bot),x))).
 8487 [5471,10]      d(b(i(i(i(x,bot),y),z)),b(i(x,z))).
10097 [7455,4,6822]  d(c1,b(i(i(i(i(c3,x),y),bot),x))).
10955 [8290,4,10097] d(c1,b(i(i(x,bot),i(i(c3,x),y)))).
10989 [8487,4,10955] d(c1,b(i(x,i(i(c3,i(x,bot)),y)))).
11000 [10989,2,7513] d(c1,b(i(i(c3,i(c2,bot)),x))).
11001 [11000,13,7739,7383] F.

<

Lemma A.13 (Seriality for ⇝) We prove ∀w, p ∃q w ⊢^{2} p ⇝ q.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
% negated theorem.
-(all w p exists q d(w,i(p,q))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5  -d(c2,i(c1,x13)).
----> UNIT CONFLICT at   0.06 sec ----> 12 [11,5] F.
 7 [2,3,1] d(i(i(x,y),x),i(z,x)).
11 [7,2,7] d(x,i(y,y)).
12 [11,5]  F.

<

Lemma A.14 (Seriality for □) We prove ∀w ∃q w ⊢^{2} □q.

set(hyper_res).
formula_list(sos).
all r p q s d(i(i(p,q),r),i(i(r,p),i(s,p))).
all p q r s (d(p,q)&d(i(p,q),i(r,s))->d(r,s)).
all p d(p,p).
all p q r (d(p,q)&d(q,r)->d(p,r)).
all p ((all x d(x,p))-> (all x d(x,b(p)))).
all p q d(b(i(p,q)),i(b(p),b(q))).
all p q (d(p,q)->d(b(p),b(q))).
-(all w exists p d(w,b(p))).
end_of_list.
-------> sos clausifies to:
1   d(i(i(x1,x2),x3),i(i(x3,x1),i(x4,x1))).
2  -d(x5,x6)| -d(i(x5,x6),i(x7,x8))|d(x7,x8).
3   d(x9,x9).
4  -d(x10,x11)| -d(x11,x12)|d(x10,x12).
5  -d(f1(x13),x13)|d(x,b(x13)).
6   d(b(i(x14,x15)),i(b(x14),b(x15))).
7  -d(x16,x17)|d(b(x16),b(x17)).
8  -d(c1,b(x18)).
----> UNIT CONFLICT at   0.11 sec ----> 23 [22,8] F.
14 [2,3,1]   d(i(i(x,y),x),i(z,x)).

19 [14,2,14] d(x,i(y,y)).
22 [19,5]    d(x,b(i(y,y))).
23 [22,8]    F.

<

Lemma A.15 (Collapsing Lemmas for ⇝) We prove from (64) and (65) the general reflexivity ∀x R(x, x, x). Instead of the built–in equality handling we use equality axioms together with the unit resulting (UR) strategy. Other parameter settings did not work.

set(ur_res).
formula_list(sos).
all w exists x (R(x,w,w)& (all u v (R(x,u,v)->u=v))).
all w a b c d (R(w,a,b)&R(b,c,d)->
   (exists u v (R(w,u,v)&R(a,v,d)& (all x y (R(u,x,y)->x=d))))).
% equality axioms
all x (x=x).
all x y z u v w (x=y&z=u&v=w&R(x,z,v)->R(y,u,w)).
% negated theorem
-(all x R(x,x,x)).
end_of_list.
-------> sos clausifies to:
1  R(f(w),w,w).
2  -R(f(w),u,v)|u=v.
3  -R(w,x1,x2)| -R(x2,x3,x4)|R(w,h(w,x1,x2,x3,x4),g(w,x1,x2,x3,x4)).
4  -R(w,x1,x2)| -R(x2,x3,x4)|R(x1,g(w,x1,x2,x3,x4),x4).
5  -R(w,x1,x2)| -R(x2,x3,x4)| -R(h(w,x1,x2,x3,x4),x,y)|x=x4.
6  x=x.
7  x!=y|z!=u|v!=w| -R(x,z,v)|R(y,u,w).
8  -R(c,c,c).
----> UNIT CONFLICT at   1.89 sec ----> 297 [296,287] F.
abbreviations:
    f(f(x))               := k(x)
    g(k(x),f(x),f(x),x,x) := g1(x)
    f(c)                  := d
    f(d) = f(f(c))        := e = k(c)
---------------- PROOF ----------------
  9 [4,1,1]         R(f(x),g1(x),x).
 13 [9,2]           g1(x)=x.
 15 [7,13,6,9,8]    d!=c.
 24 [7,6,13,13,1]   R(f(g1(x)),x,x).
 27 [15,2]         -R(f(x),d,c).
 30 [27,7,6,6,1]    c!=d.
192 [5,1,1,30]     -R(h(f(e),e,e,d,d),c,x).
244 [192,7,13,6,9]  d!=h(f(e),e,e,d,d).
258 [244,2]        -R(f(x),d,h(f(e),e,e,d,d)).
261 [258,7,6,6,24]  h(f(e),e,e,d,d)!=d.
279 [261,2]        -R(f(x),h(f(e),e,e,d,d),d).
287 [279,7,6,6,13] -R(f(x),h(f(e),e,e,d,d),g(f(e),e,e,d,d)).
296 [3,1,1]         R(k(x),h(k(x),f(x),f(x),x,x),g1(x)).
297 [296,287]       F.

Now we prove from (64), (65) and the general reflexivity that the first two arguments of R collapse; ∀w, u, v R(w, u, v) ⇒ w = u.

set(ur_res).
assign(max_weight,40).
formula_list(sos).
all w exists x (R(x,w,w)& (all u v (R(x,u,v)->u=v))).
all w a b c d (R(w,a,b)&R(b,c,d)->

   (exists u v (R(w,u,v)&R(a,v,d)& (all x y (R(u,x,y)->x=d))))).
all x (x=x).
% equality axioms
all x y z u v w (x=y&z=u&v=w&R(x,z,v)->R(y,u,w)).
all x R(x,x,x).
% negated theorem
-(all w u v (R(w,u,v)->w=u)).
end_of_list.
-------> sos clausifies to:
 1   R(f(w),w,w).
 2  -R(f(w),u,v)|u=v.
 3  -R(w,x1,x2)| -R(x2,x3,x4)|R(w,h(w,x1,x2,x3,x4),g(w,x1,x2,x3,x4)).
 4  -R(w,x1,x2)| -R(x2,x3,x4)|R(x1,g(w,x1,x2,x3,x4),x4).
 5  -R(w,x1,x2)| -R(x2,x3,x4)| -R(h(w,x1,x2,x3,x4),x,y)|x=x4.
 6   x=x.
 7   x!=y|z!=u|v!=w| -R(x,z,v)|R(y,u,w).
 8   R(x,x,x).
 9   R(e,d,c).
10   e!=d.
----> UNIT CONFLICT at 435.17 sec ----> 8504 [binary,8503,7238] F.
---------------- PROOF ----------------
  11 [2,10]            -R(f(x),e,d).
  15 [4,8,1]            R(f(x),g(f(x),f(x),f(x),x,x),x).
  18 [4,1,1]            R(f(x),g(f(f(x)),f(x),f(x),x,x),x).
  69 [15,2]             g(f(x),f(x),f(x),x,x)=x.
  81 [18,2]             g(f(f(x)),f(x),f(x),x,x)=x.
 247 [7,6,6,1,11]       d!=e.
 294 [7,81,81,6,8]      R(x,x,g(f(f(x)),f(x),f(x),x,x)).
 297 [7,69,69,6,8]      R(x,x,g(f(x),f(x),f(x),x,x)).
 463 [294,2]            f(x)=g(f(f(f(x))),f(f(x)),f(f(x)),f(x),f(x)).
1079 [463,7,81,6,18]    R(g(f(f(f(x))),f(f(x)),f(f(x)),f(x),f(x)),x,x).
4609 [5,8,8,247]       -R(h(e,e,e,e,e),d,x).
7001 [5,8,8,297]        h(x,x,x,x,x)=x.
7238 [7001,7,81,6,1079] R(f(h(x,x,x,x,x)),x,h(x,x,x,x,x)).
8481 [4609,7,6,6,9]     e!=h(e,e,e,e,e).
8503 [8481,2]          -R(f(x),e,h(e,e,e,e,e)).
8504 [8503,7238]        F.

Now we prove from (64), (65), the general reflexivity, and collapsing of the first two arguments of R, that the last two arguments collapse as well: ∀w, u, v R(w, u, v) ⇒ u = v.

set(ur_res).
assign(max_weight,40).
formula_list(sos).
all w exists x (R(x,w,w)& (all u v (R(x,u,v)->u=v))).
all w a b c d (R(w,a,b)&R(b,c,d)->
   (exists u v (R(w,u,v)&R(a,v,d)& (all x y (R(u,x,y)->x=d))))).
% equality axioms
all x (x=x).
all x y z u v w (x=y&z=u&v=w&R(x,z,v)->R(y,u,w)).
all x R(x,x,x).
all w u v (R(w,u,v)->w=u).
%negated theorem
-(all w u v (R(w,u,v)->u=v)).
end_of_list.
-------> sos clausifies to:
1  R(f(w),w,w).
2  -R(f(w),u,v)|u=v.
3  -R(w,x1,x2)| -R(x2,x3,x4)|R(w,h(w,x1,x2,x3,x4),g(w,x1,x2,x3,x4)).

4  -R(w,x1,x2)| -R(x2,x3,x4)|R(x1,g(w,x1,x2,x3,x4),x4).
5  -R(w,x1,x2)| -R(x2,x3,x4)| -R(h(w,x1,x2,x3,x4),x,y)|x=x4.
6  x=x.
7  x!=y|z!=u|v!=w| -R(x,z,v)|R(y,u,w).
8  R(x,x,x).
9  -R(w,u,v)|w=u.
10  R(e,d,c).
11  d!=c.
----> UNIT CONFLICT at 555.50 sec ----> 9689 [9688,8630] F.
---------------- PROOF ----------------
  14 [9,1]          f(x)=x.
  15 [2,11]        -R(f(x),d,c).
  21 [4,1,8]        R(x,g(f(x),x,x,x,x),x).
  66 [21,2]         g(f(f(x)),f(x),f(x),f(x),f(x))=f(x).
 275 [7,6,6,10,15]  e!=f(x).
8630 [7,14,66,6,21] R(x,f(x),f(x)).
9688 [275,9]       -R(e,f(x),y).
9689 [9688,8630]    F.

<

[figure: I N F O R M A T I K]

Below you find a list of the most recent technical reports of the research group Logic of Programming at the Max-Planck-Institut für Informatik. They are available by anonymous ftp from our ftp server ftp.mpi-sb.mpg.de under the directory pub/papers/reports. If you have any questions concerning ftp access, please contact reports@mpi-sb.mpg.de. Paper copies (which are not necessarily free of charge) can be ordered either by regular mail or by e-mail at the address below.

Max-Planck-Institut für Informatik Library attn. Regina Kraemer Im Stadtwald D-66123 Saarbrücken GERMANY

            e-mail: kraemer@mpi-sb.mpg.de

MPI-I-94-216 P. Barth  Linear 0-1 Inequalities and Extended Clauses
MPI-I-94-209 D. A. Basin, T. Walsh  Termination Orderings for Rippling
MPI-I-94-208 M. Jäger  A probabilistic extension of terminological logics
MPI-I-94-207 A. Bockmayr  Cutting planes in constraint logic programming

MPI-I-94-201 M. Hanus The Integration of Functions into Logic Programming: A Survey

MPI-I-93-267 L. Bachmair, H. Ganzinger  Associative-Commutative Superposition
MPI-I-93-265 W. Charatonik, L. Pacholski  Negativ set constraints: an easy proof of decidability

MPI-I-93-264 Y. Dimopoulos, A. Torres Graph theoretical structures in logic programs and default theories

MPI-I-93-260 D. Cvetković The logic of preference and decision supporting systems

MPI-I-93-257 J. Stuber Computing Stable Models by Program Transformation

MPI-I-93-256 P. Johann, R. Socher  Solving simplifications ordering constraints
MPI-I-93-250 L. Bachmair, H. Ganzinger  Ordered Chaining for Total Orderings
MPI-I-93-249 L. Bachmair, H. Ganzinger  Rewrite Techniques for Transitive Relations
MPI-I-93-243 S. Antoy, R. Echahed, M. Hanus  A needed narrowing strategy
MPI-I-93-237 R. Socher-Ambrosius  A Refined Version of General E-Unification

MPI-I-93-236 L. Bachmair, H. Ganzinger, C. Lynch, W. Snyder

Basic Paramodulation

MPI-I-93-235 D. Basin, S. Matthews A Conservative Extension of First-order Logic and its Application to Theorem Proving

MPI-I-93-234 A. Bockmayr, F. J. Radermacher  Künstliche Intelligenz und Operations Research

MPI-I-93-233 A. Bockmayr, S. Krischer, A. Werner Narrowing Strategies for Arbitrary Canonical Rewrite Systems

MPI-I-93-231 D. Basin, A. Bundy, I. Kraan, S. Matthews A Framework for Program Development Based on Schematic Proof