Philippe Balbiani

Martin Diéguez

Here and There modal logic with dual implication

Keywords: modal logic, Here and There logic, dual implication, axiomatization and completeness, Hennessy-Milner property

We define and study an extension of the logic of Here and There with dual implication and modal operators of necessity and possibility. We provide a complete axiomatisation. We prove as well other results such as the interdefinability of modal operators and the Hennessy-Milner property. We give an upper bound to the complexity of the satisfiability problem.

Introduction

In the last twenty years, research on extensions of the logic of Here and There [START_REF] Gödel | Zum intuitionistischen Aussagenkalkül[END_REF][START_REF] Heyting | Die formalen Regeln der intuitionistischen Logik[END_REF][START_REF] Smetanich | On the completeness of the propositional calculus with additional operations in one argument[END_REF] (HT) have been very active due to the advent of Equilibrium Logic [START_REF] Pearce | A new logical characterisation of stable models and answer sets[END_REF][START_REF] Pearce | Equilibrium logic[END_REF], which is considered the best-known logical characterisation of the Stable Models Semantics [START_REF] Gelfond | The stable model semantics for logic programming[END_REF] and Answer Sets Semantics [START_REF] Brewka | Answer set programming at a glance[END_REF] in Logic Programming (LP). Recently, combinations of intermediate and modal logics [START_REF] Balbiani | Temporal Here and There[END_REF][START_REF] Cabalar | Temporal Equilibrium Logic: a first approach[END_REF][START_REF] Del Cerro | Epistemic Equilibrium Logic[END_REF][START_REF] Diéguez | Temporal answer set programming[END_REF][START_REF] Su | Extensions of Equilibrium Logic by Modal Concepts[END_REF] have caught the attention of the LP community since they can support the definition of non-monotonic modal logics [START_REF] Cabalar | Temporal Equilibrium Logic: a first approach[END_REF][START_REF] Balbiani | Temporal Here and There[END_REF]. Extending intermediate logics [START_REF] Mints | A Short Introduction to Intuitionistic Logic[END_REF] (IL) with modalities is not new, since several semantics and properties have been studied about this topic in both philosophy and formal logic [START_REF] Boi | Models for normal intuitionistic modal logics[END_REF][START_REF] Bull | A modal extension of intuitionist logic[END_REF][START_REF] Ono | On Some Intuitionistic Modal Logics[END_REF][START_REF] Servi | On modal logic with an intuitionistic base[END_REF][START_REF] Simpson | The Proof Theory and Semantics of Intuitionistic Modal Logic[END_REF] and computer science [START_REF] Balbiani | Bisimulations for intuitionistic temporal logics[END_REF][START_REF] Boudou | A decidable intuitionistic temporal logic[END_REF][START_REF] Fairtlough | An intuitionistic modal logic with applications to the formal verification of hardware[END_REF][START_REF] Marti | A Hennessy-Milner property for many-valued modal logics[END_REF][START_REF] Plotkin | A framework for intuitionistic modal logics[END_REF].

Also related to IL, several types of negation were considered: for instance, Nelson's Constructive Logic [START_REF] Nelson | Constructible falsity[END_REF] was used by [START_REF] Pearce | Equilibrium logic[END_REF] in order to characterise the strong negation in LP. However, other dual operators of IL 1 have not been considered in the HT setting. More precisely, we focused on the dual implication proposed by C. Rauszer [START_REF] Rauszer | An Algebraic and Kripke-style Approach to a Certain Extension of Intuitionistic Logic[END_REF].

Rauszer proposed an extension of intuitionistic logic equipped with a new implication (denoted by ←) in order to provide "a more elegant algebraic and model-theoretic theory than in ordinary intuitionistic logic" [START_REF] Rauszer | An Algebraic and Kripke-style Approach to a Certain Extension of Intuitionistic Logic[END_REF]. Later on, this new implication was further studied: in [START_REF] Wolter | On Logics with Coimplication[END_REF] this new operator is added to the intuitionistic modal language providing several results such as matrix and Kripke semantics or embeddings into (extended) tense logics. A display calculus unifying intuitionistic and dual-intuitionistic logic was presented in [START_REF] Goré | A Uniform Display System For Intuitionistic And Dual Intuitionistic Logic[END_REF] and refined in [START_REF] Goré | Dual intuitionistic logic revisited[END_REF]. Recently, in [START_REF] Goré | Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic[END_REF], a cut-free sequent calculi in terms of derivations and refutations have been introduced 2 .

In this paper, we have considered the combination of propositional HT with dual implication and modal logic K. On it, we have defined the concept of modal equilibrium model and we study several interesting properties, which can serve as a starting point for future modal extensions. These properties are presented along this paper in the following way. In Section 2, we present syntax and two equivalent alternative semantics based on Kripke models. The former semantics (the "Here and There" semantics) is simulated by two valuation functions while the latter semantics possesses two accessibility relations to interpret implication, dual implication and modal operators. In Section 3 and Section 4, we present an axiomatisation of this logic and we prove its completeness with respect to the birelational semantics. In Section 5, we establish the complexity, in PSPACE, of the satisfiability problem in this logic. In Section 6 we define bisimulations for our BHT -modal extensions and we use them to prove the Hennessy-Milner property. In Section 7 we define the concept of modal equilibrium logic and shows that such definition is suitable for proving the theorem of strong equivalence.

Syntax and semantics

In this section, we present the syntax and the semantics of BHT .

Syntax

Let V AR be a countable set of propositional variables (denoted p, q, etc). The set F OR of all formulas (denoted ϕ, ψ, etc) is defined as follows:

ϕ, ψ ∶∶= p ⊺ (ϕ ∨ ψ) (ϕ ∧ ψ) (ϕ → ψ) (ϕ ← ψ) ◻ϕ ϕ (1)
We follow the standard rules for omission of the parentheses. As in [START_REF] Rauszer | An Algebraic and Kripke-style Approach to a Certain Extension of Intuitionistic Logic[END_REF], two negations can be defined:

¬ϕ def = ϕ → and ⨽ϕ def = ⊺ ← ϕ.
Let ϕ denote the number of symbol occurrences in ϕ. A set Σ of formulas is closed iff it is closed under subformulas and for all formulas ϕ, if ϕ ∈ Σ then ¬ϕ ∈ Σ and ⨽ϕ ∈ Σ. The modal degree of a formula ϕ (in symbols deg(ϕ)) is defined as follows:

deg(ϕ) def = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ 0 if ϕ = p (p ∈ V AR) or ϕ = or ϕ = ⊺ max(deg(ψ), deg(χ)) if ϕ = ψ ⊙ χ, with ⊙ ∈ {∨, ∧, →, ←} 1 + deg(ψ) if ϕ = ⊙ψ, with ⊙ ∈ {◻, }
A theory is a set of formulas. For all theories x, y, we define the theories

◻x def = {ϕ ◻ϕ ∈ x} and y def = { ϕ ϕ ∈ y}.

BHT semantics

Given a nonempty set W and

H, T ∶ V AR → 2 W , we say that H is included in T (in symbols H ≤ T ) iff for all p ∈ V AR, H(p) ⊆ T (p). A BHT -frame is a structure (W, R)
where W is a nonempty set and R is a binary relation on

W . A BHT -model is a structure M = ⟨W, R, H, T ⟩ where (W, R) is a BHT - frame and H, T ∶ V AR → 2 W are such that H ≤ T . Given a BHT -model M = ⟨W, R, H, T ⟩, x ∈ W ,
and α ∈ {h, t}, interpreting , ⊺, ∨ and ∧ as usual, the satisfaction of a formula ϕ at (x, α) in M (in symbols M, (x, α) ⊧ ϕ) is defined as follows:

• M, (x, h) ⊧ p iff x ∈ H(p) and M, (x, t) ⊧ p iff x ∈ T (p), • M, (x, α) ⊧ ϕ → ψ iff for all α ′ ∈ {α, t}, M, (x, α ′ ) ⊧ ϕ, or M, (x, α ′ ) ⊧ ψ, • M, (x, α) ⊧ ϕ ← ψ iff there exists α ′ ∈ {h, α} such that M, (x, α ′ ) ⊧ ϕ and M, (x, α ′ ) ⊧ ψ, • M, (x, α) ⊧ ◻ϕ iff for all y ∈ W , if xR y then M, (y, α) ⊧ ϕ,
• M, (x, α) ⊧ ϕ iff there exists y ∈ W such that xR y and M, (y, α) ⊧ ϕ. As a result, M, (x, α) ⊧ ¬ϕ iff for all α ′ ∈ {α, t}, M, (x, α ′ ) ⊧ ϕ and M, (x, α) ⊧ ⨽ϕ iff there exists α ′ ∈ {h, α} such that M, (x, α ′ ) ⊧ ϕ. Notice that if H = T then the satisfaction relation is essentially the same as the satisfaction relation used in classical modal logic [START_REF] Chagrov | Modal Logic[END_REF]. We say that the formulas ϕ and ψ are BHTequivalent (in symbols ϕ ≃ ψ) iff for all BHT models M = ⟨W, R, H, T ⟩, for all x ∈ W and for all α ∈ {h, t}, M, (x, α) ⊧ ϕ iff M, (x, α) ⊧ ψ. The satisfaction of a theory Γ at (x, α) in M (in symbols M, (x, α) ⊧ Γ) is defined as usual. Two theories Γ 1 and Γ 2 are BHT -equivalent (in symbols Γ 1 ≃ Γ 2 ) iff for all BHT models M = ⟨W, R, H, T ⟩, for all x ∈ W and for all α ∈ {h, t}, M, (x, α)

⊧ Γ 1 iff M, (x, α) ⊧ Γ 2 .
Lemma 2.1 Let ϕ be a formula. For all BHT -models M = ⟨W, R, H, T ⟩ and for all x ∈ W , if M, (x, h) ⊧ ϕ then M, (x, t) ⊧ ϕ.

As a result, for arbitrary

x ∈ W and α ∈ {h, t}, M, (x, α) ⊧ ¬ϕ iff M, (x, t) ⊧ ϕ and M, (x, α) ⊧ ⨽ϕ iff M, (x, h) ⊧ ϕ. Hence, M, (x, t) ⊧ ϕ ∨ ¬ϕ and M, (x, h) ⊧ ϕ∧⨽ϕ. Remark also that M, (x, α) ⊧ ¬¬ϕ iff M, (x, t) ⊧ ϕ and M, (x, α) ⊧ ⨽⨽ϕ iff M, (x, h) ⊧ ϕ.
A formula ϕ is said to be satisfiable iff there exists a BHT model M = ⟨W, R, H, T ⟩, there exists x ∈ W and there exists α ∈ {h, t} such that M, (x, α) ⊧ ϕ. A formula ϕ is said to be valid iff for all BHT models M = ⟨W, R, H, T ⟩, for all x ∈ W and for all α ∈ {h, t}, M, (x, α) ⊧ ϕ. In order to grasp the differences between ¬ and ⨽, let us notice that, although p ∨ ¬p is not valid and p ∧ ⨽p is satisfiable, we have ϕ ∨ ⨽ϕ is valid and ϕ ∧ ¬ϕ is not satisfiable for arbitrary formula ϕ. In other respect, by Lemma 2.1, one can readily conclude that ϕ is valid iff for all BHT models M = ⟨W, R, H, T ⟩ and for all x ∈ W , M, (x, h) ⊧ ϕ and ϕ is not satisfiable iff for all BHT models M = ⟨W, R, H, T ⟩ and for all x ∈ W , M, (x, t) ⊧ ϕ. It can be easily checked that if a formula ϕ is not satisfiable then ¬ϕ is valid and if ϕ is valid then ⨽ϕ is not satisfiable. Finally, remark that for all formulas ϕ, ψ, ϕ → ψ is valid iff ϕ ← ψ is not satisfiable.

Lemma 2.2

The following formulas are valid:

1) Standard axioms of Intuitionistic Propositional Calculus (IP C):

• ϕ → (ψ → ϕ), • (ϕ → (ψ → χ)) → ((ϕ → ψ) → (ϕ → χ)), • (ϕ → χ) → ((ψ → χ) → (ϕ ∨ ψ → χ)), • ϕ → ϕ ∨ ψ, • ψ → ϕ ∨ ψ, • ϕ ∧ ψ → ϕ, • ϕ ∧ ψ → ψ, • ϕ → (ψ → ϕ ∧ ψ), • → ϕ,
2) Hosoi formula [START_REF] Hosoi | The Axiomatization of the Intermediate Propositional Systems S 2 of Gödel[END_REF]: ϕ ∨ (ϕ → ψ) ∨ ¬ψ, 3) Fisher Servi axioms: [START_REF] Boudou | A decidable intuitionistic temporal logic[END_REF] Additional formulas:

• ◻(ϕ → ψ) → (◻ϕ → ◻ψ), • ◻(ϕ → ψ) → ( ϕ → ψ), • (ϕ ∨ ψ) → ϕ ∨ ψ, • ( ϕ → ◻ψ) → ◻(ϕ → ψ), • ¬ ,
• ϕ → (ϕ ← ψ) ∨ ψ, • ϕ ∨ ⨽ϕ,
• ¬ϕ ∨ ¬¬ϕ,

• ⨽ (ϕ ∧ ⨽ϕ),

• ¬¬ ◻ ϕ → ◻¬¬ϕ and ¬¬ϕ → ¬¬ ϕ,

• ⨽⨽ ◻ ϕ → ◻⨽⨽ϕ and ⨽⨽ϕ → ⨽⨽ ϕ.

Lemma 2.3

The following formulas are valid:

1) Negation-dual of standard axioms of Intuitionistic Logic:

• ¬((ϕ ← ψ) ← ϕ), • ¬(((χ ← ϕ) ← (ψ ← ϕ)) ← ((χ ← ψ) ← ϕ)), • ¬(((χ ← ψ ∧ ϕ) ← (χ ← ψ)) ← (χ ← ϕ)), • ¬(ψ ∧ ϕ ← ϕ), • ¬(ψ ∧ ϕ ← ψ), • ¬(ϕ ← ψ ∨ ϕ), • ¬(ψ ← ψ ∨ ϕ), • ¬((ψ ∨ ϕ ← ψ) ← ϕ), • ¬(ϕ ← ⊺).
2) Negation-dual of Hosoi formula: ¬(⨽ψ ∧ (ψ ← ϕ) ∧ ϕ), 3) Negation-dual of Fisher Servi axioms:

• ¬(( ψ ← ϕ) ← (ψ ← ϕ)), • ¬((◻ψ ← ◻ϕ) ← (ψ ← ϕ)), • ¬(◻ψ ∧ ◻ϕ ← ◻(ψ ∧ ϕ)), • ¬( (ψ ← ϕ) ← ( ψ ← ◻ϕ)), • ¬⨽ ◻ ⊺, 4
) Negation-dual of additional formulas:

• ¬(ψ ∧ (ψ → ϕ) ← ϕ),
• ¬(¬ϕ ∧ ϕ),

• ¬(⨽⨽ϕ ∧ ⨽ϕ),

• ¬¬ ◻ (¬ϕ ∨ ϕ),

• ¬( ⨽⨽ϕ ← ⨽⨽ ϕ) and ¬(⨽⨽ ◻ ϕ ← ◻⨽⨽ϕ),

• ¬( ¬¬ϕ ← ¬¬ ϕ) and ¬(¬¬ ◻ ϕ ← ◻¬¬ϕ).

From now on, the set of all valid formulas is denoted BHT .

Lemma 2.4 In the following tables, the formulas on the left are BHTequivalent to the corresponding formulas on the right. In most modal extensions of intuitionistic logic, ◻ and are non-interdefinable. Within the context of BHT , this is no longer the case.

¬ (ϕ ∨ ψ) ¬ϕ ∧ ¬ψ ¬ (ϕ ∧ ψ) ¬ϕ ∨ ¬ψ ⨽ (ϕ ∨ ψ) ⨽ϕ ∧ ⨽ψ ⨽ (ϕ ∧ ψ) ⨽ϕ ∨ ⨽ψ ¬ (ϕ → ψ) ¬¬ϕ ∧ ¬ψ ¬ (ϕ ← ψ) ¬ϕ ∨ ⨽⨽ψ ∨ (⨽ϕ ∧ ¬¬ψ) ⨽ (ϕ → ψ) ¬¬ϕ ∧ ⨽ψ ∧ (⨽⨽ϕ ∨ ¬ψ) ⨽ (ϕ ← ψ) ⨽ϕ ∨
Lemma 2.6 In the following table, the formulas on the left are BHTequivalent to the corresponding formulas on the right.

◻ϕ (ϕ ∧ ⨽ϕ) ∨ ⨽ ⨽ϕ ← ¬ϕ ◻ϕ (¬ (ϕ ∧ ⨽ϕ) ∨ (ϕ ∧ ⨽ϕ) ∨ ⨽ ⨽ϕ) ∧ ¬ ¬ϕ ϕ ◻⨽ϕ → ¬ ◻ ¬ϕ ∧ ◻(ϕ ∨ ¬ϕ) ϕ ⨽ ◻ ⨽ϕ ∨ (¬ ◻ ¬ϕ ∧ ◻(ϕ ∨ ¬ϕ) ∧ ⨽ ◻ (ϕ ∨ ¬ϕ))

Birelational semantics

A standard approach in the semantics of a modal intuitionistic logic is to consider structures based on a partial order and a binary relation [START_REF] Simpson | The Proof Theory and Semantics of Intuitionistic Modal Logic[END_REF]. A birelational frame is a structure (W, ≤, R) where W is a nonempty set, ≤ is a partial order on W and R is a binary relation on W . A birelational frame (W, ≤, R) is normal iff it satisfies the following conditions for all x, y, z ∈ W :

1) if x ≤ y and x ≤ z then x = y, or x = z, or y = z, 2) if x ≤ z and y ≤ z then x = y, or x = z, or y = z.
As a result, if (W, ≤, R) is normal then for all x ∈ W , x is a maximal element with respect to ≤, or there exists exactly one y ∈ W such that x ≤ y and x = y.

In the former case let x denote x. In the latter case, let x denote this y. From this definition, it follows that for all x, y ∈ W , x ≤ y iff y = x, or y = x. Similarly, if (W, ≤, R) is normal then for all x ∈ W , x is a minimal element with respect to ≤, or there exists exactly one y ∈ W such that y ≤ x and x = y. In the former case, let q x denote x. In the latter case, let q x denote this y. From this definition it follows that for all x, y ∈ W , y ≤ x iff x = y, or q x = y. Obviously, for all

x ∈ W , q x = x and q x = q x. A normal birelational frame (W, ≤, R) is Cartesian iff it satisfies the following conditions for all x, y ∈ W : 1) if q xRy then q y = y and xRŷ, 2) if xRy then ŷ = y and q xRq y.

Lemma 2.7 Let (W, ≤, R) be a Cartesian birelational frame. For all x, y ∈ W , if xRy then xRŷ and q xRq y.

A birelational model is a structure ⟨W, ≤, R, V ⟩ where (W, ≤, R) is a birelational frame and V ∶ V AR → 2 W is such that for all x, y ∈ W , if x ≤ y then for all p ∈ V AR, if x ∈ V (p) then y ∈ V (p)
. Given a birelational model M = ⟨W, ≤, R, V ⟩ and x ∈ W , interpreting , ⊺, ∨ and ∧ as usual, the satisfaction of a formula ϕ at x in M (in symbols M, x ⊧ ϕ) is defined as follows:

(i) M, x ⊧ p iff x ∈ V (p), (ii) M, x ⊧ ϕ → ψ iff for all y ∈ W if x ≤ y then M, y ⊧ ϕ, or M, y ⊧ ψ, (iii) M, x ⊧ ϕ ← ψ iff there exists y ∈ W such that y ≤ x, M, y ⊧ ϕ and M, y ⊧ ψ, (iv) M, x ⊧ ◻ϕ iff for all y, z ∈ W , if x ≤ y and yR z then M, z ⊧ ϕ, (v)

Equivalence between the two semantics

In this section, we prove that a formula is satisfiable (respectively, valid) in the BHT semantics iff it is satisfiable (respectively, valid) in the birelational semantics. Let M = ⟨W, R , H, T ⟩ be a BHT model. We define the birelational model

M ′ = ⟨W ′ , ≤ ′ , R ′ , V ′ ⟩ as follows: 1) W ′ = W × {h, t}, 2) (x, α) ≤ ′ (y, β) iff x = y and α = h, or β = t, 3) (x, α)R ′ (y, β) iff xR y and α = β, 4) V ′ (p) = {(x, h) ∶ x ∈ H(p)} ∪ {(x, t) ∶ x ∈ T (p)}.
The reader can easily check that M ′ satisfies the conditions to be normal. Moreover, the reader can check that for all (x, α) ∈ W ′ , (x, α) = (x, h), and

(x, α) = (x, t). Let us prove that M ′ is Cartesian. Let us consider (x, α) and (y, β) in W ′ satisfying (x, α)R ′ (y, β)
. By definition, (x, h)R ′ (y, β), so xRy and β = h. Again, by definition (y, β) = (y, β). Assume that not (x, α)R ′ (y, β), By definition not (x, t)R ′ (y, t). By definition we conclude not xRy: a contradiction. Therefore (x, α)R ′ (y, β). Let us consider now (x, α) and (y, β) in W ′ satisfying (x, α)R ′ (y, β). By definition, (x, t)R ′ (y, β), so xRy and β = t. Again, by definition (y, β) = (y, β). Assume that not (x, α)R ′ (y, β), By defi-nition not (x, h)R ′ (y, h). By definition we conclude not xRy: a contradiction. Therefore (x, α)R ′ (y, β). Finally, we can prove the following correspondence between M and M ′ . Lemma 2.8 Let ϕ be a formula. For all x ∈ W and for all α ∈ {h, t},

M, (x, α) ⊧ ϕ iff M ′ , (x, α) ⊧ ϕ.
Proof. By induction on ϕ. In the case of a propositional variable p, if

M, (x, h) ⊧ p then x ∈ H(p) so, by definition, (x, h) ∈ V (p), so M ′ , (x, h) ⊧ p. If M, (x, t) ⊧ p then x ∈ T (p) so, by definition, (x, t) ∈ V (p), so M ′ , (x, t) ⊧ p.
The converse direction is proved in a similar way. Also, the cases of conjunction and disjunction are proved by using the induction hypothesis. We consider the operators → and ◻ below:

• Case ϕ → ψ: from left to right, assume by contradiction that M ′ , (x, α) ⊧ ϕ → ψ. Therefore, there exists (y, β) ∈ W ′ such that (x, α) ≤ ′ (y, β) and M ′ , (y, β) ⊧ ϕ and M ′ , (y, β) ⊧ ψ. By induction hypothesis we get that M, (y, β) ⊧ ϕ → ψ. By definition x = y and either α = h or

β = t. If α = h then there exists β ∈ {h, t}, M, (x, β) ⊧ ϕ → ψ, so M, (x, α) ⊧ ϕ → ψ: a contradiction. If β = t then for all α ∈ {h, t}, M, (x, α) ⊧ ϕ → ψ: a contradiction. For the converse direction, let us consider M, (x, α) ⊧ ϕ → ψ. Therefore there exists some β ∈ {α, t}, M, (x, β) ⊧ ϕ and M, (x, β) ⊧ ψ. By induction M ′ , (x, β) ⊧ ϕ and M ′ , (x, β) ⊧ ψ. Therefore M ′ , (x, β) ⊧ ϕ → ψ. If β = α we get M ′ , (x, α) ⊧ ϕ → ψ : a contradiction. If β = t then (x, α) ≤ ′ (x, β) and M ′ , (x, β) ⊧ ϕ → ψ: a contradiction.
• Case ◻ψ: from left to right, assume by contradiction that M ′ , (x, α) ⊧ ◻ψ. This means that there exists (x ′ , β) and (y, γ) in W ′ such that (x, α) ≤ ′ (x ′ , β)R ′ (y, γ) and M ′ , (y, γ) ⊧ ϕ. By induction M, (x, γ) ⊧ ψ. By definition x ′ Ry and γ = β (so M, (x ′ , β) ⊧ ◻ψ). Again, by definition x = x ′ and either β = t or α = h. Any of the cases leads to M, (x, α) ⊧ ◻ψ. Conversely, assume by contradiction that M, (x, α) ⊧ ◻ψ. Therefore M, (y, α) ⊧ ψ for some xRy. By induction M ′ , (y, α) ⊧ ψ. By definition (x, α)R ′ (y, α) and

(x, α) ≤ ′ (x, α), so M ′ , (x, α) ⊧ ◻ψ. ◻ Let M = ⟨W, ≤, R, V ⟩ be a Cartesian birelational model. We define the BHT model M ′ = ⟨W ′ , R ′ , H ′ , T ′ ⟩ as follows: 1) W ′ = {(q x, x) x ∈ W }, 2) (q x, x)R ′ (q y, ŷ) iff q xRq y and xRŷ, 3) H ′ (p) = {(q x, x) ∶ q x ∈ V (p)}, 4) T ′ (p) = {(q x, x) ∶ x ∈ V (p)}.
Take (q x, x) ∈ H ′ (p). By definition q x ∈ V (p). Since q x ≤ x then, by definition, x ∈ V (p). Finally, by definition, (q x, x) ∈ T ′ (p). Thus, H ′ ≤ T ′ . Moreover, the following result relates birelational and BHT semantics. Lemma 2.9 Let ϕ be a formula. For all x ∈ W ,

1) M, q x ⊧ ϕ iff M ′ , ((q x, x), h) ⊧ ϕ, 2) M, x ⊧ ϕ iff M ′ , ((q x, x), t) ⊧ ϕ.
Proof. By induction on ϕ. For the case of a propositional variable p we get that if M, q x ⊧ p then q x ∈ V (p) and, by definition, (q x, x) ∈ H ′ (p). Therefore, M ′ , ((q x, x), h) ⊧ p. The converse direction follows a similar reasoning. If M, x ⊧ p then x ∈ V (p) and, by definition, (q x, x) ∈ T ′ (p). Therefore, M ′ , ((q x, x), t) ⊧ p. The converse direction follows a similar reasoning. The cases of conjunction and disjunction are proved by induction. We present the proof for the → and ◻ connectives below:

• Case ϕ → ψ: from M, q x ⊧ ϕ → ψ then for all x ′ ∈ {q x, x}, either M, x ′ ⊧ ϕ or M, x ′ ⊧ ψ.
From the induction hypothesis we get that for all α ∈ {h, t}, M ′ , ((q x, x), α) ⊧ ϕ or M ′ , ((q x, x), α) ⊧ ψ, so M ′ , ((q x, x), α) ⊧ ϕ → ψ. The converse direction and the second part of the theorem are proved in a similar way.

• Case ◻ψ: in the first case, assume by contradiction that M ′ , ((q x, x), h) ⊧ ◻ψ. Therefore, M ′ , ((q y, ŷ), h) ⊧ ψ for some (q y, ŷ) ∈ W ′ satisfying (q x, x)R ′ (q y, ŷ). By induction hypothesis M, q y ⊧ ψ. By definition, q xRq y. Therefore, M, q

x ⊧ ◻ψ: a contradiction. Conversely, assume by contradiction that M, q

x ⊧ ◻ψ. Therefore there exists y ∈ W such that q x ≤ x ′ Ry and M, y ⊧ ψ. If x ′ = q

x, we use the first condition of being Cartesian to conclude that q y = y (so q xRq y) and xRŷ. By definition (q x, x)R ′ (q y, ŷ). By induction M ′ , ((q y, ŷ), h) ⊧ ψ. Therefore M ′ , ((q x, x), h) ⊧ ◻ψ. If x ′ = x, we use the second condition of being Cartesian to conclude that ŷ = y (so xRŷ) and q xRq y. By definition (q x, x)R ′ (q y, ŷ). By induction M ′ , ((q y, ŷ), t) ⊧ ψ. Therefore M ′ , ((q x, x), t) ⊧ ◻ψ. By Lemma 2.1, M ′ , ((q x, x), h) ⊧ ◻ψ. The proof of the second second item is similar. ◻ Proposition 2.10 For any modal formula ϕ, ϕ is satisfiable (respectively, valid) in the class of all BHT -frames iff ϕ is satisfiable (respectively, valid) in the class of all Cartesian birelational frames.

Axiomatisation

The axiomatic system of BHT consists of the formulas considered in Lemmas 2.2 and 2.3 plus the following inference rules:

M P ϕ ϕ→ψ ψ , N ec ϕ ◻ϕ , M R → χ∧ψ→ϕ χ→(ψ→ϕ) , M R ← ϕ→ψ∨χ (ϕ←ψ)→χ , M R ◻ ϕ→ψ∨χ ◻ϕ→ ψ∨◻χ , M R χ∧ψ→ϕ ◻χ∧ ψ→ ϕ .
The notion of BHT -derivability is defined as usual.

Lemma 3.1 ⊺ is derivable in BHT . Proof. Notice that ⊺ is valid in IP C (in fact it is equivalent to ¬ ). Since IP C ⊆ BHT we conclude that ⊺ is derivable in BHT . ◻ Proposition 3.2 (Soundness)
Let ϕ be a formula. If ϕ is BHT -derivable then ϕ is valid in the class of all BHT -model.

Proof. It suffices to check that all axioms are valid and the inference rules preserve validity. ◻ Let x, y be theories. We say that x derives y (in symbols x ⊢ y) iff there exists m, n ≥ 0, there exists formulas ϕ 1 , . . . , ϕ m ∈ x and there exists formulas

ψ 1 , . . . , ψ n ∈ y such that ϕ 1 ∧ . . . ∧ ϕ m → ψ 1 ∨ . . . ∨ ψ n is BHT -derivable.

Completeness

We base our proof of completeness on the canonical model construction.

Tableaux

A tableau is a couple of theories. We say that a tableau (x, y) is consistent iff x ⊢ y. The tableau (x, y) is said to be maximal iff for all formulas ϕ, ϕ ∈ x, or ϕ ∈ y. We say that a tableau (x, y) is disjoint iff x ∩ y = ∅. The tableau (x, y) is said to be saturated iff ∈ y, ⊺ ∈ x and for all formulas ϕ, ψ,

(i) if ϕ ∨ ψ ∈ x then ϕ ∈ x, or ψ ∈ x, (ii) if ϕ ∨ ψ ∈ y then ϕ ∈ y and ψ ∈ y, (iii) if ϕ∧ψ ∈ x then ϕ ∈ x and ψ ∈ x, (iv) if ϕ ∧ ψ ∈ y then ϕ ∈ y, or ψ ∈ y, (v) if ϕ → ψ ∈ x then ϕ ∈ y, or ψ ∈ x, (vi) if ϕ ← ψ ∈ y then ϕ ∈ y, or ψ ∈ x.
Lemma 4.1 Every consistent tableau is disjoint.

Thus, if (x, y), (x ′ , y ′ ) are maximal consistent tableaux then x ⊆ x ′ iff y ⊇ y ′ .

Lemma 4.2 (Lindenbaum Lemma) Let (x, y) be a tableau. If (x, y) is consistent then there exists a maximal consistent tableau (x ′ , y ′ ) such that x ⊆ x ′ and y ⊆ y ′ .

Lemma 4.3 If (x, y) is a maximal consistent tableau then x contains the set of all BHT -derivable formulas and x is closed under the rule M P . Moreover, x and y constitute a partition of the set of all formulas.

Lemma 4.4 Every maximal consistent tableau is saturated.

Proof. Let (x, y) be a maximal consistent tableau. We demonstrate (x, y) is saturated, which amounts to prove that conditions (i)-(vi) of the definition of saturated tableaux are satisfied. We only present the proof for conditions (v) and (vi). Suppose ϕ → ψ ∈ x, ϕ ∈ y and ψ ∈ x. Since (x, y) is maximal consistent, therefore ϕ → ψ ∈ y and ψ ∈ y. Moreover, ϕ ∧ (ϕ → ψ) ← ψ is in y. Since ψ ∈ y, therefore ϕ ∧ (ϕ → ψ) ∈ y (otherwise, we would obtain x ⊢ y which contradicts the maximal consistency of (x, y)). Hence, ϕ ∈ y, or ϕ → ψ ∈ y. Since ϕ ∈ y, therefore ϕ → ψ ∈ y: a contradiction. Suppose ϕ ← ψ ∈ y, ϕ ∈ y and ψ ∈ x. Since (x, y) is maximal consistent, therefore ϕ ← ψ ∈ x and ϕ ∈ x. Moreover, ϕ → (ϕ ← ψ) ∨ ψ is in x. Since ϕ ∈ x, therefore (ϕ ← ψ) ∨ ψ ∈ x (otherwise, we would obtain x ⊢ y which contradicts the maximal consistency of (x, y)). Hence, ϕ ← ψ ∈ x, or ψ ∈ x. Since ψ ∈ x, therefore ϕ ← ψ ∈ x: a contradiction. ◻ Lemma 4.5 (Hosoi Lemma) Let (x, y), (x ′ , y ′ ) and (x ′′ , y ′′ ) be maximal consistent tableaux. if x ⊆ x ′ and x ⊆ x ′′ then x = x ′ , or x = x ′′ , or x ′ = x ′′ .

Proof. Suppose x ⊆ x ′ , x ⊆ x ′′ , x = x ′ , x = x ′′ and x ′ = x ′′ . Without loss of generality, suppose x ′ ⊆ x ′′ . Let ϕ be a formula such that ϕ ∈ x ′ and ϕ ∈ x ′′ . Since x ⊆ x ′ , therefore ¬ϕ ∈ x (otherwise, we would obtain ϕ ∧ ¬ϕ ∈ x ′ which contradicts the maximal consistency of (x ′ , y ′ )). Since x ⊆ x ′′ and x = x ′′ , therefore let ψ be a formula such that ψ ∈ x and ψ

∈ x ′′ . Since (x, y) is maximal consistent, therefore ψ ∨ (ψ → ϕ) ∨ ¬ϕ (Hosoi axiom) is in x. Hence, ψ ∈ x, or ψ → ϕ ∈ x, or ¬ϕ ∈ Since ¬ϕ ∈ x and ψ ∈ x, therefore ψ → ϕ ∈ x. Since x ⊆ x ′′ , therefore ψ → ϕ ∈ x ′′ . Since ψ ∈ x ′′ , therefore ϕ ∈ x ′′ : a contradiction. ◻ Lemma 4.6 (Negation-dual of Hosoi Lemma) Let (x, y), (x ′ , y ′ ) and (x ′′ , y ′′ ) be maximal consistent tableaux. if x ⊇ x ′ and x ⊇ x ′′ then x = x ′ , or x = x ′′ , or x ′ = x ′′ . Proof. Suppose x ⊇ x ′ , x ⊇ x ′′ , x = x ′ , x = x ′′ and x ′ = x ′′ . Without loss of generality, suppose x ′ ⊇ x ′′ .
Let ϕ be a formula such that ϕ ∈ x ′ and ϕ ∈ x ′′ . Since x ⊇ x ′ , therefore ⨽ϕ ∈ x (otherwise, we would obtain ϕ ∨ ⨽ϕ ∈ x ′ which contradicts the maximal consistency of (x ′ , y ′ )). Since x ⊇ x ′′ and x = x ′′ , therefore let ψ be a formula such that ψ ∈ x and ψ ∈ x ′′ . Since (x, y) is maximal consistent, therefore ¬(⨽ϕ ∧ (ϕ ← ψ) ∧ ψ) (dual of Hosoi axiom) is in x and ⨽ϕ ∧ (ϕ ← ψ) ∧ ψ is not in x. Hence, ⨽ϕ ∈ x, or ϕ ← ψ ∈ x, or ψ ∈ x. Since ⨽ϕ ∈ x and ψ ∈ x, therefore ϕ ← ψ ∈ x. Since x ⊇ x ′′ , therefore ϕ ← ψ ∈ x ′′ . Since ψ ∈ x ′′ , therefore ϕ ∈ x ′′ : a contradiction. ◻

Canonical model

The canonical model M c is defined as the structure M c = ⟨W c , ≤ c , R c , V c ⟩ where:

• W c is the set of all maximal consistent tableaux,

• ≤ c is defined by (x, y) ≤ c (x ′ , y ′ ) iff x ⊆ x ′ and y ⊇ y ′ , • R c is defined by (x, y)R c (x ′ , y ′ ) iff ◻x ⊆ x ′ and x ⊇ x ′ , • V c ∶ V AR → 2 Wc is defined by (x, y) ∈ V c (p) iff p ∈ x, Lemma 4.7 M c is normal. Lemma 4.8 M c is Cartesian. Proof. Suppose M c is not Cartesian. Let (x, y), (x ′ , y ′ ) ∈ W c be such that (x, y)R c (x ′ , y ′ ) and (x ′ , y ′ ) = (x ′ , y ′ ), or (x, y)R c (x ′ , y ′ ) and not (x, y)R c (x ′ , y ′ ), or (x, y)R c (x ′ , y ′ ) and (x ′ , y ′ ) = (x ′ , y ′ ), or (x, y)R c (x ′ , y ′ ) and not (x, y)R c (x ′ , y ′ ). Let x ↓ , x ↑ , y ↓ , y ↑ , x ′ ↓ , x ′ ↑ , y ′ ↓ and y ′ ↑ be the- ories such that (x, y) = (x ↓ , y ↓ ), (x, y) = (x ↑ , y ↑ ), (x ′ , y ′ ) = (x ′ ↓ , y ′ ↓ ) and (x ′ , y ′ ) = (x ′ ↑ , y ′ ↑ ). Suppose (x, y)R c (x ′ , y ′ ) and (x ′ , y ′ ) = (x ′ , y ′ ). Let ϕ be a formula such that ϕ ∈ x ′ and ϕ ∈ x ′ ↓ . Since ϕ ∨ ⨽ϕ is derivable, therefore ⨽ϕ ∈ x ′ ↓ . Hence, ⨽ϕ ∈ x ′ . Since ϕ ∈ x ′ , therefore ϕ ∧ ⨽ϕ ∈ x ′ . Since (x, y)R c (x ′ , y ′ ), therefore (ϕ ∧ ⨽ϕ) ∈ x ↓ . Thus, ⨽⨽ (ϕ ∧ ⨽ϕ) ∈ x ↓ . Consequently, ⨽ (ϕ ∧ ⨽ϕ) ∈ x ↓
(otherwise we would obtain ⨽ (ϕ ∧ ⨽ϕ) ∧ ⨽⨽ (ϕ ∧ ⨽ϕ) ∈ x ↓ which contradicts the maximal consistency of (x ↓ , y ↓ )). Hence, ⨽ (ϕ ∧ ⨽ϕ) is not derivable: a contradiction.

Suppose (x, y)R c (x ′ , y ′ ) and not (x, y)R c (x ′ , y ′ ). Let ϕ be a formula such that ◻ϕ ∈ x ↑ and ϕ ∈ x ′ ↑ , or ϕ ∈ x ↑ and ϕ ∈ x ′ ↑ . In the former case, ¬¬◻ϕ

∈ x ↓ . Since ¬¬ ◻ ϕ → ◻¬¬ϕ is derivable, therefore ◻¬¬ϕ ∈ x ↓ . Since (x, y)R c (x ′ , y ′ ), therefore ¬¬ϕ ∈ x ′ . Hence, ϕ ∈ x ′ ↑ : a contradiction. In the latter case, ¬¬ϕ ∈ x ′ . Since (x, y)R c (x ′ , y ′ ), therefore ¬¬ϕ ∈ x ↓ . Since ¬¬ϕ → ¬¬ ϕ is derivable, therefore ¬¬ ϕ ∈ x ↓ . Thus, ϕ ∈ x ↑ : a contradiction.
The cases when (x, y)R c (x ′ , y ′ ) and (x ′ , y ′ ) = (x ′ , y ′ ), or (x, y)R c (x ′ , y ′ ) and not (x, y)R c (x ′ , y ′ ) are addressed in a similar way. ◻

Truth Lemma

We prepare ourselves for the prof of the Truth Lemma.

Lemma 4.9 Let ϕ, ψ be formulas. Let (x, y) be a maximal consistent tableau. If ϕ → ψ ∈ y then there exists a maximal consistent tableau

(x ′ , y ′ ) such that x ⊆ x ′ , ϕ ∈ x ′ and ψ ∈ y ′ .
Proof. Suppose ϕ → ψ ∈ y. Let x ′ = x ∪ {ϕ} and y ′ = {ψ}. Suppose the tableau (x ′ , y ′ ) is not consistent. Let n ≥ 0 and χ 1 , . . . , χ n ∈ x ′ be such that χ 1 ∧ . . . ∧ χ n → ψ is BHT -derivable. There are 2 cases: there exists a positive integer i ≤ n such that χ i = ϕ, or such integer does not exist. In the former case, since χ 1 ∧ . . . ∧ χ n → ψ is BHT -derivable, therefore χ ∧ ϕ → ψ is BHT -derivable where χ is the conjunction of the formulas in χ 1 , . . . , χ n which are not equal to ϕ. Hence, by M R → , χ → (ϕ → ψ) is BHT -derivable: a contradiction with the consistency of (x, y). In the latter case, since

χ 1 ∧ . . . ∧ χ n → ψ is BHT - derivable, therefore χ 1 ∧ . . . ∧ χ n → (ϕ → ψ) is BHT -derivable: a contradiction
with the consistency of (x, y). Consequently, the tableau (x ′ , y ′ ) is consistent. By Lindenbaum Lemma, let (x ′′ , y ′′ ) be a maximal consistent tableau such that x ′ ⊆ x ′′ and y ′ ⊆ y ′′ . Obviously, ϕ ∈ x ′′ and ψ ∈ y ′′ . Moreover, x ⊆ x ′′ . ◻ Lemma 4.10 Let ϕ, ψ be formulas. Let (x, y) be a maximal consistent tableau. If ϕ ← ψ ∈ x then there exists a maximal consistent tableau

(x ′ , y ′ ) such that x ⊇ x ′ , ϕ ∈ x ′ and ψ ∈ y ′ .
Proof. Suppose ϕ ← ψ ∈ x. Let x ′ = {ϕ} and y ′ = y ∪ {ψ}. Suppose the tableau (x ′ , y ′ ) is not consistent. Let n ≥ 0 and χ 1 , . . . , χ n ∈ y ′ be such that ϕ → χ 1 ∨ . . . ∨ χ n is BHT -derivable. There are 2 cases: there exists a positive integer i ≤ n such that χ i = ψ, or such integer does not exist. In the former case, since ϕ → χ 1 ∨ . . . ∨ χ n is BHT -derivable, therefore ϕ → χ ∨ ψ is BHTderivable where χ is the disjunction of the formulas in χ 1 , . . . , χ n which are not equal to ψ. Hence, by M R ← , (ϕ ← ψ) → χ is BHT -derivable: a contradiction with the consistency of (x, y). In the latter case, since ϕ → χ 1 ∨ . . . ∨ χ n is BHT -derivable, therefore (ϕ ← ψ) → χ is BHT -derivable: a contradiction with the consistency of (x, y). Consequently, the tableau (x ′ , y ′ ) is consistent. By Lindenbaum Lemma, let (x ′′ , y ′′ ) be a maximal consistent tableau such that x ′ ⊆ x ′′ and y ′ ⊆ y ′′ . Obviously, ϕ ∈ x ′′ and ψ ∈ y ′′ . Moreover, x ⊇ x ′′ . ◻ Lemma 4.11 Let ϕ be a formula. Let (x, y) be a maximal consistent tableau.

If ◻ϕ ∈ y then there exists a maximal consistent tableau (x ′ , y ′ ) such that ◻x ⊆ x ′ , x ⊇ x ′ and ϕ ∈ y ′ .

Proof. Suppose ◻ϕ ∈ y. Let x ′ = ◻x and y ′ = {χ ∶ χ ∈ y} ∪ {ϕ}. Suppose the tableau (x ′ , y ′ ) is not consistent. Let m, n ≥ 0, ψ 1 , . . . , ψ m ∈ x ′ and χ 1 , . . . , χ n ∈ y ′ be such that ψ 1 ∧. . .∧ψ m → χ 1 ∨. . .∨χ n is BHT -derivable. There are 2 cases: there exists a positive integer i ≤ n such that χ i = ϕ, or such integer does not exist. In the former case, since ψ 1 ∧ . . . ∧ ψ m → χ 1 ∨ . . . ∨ χ n is BHT -derivable, therefore ψ → χ∨ϕ is BHT -derivable where ψ is the conjunction of the formulas in ψ 1 , . . . , ψ m and χ is the disjunction of the formulas in χ 1 , . . . , χ n which are not equal to ϕ. Hence, by M R ◻ , ◻ψ → χ ∨ ◻ϕ is BHT -derivable: a contradiction with the consistency of (x, y). In the latter case, since ψ 1 ∧. . .∧ψ m → χ 1 ∨. . .∨χ n is BHT -derivable, therefore ψ → χ∨ϕ is BHT -derivable. Hence, ◻ψ → χ∨◻ϕ is BHT -derivable: a contradiction with the consistency of (x, y). Consequently, the tableau (x ′ , y ′ ) is consistent. By Lindenbaum Lemma, let (x ′′ , y ′′ ) be a maximal consistent tableau such that x ′ ⊆ x ′′ and y ′ ⊆ y ′′ . Obviously, ◻x ⊆ x ′′ and x ⊇ x ′′ . Moreover, ϕ ∈ y ′′ . ◻ Lemma 4.12 Let ϕ be a formula. Let (x, y) be a maximal consistent tableau. If ϕ ∈ x then there exists a maximal consistent tableau (x ′ , y ′ ) such that ◻x ⊆ x ′ , x ⊇ x ′ and ϕ ∈ x ′ .

Proof. Suppose ϕ ∈ x. Let x ′ = ◻x ∪ {ϕ} and y ′ = {χ ∶ χ ∈ y}. Suppose the tableau (x ′ , y ′ ) is not consistent. Let m, n ≥ 0, ψ 1 , . . . , ψ m ∈ x ′ and χ 1 , . . . , χ n ∈ y ′ be such that ψ 1 ∧ . . . ∧ ψ m → χ 1 ∨ . . . ∨ χ n is BHT -derivable. There are 2 cases: there exists a positive integer i ≤ m such that ψ i = ϕ, or such integer does not exist. In the former case, since ψ 1 ∧ . . . ∧ ψ m → χ 1 ∨ . . . ∨ χ n is BHTderivable, therefore ψ ∧ ϕ → χ is BHT -derivable where ψ is the conjunction of the formulas in ψ 1 , . . . , ψ m which are not equal to ϕ and χ is the disjunction of the formulas in χ 1 , . . . , χ n . Hence, by M R , ◻ψ ∧ ϕ → χ is BHTderivable: a contradiction with the consistency of (x, y). In the latter case, since

ψ 1 ∧ . . . ∧ ψ m → χ 1 ∨ . . . ∨ χ n is BHT -derivable, therefore ψ ∧ ϕ → χ is BHT -derivable.
Hence, ◻ψ∧ ϕ → χ is BHT -derivable: a contradiction with the consistency of (x, y). Consequently, the tableau (x ′ , y ′ ) is consistent. By Lindenbaum Lemma, let (x ′′ , y ′′ ) be a maximal consistent tableau such that x ′ ⊆ x ′′ and y ′ ⊆ y ′′ . Obviously, ◻x ⊆ x ′′ and x ⊇ x ′′ . Moreover, ϕ ∈ x ′′ . ◻ for all

y 1 ∈ W 1 , if x 1 R 1 y 1 then (y 1 , α 1 )) ) ↭(y 2 , α 2 ) and (y 1 , α 1 )) ) ↭(y 2 , t). Let R 2 (x 2 ) def = {(y 2 , α 2 ) ∈ D 2 x 2 R 2 y 2 } and R 1 (x 1 ) def = {(y 1 , α 1 ) x 1 R 1 y 1 }. Let I ⊆ R 1 (x 1 ), J ⊆ R 1 (x 1
) and for all (y 1 , α 1 ) ∈ R 1 (x 1 ), let ψ(y 1 , α 1 ) and ϕ(y 1 , α 1 ) be formulas such that:

1) M 1 , (y 1 , α 1 ) ⊧ ϕ(y 1 , α 1 ) and M 2 , (y 2 , α 2 ) ⊧ ϕ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I; 2) M 1 , (y 1 , α 1 ) ⊧ ϕ(y 1 , α 1 ) and M 2 , (y 2 , α 2 ) ⊧ ϕ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I; 3) M 1 , (y 1 , α 1 ) ⊧ ψ(y 1 , α 1 ) and M 2 , (y 2 , t) ⊧ ψ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ J; 4) M 1 , (y 1 , α 1 ) ⊧ ψ(y 1 , α 1 ) and M 2 , (y 2 , t) ⊧ ψ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ J.
Let us consider the formula χ(y 1 , α 1 ) defined as

χ(y 1 , α 1 ) = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ ϕ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I; ϕ(y 1 , α 1 ) → ψ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I ∩ J; ¬ψ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I ∩ J. It follows that M 1 , (y 1 , α 1 ) ⊧ χ(y 1 , α 1 ) and M 2 , (y 2 , α 2 ) ⊧ χ(y 1 , α 1 ), for all (y 1 , α 1 ) ∈ R 1 (x 1 ). Therefore M 2 , (x 2 , α 2 ) ⊧ ⋀ (y1,α1)∈R1(x1) χ(y 1 , α 1 ) while M 1 , (x 1 , α 1 ) ⊧ ⋀ (y1,α1)∈R1(x1)
χ(y 1 , α 1 ): a contradiction. The proof for Condition 6) is similar to the proof for Condition 5) but using

χ(y 1 , α 1 ) def = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ ϕ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I; ϕ(y 1 , α 1 ) → ψ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I ∩ J; ¬ψ(y 1 , α 1 ) if (y 1 , α 1 ) ∈ I ∩ J.
The proof for Condition 7) is similar to the proof for Condition 4) but using

χ(y 2 , α 2 ) = ⎧ ⎪ ⎪ ⎪ ⎨ ⎪ ⎪ ⎪ ⎩ ϕ(y 2 , α 2 ) if (y 2 , α 2 ) ∈ I; ϕ(y 2 , α 2 ) → ψ(y 2 , α 2 ) if (y 2 , α 2 ) ∈ I ∩ J; ¬ψ(y 2 , α 2 ) if (y 2 , α 2 ) ∈ I ∩ J. (2)

◻

Remark how the formulas defining χ(y 1 , α 1 ) and χ(y 2 , α 2 ) above are related to the Hosoi Axiom.

Strong equivalence property

Pearce's Equilibrium logic [START_REF] Pearce | A new logical characterisation of stable models and answer sets[END_REF] is the best-known logical characterization of the stable models semantics [START_REF] Gelfond | The stable model semantics for logic programming[END_REF] and of Answer Sets [START_REF] Brewka | Answer set programming at a glance[END_REF]. It is defined in terms of the monotonic logic of Here and There [START_REF] Pearce | Equilibrium logic[END_REF] (HT) plus a minimisation criterion among the given models. This simple definition led to several modal extensions of Answer Set Programming [START_REF] Cabalar | Temporal Equilibrium Logic: a first approach[END_REF][START_REF] Del Cerro | Epistemic Equilibrium Logic[END_REF]. All these extensions have their roots in the corresponding modal extensions of HT-logic defined as the combination of propositional HT and any modal logic [START_REF] Gabbay | Many-Dimensional Modal Logics: Theory and Applications[END_REF]) that play an important role in the proof of several interesting properties of the resulting formalisms such as strong equivalence [START_REF] Cabalar | Strong equivalence of non-monotonic temporal theories[END_REF][START_REF] Del Cerro | Epistemic Equilibrium Logic[END_REF][START_REF] Lifschitz | Strongly equivalent logic programs[END_REF]. In this section, we define the concept of modal equilibrium model and prove the associated theorem of strong equivalence. A BHT -model M = ⟨W, R, H, T ⟩, is said to be total iff H = T . Given a BHTmodel M = ⟨W, R, H, T ⟩, x ∈ W and k ∈ N, we say that H is strictly included in T with respect to x and k (in symbols H < k x T ) iff there exists y ∈ W such that xR ≤k y and H(y

) = T (y). A total BHT -model M = ⟨W, R, T, T ⟩ is a Modal Equilibrium Model of a formula ϕ iff there exists x ∈ W such that 1) M, (x, h) ⊧ ϕ; 2) For all M ′ = ⟨W, R, H, T ⟩, if H < deg(ϕ) x T then M ′ , (x, h) ⊧ ϕ.
The notion of modal equilibrium model of a theory is defined in a similar way. When dealing with non-monotonicity the relation of equivalence between theories depends on the context where they are considered. We say that two theories Γ 1 and Γ 2 are strongly equivalent (in symbols Γ 1 ≡ s Γ 2 ) iff for all theories Γ, the equilibrium models of Γ 1 ∪ Γ and Γ 2 ∪ Γ coincide [START_REF] Lifschitz | Strongly equivalent logic programs[END_REF].

Proposition 7.1 For all theories Γ 1 and Γ 2 , Γ 1 ≡ s Γ 2 iff Γ 1 and Γ 2 are BHTequivalent.

Proof. Suppose Γ 1 and Γ 2 are BHT -equivalent. Let Γ be an arbitrary theory. Thus Γ 1 ∪ Γ and Γ 2 ∪ Γ are BHT -equivalent. Therefore Γ 1 ∪ Γ and Γ 2 ∪ Γ have the same equilibrium models. Reciprocally, suppose that Γ 1 and Γ 2 are not BHT -equivalent.

• First case: Γ 1 and Γ 2 are not K-equivalent. Without loss of generality, there exists a total BHT -model M = ⟨W, R, T, T ⟩ and x ∈ W such that M, (x, h) ⊧ Γ 1 but M, (x, h) ⊧ Γ 2 . Let Γ 0 def = {◻ k (p ∨ ¬p) k ≥ 0 and p ∈ V AR}. It can be checked that M is an equilibrium model of Γ 1 ∪ Γ 0 but not of Γ 2 ∪ Γ 0 .

• Second case: Γ 1 and Γ 2 are K-equivalent. Without loss of generality, there exists a BHT -model M = ⟨W, R, H, T ⟩ ( M = ⟨W, R, T, T ⟩ denote its corresponding total model) such that (1) for all y ∈ W , M, (y, t) ⊧ Γ 1 iff M, (y, t) ⊧ Γ 2 ;

(2) there exists x ∈ W such that M, (x, h) ⊧ Γ 1 and M, (x, h) ⊧ Γ 2 .

Therefore there exists ϕ ∈ Γ 2 such that M, (x, h) ⊧ ϕ. Let Γ def = {ϕ → ◻ k (p ∨ ¬p) k ≥ 0 and p ∈ V AR}. It follows that M, (x, h) ⊧ Γ 1 ∪ Γ, since M, (x, h) ⊧ ϕ and M, (x, t) ⊧ ◻ k (p ∨ ¬p), for all k ≥ 0 and for all p ∈ V AR. Therefore M is not an equilibrium model of Γ 1 ∪ Γ. Since Γ 1 ≡ s Γ 2 , M is not an equilibrium model of Γ 2 ∪ Γ. Since M, (x, h) ⊧ Γ 2 ∪ Γ, therefore there exists a BHT -model M ′ = ⟨W, R, H ′ , T ⟩ such that H ′ < deg(Γ2∪Γ) x T and M ′ , (x, h) ⊧ Γ 2 ∪ Γ. However, from M ′ , (x, h) ⊧ Γ 2 and M ′ , (x, h) ⊧ Γ we conclude that M ′ , (x, h) ⊧ Γ 0 , thus H ′ = T and this is a contradiction. ◻

The theorem played a important role in the area of Answer Set Programming [START_REF] Brewka | Answer set programming at a glance[END_REF] since it allows, under ASP semantics, to exchange two logic programs (or theories) regardless the context in which they are considered. This theorem also justifies the use of BHT as a monotonic basis supporting non-monotonicity.

Conclusions

In this paper we have studied a combination of the modal logic of Here and There equipped with the dual implication [START_REF] Rauszer | An Algebraic and Kripke-style Approach to a Certain Extension of Intuitionistic Logic[END_REF]. For this new logic we have presented two alternative (and equivalent) semantics as well as several results concerning axiomatisation, bisimulation, Hennessy-Milner property, decidability and complexity. Finally we have considered the property of strong equivalence from Answer Set Programming [START_REF] Brewka | Answer set programming at a glance[END_REF][START_REF] Pearce | Equilibrium logic[END_REF] in our setting.

The reader might have noticed that the dual implication is not used in the proof of the strong equivalence theorem. This fact gives us the idea that this new operator would allow us to characterise, in terms of strong equivalence, new kinds of minimal models like the ones introduced in [START_REF] Amendola | Semi-equilibrium models for paracoherent answer set programs[END_REF].

Another area of potential application of this logic could be Inductive Logic Programming [START_REF] Shapiro | Inductive inference of theories from facts[END_REF][START_REF] Plotkin | Automatic Methods of Inductive Inference[END_REF] (ILP). Among other techniques used to infer rules from facts, called Inverse Entailment [START_REF] Muggleton | Inverse entailment and progol[END_REF] (IE) reverse the ordinary semantical consequence (⊧). This technique was revisited under the perspective of ASP in [START_REF] Sakama | Inverse entailment in nonmonotonic logic programs[END_REF]. Thanks to the dual implication we can define an inverse entailment relation ( ) in a very natural way allowing us to use this logic for ILP in modal contexts.

  M, y ⊧ ϕ iff there exists y ∈ W such that xR y and M, y ⊧ ϕ.Remark that the clause concerning ◻ imitates the clause for the quantifier ∀ in first-order intuitionistic logic. Nevertheless, it can be proved that in a Cartesian model M = ⟨W, ≤, R, V ⟩, replacing the clause concerning ◻ by the clause M, x ⊧ ′ ◻ϕ iff for all y ∈ W , if xR y then M, y ⊧ ′ ϕ would define a satisfaction relation equivalent to the relation ⊧ defined above.

Lemma 4 . 13 (

 413 Truth Lemma) For all formulas ϕ and for all (x, y) ∈ W c , ϕ ∈ x iff M c , (x, y) ⊧ ϕ and ϕ ∈ y iff M c , (x, y) ⊧ ϕ.

Proposition 4 . 14 (

 414 Completeness) Let ϕ be a formula. If ϕ is valid in the class of all BHT -frames then ϕ is BHT -derivable.

  Let ϕ be a formula. The least closed set of formulas containing ϕ contains at most 5 ϕ equivalence classes of formulas modulo ≃.

		¬¬¬ϕ ¬ϕ
		¬¬⨽ϕ ⨽ϕ
		¬⨽¬ϕ ¬ϕ
	¬⨽ϕ ⨽⨽ϕ	⨽¬¬ϕ ¬ϕ
	⨽¬ϕ ¬¬ϕ	¬⨽⨽ϕ ⨽ϕ
		⨽¬⨽ϕ ⨽ϕ
		⨽⨽¬ϕ ¬ϕ
	⨽⨽ψ	⨽⨽⨽ϕ ⨽ϕ
	Lemma 2.5

See the discussion presented in[START_REF] Wansing | Constructive negation, implication, and co-implication[END_REF].

Derivation Calculi are used to reason about a syntactic derivability relation (⊢). usually associated with the ordinary implication (→). Conversely, Refutation Calculi[START_REF] Goranko | Refutation systems in modal logic[END_REF] are thought for reasoning about a syntactic refutability relation (⊣) and it comes from the use of the dual implication (←).

Proof. Suppose ϕ is not BHT -derivable. Hence, the tableau (∅, {ϕ}) is consistent. By Lindenbaum Lemma, let (x, y) be a maximal consistent tableau such that ϕ ∈ y. By the Truth Lemma, M c , (x, y) ⊧ ϕ. By Proposition 2.10, ϕ is not valid in the class of all BHT -frames.

◻ 5 Decidability/complexity

There is a classical method for building finite models, namely filtration, and this method could easily be adapted to the BHT setting. Nevertheless, it will fail to give us a tight upper bound for the complexity of the satisfiability problem in BHT . The truth is that, as shown in this section, see below Proposition 5.7, the satisfiability problem is in PSPACE. Our argument is based on a translation into modal logic. In order to define a translation from the BHT to modal logic K, we need for all formulas ϕ, two new variables: a ϕ and b ϕ . Let h() and t() be translations that are structure-preserving for , ⊺, ∨, ∧, ◻ and such that

Lemma 5.1 For all formulas ϕ, h(ϕ) ≤ 11 ϕ and t(ϕ) ≤ 11 ϕ .

For all formulas ϕ, let µ(ϕ) be the conjunction of the following formulas:

• a p → b p for each ϕ's variable p,

• a ψ ↔ h(ψ) for each ϕ's subformula ψ,

• b ψ ↔ t(ψ) for each ϕ's subformula ψ.

Lemma 5.2 For all formulas ϕ, µ(ϕ) = O( ϕ 2 ).

For all formulas ϕ, let ν(ϕ) = µ(ϕ) ∧ ◻µ(ϕ) ∧ . . . ∧ ◻ deg(ϕ) µ(ϕ).

Lemma 5.3 For all formulas ϕ, ν(ϕ) = O( ϕ 3 ).

Given a BHT -model M = ⟨W, R, H, T ⟩, we define its associated model M = ⟨W, R, V ⟩ as follows:

This associated model M is considered as a model of modal logic K. Obviously, for all ϕ's variables p, V (a p ) ⊆ V (b p ). Moreover, Lemma 5.4 For all ϕ's subformulas ψ and for all x ∈ W ,

Thus, for all x ∈ W , M, x ⊧ µ(ϕ). Consider now a generated model M = ⟨W, R, V ⟩ of modal logic K of depth at most deg(ϕ) such that for all x ∈ W , M, x ⊧ µ(ϕ). We define the corresponding BHT -model M = ⟨W, R, H, T ⟩ as follows:

1)

Obviously, M is a BHT -model. Moreover, Lemma 5.5 For all ϕ's subformulas ψ and for all x ∈ W ,

Proposition 5.6 For all formulas ϕ,

Proposition 5.7 The satisfiability problem in BHT is in PSPACE.

Bisimulations

Bisimulations are binary relations that relate elements of models carrying the same modal information. We now adapt the definition of bisimulations to the BHT setting.

Bisimulations for BHT

A binary relation Z between D 1 and D 2 is a bisimulation iff the following conditions are satisfied:

) and x 1 R 1 y 1 then there exists y 2 ∈ W 2 such that x 2 R 2 y 2 and (y 1 , α 1 )Z(y 2 , α 2 ), or (y 1 , α 1 )Z(y 2 , t).

Lemma 6.1 (Bisimulation Lemma) Let ϕ be a formula. For all (x 1 , α 1 ) ∈ D 1 and for all

Obviously, the union of two bisimulations is also a bisimulation.

Hennessy-Milner property

In this section we show that BHT possesses the Hennessy-Milner property. Our proof follows the line of reasoning suggested in [START_REF] Marti | A Hennessy-Milner property for many-valued modal logics[END_REF]. Let

We define the binary relation ↭ between D 1 and D 2 as follows: Proof. Suppose ↭ is not a bisimulation. Hence, one of the conditions 1)-7) does not hold for some (x 1 , α 1 ) ∈ D 1 and some (x 2 , α 2 ) ∈ D 2 . Suppose Condition 1) is not satisfied. Hence, there exists a variable p such that, without loss of generality, M 1 , (x 1 , α 1 ) ⊧ p and M 2 , (x 2 , α 2 ) ⊧ p. Thus,

⊧ ⨽⨽ϕ and M 2 , (x 2 , α 2 ) ⊧ ⨽⨽ϕ. Consequently, (x 1 , α 1 ) ↭ (x 2 , α 2 ): a contradiction. Suppose Condition 4) is not satisfied: Then (x 1 , α 1 ) ↭ (x 2 , α 2 ) and there exists

) and for all (y 2 , α 2 ) ∈ R 2 (x 2 ), let ϕ(y 2 , α 2 ) and ψ(y 2 , α 2 ) be formulas such that 1) M 1 , (y 1 , α 1 ) ⊧ ϕ(y 2 , α 2 ) and M 2 , (y 2 , α 2 ) ⊧ ϕ(y 2 , α 2 ) if (y 2 , α 2 ) ∈ I;

Let us define χ(y 2 , α 2 ) as the following formula: