Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus

Abstract

This paper positively solves an open problem if it is possible to provide a Hilbert system to Epistemic Logic of Friendship (EFL) by Seligman, Girard and Liu. To find a Hilbert system, we first introduce a sound, complete and cut-free tree (or nested) sequent calculus for EFL, which is an integrated combination of Seligman’s sequent calculus for basic hybrid logic and a tree sequent calculus for modal logic. Then we translate a tree sequent into an ordinary formula to specify a Hilbert system of EFL and finally show that our Hilbert system is sound and complete for an intended two-dimensional semantics.

1 Introduction

Epistemic Logic of Friendship ($\mathbf {EFL}$) is a version of two-dimensional modal logic proposed by [22,23,24]. Compared to the ordinary epistemic logic [14], one of the key features of their logic is to encode the information of agents into the object language by a technique of hybrid logic [1, 3]. Then, a propositional variable p can be read as an indexical proposition such as “I am p" and we may formalize the sentences like “I know that all my friends is p" or “Each of my friends knows that he/she is p". Moreover, the authors of [23, 24] provided a dynamic mechanism for capturing public announcements [19], announcements to all the friends, and private announcements [2] and established a relative completeness result (cf. [12, 23, 24]). This paper focuses on the problem of axiomatizing $\mathbf {EFL}$ in terms of Hilbert system, i.e., the static part of their framework.

A difficulty of the problem comes from a combination of modal logic for agents’ knowledge and hybrid logic for a friendship relation among agents. If we combine two hybrid logics over two-dimensional semantics of [22,23,24], it is noted that there is an axiomatization of all valid formulas in the semantics by [20, p. 471]. Our approach to tackle the problem is via a sequent calculus, whose idea is originally from Gentzen. In particular, our notion of sequent for $\mathbf {EFL}$ can be regarded as a combination of a tree or nested sequent [8, 15] for modal logic and @-prefixed sequent [7, 21] for hybrid logic. One of the merits of our notion of sequent is that we can translate our sequent into an ordinary formula. This allows us to specify our desired Hilbert system for $\mathbf {EFL}$. We note that [9] independently provided a prefixed tableau system for a dynamic extension of $\mathbf {EFL}$. There are at least three points we should emphasize on our work. First, our tree sequent system is quite simpler than the tableau system given in [9], i.e., the number of rules of our sequent system is almost half of the number of rules of their system. Second, it is not clear if a prefixed formula in [9] for the tableau calculus can be translated into an ordinary formula. Their result is not concerned with Hilbert system. Third, their syntax contains a special kind of propositional variable (called feature proposition) and they include a tableau rule called propositional cut to handle such propositions. On the other hand, we can show that our tree sequent calculus enjoys the cut elimination theorem, the most fundamental theorem in proof-theory.

We proceed as follows. Section 2 introduces the syntax and semantics of $\mathbf {EFL}$. Section 3 provides a tree sequent calculus for $\mathbf {EFL}$ and establishes the soundness of the sequent calculus (Theorem 1). Section 4 establishes a completeness result of a cut-free fragment of our sequent calculus (Theorem 2). As a corollary, we also provide a semantic proof of the cut elimination theorem of our sequent calculus (Corollary 1). Section 5 specifies a Hilbert system of $\mathbf {EFL}$, and provides a syntactic proof of the equipollence between our proposed Hilbert system and our tree sequent calculus, which implies the soundness and completeness results for our Hilbert system (Corollary 2). Section 6 extends our technical results to cover extensions of $\mathbf {EFL}$ where a modal operator for states (or a knowledge operator) obeys $\mathbf {S4}$ or $\mathbf {S5}$ axioms and a friendship relation satisfies some universal properties (Theorem 5). The result of this section subsumes the logic given in [9], provided we drop the dynamic operator from the syntax of [9]. Section 7 concludes this paper.

2 Syntax and Two-Dimensional Kripke Semantics

Our syntax $\mathcal {L}$ consists of the following vocabulary: a countably infinite set $\mathsf {Prop} = \{{p,q,r,\ldots }\}$ of propositional variables, a countably infinite set $\mathsf {Nom} = \{{n,m,l,\ldots }\}$ of agent nominal variables, the Boolean connectives of $\rightarrow$ (the implication) and $\bot$ (the falsum), the satisfaction operators @ and the friendship operator $\mathsf {F}$ as well as the modal operator $\Box$. We note that an agent nominal $n \in \mathsf {Nom}$ is a syntactic name of an agent or an individual, which amounts to a constant symbol of the first-order logic, while n is read indexically as “I am n.” Similarly, we read a propositional variable $p \in \mathsf {Prop}$ also indexically by “I am p,” e.g., “I am in danger.” The set $\mathsf {Form}$ of formulas in $\mathcal {L}$ is defined inductively as follows:

$$ \mathsf {Form} \ni \varphi {:}{:} = n \,|\, p \,|\, \bot \,|\, \varphi \rightarrow \varphi \,|\, @_{n}\varphi \,|\, \mathsf {F} \varphi \,|\, \Box \varphi , $$

where $n \in \mathsf {Nom}$ and $p \in \mathsf {Prop}$. Boolean connectives other than $\rightarrow$ or $\bot$ are introduced as ordinary abbreviations. We define the dual of $\Box$ as $\Diamond := \lnot \Box \lnot$ and the dual of $\mathsf {F}$ as $\langle \mathsf {F} \rangle := \lnot \mathsf {F} \lnot$. Moreover, a formula of the form $@_{n} \varphi$ is said to be @-prefixed. Let us read $\Box$ as “I know that.” Here are some examples of how to read formulas:

• $\Box p$, read as “I know that I am p.”

• $@_{n}\Box p$, read as “n knows that she is p.”

• $\Box @_{n}p$, read as “I know that agent n is p.”

• $\mathsf {F} p$, read as “all my friends are p.”

• $\mathsf {F} \Box p$, read as “all my friends know that they are p.”

• $\Box \mathsf {F} p$, read as “I know that all my friends are p.”

• $@_{n} \langle \mathsf {F}\rangle m$, read as “agent m is a friend of agent n.”

We say that a mapping $\sigma : \mathsf {Prop} \cup \mathsf {Nom} \rightarrow \mathsf {Form}$ is a uniform substitution if $\sigma$ uniformly substitutes propositional variables by formulas and agent nominals by agent nominals and we use $\varphi \sigma$ to mean the result of applying a uniform substitution $\sigma$ to $\varphi$. In particular, we use $\varphi [n/k]$ to mean the result of substituting each occurrence of agent nominal k in $\varphi$ uniformly with agent nominal n.

An model $\mathfrak {M}$ for our syntax $\mathcal {L}$ is a tuple $(W, A, (R_{a})_{a \in A}, (\asymp _{w})_{w \in W},V)$, where W is a non-empty set of possible states, A is a non-empty set of agents, $R_{a}$ is a binary relation on W ($a \in A$), $\asymp _{w}$ is a binary relation on A (called a friendship relation, $w \in W$), V is a valuation function $\mathsf {Prop} \cup \mathsf {Nom} \rightarrow \mathcal {P}(W \times A)$ such that V(n) is a subset of $W \times A$ of the form $W \times \{{a}\}$, where we denote such unique element a by $\underline{n}$. We do not require any property for $R_{a}$ and $\asymp _{w}$ but we will come back to this point in Sect. 6. We say that a tuple $\mathfrak {F} = (W, A, (R_{a})_{a \in A}, (\asymp _{w})_{w \in W})$ without a valuation is a frame.

Let $\mathfrak {M} = (W, A, (R_{a})_{a \in A}, (\asymp _{w})_{w \in W},V)$ be a model. Given a pair $(w,a) \in W \times A$ and a formula $\varphi$, the satisfaction relation $\mathfrak {M},(w,a) \, \models \,\varphi$ (read “agent a satisfies $\varphi$ at w in $\mathfrak {M}$ ”) inductively as follows:

$$ \begin{array}{ll} \mathfrak {M}, (w,a) \, \models \, p &{} \,\mathrm {iff}\,\; (w,a) \in V(p), \\ {\mathfrak {M}}, (w,a) \, \models \, n &{} \,\mathrm {iff}\,\; \underline{n} = a, \\ {\mathfrak {M}}, (w,a) \,\not \models \,\bot &{} \\ {\mathfrak {M}}, (w,a) \, \models \, \varphi \rightarrow \psi &{} \,\mathrm {iff}\,\; {\mathfrak {M}}, (w,a) \, \models \, \varphi \text { implies } {\mathfrak {M}}, (w,a) \, \models \, \psi \\ {\mathfrak {M}}, (w,a)\, \models \,@_{n} \varphi &{} \,\mathrm {iff}\,\; \mathfrak {M}, (w,\underline{n}) \, \models \, \varphi , \\ \mathfrak {M}, ({w},a) \, \models \,\mathsf {F} \varphi &{} \,\mathrm {iff}\,\; (a\asymp _{{w}}b \text { implies }\mathfrak {M}, ({w},b) \, \models \, \varphi ) \text { for all agents } b \in A, \\ \mathfrak {M}, (w,{a}) \, \models \, \Box \varphi &{} \,\mathrm {iff}\,\; (wR_{{a}}v \text { implies }\mathfrak {M}, (v,{a}) \, \models \, \varphi ) \text { for all states } v \in W. \\ \end{array} $$

Given a class $\mathbb {M}$ of models, we say that a formula $\varphi$ is valid in $\mathbb {M}$ when $\mathfrak {M}, (w,a) \, \models \, \varphi$ for all pairs (w, a) in $\mathfrak {M}$ and all models $\mathfrak {M} \in \mathbb {M}$. This paper tackles the question if the set of all valid formulas in the class of all models is axiomatizable.

Fig. 1.

A tree sequent

3 Tree Sequent Calculus of Epistemic Logic of Friendship

A label is inductively defined as follows: Any natural number is a label; if $\alpha$ is a label, n is an agent nominal in $\mathsf {Nom}$ and i is a natural number, then $\alpha \cdot _{n} i$ is also a label. When $\beta$ is $\alpha \cdot _{n} i$, then we say that $\beta$ is an n -child of $\alpha$ or that $\alpha$ is an n -parent of $\beta$. A tree $\mathcal {T}$ is a set of labels such that the set contains the unique natural number j as the root label and the set is closed under taking the parent of a label, i.e., $\alpha \cdot _{n} i \in \mathcal {T}$ implies $\alpha \in \mathcal {T}$ for all labels $\alpha$, agent nominals n and natural numbers i. For example, all of 0, $0\cdot _{n}1$ and $0\cdot _{k} 2$ are labels and they form a finite tree.

Given a label $\alpha$ and an @-prefixed formula $\varphi$, the expression $\alpha : \varphi$ is said to be a labelled formula, where recall that an @-prefixed formula is of the form $@_{n}\varphi$. A tree sequent is an expression of the form

$$\begin{aligned} \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \end{aligned}$$

where $\varGamma$ and $\varDelta$ are finite sets of labelled formulas, $\mathcal {T}$ is a finite tree of labels, and all the labels in $\varGamma$ and $\varDelta$ are in $\mathcal {T}$. A tree sequent “$\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$” is read as “if we assume all labelled formulas in $\varGamma$, then we may conclude some labelled formulas in $\varDelta$.” A tree sequent $0:@_{n}\varphi , 0\cdot _{k}2: @_{m} \rho \mathop {\Rightarrow }\limits ^{\mathcal {T}} 0:@_{m}\psi , 0\cdot _{n}1: @_{k} \theta$ is represented as in Fig. 1, where $\mathcal {T} = \{{0, 0\cdot _{n}1, 0\cdot _{k} 2}\}$. That is, 0, $0\cdot _{n}1$ and $0\cdot _{k} 2$ are “addresses” of the root, the left leaf, and the right leaf, respectively.

Table 1. Tree Sequent Calculus $\mathsf {T}\mathbf {EFL}$

Table 1 provides all the initial sequents and all the inference rules of tree sequent calculus $\mathsf {T}\mathbf {EFL}$, where recall that $\varphi [m/k]$ is the result of substituting each occurrence of agent nominal k in $\varphi$ with agent nominal m. The system without the cut rule is denoted by $\mathsf {T}\mathbf {EFL}^{-}$. A derivation in $\mathsf {T}\mathbf {EFL}$ (or $\mathsf {T}\mathbf {EFL}^{-}$) is a finite tree generated from initial sequents by inference rules of $\mathsf {T}\mathbf {EFL}$ (or $\mathsf {T}\mathbf {EFL}^{-}$, respectively). The height of a derivation is defined as the maximum length of branches in the derivation from the end (or root) sequent to an initial sequent. A tree sequent $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is said to be provable in $\mathsf {T}\mathbf {EFL}$ (or $\mathsf {T}\mathbf {EFL}^{-}$) if there is a derivation in $\mathsf {T}\mathbf {EFL}$ (or $\mathsf {T}\mathbf {EFL}^{-}$, respectively) such that the root of the tree is $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$.

Let $\mathfrak {M} = (W, A, (R_{a})_{a \in A}, (\asymp _{w})_{w \in W},V)$ be a model and $\mathcal {T}$ a tree of labels. A function $f: \mathcal {T} \rightarrow W$ is a $\mathcal {T}$ -assignment in $\mathfrak {M}$ if, whenever $\beta$ is an n-child of $\alpha$ in $\mathcal {T}$, $f(\alpha ) R_{\underline{n}} f(\beta )$ holds. When it is clear from the context, we drop “$\mathcal {T}$-” from “$\mathcal {T}$-assignment”. Given any labelled formula $\alpha :@_{n}\varphi$ with $\alpha \in \mathcal {T}$ and any $\mathcal {T}$-assignment in $\mathfrak {M}$, we define the satisfaction for a labelled formula as follows:

$$ \mathfrak {M},f \, \models \, \alpha :@_{n}\varphi \; \,\mathrm {iff}\,\; \mathfrak {M}, ({f}(\alpha ), \underline{n}) \, \models \, \varphi . $$

where “$\mathfrak {M},f \,\models \, \alpha :@_{n}\varphi$” is read as “$\alpha :@_{n}\varphi$ is true at $(\mathfrak {M},f)$”. Given a tree sequent $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ and a $\mathcal {T}$-assignment in $\mathfrak {M}$, we say that $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is true in $(\mathfrak {M}, f)$ (notation: $\mathfrak {M},f \, \models \, \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$) if, whenever all labelled formulas of $\varGamma$ is true in $(\mathfrak {M}, f)$, some labelled formulas of $\varDelta$ is true in $(\mathfrak {M}, f)$. The following theorem is easy to establish.

Theorem 1

(Soundness of $\mathsf {T}\mathbf {EFL}$ ). If a tree sequent $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}$ then $\mathfrak {M},f \, \models \, \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ for all models $\mathfrak {M}$ and all assignments f.

Let us say that an inference rule is height-preserving admissible in $\mathsf {T}\mathbf {EFL}^{-}$ (or $\mathsf {T}\mathbf {EFL}$) if, whenever all uppersequents (premises) of the inference rule is provable by derivations with height no more than n, then the lowersequent (conclusion) of the rule is provable by a derivation whose height is at most n. By induction on height n of a derivation, we can prove the following.

Proposition 1

The following weakening rules $(\mathsf {w}R)$ and $(\mathsf {w}L)$ are height-preserving admissible in $\mathsf {T}\mathbf {EFL}^{-}$ and $\mathsf {T}\mathbf {EFL}$. Moreover, the following substitution rule $(\mathsf {sub})$ is height-preserving admissible in $\mathsf {T}\mathbf {EFL}^{-}$ and $\mathsf {T}\mathbf {EFL}$:

where $\sigma$ is a uniform substitution, $\mathcal {T}\sigma$ is the resulting tree by substituting agent nominals in $\mathcal {T}$ by $\sigma$, $\varTheta \sigma := \{{\alpha \sigma : \varphi \sigma \in } \,|\, {\alpha :\varphi \in \varTheta } \}$ and $\alpha \sigma \in \mathcal {T} \sigma$ is the corresponding label to $\alpha \in \mathcal {T}$ by $\sigma$.

4 Semantic Completeness of Tree Sequent Calculus of Epistemic Logic of Friendship

In what follows in this section, sets $\varGamma$, $\varDelta$, etc. of labelled formulas and a tree $\mathcal {T}$ of labels can be possibly (countably) infinite. Following this change, we say that a possibly infinite tree-sequent $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}^{-}$ if there exist finite sets $\varGamma ' \subseteq \varGamma$ and $\varDelta ' \subseteq \varDelta$ and finite subtree $\mathcal {T}'$ of $\mathcal {T}$ such that $\varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}'} \varDelta '$ is provable in $\mathsf {T}\mathbf {EFL}^{-}$.

Definition 1 (Saturated tree sequent)

A possibly infinite tree sequent$\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is saturated if it satisfies the following conditions:

(rep1) :

If $\alpha :@_{n}m \in \varGamma$ and $\alpha : \varphi [n/k] \in \varGamma$ then $\alpha : \varphi [m/k] \in \varGamma$.

(rep2) :

If $\alpha :@_{m}n \in \varGamma$ and $\alpha : \varphi [n/k] \in \varGamma$ then $\alpha : \varphi [m/k] \in \varGamma$.

(ref $_{=}$ ) :

$\alpha :@_{n}n \in \varGamma$ for all labels $\alpha \in \mathcal {T}$.

(rigid $_{=}$ ) :

If $\alpha :@_{n}m \in \varGamma$ then $\beta : @_{n}m \in \varGamma$ for all labels $\beta \in \mathcal {T}$.

( $\rightarrow$ r) :

If $\alpha :@_{n}(\varphi \rightarrow \psi ) \in \varDelta$ then $\alpha :@_{n} \varphi \in \varGamma$ and $\alpha :@_{n} \psi \in \varDelta$.

( $\rightarrow$ l) :

If $\alpha :@_{n}(\varphi \rightarrow \psi ) \in \varGamma$ then $\alpha :@_{n}\varphi \in \varDelta$ or $\alpha :@_{n} \psi \in \varGamma$.

(@r) :

If $\alpha :@_{n}@_{m}\varphi \in \varDelta$ then $\alpha :@_{m}\varphi \in \varDelta$.

(@l) :

If $\alpha :@_{n}@_{m}\varphi \in \varGamma$ then $\alpha :@_{m}\varphi \in \varGamma$.

( $\mathsf {F}$ r) :

If $\alpha :@_{n}\mathsf {F}\varphi \in \varDelta$ then $\alpha :@_{n} \langle \mathsf {F} \rangle m \in \varGamma$ and $\alpha :@_{m}\varphi \in \varDelta$ for some nominal m.

( $\mathsf {F}$ l) :

If $\alpha :@_{n}\mathsf {F}\varphi \in \varGamma$ then $\alpha :@_{n}\langle \mathsf {F}\rangle m \in \varDelta$ or $\alpha : @_{m}\varphi \in \varGamma$ for all nominals m.

( $\Box$ r) :

If $\alpha :@_{n}\Box \varphi \in \varDelta$ then $\beta :@_{n}\varphi \in \varDelta$ for some n-child $\beta$ of $\alpha$.

( $\Box$ l) :

If $\alpha :@_{n}\Box \varphi \in \varGamma$ then $\beta :@_{n}\varphi \in \varGamma$ for all n-children $\beta$ of $\alpha$.

By the standard argument, we can show the following saturation lemma.

Lemma 1

Let $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ be an unprovable tree sequent in $\mathsf {T}\mathbf {EFL}^{-}$. Then, there exists a saturated (possibly infinite) sequent $\varGamma ^{+} \mathop {\Rightarrow }\limits ^{\mathcal {T}^{+}} \varDelta ^{+}$ such that it is still unprovable in $\mathsf {T}\mathbf {EFL}^{-}$ and it extends the original tree sequent, i.e., $\varGamma \subseteq \varGamma ^{+}$, $\varDelta \subseteq \varDelta ^{+}$ and $\mathcal {T} \subseteq \mathcal {T}^{+}$.

Lemma 2

Let $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ be a saturated and unprovable tree sequent in $\mathsf {T}\mathbf {EFL}^{-}$. Define the derived model $\mathfrak {M} = (\mathcal {T}, A, (R_{a})_{a \in A}, (\asymp _{\alpha })_{\alpha \in \mathcal {T}},V)$ from $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ by:

• $A := \{{|n|} \,|\, {n\; is\; an\; agent\; nominal} \}$, where |n| is an equivalence class of an equivalence relation $\sim$ which is defined as: $n \sim m$ $\,\mathrm {iff}\,$ $\alpha :@_{n}m \in \varGamma$ for some $\alpha \in \mathcal {T}$.

• $\alpha R_{|n|} \beta$ iff $\beta$ is an m-child of $\alpha$ for some $m \in |n|$.

• $|n| \asymp _{\alpha } |m|$ iff $\alpha : @_{n} \langle \mathsf {F} \rangle m \in \varGamma$.

• $(\alpha , |n|) \in V(m)$ iff $\alpha : @_{n} m \in \varGamma$ $(m \in \mathsf {Nom})$.

• $(\alpha , |n|) \in V(p)$ iff $\alpha : @_{n} p \in \varGamma$ $(p \in \mathsf {Prop})$.

Then, $\mathfrak {M}$ is a model. Moreover, for every labelled formula $\alpha :@_{n}\varphi$, we have

$(\mathrm {i})$ If $\alpha :@_{n}\varphi \in \varGamma$ then $\mathfrak {M},(\alpha ,|n|) \, \models \, \varphi$;

$(\mathrm {ii})$ If $\alpha :@_{n}\varphi \in \varDelta$ then $\mathfrak {M},(\alpha ,|n|) \,\not \models \, \varphi$.

Proof

First, let us check that $\mathfrak {M}$ is a model. First of all, note that we can easily verify that $\sim$ is an equivalence relation by the conditions $(\mathbf {ref}_{=})$, $(\mathbf {rep}_{i})$ and $(\mathbf {rigid}_{=})$ of Definition 1. We can also check that if $n \sim m$ then $R_{|n|} = R_{|m|}$ and that if $n \sim n'$ and $m \sim m'$ then $\alpha :@_{n}\langle \mathsf {F}\rangle m \in \varGamma$ iff $\alpha :@_{n'}\langle \mathsf {F}\rangle m' \in \varGamma$. So both of $R_{|n|}$ and $\asymp _{\alpha }$ are well-defined. As for the valuation of propositional variables, when $n \sim m$ holds, the equivalence between $\alpha : @_{n}p \in \varGamma$ and $\alpha : @_{m}p \in \varGamma$ holds by the saturation conditions $(\mathbf {rep}_{1})$ and $(\mathbf {rep}_{2})$. For the valuation for agent nominals m, we need to check that $\{{(\alpha ,|n|)} \,|\, {\alpha : @_{n} m \in \varGamma } \}$ is $\mathcal {T} \times \{{|m|}\}$. But this is clear from the saturation condition $(\mathbf {rigid}_{=})$ and the fact that $\sim$ is an equivalence relation.

Now we move to check items (i) and (ii) by induction on $\varphi$. We only check the cases where $\varphi$ is of the form: $\mathsf {F}\varphi$ or $\Box \varphi$, since the other cases are easy to establish by the corresponding saturation conditions of Definition 1.

• Let $\varphi$ be of the form $\mathsf {F} \varphi$. For (i), assume that $\alpha :@_{n} \mathsf {F} \varphi \in \varGamma$. We need to show $\mathfrak {M}, (\alpha ,|n|)\, \models \, \mathsf {F} \varphi$, so let us fix any agent nominal m such that $|n| R_{\alpha } |m|$. Our goal is to show $\mathfrak {M}, (\alpha ,|m|) \, \models \, \varphi$. From $|n| R_{\alpha } |m|$, we get $\alpha : @_{n}\langle \mathsf {F} \rangle m \in \varGamma$ hence $\alpha : @_{n}\langle \mathsf {F} \rangle m \notin \varDelta$ by the unprovability of $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$. By the condition $(\mathsf {F}\mathbf {l})$, we obtain $\alpha :@_{m}\varphi \in \varGamma$, which implies our goal by induction hypothesis.

  For (ii), assume that $\alpha :@_{n} \mathsf {F} \varphi \in \varDelta$. By the condition $(\mathsf {R}\mathbf {r})$, $\alpha :@_{n}\langle \mathsf {F} \rangle m \in \varGamma$ and $\alpha : @_{n}m \in \varDelta$ for some agent nominal m. With the help of induction hypothesis, we have $|n| R_{\alpha } |m|$ and $\mathfrak {M},(\alpha ,|m|) \, \not \models \, \varphi$ for some agent nominal m. Hence $\mathfrak {M}, (\alpha ,|n|) \, \not \models \, \mathsf {F} \varphi$, as desired.

• Let $\varphi$ be of the form $\Box \varphi$. To show (i), assume that $\alpha :@_{n}\Box \varphi \in \varGamma$. We need to show $\mathfrak {M}, (\alpha ,|n|)\, \models \, \Box \varphi$, so let us fix any label $\beta$ such that $\alpha R_{|n|} \beta$. Our goal is to show $\mathfrak {M}, (\beta ,|n|) \, \models \, \varphi$. By $\alpha R_{|n|} \beta$, we can find an agent nominal $m \in |n|$ such that $\beta$ is an m-child of $\alpha$. It follows from $m \in |n|$ that $\gamma :@_{n}m \in \varGamma$ for some label $\gamma$. By $\alpha :@_{n}\Box \varphi \in \varGamma$ and $\gamma :@_{n}m \in \varGamma$, the saturation condition ($\mathbf {rep}_{1}$) implies that $\alpha :@_{m}\Box \varphi \in \varGamma$. By the saturation condition ($\Box \mathbf {l}$) and the fact that $\beta$ is an m-child of $\alpha$, we obtain $\beta :@_{m} \varphi \in \varGamma$. By induction hypothesis, $\mathfrak {M}, (\beta ,|m|) \, \models \, \varphi$ hence we obtain our goal by $|m| = |n|$. This finishes to show (i).

  For (ii), assume that $\alpha :@_{n}\Box \varphi \in \varDelta$. By the saturation condition $(\Box \mathbf {r})$, $\beta :@_{n}\varphi \in \varDelta$ for some n-child $\beta$ of $\alpha$, i.e., $\alpha R_{|n|}\beta$. By induction hypothesis, $\mathfrak {M},(\beta ,|n|) \, \not \models \, \varphi$. So we conclude that $\mathfrak {M},(\alpha ,|n|) \, \not \models \, \Box \varphi$.    $\square$

Theorem 2

(Completeness of cut-free $\mathsf {T}\mathbf {EFL}^{-}$ ). If $\mathfrak {M},f \, \models \, \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ for all models $\mathfrak {M}$ and all assignments f, then $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}^{-}$.

Proof

Suppose for contradiction that $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is unprovable in $\mathsf {T}\mathbf {EFL}^{-}$. By Lemma 1, we can extend this tree sequent into a saturated (possibly infinite) tree sequent $\varGamma ^{+} \mathop {\Rightarrow }\limits ^{\mathcal {T}^{+}} \varDelta ^{+}$ which is still unprovable in $\mathsf {T}\mathbf {EFL}^{-}$. Let $\mathfrak {M}$ be the derived model from $\varGamma ^{+} \mathop {\Rightarrow }\limits ^{\mathcal {T}^{+}} \varDelta ^{+}$. Let us define $f: \mathcal {T} \rightarrow \mathcal {T}$ as the identity mapping. Then it follows from Lemma 2 that $\mathfrak {M},f \, \not \models \, \varGamma \Rightarrow \varDelta$, as required.    $\square$

By Theorems 1 and 2, the cut elimination theorem of $\mathsf {T}\mathbf {EFL}$ follows.

Corollary 1

The following are all equivalent:

• 1. $\mathfrak {M},f \, \models \, \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ for all models $\mathfrak {M}$ and all assignments f.

• 2. $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}^{-}$.

• 3. $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}$.

Therefore, $\mathsf {T}\mathbf {EFL}$ enjoys the cut-elimination theorem.

5 Hilbert System of Epistemic Logic of Friendship

This section provides a Hilbert system of the epistemic logic of friendship by “translating” a tree sequent into a formula in $\mathcal {L}$. First of all, let us introduce the notion of necessity form, originally proposed in [13] by Goldblatt and used also in [6, 11]. Necessity forms are employed to formulate an inference rule of our Hilbert system.

Definition 2 (Necessity form)

Fix an arbitrary symbol $\#$ not occurring in the syntax $\mathcal {L}$. A necessity form is defined inductively as follows: $(\mathrm {i})$ $\#$ is a necessity form; $(\mathrm {ii})$ If L is a necessity form and $\varphi$ is a formula, then $\varphi \rightarrow L$ is also a necessity form; $(\mathrm {iii})$ If L is a necessity form and n is an agent nominal, then $@_{n}\Box L$ is also a necessity form. Given a necessity form $L(\#)$ and a formula $\varphi$ of $\mathcal {L}$, we use $L(\varphi )$ to denote the formula obtained by replacing the unique occurrence of $\#$ in L by the formula $\varphi$.

When $L(\#)$ is a necessity form of $\psi _{0} \rightarrow @_{n}\Box (\psi _{1} \rightarrow @_{m}\Box (\psi _{2} \rightarrow \#))$, then $L(\varphi )$ is $\psi _{0} \rightarrow @_{n}\Box (\psi _{1} \rightarrow @_{m}\Box (\psi _{2} \rightarrow \varphi ))$. Intuitively, this notion allows us to capture the unique path from a label in a tree of a tree sequent to the root label of the tree.

Table 2. Hilbert System $\mathsf {H}\mathbf {EFL}$

Table 2 presents our Hilbert system $\mathsf {H}\mathbf {EFL}$. The underlying idea of the system is: on the top of the propositional part ($\texttt {Taut}$ and $\texttt {MP}$), we combine the axiomatization of modal logic $\mathbf {K}$ for the modal operator $\Box$ and the axiomatization of a basic hybrid logic $\mathbf {K}_{\mathcal {H}(@)}$ (see [4, 5]) for the modal operator $\mathsf {F}$, with some modification (we need to modify $\mathbf {BG}$, the rule of bounded generalization, with the help of necessity forms), and then we add three interaction axioms: (Rigid $_{=}$), (Rigid $_{\ne }$), and (DCom $@\Box$). We note that the axiom (DCom $@\Box$) is also used for axiomatizing the dependent product of two hybrid logics in [20]. Let us define the notion of provability in $\mathsf {H}\mathbf {EFL}$ in as usual. We write $\vdash _{\mathsf {H}\mathbf {EFL}} \varphi$ to means that $\varphi$ is provable in $\mathsf {H}\mathbf {EFL}$.¹ $^{,}$ ²

Proposition 2

All the following are provable in $\mathsf {H}\mathbf {EFL}$.

• 1. $@_{m}@_{n}\varphi \leftrightarrow @_{n}\varphi$.

• 2. $n \rightarrow (@_{n} \varphi \leftrightarrow \varphi )$.

• 3. $@_{n}m \rightarrow (@_{n} \varphi \leftrightarrow @_{m}\varphi )$.

• 4. $@_{n}m \leftrightarrow @_{m}n$.

• 5. $@_{n}(\varphi \rightarrow \psi ) \leftrightarrow (@_{n}\varphi \rightarrow @_{n}\psi )$.

• 6. $@_{n}m \rightarrow (\varphi [n/k] \leftrightarrow \varphi [m/k])$.

Proof

For the provability of item 1, it suffices to show the right-to-left direction, which is shown by (Agree) and (Selfdual). For the provability of item 2, it suffices to show $n \rightarrow (\varphi \rightarrow @_{n} \varphi )$, whose provability is shown by the contraposition of $(\texttt {Elim})$ and $(\texttt {Selfdual})$. Then items 3 to 5 are proved similarly as given in [5, p. 293, Lemma 2]. Finally, item 6 is proved by induction on $\varphi$. Here we show the case where $\varphi \equiv \Box \psi$ alone, while we note that we need to use item 5 for the case where $\varphi \equiv @_{l}\psi$. By induction hypothesis, we obtain $\vdash _{\mathsf {H}\mathbf {EFL}} @_{n}m \rightarrow (\psi [n/k] \leftrightarrow \psi [m/k])$. By $(\texttt {K}_{\Box })$ and $(\texttt {Nec}_{\Box })$, we get $\vdash _{\mathsf {H}\mathbf {EFL}} \Box @_{n}m \rightarrow (\Box (\psi [n/k]) \leftrightarrow \Box (\psi [m/k]))$. It follows from the axiom $(\texttt {rigid}_{=})$ that $\vdash _{\mathsf {H}\mathbf {EFL}} @_{n}m \rightarrow ((\Box \psi )[n/k] \leftrightarrow (\Box \psi )[m/k]))$, as desired.    $\square$

The following translation is a key to specify our Hilbert system $\mathsf {H}\mathbf {EFL}$.

Definition 3 (Formulaic translation)

Given a set $\varTheta$ of labelled formulas and a label $\alpha$, we define $\varTheta _{\alpha } := \{{\varphi } \,|\, {\alpha :\varphi \in \varTheta } \}$. Let $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ be a tree sequent. Then the formulaic translation of the sequent at $\alpha$ is defined as:

$$ \left[ \!\!\left[ \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{\alpha } := \bigwedge \varGamma _{\alpha } \rightarrow \bigvee \left( \varDelta _{\alpha }, @_{n_{1}}\Box \left[ \!\!\left[ \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{\beta _{1}}, \ldots , @_{n_{k}}\Box \left[ \!\!\left[ \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{\beta _{k}} \right) , $$

where $\beta _{i}$ is an $n_{i}$-child of $\alpha$, $\beta _{i}$s enumerate all children of $\alpha$, $\bigwedge \emptyset := \top$, and $\bigvee \emptyset := \bot$.

The formulaic translation of a tree sequent of Fig. 1 of Sect. 3 at the root 0 is

$$\begin{aligned} @_{n}\varphi \rightarrow (@_{m}\psi \vee @_{n}\Box (\top \rightarrow @_{k}\theta ) \vee @_{k}\Box (@_{m} \rho \rightarrow \bot )). \end{aligned}$$

Theorem 3

If a tree sequent $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}$ then the formulaic translation $[\![ \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta ]\!]_{i}$ is provable in $\mathsf {H}\mathbf {EFL}$, where a natural number i is the root of $\mathcal {T}$.

Proof

By induction on height n of a derivation of $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ in $\mathsf {T}\mathbf {EFL}$, where i is the root of the tree $\mathcal {T}$. We skip the base case where $n = 0$. Let $n>0$. It is remarked that, when the sequent is obtained by $(\mathsf {rep}_{l})$, $(\mathsf {ref}_{=})$, (@L), or (@R), respectively, the translation of the sequent at the root is provable by Proposition 2 (6), the axiom (Ref), (Agree), or Proposition 2 (1), respectively. Here we focus on the cases where $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is obtained by $(\Box L)$, $(\mathsf {F}R)$ or $(\mathsf {rigid}_{=})$, since these are the cases where we need to be careful and the other cases are easy to establish.

($\Box L$):

Suppose that $\alpha :@_{n}\Box \varphi , \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is obtained by ($\Box L$) from $\beta :@_{n}\varphi , \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$, where $\beta \in \mathcal {T}$ is an n-child of $\alpha$. By induction hypothesis, we obtain $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \beta :@_{n}\varphi , \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{i}$. We show that $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \alpha :@_{n}\Box \varphi , \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{i}$. Let $(\alpha _{0}, \alpha _{1}, \ldots , \alpha _{l})$ be the unique path from $\alpha$ ($\equiv$ $\alpha _{l}$) to the root i ($\equiv$ $\alpha _{0}$) of tree $\mathcal {T}$. By induction on $0 \leqslant h \leqslant l$, we show that $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \beta :@_{n}\varphi , \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{\alpha _{l-h}} \rightarrow \left[ \!\!\left[ \alpha :@_{n}\Box \varphi , \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{\alpha _{l-h}}$.

Let $h = 0$ and so $\alpha _{l-h} = \alpha$. It suffices to show that a formula of the form

$$ \left( \gamma _{1} \rightarrow (\delta \vee @_{n}\Box ( (\gamma _{2} \wedge @_{n}\varphi ) \rightarrow \psi _{2}) \right) \rightarrow \left( (@_{n}\Box \varphi \wedge \gamma _{1} ) \rightarrow (\delta \vee @_{n}\Box ( \gamma _{2} \rightarrow \psi _{2})) \right) . $$

is provable in ${\mathsf {H}\mathbf {EFL}}$. This reduces to the provability of

$$ @_{n}\Box \varphi \wedge @_{n}\Box ( (\gamma _{2} \wedge @_{n}\varphi ) \rightarrow \psi _{2})) \rightarrow @_{n}\Box ( \gamma _{2} \rightarrow \psi _{2})) $$

in ${\mathsf {H}\mathbf {EFL}}$. This holds by the axiom $(\texttt {Dcom}\Box @)$ $@_{n}\Box @_{n} \varphi \leftrightarrow @_{n}\Box \varphi$. Let $h>0$. But this case is shown with the help of $(\mathsf {Nec}_{\Box })$ and $(\mathsf {Nec}_{@})$. This completes our induction on h. So we conclude $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \alpha :@_{n}\Box \varphi , \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{i}$.

($\mathsf {F}R$):

Suppose that $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta ', \alpha :@_{n}\mathsf {F}\varphi$ is obtained by ($\mathsf {F}R$) from $\alpha : @_{n}\langle \mathsf {F}\rangle m, \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta ', \alpha :@_{m} \varphi$ where m is fresh in the conclusion. By induction hypothesis, we have $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \alpha : @_{n}\langle \mathsf {F}\rangle m, \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta ', \alpha :@_{m} \varphi \right] \!\!\right] _{i}$, which is equivalent to $\vdash _{\mathsf {H}\mathbf {EFL}} L(@_{n}\langle \mathsf {F}\rangle m \rightarrow @_{m} \varphi )$ for some necessitation form L. Fix such necessitation form L. By the inference rule $L(\texttt {BG})$ of $\mathsf {H}\mathbf {EFL}$, we can obtain $\vdash _{\mathsf {H}\mathbf {EFL}} L(@_{n} \mathsf {F} \varphi )$, which is equivalent to $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta ', \alpha :@_{n}\mathsf {F}\varphi \right] \!\!\right] _{i}$.

$(\mathsf {rigid}_{=})$ :

Instead of dealing with a general case, we handle a simple example of $\mathcal {T}$ to extract an essence of this case, where we need to use the axioms $(\texttt {Rigid}_{=})$ and $(\texttt {Rigid}_{\ne })$. Let $\mathcal {T}$ consists of three labels, i.e., the root i, a k-child $\alpha$ of i and a $k'$-child $\beta$ of i. Let us suppose that $\beta : @_{n}m, \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is obtained by $(\mathsf {rigid}_{=})$ from $\alpha : @_{n}m, \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$. In what follows, for every $\eta \in \mathcal {T}$, let us write $\bigwedge \varGamma '_{\eta }$ and $\bigvee \varDelta _{\eta }$ by $\gamma _{\eta }$ and $\delta _{\eta }$, respectively. Here we note that the following hold:

($\alpha$ to i) $\vdash _{\mathsf {H}\mathbf {EFL}} (@_{k}\Box ((@_{n}{m} \wedge \gamma _{\alpha }) \rightarrow \delta _{\alpha }) \wedge @_{n}m) \rightarrow @_{k} \Box (\gamma _{\alpha } \rightarrow \delta _{\alpha }))$.

(i to $\beta$) $\vdash _{\mathsf {H}\mathbf {EFL}} \lnot @_{n}m \rightarrow @_{k'}\Box ((@_{n}m \wedge \gamma _{\beta }) \rightarrow \delta _{\beta })$

For ($\alpha$ to i), it suffices to show $\vdash _{\mathsf {H}\mathbf {EFL}} @_{n}m \rightarrow @_{k}\Box @_{n}m$, which holds by $(\texttt {Rigid}_{=})$, the distribution of @ over the implication and Proposition 2 (1). For (i to $\beta$), it suffices to show $\vdash _{\mathsf {H}\mathbf {EFL}} \lnot @_{n}m \rightarrow @_{k'}\Box \lnot @_{n}m$, which holds by $(\texttt {Rigid}_{\ne })$, $(\texttt {Selfdual})$ and Proposition 2 (1).

By induction hypothesis, we obtain $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \alpha : @_{n}m, \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{i}$, i.e.,

$$ \vdash _{\mathsf {H}\mathbf {EFL}} \gamma _{i} \rightarrow \left( \delta _{i} \vee @_{k}\Box ((@_{n}m \wedge \gamma _{\alpha }) \rightarrow \delta _{\alpha }) \vee @_{k'}\Box (\gamma _{\beta } \rightarrow \delta _{\beta }) \right) . $$

It follows from item ($\alpha$ to i) that

$$ \vdash _{\mathsf {H}\mathbf {EFL}} (@_{n}m \wedge \gamma _{i}) \rightarrow \left( \delta _{i} \vee @_{k}\Box (\gamma _{\alpha } \rightarrow \delta _{\alpha }) \vee @_{k'}\Box (\gamma _{\beta } \rightarrow \delta _{\beta }) \right) . $$

By this and item (i to $\beta$), we can establish:

$$ \vdash _{\mathsf {H}\mathbf {EFL}} \gamma _{i} \rightarrow \left( \delta _{i} \vee @_{k}\Box (\gamma _{\alpha } \rightarrow \delta _{\alpha }) \vee @_{k'}\Box ((@_{n}m \wedge \gamma _{\beta }) \rightarrow \delta _{\beta }) \right) , $$

which is equivalent to: $\vdash _{\mathsf {H}\mathbf {EFL}} \left[ \!\!\left[ \beta : @_{n}m, \varGamma ' \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta \right] \!\!\right] _{i}$, as desired.    $\square$

In what follows in this section, we prove the soundness of $\mathsf {H}\mathbf {EFL}$ for the tree sequent calculus $\mathsf {T}\mathbf {EFL}$ with cut rule. The cut rule is necessary to prove the following.

Lemma 3

The rules $(\rightarrow R)$, $(\Box R)$, (@R), and (@L) are invertible, i.e., if the lower sequent is provable in $\mathsf {T}\mathbf {EFL}$ then the upper sequent is also provable in $\mathsf {T}\mathbf {EFL}$.

Proof

We only prove the invertibility of $(\rightarrow R)$ and $(\Box R)$. First we deal with $(\rightarrow R)$. Suppose that $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta , \alpha :@_{n}(\varphi \rightarrow \psi )$ is provable in $\mathsf {T}\mathbf {EFL}$. This is shown as follows:

where the rightmost tree sequent is provable in $\mathsf {T}\mathbf {EFL}$ by $(\rightarrow L)$. Second we move to $(\Box R)$. Suppose that $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta , \alpha : @_{n}\Box \varphi$ is provable in $\mathsf {T}\mathbf {EFL}$. Then the provability of the upper sequent of $(\Box R)$ is established as follows:

   $\square$

Theorem 4

If $\varphi$ is provable in $\mathsf {H}\mathbf {EFL}$, then $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{n}\varphi$ is provable in $\mathsf {T}\mathbf {EFL}$ for all trees $\mathcal {T}$, $\alpha \in \mathcal {T}$ and nominals n fresh in $\varphi$.

Proof

Suppose that there is a proof $(\varphi _{0}, \ldots , \varphi _{h})$ of $\varphi$ in $\mathsf {H}\mathbf {EFL}$. By induction on $0 \leqslant j \leqslant h$, we show that $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{n}\varphi _{j}$ is provable in $\mathsf {T}\mathbf {EFL}$ for all nominals n fresh in $\varphi _{j}$ and $\alpha \in \mathcal {T}$. Since the space is limited, we demonstrate some cases. Let us start with (Rigid $_{=}$), which is shown by the left derivation below. Now we move to (DCom $@\Box$). We show the right-to-left direction alone, since the converse direction is shown similarly. Let us see the right derivation below, from which we can obtain the provability of $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha :@_{m}(@_{n} \Box @_{n} p \rightarrow @_{n} \Box p)$ in $\mathsf {T}\mathbf {EFL}$. Now we deal with some inference rules below.

(L(BG)):

Let $\varphi _{j}$ $\equiv$ $\Box \psi$ be obtained by $(L(\texttt {BG}))$. Fix any tree $\mathcal {T}$, $\alpha \in \mathcal {T}$ and fresh nominal k. By induction hypothesis, $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{k} L(@_{n} \langle \mathsf {F} \rangle m \rightarrow @_{m}\varphi )$ is provable in $\mathsf {T}\mathbf {EFL}$, where m satisfies the freshness condition. By applying Lemma 3 (i.e., the invertibility of the right rules) repeatedly to the consequent of a resulting tree sequent, we obtain the provability of a tree sequent of the form $\varGamma , \beta : @_{n} \langle \mathsf {F} \rangle m \mathop {\Rightarrow }\limits ^{\mathcal {T}'} \varDelta , \beta : @_{m}\varphi$. Then we apply the right rules in a converse direction of our repeated application of Lemma 3 to conclude that $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{k} L(@_{n} \mathsf {F} \varphi )$ is provable in $\mathsf {T}\mathbf {EFL}$. To illustrate this argument, let L $\equiv$ $@_{n}\Box (\psi \rightarrow \#)$. By induction hypothesis, $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{k} @_{n}\Box (\psi \rightarrow (@_{n} \langle \mathsf {F} \rangle m \rightarrow @_{m}\varphi ))$ is provable in $\mathsf {T}\mathbf {EFL}$, where m satisfies the freshness condition. By applying Lemma 3 repeatedly, we obtain the provability of $\alpha \cdot _{n} i: @_{n}\psi , \alpha \cdot _{n} i: @_{n} \langle \mathsf {F} \rangle m \mathop {\Rightarrow }\limits ^{\mathcal {T} \cup \{{\alpha \cdot _{n}i}\}} \alpha \cdot _{n} i: @_{m}\varphi$ in $\mathsf {T}\mathbf {EFL}$ for some fresh i. Then we proceed as follows:

as required.

(Nec $_{\Box }$):

Let $\varphi _{j}$ $\equiv$ $\Box \psi$ be obtained by $(\texttt {Nec}_{\Box })$. Fix any tree $\mathcal {T}$, $\alpha \in \mathcal {T}$ and fresh nominal n. By induction hypothesis, $\mathop {\Rightarrow }\limits ^{\mathcal {T}\cup \{{\alpha \cdot _{n} i}\}} \alpha \cdot _{n} i : @_{n} \psi$ is provable in $\mathsf {T}\mathbf {EFL}$, where i is fresh in $\mathcal {T}$. By the rule $(\Box R)$ of $\mathsf {T}\mathbf {EFL}$, the provability of $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{n} \Box \psi$ follows, as desired.

(Nec $_{\mathsf {F}}$):

Let $\varphi _{j}$ $\equiv$ $\mathsf {F} \psi$ be obtained by $(\texttt {Nec}_{\mathsf {F}})$. Fix any tree $\mathcal {T}$, $\alpha \in \mathcal {T}$ and fresh nominal n. Let m be a fresh nominal in $\psi$. By induction hypothesis, $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{m} \psi$ is provable in $\mathsf {T}\mathbf {EFL}$. By the admissibility of weakening rule from Proposition 1, we obtain the provability of $\alpha :@_{n}\langle \mathsf {F}\rangle m \mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{m} \psi$. Since m is fresh in $\psi$, the rule $(\mathsf {F}R)$ enables us to derive the provability of $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{n}\mathsf {F} \psi$ in $\mathsf {T}\mathbf {EFL}$, as desired.    $\square$

Corollary 2

(Soudness and Completenss of $\mathsf {H}\mathbf {EFL}$ ). The following are all equivalent: for every formula $\varphi$,

• 1. $\varphi$ is valid in the class of all models,³

• 2. $\mathop {\Rightarrow }\limits ^{\mathcal {T}}\alpha : @_{n}\varphi$ is provable in $\mathsf {T}\mathbf {EFL}^{-}$ for all $\mathcal {T}$, $\alpha \in \mathcal {T}$ and nominals n fresh in $\varphi$,

• 3. $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{n}\varphi$ is provable in $\mathsf {T}\mathbf {EFL}$ for all $\mathcal {T}$, $\alpha \in \mathcal {T}$ and nominals n fresh in $\varphi$,

• 4. $\varphi$ is provable in $\mathsf {H}\mathbf {EFL}$.

Proof

Item 1 is equivalent to the following: $\mathop {\Rightarrow }\limits ^{\mathcal {T}} \alpha : @_{n}\varphi$ is true for all pairs $(\mathfrak {M}, f)$ of models and assignments, trees $\mathcal {T}$, $\alpha \in \mathcal {T}$ and nominals n fresh in $\varphi$. Then the equivalence between items 1, 2 and 3 holds by Corollary 1. The direction from item 4 to item 3 holds by Theorem 4. Finally, the direction from item 3 to item 4 is established as follows. Suppose item 3. Let n be a fresh nominal. By the supposition, $\mathop {\Rightarrow }\limits ^{\{{0}\}} 0: @_{n}\varphi$ is provable in $\mathsf {T}\mathbf {EFL}$. It follows from Theorem 3 that $\vdash _{\mathsf {H}\mathbf {EFL}} [\![ \mathop {\Rightarrow }\limits ^{\{{0}\}} 0: @_{n}\varphi ]\!]_{0}$, which implies $\vdash _{\mathsf {H}\mathbf {EFL}} @_{n}\varphi$. By the axiom (Elim), we obtain $\vdash _{\mathsf {H}\mathbf {EFL}} n \rightarrow \varphi$ hence $\vdash _{\mathsf {H}\mathbf {EFL}} \varphi$ by $(\texttt {Name})$, as required.    $\square$

6 Extensions of Epistemic Logic of Friendship

This section outlines how we extend our tree sequent calculus $\mathsf {T}\mathbf {EFL}$ and Hilbert system $\mathsf {H}\mathbf {EFL}$. In particular, we discuss extensions where $\Box$ follows $\mathbf {S4}$ or $\mathbf {S5}$ axioms and/or the friendship relation $\asymp _{w}$ satisfies some universal properties such as irreflexivity, symmetry, etc. ($w \in W$). We note that [23, 24] assume that the friendship relation $\asymp _{w}$ satisfies irreflexivity and symmetry and that $\Box$ obeys $\mathbf {S5}$ axioms.

Let us denote a set $\{{\Box p \rightarrow p, \Box p \rightarrow \Box \Box p}\}$ by $\mathbf {S4}$ and a set $\mathbf {S4} \cup \{{ p \rightarrow \Box \lnot \Box \lnot p }\}$ by $\mathbf {S5}$. Let us consider formulas of the form $@_{n}m$ or $@_{n}\langle \mathsf {F} \rangle m$, which are denoted by $\rho _{i}$, $\rho _{i}'$, etc. below. Let us consider a formula $\varphi$ of the following form:

$$\begin{aligned} \left( \rho _{1} \wedge \cdots \wedge \rho _{h} \right) \rightarrow \left( \rho _{1}' \vee \cdots \vee \rho _{l}' \right) , \end{aligned}$$

where we note that h and l are possibly zero. We say that a formula of such form is a regular implication [17, Sect. 6] (we may even consider a more general class of formulas called geometric formulas (cf. [8]), but we restrict our attention to regular implications in this paper for simplicity). The corresponding frame property of a regular implication is obtained by regarding $@_{n}m$ or $@_{n}\langle \mathsf {F} \rangle m$ by “$a_n = a_m$” and “$a_n \asymp _{w} a_m$” and putting the universal quantifiers for all agents and w. For example, irreflexivity and symmetry of $\asymp _{w}$ are defined by $@_{n}\langle \mathsf {F}\rangle n \rightarrow \bot$ and $@_{n}\langle \mathsf {F}\rangle m \rightarrow @_{m}\langle \mathsf {F}\rangle n$, respectively. When $\varLambda$ is one of $\mathbf {S4}$ and $\mathbf {S5}$ and $\varTheta$ is a finite set of regular implications, a Hilbert system $\mathsf {H}\mathbf {EFL}(\varLambda \cup \varTheta )$ is defined as the axiomatic extension of $\mathsf {H}\mathbf {EFL}$ by new axioms $\varLambda \cup \varTheta$.

Now let us move to tree sequent systems. First, we introduce an inference rule for a regular implication. For a regular implication $\varphi$ displayed above, we can define the corresponding inference rule $(\mathsf {ri}(\varphi ))$ for tree sequent calculus as follows (cf. [8, 17, Sect. 6]):

When $\asymp _{w}$ is irreflexive or symmetric for all $w \in W$, we can obtain the following rule $(\mathsf {irr}_{\asymp })$ or $(\mathsf {sym}_{\asymp })$, respectively:

Let $\varLambda$ be one of $\mathbf {S4}$ and $\mathbf {S5}$ and $\varTheta$ be a possibly empty finite set of regular implications. In what follows, we define the tree sequent system $\mathsf {T}\mathbf {EFL}(\varLambda ;\varTheta )$. Recall that the side condition $\ddagger$ of the rule $(\Box L)$ of Table 1. First, depending on the choice of $\varLambda$, we change the side condition $\ddagger$ of $\mathsf {T}\mathbf {EFL}$ into the following one:

• $\ddagger _{\mathbf {S4}}$: $\alpha$ $\preceq _{n}$ $\beta$, where $\preceq _{n}$ is the reflexive transitive closure of the n-children relation.

• $\ddagger _{\mathbf {S5}}$: $\alpha$ $\sim _{n}$ $\beta$, where $\sim _{n}$ is the reflexive, symmetric, transitive closure of the n-children relation.

Second, we extend the resulting system with a set $\{{(\mathsf {ri}(\varphi ))} \,|\, {\varphi \in \varTheta } \}$ of inference rules to finish to define the system $\mathsf {T}\mathbf {EFL}(\varLambda ;\varTheta )$. We define $\mathsf {T}\mathbf {EFL}(\varLambda ;\varTheta )^{-}$ as the system $\mathsf {T}\mathbf {EFL}(\varLambda ;\varTheta )$ without the cut rule.

Given a set $\varPsi$ of formulas and a frame $\mathfrak {F} = (W, A, (R_{a})_{a \in A}, (\asymp _{w})_{w \in W})$ (a model without a valuation), we say that $\varPsi$ is valid in $\mathfrak {F}$ (notation: $\mathfrak {F} \, \models \, \varPsi$) if $(\mathfrak {F},V), (w,a) \, \models \, \psi$ for all $\psi \in \varPsi$, valuations V and pairs $(w,a) \in W\times A$. We define a class $\mathbb {M}_{\varPsi }$ of models as $\{{(\mathfrak {F},V)} \,|\, {\mathfrak {F} \, \models \, \varPsi } \}$. While we omit the detail of the proof, we can obtain the following two theorems by similar arguments to $\mathsf {T}\mathbf {EFL}$ and $\mathsf {H}\mathbf {EFL}$.

Theorem 5

Let $\varLambda$ be one of $\mathbf {S4}$ and $\mathbf {S5}$ and $\varTheta$ be a possibly empty finite set of regular implications. The following are all equivalent:

• 1. $\mathfrak {M},f \, \models \, \varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ for all models $\mathfrak {M} \in \mathbb {M}_{\varLambda \cup \varTheta }$ and all assignments f.

• 2. $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}(\varLambda ;\varTheta )^{-}$.

• 3. $\varGamma \mathop {\Rightarrow }\limits ^{\mathcal {T}} \varDelta$ is provable in $\mathsf {T}\mathbf {EFL}(\varLambda ;\varTheta )$.

Therefore, $\mathsf {T}\mathbf {EFL}(\varLambda ;\varTheta )$ enjoys the cut-elimination theorem. Moreover, for every formula $\varphi$, $\varphi$ is valid in $\mathbb {M}_{\varLambda \cup \varTheta }$ iff $\varphi$ is provable in $\mathsf {H}\mathbf {EFL}(\varLambda \cup \varTheta )$.

7 Further Directions

This paper positively answered the question if the set of all valid formulas of $\mathbf {EFL}$ in the class of all models is axiomatizable. We list some directions for further research.

• 1. Is $\mathsf {H}\mathbf {EFL}$ or $\mathsf {T}\mathbf {EFL}$ decidable?

• 2. Is it possible to provide a syntactic proof of the cut elimination theorem of $\mathsf {T}\mathbf {EFL}$?

• 3. Can we reformulate our sequent calculus into a G3-style calculus, i.e., a contraction-free calculus, all of whose rules are height-preserving invertible?

• 4. Provide a G3-style labelled sequent calculus for $\mathbf {EFL}$ based on the idea of doubly labelled formula $(x,y):\varphi$. This is an extension of G3-style labelled sequent calculus for modal logic in [16, 18].

• 5. Prove the semantic completeness of $\mathsf {H}\mathbf {EFL}$ and its extensions by specifying the notion of canonical model.

• 6. Can we apply our technique of this paper to obtain a Hilbert-system of Term Modal Logics which is proposed in [10]?