Completeness and Incompleteness in the Bimodal Base ℒ(R,−R)

The paper deals with a modal language ℒ(R,−R), having an ordinary modality ⊞ (dual — S) with an usual Kripke-semantics x⊧⊞ϕ iff ∀y(Rxy ⇒ y⊧ϕ) and an additional modality ⊟ (dual — S), with the same semantics however over the complement −R of R: x⊧⊟ϕ iff ∀y(−Rxy ⇒ y⊧ϕ). Such a modality has been considered by some authors in different contexts — see e.g. [Hum] and [GPT], where the completeness theorems for the minimal normal ℒ(R,−R) — logic are independently proved. This language appears as a special case of the notion polymodal base, introduced by the author in [Gor]. This notion combines a polymodal language ℒ(□1,…,□n) with a set of formulae Φ, having a usual relational semantics over structures (frames) and a theory T in some language (for definiteness — first-order) for such structures. We shall denote such a base ℒT(R1,…,Rn). The models of the theory T will be called standard frames of this base. In particular, when the theory T determines some of the relations R1,…,Rn by means of the rest of them, the polymodal base becomes an enriched [poly]modal language. A typical example of it provides the modal language for tense logics — it is a bimodal base with a theory T−1 having a single axiom (−1) ∀xy(R1xy ↔ R2yx) and standard frames — it is an enriched modal language for . Another example is the language in question. ℒ(R,−R) being a bimodal base with theory T− with an axiom (−) ∀xy(R1xy ↔ −R2xy) and standard frames .