# Completeness of Tableau Calculi for Two-Dimensional Hybrid Logics

Yuki Nishimura

###### Abstract

Hybrid logic is one of the extensions of modal logic. The many-dimensional
product of hybrid logic is called hybrid product logic (HPL). We construct a
sound and complete tableau calculus for two-dimensional HPL. Also, we made a
tableau calculus for Hybrid dependent Product Logic (HdPL), where one
dimension depends on the other. In addition, we add the special rule to the
tableau calculus for HdPL and show that it is still sound and complete. All of
them lack termination, however.

##  1 Introduction

Hybrid logic is an extension of basic modal logic by adding propositional
symbols called nominals, and an operator called satisfaction operator $@$. A
nominal is a formula that is true only in a single possible world in a Kripke
model. Simply, we can assume that it is a syntactic name of a possible world.
Also, by the satisfaction operator, we can create a formula of the form
$@_{i}p$, which means “the proposition $p$ holds at point $i$.” Hybrid logic
was first invented by A. N. Prior [15, 16] and has evolved in various ways
since then (see [20, 5, 9]).

For example, consider the following sentence: “Alice publishes a book on
September 1.” Using hybrid language, we can write it as $@_{i}p$, where $p=$
“Alice will publish a book.” and $i=$ “It is September 1.” Like this, we can
describe one particular point, such as a moment, a place, or a person.

Needless to say, $\square$ and $\diamondsuit$ are languages of modal logic. On
the other hand, nominals can be said to incorporate the idea of “individual
constants” in predicate logic. In this respect, hybrid logic is a “hybrid” of
modal logic and predicate logic. Furthermore, we can also reinterpret the word
“hybrid” from a different perspective. In modal logic, $\square$ and
$\diamondsuit$ are local descriptions from the viewpoint where we are now. On
the other hand, the nominals, which name the individual worlds, are a global
description from a bird’s-eye view of the model. In this respect, hybrid logic
is a hybrid of local and global descriptions ([4, 2]).

The advantage of hybrid logic is that, when considering modal logic as “logic
of relational structures”, hybrid logic is more expressive than modal logic in
terms of definability of relational structures, i.e., frame definability. For
example, in basic modal logic, there is no axiom corresponding to the
irreflexivity of the model. In hybrid logic, however, we have a simple form of
axiom, $@_{i}\neg\diamondsuit i$, where $i$ is a nominal [6].

The extension of hybrid logic to multiple dimensions is called many-
dimensional hybrid logic. One example is called Facebook Logic [19], which
multiplies two concepts, personal friendships and knowledge, and describes the
influence of each other. Friendship has a property that everyone is not
friends with oneself, and the corresponding property of the binary relation is
irreflexivity. As mentioned earlier, this property can be expressed not in the
modal language, but the hybrid language. Furthermore, by mapping a nominal of
the hybrid language to an agent, it is possible to construct a proposition of
a specific individual. For instance, $@_{i}p=$ “Agent $i$ has a property $p$.”

In particular, when all the dimensions are independent of each other, it is
called hybrid product logic (HPL, in short). For the two-dimensional HPL, a
Hilbert-style axiomatization was made in [17]. In addition, the sequent
calculus of HPL that the cut-elimination theorem holds was proposed in [18].
However, there is no tableau calculus of many-dimensional hybrid logic.

Let us point out the advantages of the system of the tableau calculus.
Whenever a logic has decidability, we can determine the validity of an
arbitrary formula mechanically by a tableau, making it easy to prove.
Furthermore, if the formula is not valid, we can construct a model by the
tableau in which this is not the case. Some of the tableau calculi have a
property that every tableau stops at a finite length, which is called
termination. For a given logic, if we can prove that its tableau calculus has
a termination, we can show that the logic is decidable.

Tableau calculus of orthodox (so to say one-dimensional) hybrid logic has been
studied extensively in [7] (see also [8, 3, 12]). In the case of modal logic,
tableau calculus uses labeled formulae of the form $(x,y):\varphi$ instead of
ordinary formulae. However, the internalized tableau calculus they propose
treats the labels as part of the hybrid formulae (we write $@_{i}@_{a}\varphi$
as the meaning of $(x,y):\varphi$), allowing us to create tableaus in which
only non-labeled formulae appear. However, no work has been done on the
tableau calculus of HPL.

In this paper, we have constructed a sound and complete tableau calculus for
two-dimensional HPL, and also for Hybrid dependent Product Logic, where one
dimension depends on the other, based on the method of [7]. It lacks
termination, however, so the decidability of HPL is still an open problem.

We proceed as follows: Section 2 introduces the semantics of HPL according to
[17], and Section 3 will introduce the tableau calculus of HPL. Then, we show
soundness and completeness in Sections 4 and 5 respectively. Furthermore, in
Section 6, we introduce the semantics and the tableau calculus of hybrid
dependent product logic (HdPL), a logic with dependencies on dimensions, and
show that soundness and completeness holds. In particular, in Section 6.4, we
introduce the property “increasing” of the HdPL model and show that it can be
successfully incorporated into the tableau calculus of HdPL.

##  2 Kripke Semantics of Hybrid Product Logic

######  Definition 2.1.

The vocabulary of Hybrid Product Logic (HPL) are the following:

  1. i)

a countable set $\mathbf{Prop}=\\{p,q,r,\dots\\}$ of propositional variables,

  2. ii)

two disjoint countable sets $\mathbf{Nom}_{1}=\\{i,j,k,\dots\\}$ and
$\mathbf{Nom}_{2}=\\{a,b,c,\dots\\}$ of nominals, which are disjoint from
$\mathbf{Prop}$,

  3. iii)

two boolean connectives: $\neg,\land$,

  4. iv)

two modal operators: $\diamondsuit_{1},\diamondsuit_{2}$,

  5. v)

two kinds of satisfaction operators:
$@_{i}(i\in\mathbf{Nom}_{1}),@_{a}(a\in\mathbf{Nom}_{2})$.

We denote a set of whole nominals by $\mathbf{Nom}$, i.e.,
$\mathbf{Nom}=\mathbf{Nom}_{1}\cup\mathbf{Nom}_{2}$.

######  Definition 2.2.

The set of formulas of HPL $\mathcal{L}_{\textbf{HPL}}$ is defined inductively
as following:

$\displaystyle\varphi\Coloneqq p\mid i\mid
a\mid\neg\varphi\mid\varphi\land\varphi\mid\diamondsuit_{1}\varphi\mid\diamondsuit_{2}\varphi\mid@_{i}\varphi\mid@_{a}\varphi,$

where $p\in\mathbf{Prop},i\in\mathbf{Nom}_{1},a\in\mathbf{Nom}_{2}$.

We define the following abbreviations by:

$\displaystyle\varphi\lor\psi\coloneqq\neg(\neg\varphi\land\neg\psi),\
\varphi\rightarrow\psi\coloneqq\neg(\varphi\land\neg\psi),\
\square_{k}\varphi\coloneqq\neg\diamondsuit_{k}\neg\varphi\ (k=1,2).$

Also, we use the following abbreviations for a finite set of formulae
$\Gamma=\\{\gamma_{1},\ldots,\gamma_{n}\\}$:

$\displaystyle\bigwedge\Gamma$
$\displaystyle\coloneqq\gamma_{1}\land\cdots\land\gamma_{n},$
$\displaystyle\bigvee\Gamma$
$\displaystyle\coloneqq\gamma_{1}\lor\cdots\lor\gamma_{n}.$

Now, we have prepared for providing semantics. Before showing the definition
of models of HPL, let us review the Kripke frame of basic (one-dimension)
modal logic.

######  Definition 2.3.

A _Kripke frame_ $\mathfrak{F}=(W,R)$ is defined as follows:

  * •

$W$ is a non-empty countable set.

  * •

$R$ is a binary relation on $W$. That is, $R\subseteq W\times W$.

We call an element of $W$ _possible world_ , and $R$ _accessibility relation_.

For any binary relation $X$ on a set, we write $xXy$ to mean $(x,y)\in X$.

Now we show the semantics of HPL, product Kripke model.

######  Definition 2.4.

Given two Kripke frames
$\mathfrak{F}_{1}=(W_{1},R_{1}),\mathfrak{F}_{2}=(W_{2},R_{2})$, _product
Kripke frame (product frame)_ $\mathfrak{F}=(W,R_{h},R_{v})$ is defined as
follows:

  * •

$W=W_{1}\times W_{2}$.

  * •

$(x,y)R_{h}(x^{\prime},y^{\prime})$ iff $xR_{1}x^{\prime}$ and $y=y^{\prime}$,

  * •

$(x,y)R_{v}(x^{\prime},y^{\prime})$ iff $x=x^{\prime}$ and $yR_{2}y^{\prime}$.

More, we define _product Kripke model (product model)_
$\mathfrak{M}=(\mathfrak{F},V)$ as follows:

  * •

$\mathfrak{F}$ is a product frame.

  * •

$V:\mathbf{Prop}\cup\mathbf{Nom}\rightarrow\mathcal{P}(W)$, where

    * –

If $i\in\mathbf{Nom}_{1}$, then $V(i)=\\{x\\}\times W_{2}\ \text{for some}\
x\in W_{1}$.

    * –

If $a\in\mathbf{Nom}_{2}$, then $V(a)=W_{1}\times\\{y\\}\ \text{for some}\
y\in W_{2}$.

We call $V$ _valuation function_.

The subscripts $h,v$ of $R_{h},R_{v}$ are capitals of “horizontal” and
“vertical”. Figure 1 is an example of product frame. Like this, we often
denote the product frame as if we write Cartesian coordinates.

Figure 1: A product Kripke model.

We abbreviate $x\in W_{1}$ such that $V(i)=\\{x\\}\times W_{2}$ by $i^{V}$. We
do the same for $a^{V}$.

######  Definition 2.5.

Given a product model $\mathfrak{M}$, a pair of possible world $(x,y)$ in
$\mathfrak{M}$ and a formula $\varphi$, _satisfaction relation_
$\mathfrak{M},(x,y)\models\varphi$ is defined inductively as follows:

$\displaystyle\mathfrak{M},(x,y)\models p\quad$
$\displaystyle\text{iff}\quad(x,y)\in V(p),\text{where}\ p\in\mathbf{Prop},$
$\displaystyle\mathfrak{M},(x,y)\models i\quad$ $\displaystyle\text{iff}\quad
x=i^{V},\text{where}\ i\in\mathbf{Nom}_{1},$
$\displaystyle\mathfrak{M},(x,y)\models a\quad$ $\displaystyle\text{iff}\quad
y=a^{V},\text{where}\ a\in\mathbf{Nom}_{2},$
$\displaystyle\mathfrak{M},(x,y)\models\neg\varphi\quad$
$\displaystyle\text{iff}\quad\text{not}\ \mathfrak{M},(x,y)\models\varphi,$
$\displaystyle\mathfrak{M},(x,y)\models\varphi\land\psi\quad$
$\displaystyle\text{iff}\quad\mathfrak{M},(x,y)\models\varphi\ \text{and}\
\mathfrak{M},(x,y)\models\psi,$
$\displaystyle\mathfrak{M},(x,y)\models\diamondsuit_{1}\varphi\quad$
$\displaystyle\text{iff}\quad\text{there is some}\ (x^{\prime},y^{\prime})\
\text{s.t.}\ (x,y)R_{h}(x^{\prime},y^{\prime})\ \text{and}\
\mathfrak{M},(x^{\prime},y^{\prime})\models\varphi,$
$\displaystyle\mathfrak{M},(x,y)\models\diamondsuit_{2}\varphi\quad$
$\displaystyle\text{iff}\quad\text{there is some}\ (x^{\prime},y^{\prime})\
\text{s.t.}\ (x,y)R_{v}(x^{\prime},y^{\prime})\ \text{and}\
\mathfrak{M},(x^{\prime},y^{\prime})\models\varphi,$
$\displaystyle\mathfrak{M},(x,y)\models@_{i}\varphi\quad$
$\displaystyle\text{iff}\quad\mathfrak{M},(i^{V},y)\models\varphi,$
$\displaystyle\mathfrak{M},(x,y)\models@_{a}\varphi\quad$
$\displaystyle\text{iff}\quad\mathfrak{M},(x,a^{V})\models\varphi.$

A formula $\varphi$ is valid on an $\mathfrak{M}$, denoted by
$\mathfrak{M}\models\varphi$, if $\mathfrak{M},(x,y)\models\varphi$ holds for
all $(x,y)\in W$. Also, if $\mathfrak{M}\models\varphi$ holds for all model
$\mathfrak{M}$, we say $\varphi$ is _valid_ , and we write $\models\varphi$.

Moreover, for two finite sets of formulas $\Gamma,\Delta$, we write
$\Gamma\models\Delta$, if $\models\bigwedge\Gamma\rightarrow\bigvee\Delta$
holds.

Intuitively, $\diamondsuit_{1}\varphi$ ($\diamondsuit_{2}\varphi$) represents
“$\varphi$ holds somewhere in the world reachable from here by $R_{h}$
($R_{v}$).” And $@_{i}@_{a}\varphi$ means “$\varphi$ holds at the point where
$i$ and $a$ hold” or ”$\varphi$ holds at the point $(i,a)$.”

By the definition of $R_{h}$ and $R_{v}$, we can rewrite the definition of
satisfaction relation that a formula has the form
$\diamondsuit_{k}\varphi(k=1,2)$:

$\displaystyle\mathfrak{M},(x,y)\models\diamondsuit_{1}\varphi\quad$
$\displaystyle\text{iff}\quad\text{there is some}\ x^{\prime}\in W_{1}\
\text{s.t.}\ xR_{1}x^{\prime}\ \text{and}\
\mathfrak{M},(x^{\prime},y)\models\varphi,$
$\displaystyle\mathfrak{M},(x,y)\models\diamondsuit_{2}\varphi\quad$
$\displaystyle\text{iff}\quad\text{there is some}\ y^{\prime}\in W_{2}\
\text{s.t.}\ yR_{2}y^{\prime}\ \text{and}\
\mathfrak{M},(x,y^{\prime})\models\varphi.$

We can derive the following satisfaction relation for
$\lor,\rightarrow,\square_{1},$ and $\square_{2}$ as follows:

$\displaystyle\mathfrak{M},(x,y)\models\varphi\lor\psi\quad$
$\displaystyle\text{iff}\quad\mathfrak{M},(x,y)\models\varphi\ \text{or}\
\mathfrak{M},(x,y)\models\psi,$
$\displaystyle\mathfrak{M},(x,y)\models\varphi\rightarrow\psi\quad$
$\displaystyle\text{iff}\quad\text{if}\ \mathfrak{M},(x,y)\models\varphi,\
\text{then}\ \mathfrak{M},(x,y)\models\psi,$
$\displaystyle\mathfrak{M},(x,y)\models\square_{1}\varphi\quad$
$\displaystyle\text{iff}\quad\text{for all}\ (x^{\prime},y^{\prime})\
,\text{if}\ (x,y)R_{h}(x^{\prime},y^{\prime})\ \text{then}\
\mathfrak{M},(x^{\prime},y^{\prime})\models\varphi$
$\displaystyle\text{iff}\quad\text{for all}\ x^{\prime}\in W_{1},\ \text{if}\
xR_{1}x^{\prime}\ \text{then}\ \mathfrak{M},(x^{\prime},y)\models\varphi,$
$\displaystyle\mathfrak{M},(x,y)\models\square_{2}\varphi\quad$
$\displaystyle\text{iff}\quad\text{for all}\ (x^{\prime},y^{\prime})\
,\text{if}\ (x,y)R_{v}(x^{\prime},y^{\prime})\ \text{then}\
\mathfrak{M},(x^{\prime},y^{\prime})\models\varphi$
$\displaystyle\text{iff}\quad\text{for all}\ y^{\prime}\in W_{2},\ \text{if}\
yR_{2}y^{\prime}\ \text{then}\ \mathfrak{M},(x,y^{\prime})\models\varphi.$

##  3 Internalized Tableau

For modal logic, the most established tableau calculus is a prefixed tableau
calculus[14]. In this system, each formula occurred with a prefix representing
a possible world. In hybrid logic, however, we can remove all prefixes. First,
an expression of the form “$i:\varphi$” that appears in the prefix tableau can
be written as $@_{i}\varphi$. Also, the notation $irj$ which shows
reachability can be written as $@_{i}\diamondsuit j$. In the end, all symbolic
sequences that appear in a tableau can be formulae. Such a system is called
internalized tableau calculus.

This time, we will construct a tableau calculus for HPL based on this idea
proposed in [7].

######  Definition 3.1.

A _tableau_ of HPL is a well-founded tree whose nodes are HPL formulae. Given
a tableau, a formula of a root of the tableau is called _root formula_. A
maximal path of the tableau is called _branch_. If a formula $\varphi$ occurs
in a branch $\Theta$, then we write $\varphi\in\Theta$.

A branch of a tableau $\Theta$ is _closed_ if $\Theta$ satisfies at least one
condition of three:

  1. i)

There is some $\varphi$, $i\in\mathbf{Nom}_{1}$ and $a\in\mathbf{Nom}_{2}$
such that $@_{i}@_{a}\varphi,@_{i}@_{a}\neg\varphi\in\Theta$.

  2. ii)

There is some $\varphi$ and $i\in\mathbf{Nom}_{1}$ such that
$@_{i}\varphi,@_{i}\neg\varphi\in\Theta$.

  3. iii)

There is some $\varphi$ and $a\in\mathbf{Nom}_{2}$ such that
$@_{a}\varphi,@_{a}\neg\varphi\in\Theta$.

We say $\Theta$ is _open_ if it is not close. A tableau is called _closed_ if
all branches in the tableau are closed.

######  Definition 3.2.

We provide the rules of tableau calculus for HPL as Figure 2.

$\displaystyle@_{i}@_{a}\varphi@_{i}@_{a}\neg\neg\varphi\qquad@_{i}@_{a}\psi@_{i}@_{a}\varphi@_{i}@_{a}(\varphi\land\psi)\qquad@_{i}@_{a}\neg\varphi\mid@_{i}@_{a}\neg\psi@_{i}@_{a}\neg(\varphi\land\psi)$
$\displaystyle@_{j}@_{a}\varphi@_{i}\diamondsuit_{1}j@_{i}@_{a}\diamondsuit_{1}\varphi\qquad@_{i}@_{b}\varphi@_{a}\diamondsuit_{2}b@_{i}@_{a}\diamondsuit_{2}\varphi\qquad@_{j}@_{a}\neg\varphi@_{i}\diamondsuit_{1}j@_{i}@_{a}\neg\diamondsuit_{1}\varphi\qquad@_{i}@_{b}\neg\varphi@_{a}\diamondsuit_{2}b@_{i}@_{a}\neg\diamondsuit_{2}\varphi$
$\displaystyle@_{j}@_{a}\varphi@_{i}@_{a}@_{j}\varphi\qquad@_{i}@_{b}\varphi@_{i}@_{a}@_{b}\varphi\qquad@_{j}@_{a}\neg\varphi@_{i}@_{a}\neg@_{j}\varphi\qquad@_{i}@_{b}\neg\varphi@_{i}@_{a}\neg@_{b}\varphi$
$\displaystyle@_{i}s@_{i}@_{a}s\qquad@_{a}t@_{i}@_{a}t\qquad@_{j}j@_{i}\neg
j\qquad@_{b}b@_{a}\neg b$
$\displaystyle@_{j}@_{a}\varphi@_{i}j@_{i}@_{a}\varphi\qquad@_{i}@_{b}\varphi@_{a}b@_{i}@_{a}\varphi\qquad@_{j}s@_{i}j@_{i}s\qquad@_{b}t@_{a}b@_{a}t\qquad$

*1: $j\in\mathbf{Nom}_{1}$ does not occur in the branch.

*2: $b\in\mathbf{Nom}_{2}$ does not occur in the branch.

*3: This rule can be applied only one time per formula.

*4: $s=k,\neg k\ (k\in\mathbf{Nom}_{1})$.

*5: $t=c,\neg c\ (c\in\mathbf{Nom}_{2})$.

In those rules, the formulae above line show the formulae which have already
occurred in the branch, and those below line show those which will be added to
the branch. The vertical line in the $[\neg\land]$ rule means that the branch
splits to the left and right.

Figure 2: The rules of tableau calculus for HPL.

Most of these rules are based on the method of [7]. However, since we have two
dimensions, the rules related to modal and hybrid language are split into two
rules. For example, instead of $[\diamondsuit]$ in the tableau calculus for
one-dimensional hybrid logic, we have $[\diamondsuit_{1}]$ and
$[\diamondsuit_{2}]$ in that of HPL. Note that the formula
$@_{i}\diamondsuit_{1}j$ generated by $[\diamondsuit_{1}]$ relates to
accessibility relations. Since relations of two dimensions are independent of
each other, this formula consists only of the materials related to
$\mathbf{Nom}_{1}$.

The rules $[Red_{1}],[Red_{2}]$ reflect the axioms Red$@_{1}$, Red$@_{2}$ in
[17] respectively. These are:

Red$@_{1}$: $\displaystyle\quad@_{i}a\leftrightarrow a,$ Red$@_{2}$:
$\displaystyle\quad@_{a}i\leftrightarrow i.$

where $i\in\mathbf{Nom}_{1}$ and $a\in\mathbf{Nom}_{2}$. Using these rules,
hybrid formulae not only of the form $@_{i}@_{a}\varphi$ but also of the form
$@_{i}\varphi$ or $@_{a}\varphi$ occur in a tableau. Then we need four $[Id]$
rules for each dimension and each form of formula, single or double “prefix”.

######  Remark 3.3.

Considering that $\square_{1}\varphi\equiv\neg\diamondsuit_{1}\neg\varphi$,
the rule $[\neg\diamondsuit_{1}]$ is equivalent to this:

$@_{j}@_{a}\varphi@_{i}@_{a}\square_{1}\varphi,@_{i}\diamondsuit_{1}j$

We can say the same for $\square_{2}$. Moreover, we can create the rules for
boolean operators $\lor$ and $\rightarrow$, using the facts that
$\varphi\lor\psi\equiv\neg(\neg\varphi\land\neg\psi)$ and
$\varphi\rightarrow\psi\equiv\neg(\varphi\land\neg\psi)$. If we can use these
rules additionally, then we no longer have to replace these symbols in a
formula with primitive ones.

######  Definition 3.4 (Provability).

Given a formula $\varphi$, we say $\varphi$ is _provable_ and write
$\vdash\varphi$ if there is a closed tableau whose root formula is
$@_{i}@_{a}\neg\varphi$, where both
$i\in\textbf{Nom}_{1},a\in\textbf{Nom}_{2}$ are not occurred in $\varphi$.

Also, given two finite sets of formulae $\Gamma,\Delta$, we write
$\Gamma\vdash\Delta$ if there is a closed tableau whose root formula is
$@_{i}@_{a}\neg(\bigwedge\Gamma\rightarrow\bigvee\Delta)$, equivalent to
$@_{i}@_{a}(\bigwedge\Gamma\land\neg(\bigvee\Delta))$, where both
$i\in\textbf{Nom}_{1},a\in\textbf{Nom}_{2}$ are not occurred in any formula in
$\Gamma,\Delta$.

##  4 Soundness

In this section, we show that the tableau calculus of HPL is sound for the
class of product frames, i.e., if $\vdash\varphi$, then $\models\varphi$.

First, we need some preparation. Let us denote by $\Theta^{n}$ a fragment of a
branch $\Theta$ we can get by using rules $n$ time from the root formula.

Next, we define the concept _faithfulness_ for a branch $\Theta$ and a model
$\mathfrak{M}$. This is named after [14, p.31, Def.2.9.2].

######  Definition 4.1 (Faithful model).

Given a branch (or its fragment) $\Theta$ and a model
$\mathfrak{M}=(\mathfrak{F},V)$, we say $\mathfrak{M}$ is _faithful_ to
$\Theta$ if all of the following three hold:

  1. i)

If $@_{j}@_{b}\psi\in\Theta$, then $\mathfrak{M},(j^{V},b^{V})\models\psi$.

  2. ii)

If $@_{j}s\in\Theta\ (s=k,\neg k,\diamondsuit_{1}k)$, then for all $y\in
W_{2}$, $\mathfrak{M},(j^{V},y)\models s$.

  3. iii)

If $@_{b}t\in\Theta\ (t=c,\neg c,\diamondsuit_{2}c)$, then for all $x\in
W_{1}$, $\mathfrak{M},(x,b^{V})\models t$.

First we prove this lemma. This is a “step case” of Lem.4.3.

######  Lemma 4.2.

Let $\Theta=\Theta^{m}$ be a fragment of a branch and
$\mathfrak{M}=(\mathfrak{F},V)$ a model, which is faithful to $\Theta^{m}$.
Let $\Theta^{m+1}$ be a new branch (possibly it will not be the only one) we
acquire by applying one of the rules to $\Theta^{m}$. Then, there exists a
pair that consists of at least one $\Theta=\Theta^{m+1}$ and a model
$\mathfrak{M}^{\prime}=(\mathfrak{F},V^{\prime})$ that the valuation function
$V$ of $\mathfrak{M}$ is replaced with another one $V^{\prime}$, such that
$\mathfrak{M}^{\prime}$ is faithful to $\Theta^{m+1}$.

###### Proof.

This proof is divided into some cases by which rule is applied to
$\Theta^{m}$. We give the proof only for the case [$\neg\land$] and
[$\diamondsuit_{1}$]. The rest are left to the reader.

[$\neg\land$]

Suppose that we acquire two new formulae $@_{j}@_{b}\neg\psi_{1}$ ,
$@j@_{b}\neg\psi_{2}$ by applying [$\neg\land$] to $\Theta^{m}$. Let
$\Theta^{m+1}_{1}$ , $\Theta^{m+1}_{2}$ be split branches that contain
$@_{j}@_{b}\neg\psi_{1},@_{j}@_{b}\neg\psi_{2}$ respectively. Since we can
apply [$\neg\land$] to $\Theta^{m}$,
$@_{j}@_{b}\neg(\psi_{1}\land\psi_{2})\in\Theta^{m}$ holds. Then by
assumption, $(j^{V},b^{V})\models\neg(\psi_{1}\land\psi_{2})$ holds. By this
fact, we show either $(j^{V},b^{V})\models\neg\psi_{1}$ or
$(j^{V},b^{V})\models\neg\psi_{2}$ holds as follows:

$\displaystyle(j^{V},b^{V})\models\neg(\psi_{1}\land\psi_{2})\quad$
$\displaystyle\text{iff}\quad\text{not}\
(j^{V},b^{V})\models\psi_{1}\land\psi_{2}$
$\displaystyle\text{iff}\quad\text{not}\ (j^{V},b^{V})\models\psi_{1}\
\text{or not}\ (j^{V},b^{V})\models\psi_{2}$
$\displaystyle\text{iff}\quad(j^{V},b^{V})\models\neg\psi_{1}\ \text{or}\
(j^{V},b^{V})\models\neg\psi_{2}$

Therefore, $\mathfrak{M}$ is faithful either to $\Theta^{m+1}_{1}$ or
$\Theta^{m+1}_{2}$.

[$\diamondsuit_{1}$]

Suppose that we acquire two new formulae
$@_{j}\diamondsuit_{1}k,@_{k}@_{b}\psi$ by applying [$\diamondsuit_{1}$] to
$\Theta^{m}$. Let $\Theta^{m+1}$ be a branch that contains both of the two
formulae. Since we can apply [$\diamondsuit_{1}$] to $\Theta^{m}$,
$@_{j}@_{b}\diamondsuit_{1}\psi\in\Theta^{m}$ holds, and by assumption
$\mathfrak{M},(j^{V},b^{V})\models\diamondsuit_{1}\psi$ holds. This implies
that there is some $x^{\prime}\in W_{1}$ such that $j^{V}R_{1}x^{\prime}$ and
$\mathfrak{M},(x^{\prime},b^{V})\models\psi$. Now we define a new valuation
function $V^{\prime}$ as follows:

$V^{\prime}(s)=\begin{cases}\\{x^{\prime}\\}\times W_{2}&(s=k)\\\
V(s)&(\text{otherwise})\end{cases}$

Define $\mathfrak{M}^{\prime}=(\mathfrak{F},V^{\prime})$. Then we have
$j^{V^{\prime}}R_{1}k^{V^{\prime}}$ and
$\mathfrak{M}^{\prime},(k^{V^{\prime}},b^{V^{\prime}})\models\psi$. By the
latter, Definition 4.1 (i) holds for $@_{k}@_{b}\psi\in\Theta^{m+1}$ and
$(k^{V},b^{V})$. By the former,
$\mathfrak{M}^{\prime},(j^{V^{\prime}},y)\models\diamondsuit_{1}k$ holds for
an arbitrary $y$. Then, Definition 4.1 (ii) holds for
$@_{j}\diamondsuit_{1}k\in\Theta^{m+1}$ and $j^{V}$. What’s more, since $k$
does not occur in $\Theta^{m}$, interpretation of any formula in $\Theta^{m}$
does not change even if $V$ changes to $V^{\prime}$. Therefore,
$\mathfrak{M}^{\prime}$ is faithful to $\Theta^{m+1}$.

∎

######  Lemma 4.3.

Let $\mathcal{T}$ be a tableau whose root formula is $@_{i}@_{a}\varphi$ and
$\mathfrak{M}=(\mathfrak{F},V)$ be a product model such that a possible world
$(i^{V},a^{V})\in W$ satisfies $\mathfrak{M},(i^{V},a^{V})\models\varphi$.
Then, there exists a pair of a branch $\Theta$ in $\mathcal{T}$ and a model
$\mathfrak{M}^{\prime}=(\mathfrak{F},V^{\prime})$ such that
$\mathfrak{M}^{\prime}$ is faithful to $\Theta$.

###### Proof.

By assumption, $\mathfrak{M}$ is faithful to the fragment of the branch
$\Theta^{0}$ which we can get by applying rules $0$ time to the root formula
(the fragment which contains only the root formula). Using this fact and Lemma
4.2, we can construct a model
$\mathfrak{M}^{\prime}=(\mathfrak{F},V^{\prime})$ which is faithful to at
least one branch $\Theta$. This is the desired pair of a branch and a model. ∎

######  Theorem 4.4 (Soundness).

The tableau calculus of HPL is sound for the class of product frames, i.e., if
$\vdash\varphi$, then $\models\varphi$.

###### Proof.

We show the contraposition.

Assume that $\not\models\varphi$. then there are a model
$\mathfrak{M}=(\mathfrak{F},V)$ and its possible world $(x,y)$ such that
$\mathfrak{M},(x,y)\models\neg\varphi$. Now take nominals
$i\in\mathbf{Nom}_{1},a\in\mathbf{Nom}_{2}$ both of which do not occur in
$\varphi$ arbitrary. Also, define $V^{\prime}$ as follows:

$V^{\prime}(s)=\begin{cases}\\{x\\}\times W_{2}&(s=i)\\\
W_{1}\times\\{y\\}&(s=a)\\\ V(s)&(\text{otherwise})\end{cases}$

Thus for $\mathfrak{M}^{\prime}=(\mathfrak{F},V^{\prime})$, we have
$\mathfrak{M}^{\prime},(i^{V^{\prime}},a^{V^{\prime}})\models\neg\varphi$. Fix
some tableau whose root formula is $@_{i}@_{a}\neg\varphi$. Then by Lemma 4.3,
there is a pair of a branch $\Theta$ of the tableau and a model
$\mathfrak{M}^{\prime\prime}=(\mathfrak{F},V^{\prime\prime})$ such that
$\mathfrak{M}^{\prime\prime}$ is faithful to $\Theta$.

Next we show that that $\Theta$ is open. Suppose that $\Theta$ is closed. Then
at least one of following holds:

  1. 1.

There are a pair $(j,b)$ of nominals and a formula $\psi$ such that
$@_{j}@_{b}\psi,@_{j}@_{b}\neg\psi\in\Theta$.

  2. 2.

There are a nominal $j\in\mathbf{Nom}_{1}$ and a formula $\psi$ such that
$@_{j}\psi,@_{j}\neg\psi\in\Theta$.

  3. 3.

There are a nominal $b\in\mathbf{Nom}_{2}$ and a formula $\psi$ such that
$@_{b}\psi,@_{b}\neg\psi\in\Theta$.

Suppose that 1. holds. Then by Definition 4.1 (i), both
$\mathfrak{M}^{\prime\prime},(j^{V^{\prime\prime}},b^{V^{\prime\prime}})\models\psi,\mathfrak{M}^{\prime\prime},(j^{V^{\prime\prime}},b^{V^{\prime\prime}})\models\neg\psi$
hold, but that is contradiction. We can similarly show the contradiction in
the case of 2. and 3.

From the above, it follows that for all tableaux whose root formula is
$@_{i}@_{a}\neg\varphi$ there is some open branch $\Theta$. Therefore,
$\not\vdash\varphi$. ∎

######  Corollary 4.5.

Given two finite sets of formulae $\Gamma$ and $\Delta$, if
$\Gamma\vdash\Delta$, then $\Gamma\models\Delta$.

###### Proof.

By Theorem 4.4 and letting $\varphi=\bigwedge\Gamma\rightarrow\bigvee\Delta$.
∎

##  5 Completeness

In this section, we show that the tableau calculus of HPL is complete for the
class of product frames, i.e., if $\models\varphi$, then $\vdash\varphi$.

First, we define an important concept, _quasi-subformula_.

######  Definition 5.1 (Quasi-subformula).

Given two formulae $@_{i}@_{a}\varphi$ and $@_{j}@_{b}\psi$, we say
$@_{i}@_{a}\varphi$ is _a quasi-subformula_ of $@_{j}@_{b}\psi$ if one of the
followings holds:

  * •

$\varphi$ is a subformula of $\psi$.

  * •

$\varphi$ has the form $\neg\chi$ and $\chi$ is a subformula of $\psi$.

######  Lemma 5.2 (Quasi-subformula property).

Let $\mathcal{T}$ be a tableau. If a formula in $\mathcal{T}$ has the form
$@_{i}@_{a}\varphi$, then it is a quasi-subformula of the root formula of
$\mathcal{T}$.

###### Proof.

By induction on the rules of tableau calculus, except this six rules which do
not generate a formula of the form $@_{i}@_{a}\varphi$: [$Red_{1}$],
[$Red_{2}$], [$\neg_{1}$], [$\neg_{2}$], [$Id^{\prime}_{1}$], [$Id`_{2}$]. We
only do the case of [$\neg\land$], [$\diamondsuit_{1}$]. The rest are left to
the reader.

[$\neg\land$]

$@_{i}@_{a}\neg\varphi,@_{i}@_{a}\neg\psi$ are both quasi-subformulas of
$@_{i}@_{a}\neg(\varphi\land\psi)$. Also, $@_{i}@_{a}\neg(\varphi\land\psi)$
is a quasi-subformula of the root formula by induction hypothesis. Therefore
$@_{i}@_{a}\neg\varphi,@_{i}@_{a}\neg\psi$ are quasi-subformulas of the root
formula.

[$\diamondsuit_{1}$]

It suffices to show that $@_{j}@_{a}\varphi$ is a quasi-subformula of the root
formula. $@_{j}@_{a}\varphi$ is a quasi-subformula of
$@_{i}@_{a}\diamondsuit_{1}\varphi$, and by induction hypothesis,
$@_{i}@_{a}\diamondsuit_{1}\varphi$ is a quasi-subformula of the root formula.

∎

Next, we define the concept of saturation. Intuitively, a branch is saturated
if we cannot add any formula to it even if we can apply no more rules to it.
The following is the formal definition of that.

######  Definition 5.3.

A branch $\Theta$ of a tableau is _saturated_ if $\Theta$ satisfies all the
conditions below:

  1. i)

If $@_{i}@_{a}\neg\neg\varphi\in\Theta$, then $@_{i}@_{a}\varphi\in\Theta$.

  2. ii)

If $@_{i}@_{a}(\varphi\land\psi)\in\Theta$, then
$@_{i}@_{a}\varphi,@_{i}@_{a}\psi\in\Theta$.

  3. iii)

If $@_{i}@_{a}\neg(\varphi\land\psi)\in\Theta$, then either
$@_{i}@_{a}\neg\varphi\in\Theta$ or $@_{i}@_{a}\neg\psi\in\Theta$.

  4. iv)

If $@_{i}@_{a}\diamondsuit_{1}\varphi\in\Theta$, then there is some
$j\in\textbf{Nom}_{1}$ such that
$@_{i}\diamondsuit_{1}j,@_{j}@_{a}\varphi\in\Theta$.

  5. v)

If $@_{i}@_{a}\diamondsuit_{2}\varphi\in\Theta$, then there is some
$b\in\textbf{Nom}_{2}$ such that
$@_{a}\diamondsuit_{2}b,@_{i}@_{b}\varphi\in\Theta$.

  6. vi)

If $@_{i}@_{a}\neg\diamondsuit_{1}\varphi,@_{i}\diamondsuit_{1}j\in\Theta$,
then $@_{j}@_{a}\neg\varphi\in\Theta$.

  7. vii)

If $@_{i}@_{a}\neg\diamondsuit_{2}\varphi,@_{a}\diamondsuit_{2}b\in\Theta$,
then $@_{i}@_{b}\neg\varphi\in\Theta$.

  8. viii)

If $@_{i}@_{a}@_{j}\varphi\in\Theta$, then $@_{j}@_{a}\varphi\in\Theta$.

  9. ix)

If $@_{i}@_{a}@_{b}\varphi\in\Theta$, then $@_{i}@_{b}\varphi\in\Theta$.

  10. x)

If $@_{i}@_{a}\neg@_{j}\varphi\in\Theta$, then
$@_{j}@_{a}\neg\varphi\in\Theta$.

  11. xi)

If $@_{i}@_{a}\neg@_{b}\varphi\in\Theta$, then
$@_{i}@_{b}\neg\varphi\in\Theta$.

  12. xii)

If $s=k,\neg k\ (k\in\mathbf{Nom}_{1})$ and $@_{i}@_{a}s\in\Theta$, then
$@_{i}s\in\Theta$.

  13. xiii)

If $t=c,\neg c\ (c\in\mathbf{Nom}_{2})$ and $@_{i}@_{a}t\in\Theta$, then
$@_{a}t\in\Theta$.

  14. xiv)

If $@_{i}\neg j\in\Theta$, then $@_{j}j\in\Theta$.

  15. xv)

If $@_{a}\neg b\in\Theta$, then $@_{b}b\in\Theta$.

  16. xvi)

If $@_{i}@_{a}\varphi,@_{i}j\in\Theta$, then $@_{j}@_{a}\varphi\in\Theta$.

  17. xvii)

If $@_{i}@_{a}\varphi,@_{a}b\in\Theta$, then $@_{i}@_{b}\varphi\in\Theta$.

  18. xviii)

If $s=k,\neg k\ (k\in\mathbf{Nom}_{1})$ and $@_{i}s,@_{i}j\in\Theta$, then
$@_{j}s\in\Theta$.

  19. xix)

If $t=c,\neg c\ (c\in\mathbf{Nom}_{2})$ and $@_{a}t,@_{a}b\in\Theta$, then
$@_{b}\varphi\in\Theta$.

We call a tableau _saturated_ if all branches of it are saturated.

Next lemma claims that for an arbitrary root formula, we can construct a
saturated tableau.

######  Lemma 5.4.

Given an HPL formula $\varphi$, we can construct a tableau whose root formula
is $@_{i}@_{a}\varphi$ ($i$ and $a$ do not occur in $\varphi$), all the
branches of which are saturated.

###### Proof.

Given an HPL formula $\varphi$, we construct a tableau $\mathcal{T}_{n},$ as
follows:

  * •

$\mathcal{T}_{0}$ is a tableau with only the node $@_{i}@_{a}\neg\varphi$ ($i$
and $a$ do not occur in $\varphi$).

  * •

$\mathcal{T}_{n+1}$ is constructed by applying rules to all nodes in each
branch of $\mathcal{T}_{n}$ as many times as possible. During constructing it,
we have to observe the following rules:

    1. i)

If new formulae generated by applying some rules have already exists in the
same branch, they are not added to the branch.

    2. ii)

For $[\diamondsuit_{k}]\ (k=1,2)$, we can apply it only once to the same
formula of the same branch.

Now we define $\mathcal{T}^{*}$ as the closure of all $\mathcal{T}_{n}\
(n\in\mathbb{N})$. Then, all the branches of $\mathcal{T}^{*}$ are saturated;
to prove that, suppose otherwise. Then, there exists a branch $\Theta$ such
that one of the conditions of Definition 5.3 does not hold. Let
$@_{j}@_{b}\varphi$ (it may be of the form $@_{j}\psi$ or $@_{b}\psi$) be the
formula which falsify the condition of Definition 5.3 with respect to
$\Theta$. Now we can find an integer $k\in\mathbb{N}$ such that
$@_{j}@_{b}\varphi$ in $\mathcal{T}_{k}$. Then, $\mathcal{T}_{k+1}$ is a
tableau of which all the branches containing $@_{j}@_{b}\varphi$ satisfy all
the conditions of Definition 5.3 with respect to it. Thus so is
$\mathcal{T}^{*}$, but that is contradiction. ∎

Next, we define _right nominal_. Given a branch $\Theta$ of tableau,
$s\in\textbf{Nom}$ is a right nominal of $\Theta$ if there is a nominal $t$
such that $@_{t}s\in\Theta$.

We have the following property about the right nominals.

######  Lemma 5.5.

All the right nominals occurring in branch $\Theta$ occur in the root formula.

###### Proof.

Let $s$ be a right nominal occurring in $\Theta$. Then there exists another
nominal $t$ such that $@_{t}s\in\Theta$. Assume that $s,t\in\mathbf{Nom}_{1}$
(the case if $s,t\in\mathbf{Nom}_{2}$ is the same). Now, $@_{t}s$ is derived
using either [$Red_{1}$] or [$\neg_{1}$].

  1. i)

If $@_{t}s$ is derived using [$Red_{1}$], then there is a nominal
$a\in\mathbf{Nom}_{2}$ such that $@_{t}@_{a}s\in\Theta$. By Lem.5.2, $s$ is a
quasi-subformula of the root formula. Therefore, $s$ occurs in the root
formula.

  2. ii)

If $@_{t}s$ is derived using [$\neg_{1}$], then $t=s$ and there is a nominal
$i\in\mathbf{Nom}_{1}$ such that $@_{i}\neg s\in\Theta$. We obtain it by
applying one of the rules [$Red_{1}$] or [$Id^{\prime}_{1}$]; let us work in
the case [$Red_{1}$]. Then, there is another nominal $a\in\mathbf{Nom}_{2}$
such that $@_{i}@_{a}\neg s\in\Theta$. By Lem.5.2, $\neg s$ is a quasi-
subformula of the root formula. Therefore, $s$ occurs in the root formula. We
can do similarly in the case [$Id^{\prime}_{1}$].

∎

######  Definition 5.6.

Let $\Theta$ be a branch of a tableau. For any right nominals
$i,j\in\mathbf{Nom}_{1},a,b\in\mathbf{Nom}_{2}$ occurs in $\Theta$, we define
binary relations $\sim_{\Theta}^{1},\sim_{\Theta}^{2}$ as follows:

$\displaystyle i\sim_{\Theta}^{1}j\quad$
$\displaystyle\text{iff}\quad@_{i}j\in\Theta,$ $\displaystyle
a\sim_{\Theta}^{2}b\quad$<EMAIL_ADDRESS>
######  Lemma 5.7.

Let $\Theta$ be a saturated branch of a tableau. Then
$\sim_{\Theta}^{k}(k=1,2)$ of Def.5.6 are equivalent relations of
$\mathbf{Nom}_{1},\mathbf{Nom}_{2}$ respectively.

###### Proof.

It suffices to show that $\sim_{\Theta}^{1}$ is reflexive, symmetric, and
transitive.

First, we show reflexivity. Let $i$ be a right nominal. Then there is a
nominal $j$ such that $@_{j}i\in\Theta$. Using [$Id^{\prime}_{1}$] to the two
$@_{j}i$, we get $@_{i}i$. Since $\Theta$ is saturated, by Def.5.3(xviii) we
have $@_{i}i\in\Theta$. Therefore $i\sim_{\Theta}^{1}i$.

Second, we show symmetry. Let $i\sim_{\Theta}^{1}j$. By definition
$@_{i}j\in\Theta$ holds. Also, by reflexivity of $\sim_{\Theta}^{1}$, we have
$@_{i}i\in\Theta$. Since $\Theta$ is saturated, by Def.5.3(xviii) we have
$@_{j}i\in\Theta$. Therefore, $j\sim_{\Theta}^{1}i$.

Lastly, we show transitivity. Let $i\sim_{\Theta}^{1}j,j\sim_{\Theta}^{1}k$.
By definition, $@_{i}j\in\Theta,@_{j}k\in\Theta$ hold. We have
$@_{j}i\in\Theta$ by the symmetry of $\sim_{\Theta}^{1}$, and since $\Theta$
is saturated, by Def.5.3(xviii) we have $@_{i}k\in\Theta$. Therefore we have
$i\sim_{\Theta}^{1}k$. ∎

######  Definition 5.8.

Let $\Theta$ be a saturated branch of a tableau and $i\in\mathbf{Nom}_{1}$ a
right nominal occurring in $\Theta$. We denote by $[i]_{\Theta}^{1}$ an
equivalence class of a right nominal $i$ by the relation $\sim_{\Theta}^{1}$.
Similarly, we denote by $[a]_{\Theta}^{2}$ an equivalence class of a right
nominal $a$ by the relation $\sim_{\Theta}^{2}$.

Note that since $\mathbf{Nom}_{1},\mathbf{Nom}_{2}$ are both countable
infinite, We can insert linear order for each of them respectively. For a non-
empty set $A$ of nominals, we write $\min(A)$ as the minimal element in this
order. We use this notation $\min(A)$ in the following Definition 5.9 for that
meaning.

######  Definition 5.9.

Let $\Theta$ be a saturated branch of a tableau and $s$ a nominal occurring in
$\Theta$ (note that $s$ does not have to be a right nominal). We define an
_urfather_ of $s$ on $\Theta$ (denoted $u_{\Theta}(s)$) as follows:

$u_{\Theta}(s)=\begin{cases}\min([j]_{\Theta}^{1})&\text{if}\quad
s\in\mathbf{Nom}_{1}\ \text{and}\ @_{s}j\in\Theta\\\
\min([b]_{\Theta}^{2})&\text{if}\quad s\in\mathbf{Nom}_{2}\ \text{and}\
@_{s}b\in\Theta\\\ s&\text{otherwise.}\end{cases}$

######  Proposition 5.10.

$u_{\Theta}(s)$ of Def.5.9 is well-defined.

###### Proof.

Assume that $@_{s}i,@_{s}j\in\Theta$ and $s,i,j\in\mathbf{Nom}_{1}$ (we can do
the case $\mathbf{Nom}_{2}$ the same). Since $\Theta$ is saturated, by
Def.5.3(xviii) we have $@_{i}j\in\Theta$. Thus
$[i]_{\Theta}^{1}=[j]_{\Theta}^{1}$, and we have
$\min([i]_{\Theta}^{1})=\min([j]_{\Theta}^{1})$. Therefore, $u_{\Theta}(s)$ is
unique. ∎

######  Lemma 5.11.

Let $\Theta$ be a saturated branch of a tableau. Then we have the following
properties:

  1. i)

If $s\in\mathbf{Nom}$ is an right nominal occuring in $\Theta$, then
$@_{u_{\Theta}(s)}s\in\Theta$.

  2. ii)

For all $s,t\in\mathbf{Nom}$, if $@_{s}t\in\Theta$ then
$u_{\Theta}(s)=u_{\Theta}(t)$.

  3. iii)

For all $s\in\mathbf{Nom}$ occuring in $\Theta$, we have
$u_{\Theta}(u_{\Theta}(s))=u_{\Theta}(s)$.

  4. iv)

For all quasi-subformulas $@_{i}@_{a}\varphi\in\Theta$ of the root formula in
$\Theta$, we have $@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\varphi\in\Theta$.

###### Proof.

  1. i)

If $s$ is a right nominal, then by Lem.5.7 $@_{s}s\in\Theta$ holds. Thus by
definition we have $u_{\Theta}(s)=\min([s]_{\Theta}^{k})\ (k=1,2)$. From this
we have $u_{\Theta}(s)\sim_{\Theta}^{k}s$. Therefore
$@_{u_{\Theta}(s)}s\in\Theta$.

  2. ii)

First, by $@_{s}t\in\Theta$, we have $u_{\Theta}(s)=\min([t]_{\Theta}^{k})\
(k=1,2)$. Also, since $t$ is a right nominal,
$u_{\Theta}(t)=\min([t]_{\Theta}^{k})$ holds by doing the same as (i).
Therefore, $u_{\Theta}(s)=u_{\Theta}(t)$.

  3. iii)

Since the case $u_{\Theta}(s)=s$ is straightforward, so let us suppose
otherwise. Then there is a $t_{1}\in\Theta$ such that
$u_{\Theta}(u_{\Theta}(s))=\min([t_{1}]_{\Theta}^{k})\ (k=1,2)$ and
$@_{u_{\Theta}(s)}t_{1}\in\Theta$. By the definition of $\sim_{\Theta}^{k}$,
$u_{\Theta}(s)\sim_{\Theta}^{k}t_{1}$ holds. Similarly it holds that there is
another $t_{2}\in\mathbf{Nom}$ such that
$u_{\Theta}(s)=\min([t_{2}]_{\Theta}^{k})$ and $s\sim_{\Theta}^{k}t_{2}$. By
the definition of $u_{\Theta}(s)$, $u_{\Theta}(s)\sim_{\Theta}^{k}s$ holds.
From those facts,

$u_{\Theta}(u_{\Theta}(s))=\min([t_{1}]_{\Theta}^{k})=\min([u_{\Theta}(s)]_{\Theta}^{k})=\min([s]_{\Theta}^{k})=\min([t_{2}]_{\Theta}^{k})=u_{\Theta}(s).$

  4. iv)

Suppose that $@_{i}@_{a}\varphi\in\Theta$. Then we have the following four
cases:

    1. a)

$u_{\Theta}(i)=i,u_{\Theta}(a)=a$.

    2. b)

$u_{\Theta}(i)=i,u_{\Theta}(a)=\min([b]_{\Theta}^{2})$.

    3. c)

$u_{\Theta}(i)=\min([j]_{\Theta}^{1}),u_{\Theta}(a)=a$.

    4. d)

$u_{\Theta}(i)=\min([j]_{\Theta}^{1}),u_{\Theta}(a)=\min([b]_{\Theta}^{2})$.

The case (iva) is trivial. In the case (ivd), by definition we have
$@_{i}j,@_{a}b\in\Theta$. Since $\Theta$ is saturated, by Def.5.3(xvi), (xvii)
we have $@_{j}@_{b}\varphi\in\Theta$. Also because
$u_{\Theta}(i)=\min([j]_{\Theta}^{1}),u_{\Theta}(a)=\min([b]_{\Theta}^{2})$,
$j\sim_{\Theta}^{1}u_{\Theta}(i),b\sim_{\Theta}^{2}u_{\Theta}(a)$. Hence
$@_{j}u_{\Theta}(i),@_{b}u_{\Theta}(a)\in\Theta$ holds. By those facts, using
the saturateness of $\Theta$ and Def.5.3(xvi), (xvii), we have
$@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\varphi\in\Theta$. We can do the same in
the case (ivb), (ivc).

∎

To prove completeness, we construct models from tableaux.

######  Definition 5.12.

Given an open branch $\Theta$ of a tableau, product model
$\mathfrak{M}^{\Theta}=(W^{\Theta},R_{h}^{\Theta},R_{v}^{\Theta},V^{\Theta})$
is defined as follows:

$\displaystyle W_{1}^{\Theta}$ $\displaystyle=\\{i\in\mathbf{Nom}_{1}\mid i\
\text{occurs in}\ \Theta\\}$ $\displaystyle W_{2}^{\Theta}$
$\displaystyle=\\{a\in\mathbf{Nom}_{2}\mid a\ \text{occurs in}\ \Theta\\}$
$\displaystyle W^{\Theta}$ $\displaystyle=W_{1}^{\Theta}\times W_{2}^{\Theta}$
$\displaystyle R_{1}^{\Theta}$
$\displaystyle=\\{(i,u_{\Theta}(j))\mid@_{i}\diamondsuit_{1}j\in\Theta\\}$
$\displaystyle R_{2}^{\Theta}$
$\displaystyle=\\{(a,u_{\Theta}(b))\mid@_{a}\diamondsuit_{2}b\in\Theta\\}$
$\displaystyle V^{\Theta}(p)$
$\displaystyle=\\{(i,a)\mid@_{i}@_{a}p\in\Theta\\}\quad\text{where}\quad
p\in\mathbf{Prop}$ $\displaystyle V^{\Theta}(i)$
$\displaystyle=\\{(u_{\Theta}(i)\\}\times W_{2}\quad\text{where}\quad
i\in\mathbf{Nom}_{1}$ $\displaystyle V^{\Theta}(a)$
$\displaystyle=W_{1}\times\\{u_{\Theta}(a)\\}\quad\text{where}\quad
a\in\mathbf{Nom}_{2}$

######  Lemma 5.13 (Model Existence Theorem).

Let $\Theta$ be an open saturated branch of a tableau. Then we have:

$@_{i}@_{a}\varphi\in\Theta\quad\implies\quad\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\varphi.$

###### Proof.

By induction on complexity of $\varphi$.

[$\varphi=p$]

Suppose that $@_{i}@_{a}p\in\Theta$. By Lem.5.11(iv),
$@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}p\in\Theta$. Then by the definition of
$V^{\Theta}$, $(u_{\Theta}(i),u_{\Theta}(a))\in V^{\Theta}(p)$, from which it
follows that $\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models p$.

[$\varphi=\neg p$]

Suppose that $@_{i}@_{a}\neg p\in\Theta$. By Lem.5.11(iv) we have
$@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\neg p\in\Theta$. Since $\Theta$ is open,
$@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}p\notin\Theta$. Then by the definition of
$V^{\Theta}$, $(u_{\Theta}(i),u_{\Theta}(a))\notin V^{\Theta}(p)$ holds.
Therefore, $\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg p$.

[$\varphi=j$]

Suppose that $@_{i}@_{a}j\in\Theta\ (j\in\mathbf{Nom}_{1})$. Since $\Theta$ is
saturated, by Def.5.3(xii) we have $@_{i}j\in\Theta$. Then by Lem.5.11(ii)
$u_{\Theta}(i)=u_{\Theta}(j)$ holds. Thus, $(u_{\Theta}(i),u_{\Theta}(a))\in
V^{\Theta}(j)$. Therefore,
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models j$. We can do the
same in the case $\varphi=b\in\mathbf{Nom}_{2}$.

[$\varphi=\neg j$]

Suppose that $@_{i}@_{a}\neg j\in\Theta\ (j\in\mathbf{Nom}_{1})$. By
Lem.5.11(iv) we have $@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\neg j\in\Theta$.
Since $\Theta$ is saturated, by Def.5.3(xii) and (xiv), $@_{u_{\Theta}(i)}\neg
j,@_{j}j\in\Theta$. From the latter $j$ is a right nominal. Thus by
Lem.5.11(i) we have $@_{u_{\Theta}(j)}j\in\Theta$. Hence,
$@_{u_{\Theta}(i)}\neg j,@_{u_{\Theta}(j)}j\in\Theta$. Since $\Theta$ is open,
$u_{\Theta}(i)\neq u_{\Theta}(j)$. Then by the definition of $V^{\Theta}$ it
follows that $(u_{\Theta}(i),u_{\Theta}(a))\notin V^{\Theta}(j)$. Therefore,
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg j$. We can do
the same in the case $\varphi=\neg b\ (b\in\mathbf{Nom}_{2})$.

[$\varphi=(\psi_{1}\land\psi_{2})$]

Suppose that $@_{i}@_{a}(\psi_{1}\land\psi_{2})\in\Theta$. Since $\Theta$ is
saturated, by Def.5.3(ii) we have
$@_{i}@_{a}\psi_{1}<EMAIL_ADDRESS>by induction hypothesis
both $\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\psi_{1}$ and
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\psi_{2}$ holds.
Therefore by the definition of $\models$, we have
$\mathfrak{M},(u_{\Theta}(i),u_{\Theta}(a))\models\psi_{1}\land\psi_{2}$.

[$\varphi=\neg(\psi_{1}\land\psi_{2})$]

Suppose that $@_{i}@_{a}\neg(\psi_{1}\land\psi_{2})\in\Theta$. Since $\Theta$
is saturated, by Def.5.3(iii) we have either $@_{i}@_{a}\neg\psi_{1}\in\Theta$
or $@_{i}@_{a}\neg\psi_{2}\in\Theta$. However, since $\Theta$ is open, it is
not the case that both $@_{i}@_{a}\psi_{1}\in\Theta$ and
$@_{i}@_{a}\psi_{2}\in\Theta$. Hence by induction hypothesis at most one of
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\psi_{1},\
\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\psi_{2}$ holds.
This implies
$\mathfrak{M},(u_{\Theta}(i),u_{\Theta}(a))\not\models\psi_{1}\land\psi_{2}$.
Therefore,
$\mathfrak{M},(u_{\Theta}(i),u_{\Theta}(a))\models\neg(\psi_{1}\land\psi_{2})$.

[$\varphi=\diamondsuit_{1}\psi$]

Suppose that $@_{i}@_{a}\diamondsuit_{1}\psi\in\Theta$. By Lem.5.11(iv) we
have $@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\diamondsuit_{1}\psi\in\Theta$. Since
$\Theta$ is saturated, by Def.5.3(iv) there is a nominal
$j\in\mathbf{Nom}_{1}$ such that
$@_{u_{\Theta}(i)}\diamondsuit_{1}j,@_{j}@_{u_{\Theta}(a)}\psi\in\Theta$. From
the former and the definition of $R_{h}^{\Theta}$ we have
$(u_{\Theta}(i),u_{\Theta}(a))R_{h}^{\Theta}(u_{\Theta}(j),u_{\Theta}(a))$,
and applying induction hypothesis to the latter, we have
$\mathfrak{M}^{\Theta},(u_{\Theta}(j),u_{\Theta}(u_{\Theta}(a)))\models\psi$.
By Lem.5.11(iii), $u_{\Theta}(u_{\Theta}(a))=u_{\Theta}(a)$ holds. Thus
$\mathfrak{M}^{\Theta},(u_{\Theta}(j),u_{\Theta}(a))\models\psi$. Therefore
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\diamondsuit_{1}\psi$.
We can do the same in the case $\varphi=\diamondsuit_{2}\psi$.

[$\varphi=\neg\diamondsuit_{1}\psi$]

Suppose that $@_{i}@_{a}\neg\diamondsuit_{1}\psi\in\Theta$. By Lem.5.11(iv) we
have $@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\neg\diamondsuit_{1}\psi\in\Theta$.
Now assume there is a nominal $j\in\mathbf{Nom}_{1}$ such that
$(u_{\Theta}(i),u_{\Theta}(a))R_{h}^{\Theta}(j,u_{\Theta}(a))$ (if such a $j$
does not exist, in the model $\mathfrak{M}^{\Theta}$ there is no possible
world which is reachable from $(u_{\Theta}(i),u_{\Theta}(a))$ through
$R_{h}^{\Theta}$. Thus
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg\diamondsuit_{1}\psi$.)
If we take such a $j$, by the definition of $R_{h}^{\Theta}$ there is another
$k\in\mathbf{Nom}_{1}$ such that both $j=u_{\Theta}(k)$ and
$@_{u_{\Theta}(i)}\diamondsuit_{1}k\in\Theta$ hold. Using them and the fact
that $\Theta$ is saturated, by Def.5.3(vi) we have
$@_{k}@_{u_{\Theta}(a)}\neg\psi\in\Theta$. Hence, by induction hypothesis
$\mathfrak{M}^{\Theta},(u_{\Theta}(k),u_{\Theta}(u_{\Theta}(a)))\models\neg\psi$.
Since $j=u_{\Theta}(k)$ and $u_{\Theta}(u_{\Theta}(a))=u_{\Theta}(a)$, we have
$\mathfrak{M}^{\Theta},(j,u_{\Theta}(a))\models\neg\psi$. This holds for all
$j$, so we have
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\square_{1}\neg\psi$.
Therefore
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg\diamondsuit_{1}\psi$.
We can do the same in the case $\varphi=\neg\diamondsuit_{2}\psi$.

[$\varphi=@_{j}\psi$]

Suppose that $@_{i}@_{a}@_{j}\psi\in\Theta\ (j\in\mathbf{Nom}_{1})$. Since
$\Theta$ is saturated, by Def.5.3(viii) we have $@_{j}@_{a}\psi\in\Theta$. By
induction hypothesis,
$\mathfrak{M}^{\Theta},(u_{\Theta}(j),u_{\Theta}(a))\models\psi$ holds.
Therefore
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models@_{j}\psi$. We can
do the same in the case $\varphi=@_{b}\psi\ (b\in\mathbf{Nom}_{2})$.

[$\varphi=\neg@_{j}\psi$]

Suppose that $@_{i}@_{a}\neg@_{j}\psi\in\Theta\ (j\in\mathbf{Nom}_{1})$. Since
$\Theta$ is saturated, by Def.5.3(x) we have $@_{j}@_{a}\neg\psi\in\Theta$. By
induction hypothesis
$\mathfrak{M}^{\Theta},(u_{\Theta}(j),u_{\Theta}(a))\models\neg\psi$ holds.
Then
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models@_{j}\neg\psi$.
Therefore
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg@_{j}\psi$. We
can do the same in the case $\varphi=\neg@_{b}\psi\ (b\in\mathbf{Nom}_{2})$.

∎

######  Theorem 5.14 (Completeness).

The tableau calculus of HPL is complete for the class of product frames, i.e.,
if $\models\varphi$, then $\vdash\varphi$.

###### Proof.

We show the contraposition.

Suppose that $\not\vdash\varphi$. If we choose two arbitrary nominals
$i\in\mathbf{Nom}_{1},a\in\mathbf{Nom}_{2}$ such that $i,a$ do not occur in
$\varphi$, then all tableaux whose root formula is $@_{i}@_{a}\neg\varphi$ is
not closed. Thus, a saturated tableau $\mathcal{T}$ constructed by the method
of Lemma 5.4 is not closed neither. This implies that we have an open and
saturated branch $\Theta$ from $\mathcal{T}$. Then by Lem.5.13, we have
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg\varphi$. By
the definition of $\models$ we have
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\not\models\varphi$ and
this implies that there is a model in which $\varphi$ does not hold.
Therefore, $\not\models\varphi$. ∎

######  Corollary 5.15.

Given two finite sets of formulae $\Gamma$ and $\Delta$, if
$\Gamma\models\Delta$, then $\Gamma\vdash\Delta$.

###### Proof.

By Theorem 5.14 and letting $\varphi$ be
$\bigwedge\Gamma\rightarrow\bigvee\Delta$. ∎

##  6 Hybrid Dependent Product Logic (HdPL)

One property HPL has is that two diamond operators are independent of each
other. What if, for example, one diamond depends on the other? Now we deal
with that logic, called Hybrid dependent product logic (HdPL).

###  6.1 Frames and Models

Frames corresponding HdPL is called _dependent product Kripke frame_. They are
defined as follows.

######  Definition 6.1.

Given a Kripke frame $\mathfrak{F}_{1}=(W_{1},R_{1})$ and a multi-modal Kripke
frame $\mathfrak{F}_{2}=(W_{2},(R_{2}(x))_{x\in W_{1}})$, _dependent product
Kripke frame (d-product frame)_ $\mathfrak{F}=(W,R_{h},R_{v})$ is defined as
follows:

  * •

$W=W_{1}\times W_{2}$.

  * •

$(x,y)R_{h}(x^{\prime},y^{\prime})$ iff $xR_{1}x^{\prime}$ and $y=y^{\prime}$.

  * •

$(x,y)R_{v}(x^{\prime},y^{\prime})$ iff $x=x^{\prime}$ and
$yR_{2}(x)y^{\prime}$.

The definition of _dependent product Kripke model (d-product model)_ is
similar to Def.2.4.

As you can see, the second accessibility relation $R_{2}$ depends on where we
are in the world $x\in W_{1}$.

The satisfaction relation $\models$ of d-product model is the same as Def.2.5,
using the notations $R_{h}$ and $R_{v}$. If we rewrite the definition without
them, then the case of $\diamondsuit_{2}$ is different from that of HPL, as
follows:

$\mathfrak{M},(x,y)\models\diamondsuit_{2}\varphi\quad\text{iff}\quad\text{there
is some}\ y^{\prime}\in W_{2}\ \text{s.t.}\ yR_{2}(x)y^{\prime}\ \text{and}\
\mathfrak{M},(x,y^{\prime})\models\varphi.$

In d-product models, we lose some useful properties. For example, we cannot
swap the order of diamonds freely.

######  Proposition 6.2.

The formula
$\diamondsuit_{1}\diamondsuit_{2}p\leftrightarrow\diamondsuit_{2}\diamondsuit_{1}p$
is not valid on all d-product frames.

###### Proof.

Consider this model $\mathfrak{M}=(W,R_{h},R_{v},V)$ (see Figure 3):

$\displaystyle W_{1}$ $\displaystyle=\\{x_{1},x_{2}\\},\
W_{2}=\\{y_{1},y_{2}\\},$ $\displaystyle R_{1}$
$\displaystyle=\\{(x_{1},x_{2})\\},$ $\displaystyle R_{2}(x_{1})$
$\displaystyle=\emptyset,R_{2}(x_{2})=\\{(y_{1},y_{2})\\},$ $\displaystyle
V(p)$ $\displaystyle=\\{(x_{2},y_{2})\\}.$

Then $\mathfrak{M},(x_{1},y_{1})\models\diamondsuit_{1}\diamondsuit_{2}p$
holds, because we have the three facts, $(x_{1},y_{1})R_{h}(x_{2},y_{1})$,
$(x_{2},y_{1})R_{h}(x_{2},y_{2})$ and $\mathfrak{M},(x_{2},y_{2})\models p$.
However, it is false that
$\mathfrak{M},(x_{1},y_{1})\models\diamondsuit_{2}\diamondsuit_{1}p$, since
there is no world reachable from $(x_{1},y_{1})$ through $R_{v}$. ∎

Figure 3: An example of d-product frame in the proof of Lem.6.2.

######  Remark 6.3.

Note that d-product frames are generalizations of product frames. In fact, by
adding the following condition to given any d-product frame, that becomes a
product frame: For all $x,x^{\prime}\in W_{1}$, $R_{2}(x)=R_{2}(x^{\prime})$
holds.

###  6.2 Tableau Calculus of HdPL

Next, let us define the tableau calculus of HdPL. We can get it by modifying
that of HPL. First we replace two rules, [$\diamondsuit_{2}$] and
[$\neg\diamondsuit_{2}$] with the following:

$@_{i}@_{b}\varphi@_{i}@_{a}\diamondsuit_{2}b@_{i}@_{a}\diamondsuit_{2}\varphi\qquad@_{i}@_{b}\neg\varphi@_{i}@_{a}\diamondsuit_{2}b@_{i}@_{a}\neg\diamondsuit_{2}\varphi$

The restrictions that [$\diamondsuit_{2}$] rule of tableau calculus for HPL
apply to [$\diamondsuit_{2}^{d}$] rule for HdPL. That is,
[$\diamondsuit_{2}^{d}$] can be applied only once per formula and $b$ is a new
nominal in $\mathbf{Nom}_{2}$.

Moreover, we need further restrictions to get HdPL tableau calculus. To
descript them, we add a new concept called _accessibility formula_.

Applying [$\diamondsuit_{2}^{d}$] rule, two new formulae
$@_{i}@_{a}\diamondsuit_{2}b$ and $@_{i}@_{b}\varphi$ are added to the branch.
We called the former formula, containing a new nominal as a right nominal,
_accessibility formula_. Then we are ready to write restrictions to rules for
constructing tableau calculus of HdPL; any premises of rules must not be an
accessibility formula when we apply [$\diamondsuit_{2}^{d}$], [$Id_{1}$] and
[$Id_{2}$].

######  Remark 6.4.

Consider this example of a branch (here $a,b\in\mathbf{Nom}_{2}$):

$@_{i}@_{c}\diamondsuit_{2}b@_{i}@_{a}\diamondsuit_{2}c@_{i}@_{a}\diamondsuit_{2}\diamondsuit_{2}b$

Then $@_{i}@_{a}\diamondsuit_{2}c$ is an accessibility formula, but
$@_{i}@_{c}\diamondsuit_{2}b$ is not. It is because $b$ is not a new nominal
applying [$\diamondsuit_{2}^{d}$] rule.

In summary, the tableau calculus for HdPL is obtained by changing the
following points from that for HPL:

  1. i)

Replacing [$\diamondsuit_{2}$] and [$\neg\diamondsuit_{2}$] as above.

  2. ii)

Add new rule when applying [$\diamondsuit_{2}^{d}$], [$Id_{1}$] and
[$Id_{2}$]: any premises is not an accessibility formula.

###  6.3 Soundness and Completeness

######  Theorem 6.5 (Soundness).

The tableau calculus of HPL is sound for the class of product frames, i.e.,

$\vdash\varphi\quad\implies\quad\models\varphi.$

###### Proof.

The only difference between this proof and that of Thm.4.4 are the cases of
[$\diamondsuit_{2}^{d}$], [$\neg\diamondsuit_{2}^{d}$], [$Id_{1}$] and
[$Id_{2}$] in proof of Lem.4.2. We only do the case of
[$\diamondsuit_{2}^{d}$]. The rest are left to the reader.

Suppose we acquire two new formulae
$@_{j}@_{b}\diamondsuit_{2}c,@_{j}@_{c}\psi$ by applying
[$\diamondsuit_{2}^{d}$] to $\Theta^{m}$. Let $\Theta^{m+1}$ be a branch that
contains both of the two formulae. Since we can apply [$\diamondsuit_{2}^{d}$]
to $\Theta^{m}$, $@_{j}@_{b}\diamondsuit_{2}\psi\in\Theta^{m}$ holds, and by
assumption $\mathfrak{M},(j^{V},b^{V})\models\diamondsuit_{2}\psi$ holds. This
implies that there is some $y^{\prime}\in W_{2}$ such that
$b^{V}R_{2}(j^{V})y^{\prime}$ and
$\mathfrak{M},(j^{V},y^{\prime})\models\psi$. Now we define a new valuation
function $V^{\prime}$ as follows:

$V^{\prime}(s)=\begin{cases}W_{1}\times\\{y^{\prime}\\}&(s=c)\\\
V(s)&(\text{otherwise})\end{cases}$

Define $\mathfrak{M}^{\prime}=(\mathfrak{F},V^{\prime})$. Then we have
$b^{V^{\prime}}R_{2}(j^{V^{\prime}})c^{V^{\prime}}$ and
$\mathfrak{M}^{\prime},(j^{V^{\prime}},c^{V^{\prime}})\models\psi$. By the
latter, F-condition(i) holds for $@_{j}@_{c}\psi\in\Theta^{m+1}$ and
$(j^{V},c^{V})$. By the former,
$\mathfrak{M}^{\prime},(j^{V^{\prime}},b^{V^{\prime}})\models\diamondsuit_{2}c$.
Then, F-condition (i) holds for $@_{j}@_{b}\diamondsuit_{2}c\in\Theta^{m+1}$.
What’s more, since $c$ does not occur in $\Theta^{m}$, interpretation of any
formula in $\Theta^{m}$ does not change even if $V$ changes to $V^{\prime}$.
Therefore, a pair $\Theta^{m+1}$, $\mathfrak{M}^{\prime}$ satisfies
F-condition. ∎

To show completeness, we first show that quasi-subformula property holds even
in the tableau calculus for HdPL.

######  Lemma 6.6.

Let $\mathcal{T}$ be a tableau. If a formula in $\mathcal{T}$ has the form
$@_{i}@_{a}\varphi$, then one of the followings holds:

  * •

$@_{i}@_{a}\varphi$ is a quasi-subformula of the root formula of
$\mathcal{T}$.

  * •

$@_{i}@_{a}\varphi$ is an accessibility formula.

###### Proof.

We only do the case of [$\diamondsuit_{2}^{d}$]. The rest are left to the
reader. Note that we can prove this lemma the same as the proof of Lem.5.2,
except the cases of [$\diamondsuit_{2}^{d}$], [$\neg\diamondsuit_{2}^{d}$],
[$Id_{1}$] and [$Id_{2}$].

Let us consider the case of [$\diamondsuit_{2}^{d}$]. First
$@_{i}@_{a}\diamondsuit_{2}b$ is an accessibility formula. Also,
$@_{i}@_{b}\varphi$ is a quasi-subformula of
$@_{i}@_{a}\diamondsuit_{2}\varphi$, and by induction hypothesis,
$@_{i}@_{a}\diamondsuit_{2}\varphi$ is a quasi-subformula of the root formula.
∎

Next, we change the definition of saturatedness (Definition 5.3) of HdPL
tableau calculus as follows.

######  Definition 6.7.

A branch $\Theta$ of an HdPL tableau is saturated if $\Theta$ satisfies all
the conditions below (we only show the changed conditions from Def.5.3):

v)

If $@_{i}@_{a}\diamondsuit_{2}\varphi\in\Theta$ and it is not an accessibility
forumla, then there is some $b\in\textbf{Nom}_{2}$ such that
$@_{i}@_{a}\diamondsuit_{2}b,@_{i}@_{b}\varphi\in\Theta$.

vii)

If
$@_{i}@_{a}\neg\diamondsuit_{2}\varphi,@_{i}@_{a}\diamondsuit_{2}b\in\Theta$,
then $@_{i}@_{b}\neg\varphi\in\Theta$.

xvi)

If $@_{i}@_{a}\varphi,@_{i}j\in\Theta$ and $@_{i}@_{a}\varphi$ is not an
accessibility forumla, then $@_{j}@_{a}\varphi\in\Theta$.

xvii)

If $@_{i}@_{a}\varphi,@_{a}b\in\Theta$ and $@_{i}@_{a}\varphi$ is not an
accessibility forumla, then $@_{i}@_{b}\varphi\in\Theta$.

The discussion about right nominals does not change in proving the
completeness of the tableau calculus for HdPL. Thus, we can use the same
definition of an urfather of a nominal as that for HPL. Moreover, the
properties of urfathers (Lem.5.11) are preserved in the tableau calculus for
HdPL.

Then we are ready to construct a d-product model from a branch of an HdPL
tableau. Note that the only difference is how we define accessibility
relations $R_{2}$.

######  Definition 6.8.

Given an open branch $\Theta$ of an HdPL tableau, d-product model
$\mathfrak{M}^{\Theta}=(W^{\Theta},R_{h}^{\Theta},R_{v}^{\Theta},V^{\Theta})$
is defined as follows:

$\displaystyle W_{1}^{\Theta}$ $\displaystyle=\\{i\in\mathbf{Nom}_{1}\mid i\
\text{occurs in}\ \Theta\\}$ $\displaystyle W_{2}^{\Theta}$
$\displaystyle=\\{a\in\mathbf{Nom}_{2}\mid a\ \text{occurs in}\ \Theta\\}$
$\displaystyle W^{\Theta}$ $\displaystyle=W_{1}^{\Theta}\times W_{2}^{\Theta}$
$\displaystyle R_{1}^{\Theta}$
$\displaystyle=\\{(i,u_{\Theta}(j))\mid@_{i}\diamondsuit_{1}j\in\Theta\\}$
$\displaystyle R_{2}^{\Theta}(i)$
$\displaystyle=\\{(a,u_{\Theta}(b))\mid@_{i}@_{a}\diamondsuit_{2}b\in\Theta\\}$
$\displaystyle V^{\Theta}(p)$
$\displaystyle=\\{(i,a)\mid@_{i}@_{a}p\in\Theta\\}\quad\text{where}\quad
p\in\mathbf{Prop}$ $\displaystyle V^{\Theta}(i)$
$\displaystyle=\\{(u_{\Theta}(i)\\}\times W_{2}\quad\text{where}\quad
i\in\mathbf{Nom}_{1}$ $\displaystyle V^{\Theta}(a)$
$\displaystyle=W_{1}\times\\{u_{\Theta}(a)\\}\quad\text{where}\quad
a\in\mathbf{Nom}_{2}$

######  Lemma 6.9 (Model Existence Theorem for HdPL).

Let $\Theta$ be an open branch of an HdPL tableau and
$@_{i}@_{a}\varphi\in\Theta$ is a quasi-subformula of a root formula. Then we
have:

$@_{i}@_{a}\varphi\in\Theta\iff\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\varphi.$

###### Proof.

By induction on the complexity of $\varphi$. We only do the case of
$\varphi=\diamondsuit_{2}\psi$ and $\varphi=\neg\diamondsuit_{2}\psi$; the
other case is same as the proof of Lem.5.13.

[$\varphi=\diamondsuit_{2}\psi$]

Suppose that $@_{i}@_{a}\diamondsuit_{2}\psi\in\Theta$. By Lem.5.11(iv) we
have $@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\diamondsuit_{2}\psi\in\Theta$. Since
$\Theta$ is saturated, by Def.6.7(v) there is a nominal $b\in\mathbf{Nom}_{2}$
such that
$@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\diamondsuit_{2}b,@_{u_{\Theta}(i)}@_{b}\psi\in\Theta$.
From the former and the definition of $R_{v}^{\Theta}$ we have
$(u_{\Theta}(i),u_{\Theta}(a))R_{v}^{\Theta}(u_{\Theta}(i),u_{\Theta}(b))$,
and applying induction hypothesis to the latter, we have
$\mathfrak{M}^{\Theta},(u_{\Theta}(u_{\Theta}(i)),u_{\Theta}(b))\models\psi$.
By Lem.5.11(iii), $u_{\Theta}(u_{\Theta}(i))=u_{\Theta}(i)$ holds. Thus
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(b))\models\psi$. Therefore
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\diamondsuit_{2}\psi$.

[$\varphi=\neg\diamondsuit_{2}\psi$]

Suppose that $@_{i}@_{a}\neg\diamondsuit_{2}\psi\in\Theta$. By Lem.5.11(iv) we
have $@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\neg\diamondsuit_{2}\psi\in\Theta$.
Now assume there is a nominal $b\in\mathbf{Nom}_{2}$ such that
$(u_{\Theta}(i),u_{\Theta}(a))R_{v}^{\Theta}(u_{\Theta}(i),b)$ (if such a $b$
does not exist, in the model $\mathfrak{M}^{\Theta}$ there is no possible
world which is reachable from $(u_{\Theta}(i),u_{\Theta}(a))$ through
$R_{v}^{\Theta}$. Thus
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg\diamondsuit_{2}\psi$.)
If we take such a $b$, by the definition of $R_{v}^{\Theta}$ there is another
$c\in\mathbf{Nom}_{2}$ such that both $b=u_{\Theta}(c)$ and
$@_{u_{\Theta}(i)}@_{u_{\Theta}(a)}\diamondsuit_{2}c\in\Theta$ hold. Using
them and the fact that $\Theta$ is saturated, by Def.6.7(vii) we have
$@_{u_{\Theta}(i)}@_{c}\neg\psi\in\Theta$. Hence, by induction hypothesis
$\mathfrak{M}^{\Theta},(u_{\Theta}(u_{\Theta}(i)),u_{\Theta}(c))\models\neg\psi$.
Since $b=u_{\Theta}(c)$ and $u_{\Theta}(u_{\Theta}(i))=u_{\Theta}(i)$, we have
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),b)\models\neg\psi$. This holds for all
$b$, so we have
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\square_{2}\neg\psi$.
Therefore
$\mathfrak{M}^{\Theta},(u_{\Theta}(i),u_{\Theta}(a))\models\neg\diamondsuit_{2}\psi$.

∎

Then we reach the goal.

######  Theorem 6.10 (Completeness).

The tableau calculus of HdPL is complete for the class of d-product frames,
i.e., if $\models\varphi$, then $\vdash\varphi$.

###  6.4 Restriction on frames

By adding a special axiom to the HdPL, it is possible to place restrictions on
the accessibility relation of the Kripke frame. We focus on one of the
property ‘frame is increasing’ introduced in [17]. An example that this
property is used in is $T\times W$ Logic [21], which describes histories with
the same time order. In this logic, we need increasing property to express
“any relationship that exists in the present will exist in the future.”

Then we try adding a corresponding rule of tableau calculus.

######  Definition 6.11.

A d-product frame $\mathfrak{F}=(W_{1}\times W_{2},R_{h},R_{v})$ is
_increasing_ if for all $x,x^{\prime}\in W_{1}$, if $xR_{1}x^{\prime}$, then
$R_{2}(x)\subseteq R_{2}(x^{\prime})$.

######  Proposition 6.12.

[17, Proposition 4.15.] The property that d-product frame
$\mathfrak{F}=(W_{1}\times W_{2},R_{h},R_{v})$ is increasing, is definable by
the following formula:

$@_{a}\diamondsuit_{2}b\rightarrow\square_{1}@_{a}\diamondsuit_{2}b$ (AxInc)

###### Proof.

It suffices to show the following property:

$\mathfrak{F}$ is increasing $\iff$ (AxInc) is valid in $\mathfrak{F}$.

($\Rightarrow$)

Suppose that $\mathfrak{F}$ is increasing. Take a valuation function $V$ and a
point $(x,y)\in W_{1}\times W_{2}$ such that
$(\mathfrak{F},V),(x,y)\models@_{a}\diamondsuit_{2}b$ (we abbreviate it as
$(x,y)\models\varphi$). Then by definition, $a^{V}R_{2}(x)b^{V}$ holds. Take
an $x^{\prime}\in W_{1}$ such that $xR_{1}x^{\prime}$ arbitrary (if we cannot,
$(x,y)\models\square_{1}@_{a}\diamondsuit_{2}b$ is straightforward). Since
$\mathfrak{F}$ is increasing we have $a^{V}R_{2}(x^{\prime})b^{V}$, hence
$(x^{\prime},y)\models@_{a}\diamondsuit_{2}b$ holds. This holds on any
$x^{\prime}$, therefore $(x,y)\models\square_{1}@_{a}\diamondsuit_{2}b$.

($\Leftarrow$)

Suppose that (AxInc) is valid in $\mathfrak{F}$. Take states $x,x^{\prime}\in
W_{1}$ and $y,y^{\prime}\in W_{2}$ such that $xR_{1}x^{\prime}$ and
$yR_{2}(x)y^{\prime}$ . Also, take a valuation function $V$ such that
$a^{V}=y,b^{V}=y^{\prime}$. Then $(x,y)\models@_{a}\diamondsuit_{2}b$ holds,
and by (AxInc) we have $(x,y)\models\square_{1}@_{a}\diamondsuit_{2}b$. By
this fact and $xR_{1}x^{\prime}$ it follows that
$(x^{\prime},y)\models@_{a}\diamondsuit_{2}b$, hence
$yR_{2}(x^{\prime})y^{\prime}$ holds. Therefore, we conclude that
$R_{2}(x)\subseteq R_{2}(x^{\prime})$.

∎

So far, we have confirmed that the frame property of increasing is definable
in Hilbert style axiomatization of HdPL. Now we show that we can construct
HdPL tableau calculus corresponding to increasing frames. Note that the way to
construct is to add not an axiom, but a rule.

######  Definition 6.13.

The rule [$Inc$] is defined as follows:

$@_{j}@_{a}\diamondsuit_{2}b@_{i}\diamondsuit_{1}j@_{i}@_{a}\diamondsuit_{2}b$

where the formulae both above and below line is accessibility formulae.

We write $\mathbf{TAB}+Inc$ for HdPL tableau calculus with the [$Inc$] rule.

We have to fix the definition of saturation. A branch of a tableau of
$\mathbf{TAB}+Inc$ is saturated if it satisfies not only all the conditions of
Def.6.7 but also the following condition:

  * •

If $@_{i}@_{a}\diamondsuit_{2}b,@_{i}\diamondsuit_{1}j\in\Theta$ and they are
accessibility formulae, then $@_{j}@_{a}\diamondsuit_{2}b$.

######  Example 6.14.

The axiom (AxInc) of Prop.AxInc is provable in $\mathbf{TAB}+Inc$. Figure 4 is
a proof using tableau calculus. Note that
$\neg(@_{a}\diamondsuit_{2}b\rightarrow\square_{1}@_{a}\diamondsuit_{2}b)$ is
equivalent to the formula
$@_{a}\diamondsuit_{2}b\land\diamondsuit_{1}\neg@_{a}\diamondsuit_{2}b$.

$\displaystyle 1.$
$\displaystyle@_{i_{0}}@_{a_{0}}(@_{a}\diamondsuit_{2}b\land\diamondsuit_{1}\neg@_{a}\diamondsuit_{2}b)$
$\displaystyle 2.$ $\displaystyle@_{i_{0}}@_{a_{0}}@_{a}\diamondsuit_{2}b$
$\displaystyle(1,[\land])$ $\displaystyle 3.$
$\displaystyle@_{i_{0}}@_{a_{0}}\diamondsuit_{1}\neg@_{a}\diamondsuit_{2}b$
$\displaystyle(1,[\land])$ $\displaystyle 4.$
$\displaystyle@_{i_{0}}@_{a}\diamondsuit_{2}b$ $\displaystyle(2,[@_{2}])$
$\displaystyle 5.$ $\displaystyle{@_{i_{0}}\diamondsuit_{1}j}^{*}$
$\displaystyle(3,[\diamondsuit_{1}])$ $\displaystyle 6.$
$\displaystyle@_{j}@_{a_{0}}\neg@_{a}\diamondsuit_{2}b$
$\displaystyle(3,[\diamondsuit_{1}])$ $\displaystyle 7.$
$\displaystyle{@_{i_{0}}@_{a}\diamondsuit_{2}c}^{*}$
$\displaystyle(4,[\diamondsuit_{2}^{d}])$ $\displaystyle 8.$
$\displaystyle@_{i_{0}}@_{c}b$ $\displaystyle(4,[\diamondsuit_{2}^{d}])$
$\displaystyle 9.$ $\displaystyle@_{j}@_{a}\neg\diamondsuit_{2}b$
$\displaystyle(6,[\neg@_{2}])$ $\displaystyle 10.$
$\displaystyle{@_{j}@_{a}\diamondsuit_{2}c}^{*}$ $\displaystyle(5,7,[Inc])$
$\displaystyle 11.$ $\displaystyle@_{c}b$ $\displaystyle(8,[Red_{2}])$
$\displaystyle 12.$ $\displaystyle@_{j}@_{c}\neg b$
$\displaystyle(9,10,[\neg\diamondsuit_{2}^{d}])$ $\displaystyle 13.$
$\displaystyle@_{c}\neg b$ $\displaystyle(12,[Red_{2}])$ $\displaystyle 14.$
$\displaystyle\bot$ $\displaystyle(11,13)$

The formulae with ∗ is accessibility formulae.

Figure 4: A tableau for HdPL which proves (AxInc).

The next work we do is to show that $\mathbf{TAB}+Inc$ is sound and complete
for the class of increasing d-product frames.

######  Theorem 6.15.

The tableau calculus $\mathbf{TAB}+Inc$ is sound for the class of increasing
d-product frames.

###### Proof.

It suffices to show that Lem.4.2 holds for the $[Inc]$ rule. We can assume
that every d-product frame is increasing.

Let $@_{k}@_{b}\diamondsuit_{2}c$ be a formula acquired by applying $[Inc]$ to
$\Theta^{m}$. Let $\Theta^{m+1}$ be a branch adding
$@_{k}@_{b}\diamondsuit_{2}c$ to $\Theta^{m}$. Then there is some
$j\in\mathbf{Nom}_{1}$ such that
$@_{j}\diamondsuit_{1}k,@_{j}@_{b}\diamondsuit_{2}c\in\Theta^{m}$. Thus for
all $y\in W_{2}$ we have $\mathfrak{M},(j^{V},y)\models\diamondsuit_{1}k$, and
also $\mathfrak{M},(j^{V},b^{V})\models\diamondsuit_{2}c$ holds. They implies
$j^{V}R_{1}k^{V},b^{V}R_{2}(j^{V})c^{V}$. Since we are discussing an
increasing model, it follows that $b^{V}R_{2}(k^{V})c^{V}$. Hence,
$\mathfrak{M},(k^{V},b^{V})\models\diamondsuit_{2}c$ and this shows
$@_{k}@_{b}\diamondsuit_{2}c\in\Theta^{m+1}$ F-condition (i)holds for
$@_{k}@_{b}\diamondsuit_{2}c\in\Theta^{m+1}$. ∎

Proving completeness is a little more complicated. First, we show this lemma:

######  Lemma 6.16.

Let $\Theta$ be an open, saturated branch of a tableau of $\mathbf{TAB}+Inc$.
Then d-product model $\mathfrak{M}^{\Theta}$ of Def.2.4 is increasing.

###### Proof.

Take $i,j\in W_{1}^{\Theta},a,b\in W_{2}^{\Theta}$ such that
$iR_{1}^{\Theta}u_{\Theta}(j),aR_{2}^{\Theta}(i)u_{\Theta}(b)$. Then we have
$@_{i}\diamondsuit_{1}j,@_{i}@_{a}\diamondsuit_{2}b\in\Theta$. We have to
consider two cases whether $@_{i}@_{a}\diamondsuit_{2}b$ is an accessibility
formula or not.

  1. 1.

Suppose that $@_{i}@_{a}\diamondsuit_{2}b$ is an accessibility formula. In
this case, since $\Theta$ is saturated we have
$@_{j}@_{a}\diamondsuit_{2}b\in\Theta$ (by the condition corresponding to
[$Inc$] rule). Therefore $aR_{2}^{\Theta}(j)u_{\Theta}(b)$.

  2. 2.

Suppose that $@_{i}@_{a}\diamondsuit_{2}b$ is not an accessibility formula.
Since $\Theta$ is saturated, by Def.5.3(v) there is some
$c\in\mathbf{Nom}_{2}$ such that
$@_{i}@_{a}\diamondsuit_{2}c,@_{i}@_{c}b\in\Theta$. What is more, by
Def.5.3(xiii) we have $@_{c}b\in\Theta$. Since $@_{i}@_{a}\diamondsuit_{2}c$
is an accessibility formula, $@_{j}@_{a}\diamondsuit_{2}c\in\Theta$ holds.
Hence we have $aR_{2}^{\Theta}(j)u_{\Theta}(c)$. Moreover, by
$@_{c}b\in\Theta$ and Lem.5.11(ii) it follows that
$u_{\Theta}(c)=u_{\Theta}(b)$. Therefore we have
$aR_{2}^{\Theta}(j)u_{\Theta}(b)$.

∎

Now we are ready to show the completeness.

######  Theorem 6.17.

The tableau calculus $\mathbf{TAB}+Inc$ is complete for the class of
increasing d-product frames.

###### Proof.

Note that only accessibility formulae are added when we use the [$Inc$] rule.
Then Lem.5.13 holds even for a tableau branch of $\mathbf{TAB}+Inc$. Moreover,
by Lem.6.16 $\mathfrak{M}^{\Theta}$ is increasing. From these facts, the
theorem follows. ∎

##  7 Conclusion and Future Work

In this paper, we construct a tableau calculus for HPL and HdPL and show the
soundness and completeness of them. However, there is still room for further
work on the tableau calculus of many-dimensional hybrid (dependent) product
logic.

###  7.1 Termination and Decidability

As mentioned in section 1, the tableau calculus for HPL introduced above does
not have the property termination. If tableau calculus had the property
termination, then we could show the decidability of HPL. However,
unfortunately, the following proposition holds:

######  Proposition 7.1.

There is a root formula with which the tableau for HPL has a branch of
infinite length.

###### Proof.

Consider the formula
$@_{i}@_{a}(\diamondsuit_{1}p\land\square_{1}\diamondsuit_{2}q\land\square_{2}\diamondsuit_{1}r)$,
where $p,q,r\in\mathbf{Prop}$. Let us put it as a root formula and construct a
tableau. Then, an infinite branch is generated as Figure 5 (looping 7-12,
where $i_{1},i_{2},a_{1}$ are replaced with $i_{n},i_{n+1},a_{n}$
respectively). Note that we also use $[\square_{1}],[\square_{2}]$ mentioned
in Remark 3.3. ∎

$\displaystyle 1.$
$\displaystyle@_{i_{0}}@_{a_{0}}(\diamondsuit_{1}p\land\square_{1}\diamondsuit_{2}q\land\square_{2}\diamondsuit_{1}r)$
$\displaystyle 2.$ $\displaystyle@_{i_{0}}@_{a_{0}}\diamondsuit_{1}p$
$\displaystyle(1,[\land])$ $\displaystyle 3.$
$\displaystyle@_{i_{0}}@_{a_{0}}\square_{1}\diamondsuit_{2}q$
$\displaystyle(1,[\land])$ $\displaystyle 4.$
$\displaystyle@_{i_{0}}@_{a_{0}}\square_{2}\diamondsuit_{1}r$
$\displaystyle(1,[\land])$ $\displaystyle 5.$
$\displaystyle@_{i_{0}}\diamondsuit_{1}{i_{1}}$
$\displaystyle(2,[\diamondsuit_{1}])$ $\displaystyle 6.$
$\displaystyle@_{i_{1}}@_{a_{0}}p$ $\displaystyle(2,[\diamondsuit_{1}])$
$\displaystyle 7.$ $\displaystyle@_{i_{1}}@_{a_{0}}\diamondsuit_{2}q$
$\displaystyle(3,5,[\square_{1}])$ $\displaystyle 8.$
$\displaystyle@_{a_{0}}\diamondsuit_{2}{a_{1}}$
$\displaystyle(7,[\diamondsuit_{2}])$ $\displaystyle 9.$
$\displaystyle@_{i_{1}}@_{a_{1}}q$ $\displaystyle(7,[\diamondsuit_{2}])$
$\displaystyle 10.$ $\displaystyle@_{i_{0}}@_{a_{1}}\diamondsuit_{1}r$
$\displaystyle(4,8,[\square_{2}])$ $\displaystyle 11.$
$\displaystyle@_{i_{0}}\diamondsuit_{1}{i_{2}}$
$\displaystyle(10,[\diamondsuit_{1}])$ $\displaystyle 12.$
$\displaystyle@_{i_{2}}@_{a_{1}}r$ $\displaystyle(10,[\diamondsuit_{1}])$
$\displaystyle 13.$ $\displaystyle@_{i_{2}}@_{a_{0}}\diamondsuit_{2}q$
$\displaystyle(3,11,[\square_{1}])$ $\displaystyle 14.$
$\displaystyle@_{a_{0}}\diamondsuit_{2}{a_{2}}$
$\displaystyle(13,[\diamondsuit_{2}])$ $\displaystyle 15.$
$\displaystyle@_{i_{2}}@_{a_{2}}q$ $\displaystyle(13,[\diamondsuit_{2}])$
$\displaystyle 16.$ $\displaystyle@_{i_{0}}@_{a_{2}}\diamondsuit_{1}r$
$\displaystyle(4,14,[\square_{2}])$ $\displaystyle 17.$
$\displaystyle@_{i_{0}}\diamondsuit_{1}{i_{3}}$
$\displaystyle(16,[\diamondsuit_{1}])$ $\displaystyle 18.$
$\displaystyle@_{i_{3}}@_{a_{2}}r$ $\displaystyle(16,[\diamondsuit_{1}])$
$\displaystyle\vdots$ Figure 5: An example of tableau for HPL which has an
infinite branch.

Thus if we want to construct a tableau calculus with termination, we have to
modify the present system such as fixing some rules or adding some
restrictions.

The problem of whether the tableau calculus for HdPL has termination is still
an open problem. Note that with a formula
$@_{i}@_{a}(\diamondsuit_{1}p\land\square_{1}\diamondsuit_{2}q\land\square_{2}\diamondsuit_{1}r)$
we can construct a finite tableau for HdPL (we leave it to the reader).

###  7.2 What if we have more dimension?

The tableau calculus we have can be easily extended to $n$-dimensional HPL
($n\geq 3$). Soundness and completeness can be proved similarly to the method
of section 4 and 5.

However, we cannot construct any tableau calculus with termination, since it
is known that every product modal logic with more than 3-dimensions is
undecidable (see [11, 10]).

###  7.3 Adding more operators

The system we have considered so far is a system containing only the most
basic operator, @. The other operators in hybrid logic are the existential
operator $E$ and the downarrow operator $\downarrow$. In orthodox (that is,
one-dimensional) hybrid logic, $E\varphi$ can be interpreted as ”there exists
a possible world where $\varphi$ is true” and $\downarrow x.\varphi$ can be
interpreted as ”when the current world is described as $x$, $\varphi$ is
true”. See [5] for more details.

Let $E_{1},E_{2}$ be existential operators and
$\downarrow_{1}x,\downarrow_{2}y$ be downarrow operators for the first and the
second dimension. The rules for these operators will be as follows:

$\displaystyle@_{j}@_{a}\varphi@_{i}@_{a}E_{1}\varphi\qquad@_{j}@_{a}\neg\varphi@_{i}@_{a}\neg
E_{1}\varphi$
$\displaystyle@_{i}@_{a}\varphi[i/x]@_{i}@_{a}\downarrow_{1}x.\varphi\qquad@_{i}@_{b}\neg\varphi[i/x]<EMAIL_ADDRESS>
*1: $j\in\mathbf{Nom}_{1}$ does not occur in previous part of this branch.

*2: $j\in\mathbf{Nom}_{2}$ has to occur in previous part of this branch.

*3: $\varphi[i/x]$ is a formula obtained by replacing all the occurence of $x$ in $\varphi$ with a nominal $i$.

We does not know whether they affect termination of tableau calculus. However
it is shown in [1] that general hybrid logic containing $\downarrow$ is
undecidable.

###  7.4 Adding more rules

Adding axioms to the hybrid tableau calculus makes them rich. With the proper
addition of rules, we can construct tableau calculi for S4 or S5.

In a previous work [8], some axioms corresponding to reflexivity,
irreflexivity, transitivity, and so on are added to the tableau calculus for
hybrid logic with preserving termination. Applying this method, we also
acquire many-dimensional tableau calculi corresponding to S4n or S5n. In terms
of automatic calculation, however, it will be better to add axioms as the form
of an inference rule.

Moreover, for HdPL tableau calculus, some rules corresponding to dependencies
can be added like section 6.4. This should also be added in the form of
inference rules.

## Acknowledgment

This paper is based on my two presentations at conferences in Japan. The first
one related to Sections 2-5 is presented at the conference in RIMS held in
December 2021([13]). The other related to Section 6 is presented at MLG2021 in
March 2022.

I would like to thank Ryo Kashima and Katsuhiko Sano for their guidance in
writing this paper. In particular, Katsuhiko Sano taught me how to write
Figure 1 and 3. Tatsuya Abe and Ken Shiotani provided comments on my
presentation at the seminar.

## References

  * [1] Carlos Areces, Patrick Blackburn, and Maarten Marx.  A road-map on complexity for hybrid logics.  In International Workshop on Computer Science Logic, pages 307–321. Springer, 1999.
  * [2] Patrick Blackburn.  Arthur Prior and hybrid logic.  Synthese, 150:329–372, 2006.
  * [3] Patrick Blackburn, Thomas Bolander, Torben Braüner, and Klaus Frovin Jørgensen.  Completeness and termination for a seligman-style tableau system.  Journal of Logic and Computation, 27(1):81–107, 2017.
  * [4] Patrick Blackburn and Jerry Seligman.  Hybrid languages.  Journal of Logic, Language and Information, 4(3):251–272, 1995\.
  * [5] Patrick Blackburn and Balder ten Cate.  Pure extensions, proof rules, and hybrid axiomatics.  Studia Logica, 84(2):277–322, 2006.
  * [6] Patrick Blackburn and Miroslava Tzakova.  Hybrid languages and temporal logic.  Logic journal of IGPL, 7(1):27–54, 1999.
  * [7] Thomas Bolander and Patrick Blackburn.  Termination for hybrid tableaus.  Journal of Logic and Computation, 17(3):517–554, 2007.
  * [8] Thomas Bolander and Patrick Blackburn.  Terminating tableau calculi for hybrid logics extending K.  Electronic Notes in Theoretical Computer Science, 231:21–39, 2009\.
  * [9] Torben Braüner.  Hybrid Logic and its Proof-Theory, volume 37.  Springer Science & Business Media, 2011.
  * [10] Dov M. Gabbay.  Many-Dimensional Modal Logics: Theory and Applications.  Elsevier North Holland, 2003.
  * [11] Robin Hirsch, Ian Hodkinson, and Agnes Kurucz.  On modal logics between K $\times$ K $\times$ K and S5 $\times$ S5 $\times$ S5.  Journal of Symbolic Logic, 67(1):221–234, 2002.
  * [12] Andrzej Indrzejczak.  A survey of proof systems for hybrid logics.  In Hybrid Logic and Applications (HyLo 2022), 2022.
  * [13] Yuki Nishimura.  Tableau calculus of hybrid product logic.  In Theory and Applications of Proof and Computation, pages 1–11, 2022.
  * [14] Graham Priest.  An Introduction to Non-Classical Logic: From If to Is.  Cambridge University Press, second edition, 2008.
  * [15] Arthur N. Prior.  Past, Present and Future.  Oxford University Press, 1967.
  * [16] Arthur N. Prior.  Papers on Time and Tense.  Oxford University Press, 1968.
  * [17] Katsuhiko Sano.  Axiomatizing hybrid products: How can we reason many-dimensionally in hybrid logic?  Journal of Applied Logic, 8(4):459–474, 2010.
  * [18] Katsuhiko Sano.  Seligman-style internalized sequent calculus for two dimensional reasoning.  In Proceedings of the Eleventh International Workshop on Logic and Engineering of Natural Language Semantics (LENLS12), pages 163–172, 2015\.
  * [19] Jeremy Seligman, Fenrong Liu, and Patrick Girard.  Logic in the community.  In Proceedings of the 4th Indian Conference on Logic and Its Applications, pages 178–188. Springer Berlin Heidelberg, 2011.
  * [20] Balder ten Cate.  Model Theory for Extended Modal Languages.  PhD thesis, University of Amsterdam, 2005.
  * [21] Franz von Kutschera.  T $\times$ W completeness.  Journal of Philosophical Logic, 26(3):241–250, 1997.