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

Abstract

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 ℒ(□₁,…,□_n) with a set of formulae Φ, having a usual relational semantics over structures <W,R₁,…,R_n> (frames) and a theory T in some language (for definiteness — first-order) for such structures. We shall denote such a base ℒ_T(R₁,…,R_n). 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 R₁,…,R_n 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₋₁ having a single axiom (−1) ∀xy(R₁xy ↔ R₂yx) and standard frames <W,R,R⁻¹> — it is an enriched modal language for <W,R>. Another example is the language in question. ℒ(R,−R) being a bimodal base with theory T₋ with an axiom (−) ∀xy(R₁xy ↔ −R₂xy) and standard frames <W,R,−R>.