Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus

Katsuhiko Sano

arXiv:1704.07149·cs.LO·July 11, 2019

Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus

Katsuhiko Sano

PDF

Open Access

TL;DR

This paper develops a sound and complete Hilbert system for the Epistemic Logic of Friendship by constructing a tree sequent calculus and translating it into a Hilbert system, advancing formal logical foundations.

Contribution

It introduces the first sound, complete, and cut-free tree sequent calculus for EFL and derives a Hilbert system from it, solving an open problem.

Findings

01

The sequent calculus is sound and complete for EFL.

02

The Hilbert system derived is sound and complete.

03

The calculus is cut-free and integrates hybrid and modal logic.

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 the intended two-dimensional semantics.

Tables1

Table 1. Table 2: Hilbert System 𝖧 𝐄𝐅𝐋 𝖧 𝐄𝐅𝐋 \mathsf{H}\mathbf{EFL}

(Taut)	all propositional tautologies	(MP)	From $φ$ and $φ \to ψ$ , infer $ψ$
(K_□)	$□ (φ \to ψ) \to (□ φ \to □ ψ)$	(Nec_□)	From $φ$ , infer $□ φ$
(K_F)	$𝖥 (φ \to ψ) \to (𝖥 φ \to 𝖥 ψ)$	(Nec_F)	From $φ$ , infer $𝖥 φ$
(K_@)	$@_{n} (φ \to ψ) \to (@_{n} φ \to @_{n} ψ)$	(Nec_@)	From $φ$ , infer $@_{n} φ$
(Ref)	$@_{n} n$	(Selfdual)	$\neg @_{n} φ \leftrightarrow @_{n} \neg φ$
(Elim)	$@_{n} φ \to (n \to φ)$	(Agree)	$@_{n} @_{m} φ \to @_{m} φ$
(Back)	$@_{n} φ \to 𝖥 @_{n} φ$	(DCom $@ □$ )	$@_{n} □ @_{n} φ \leftrightarrow @_{n} □ φ$
(Rigid₌)	$@_{n} m \to □ @_{n} m$	(Rigid_≠)	$\neg @_{n} m \to □ \neg @_{n} m$
(Name)	From $n \to φ$ , infer $φ$ , where $n$ is fresh in $φ$ .
( $L$ (BG))	From $L (@_{n} ⟨ 𝖥 ⟩ m \to @_{m} φ)$ , infer $L (@_{n} 𝖥 φ)$ , where $m$ is fresh in $L (@_{n} 𝖥 φ)$ .

Equations79

Form ∋ φ ::= n ∣ p ∣ ⊥ ∣ φ \to φ ∣ @_{n} φ ∣ F φ ∣ □ φ,

Form ∋ φ ::= n ∣ p ∣ ⊥ ∣ φ \to φ ∣ @_{n} φ ∣ F φ ∣ □ φ,

(W, A, (R_{a})_{a \in A}, (≍_{w})_{w \in W}, V),

(W, A, (R_{a})_{a \in A}, (≍_{w})_{w \in W}, V),

\begin{array}[]{lll}\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\to\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}

\begin{array}[]{lll}\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\to\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}

\begin{array}[]{lll}\mathfrak{M},f\models\alpha:@_{n}\varphi&\,\mathrm{iff}&\mathfrak{M},({f}(\alpha),\underline{n})\models\varphi.\\ \end{array}

\begin{array}[]{lll}\mathfrak{M},f\models\alpha:@_{n}\varphi&\,\mathrm{iff}&\mathfrak{M},({f}(\alpha),\underline{n})\models\varphi.\\ \end{array}

Γ σ \Rightarrow T σ Δ σ Γ \Rightarrow T Δ,

Γ σ \Rightarrow T σ Δ σ Γ \Rightarrow T Δ,

Γ \Rightarrow T Δ, α : @_{n} φ Γ \Rightarrow T Δ, α : @_{n} φ, Γ \Rightarrow T ΔΓ \Rightarrow T Δ.

Γ \Rightarrow T Δ, α : @_{n} φ Γ \Rightarrow T Δ, α : @_{n} φ, Γ \Rightarrow T ΔΓ \Rightarrow T Δ.

Γ_{j}^{ref} := {α : @_{n} n ∣ α \in T_{j} and n occurs in Γ_{j}^{rep} \Rightarrow T_{j} Δ_{j}} .

Γ_{j}^{ref} := {α : @_{n} n ∣ α \in T_{j} and n occurs in Γ_{j}^{rep} \Rightarrow T_{j} Δ_{j}} .

⊢_{H EFL} @_{n} @_{n} m \to@_{n} ((ψ [n / k]) \leftrightarrow (ψ [m / k])) .

⊢_{H EFL} @_{n} @_{n} m \to@_{n} ((ψ [n / k]) \leftrightarrow (ψ [m / k])) .

⊢_{H EFL} @_{n} m \to (@_{n} (ψ [n / k]) \leftrightarrow@_{n} (ψ [m / k])) .

⊢_{H EFL} @_{n} m \to (@_{n} (ψ [n / k]) \leftrightarrow@_{n} (ψ [m / k])) .

⊢_{H EFL} @_{n} m \to (@_{n} (ψ [m / k]) \leftrightarrow@_{m} (ψ [m / k])) .

⊢_{H EFL} @_{n} m \to (@_{n} (ψ [m / k]) \leftrightarrow@_{m} (ψ [m / k])) .

[[Γ \Rightarrow T Δ]]_{α} := ⋀ Γ_{α} \to ⋁ (Δ_{α}, @_{n_{1}} □ [[Γ \Rightarrow T Δ]]_{β_{1}}, \dots, @_{n_{k}} □ [[Γ \Rightarrow T Δ]]_{β_{k}}),

[[Γ \Rightarrow T Δ]]_{α} := ⋀ Γ_{α} \to ⋁ (Δ_{α}, @_{n_{1}} □ [[Γ \Rightarrow T Δ]]_{β_{1}}, \dots, @_{n_{k}} □ [[Γ \Rightarrow T Δ]]_{β_{k}}),

⊢_{H EFL} [[β : @_{n} φ, Γ^{'} \Rightarrow T Δ]]_{α_{l - h}} \to [[α : @_{n} □ φ, Γ^{'} \Rightarrow T Δ]]_{α_{l - h}} .

⊢_{H EFL} [[β : @_{n} φ, Γ^{'} \Rightarrow T Δ]]_{α_{l - h}} \to [[α : @_{n} □ φ, Γ^{'} \Rightarrow T Δ]]_{α_{l - h}} .

(γ_{1} \to (δ \lor@_{n} □ ((γ_{2} \land@_{n} φ) \to ψ_{2})) \to ((@_{n} □ φ \land γ_{1}) \to (δ \lor@_{n} □ (γ_{2} \to ψ_{2}))) .

(γ_{1} \to (δ \lor@_{n} □ ((γ_{2} \land@_{n} φ) \to ψ_{2})) \to ((@_{n} □ φ \land γ_{1}) \to (δ \lor@_{n} □ (γ_{2} \to ψ_{2}))) .

@_{n} □ φ \land@_{n} □ ((γ_{2} \land@_{n} φ) \to ψ_{2})) \to@_{n} □ (γ_{2} \to ψ_{2}))

@_{n} □ φ \land@_{n} □ ((γ_{2} \land@_{n} φ) \to ψ_{2})) \to@_{n} □ (γ_{2} \to ψ_{2}))

(γ_{α} \to (δ_{α} \lor@_{k} □ ((@_{n} m \land γ_{β}) \to δ_{β}))) \to ((γ_{α} \land@_{n} m) \to (δ_{α} \lor@_{k} □ (γ_{β} \to δ_{β})))

(γ_{α} \to (δ_{α} \lor@_{k} □ ((@_{n} m \land γ_{β}) \to δ_{β}))) \to ((γ_{α} \land@_{n} m) \to (δ_{α} \lor@_{k} □ (γ_{β} \to δ_{β})))

((γ_{β} \land@_{n} m) \to (δ_{β} \lor@_{k} □ (γ_{α} \to δ_{α}))) \to (γ_{β} \to (δ_{β} \lor@_{k} □ ((@_{n} m \land γ_{α}) \to δ_{α})))

((γ_{β} \land@_{n} m) \to (δ_{β} \lor@_{k} □ (γ_{α} \to δ_{α}))) \to (γ_{β} \to (δ_{β} \lor@_{k} □ ((@_{n} m \land γ_{α}) \to δ_{α})))

α : @_{n} φ, Γ \Rightarrow T Δ, α : @_{n} ψ \lx@proof@logical@and Γ \Rightarrow T Δ, α : @_{n} (φ \to ψ) α : @_{n} (φ \to ψ), α : @_{n} φ \Rightarrow T α : @_{n} ψ,

α : @_{n} φ, Γ \Rightarrow T Δ, α : @_{n} ψ \lx@proof@logical@and Γ \Rightarrow T Δ, α : @_{n} (φ \to ψ) α : @_{n} (φ \to ψ), α : @_{n} φ \Rightarrow T α : @_{n} ψ,

Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α \cdot_{n} i : @_{n} φ \lx@proof@logical@and Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α : @_{n} □ φ Γ \Rightarrow T Δ, α : @_{n} □ φ α : @_{n} □ φ, Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α \cdot_{n} i : @_{n} φ α \cdot_{n} i : @_{n} φ, Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α \cdot_{n} i : @_{n} φ .

Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α \cdot_{n} i : @_{n} φ \lx@proof@logical@and Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α : @_{n} □ φ Γ \Rightarrow T Δ, α : @_{n} □ φ α : @_{n} □ φ, Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α \cdot_{n} i : @_{n} φ α \cdot_{n} i : @_{n} φ, Γ \Rightarrow T \cup {α \cdot_{n} i} Δ, α \cdot_{n} i : @_{n} φ .

\Rightarrow T α : @_{k} (@_{n} m \to \Box@_{n} m) α : @_{k} @_{n} m \Rightarrow T α : @_{k} \Box@_{n} m α : @_{n} m \Rightarrow T α : @_{k} \Box@_{n} m α : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{k} @_{n} m α : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{n} m α \cdot_{k} i : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{n} m

\Rightarrow T α : @_{k} (@_{n} m \to \Box@_{n} m) α : @_{k} @_{n} m \Rightarrow T α : @_{k} \Box@_{n} m α : @_{n} m \Rightarrow T α : @_{k} \Box@_{n} m α : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{k} @_{n} m α : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{n} m α \cdot_{k} i : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{n} m

\Rightarrow T α : @_{k} (\neg@_{n} m \to □ \neg@_{n} m) α : @_{k} \neg@_{n} m \Rightarrow T α : @_{k} □ \neg@_{n} m α : @_{k} \neg@_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{k} \neg@_{n} m α \cdot_{k} i : @_{k} @_{n} m, α : @_{k} \neg@_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{k} @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{k} @_{n} m α \cdot_{k} i : @_{k} @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{n} m α \cdot_{k} i : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{n} m α : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{n} m .

\Rightarrow T α : @_{k} (\neg@_{n} m \to □ \neg@_{n} m) α : @_{k} \neg@_{n} m \Rightarrow T α : @_{k} □ \neg@_{n} m α : @_{k} \neg@_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{k} \neg@_{n} m α \cdot_{k} i : @_{k} @_{n} m, α : @_{k} \neg@_{n} m \Rightarrow T \cup {α \cdot_{k} i} α \cdot_{k} i : @_{k} @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{k} @_{n} m α \cdot_{k} i : @_{k} @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{n} m α \cdot_{k} i : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{n} m α : @_{n} m \Rightarrow T \cup {α \cdot_{k} i} α : @_{n} m .

α : @_{n} \Box@_{n} p \Rightarrow T α : @_{n} □ p α : @_{n} \Box@_{n} p \Rightarrow T \cup {α \cdot_{n} i} α : \cdot_{n} i : @_{n} p α \cdot_{n} i : @_{n} @_{n} p \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} p α \cdot_{n} i : @_{n} p \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} p

α : @_{n} \Box@_{n} p \Rightarrow T α : @_{n} □ p α : @_{n} \Box@_{n} p \Rightarrow T \cup {α \cdot_{n} i} α : \cdot_{n} i : @_{n} p α \cdot_{n} i : @_{n} @_{n} p \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} p α \cdot_{n} i : @_{n} p \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} p

\Rightarrow T α : @_{k} @_{n} □ (ψ \to@_{n} F φ) \Rightarrow T α : @_{n} □ (ψ \to@_{n} F φ) \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} (ψ \to@_{n} F φ) α \cdot_{n} i : @_{n} ψ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} @_{n} F φ α \cdot_{n} i : @_{n} ψ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} F φ α \cdot_{n} i : @_{n} ψ, α \cdot_{n} i : @_{n} ⟨ F ⟩ m \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{m} φ,

\Rightarrow T α : @_{k} @_{n} □ (ψ \to@_{n} F φ) \Rightarrow T α : @_{n} □ (ψ \to@_{n} F φ) \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} (ψ \to@_{n} F φ) α \cdot_{n} i : @_{n} ψ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} @_{n} F φ α \cdot_{n} i : @_{n} ψ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} F φ α \cdot_{n} i : @_{n} ψ, α \cdot_{n} i : @_{n} ⟨ F ⟩ m \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{m} φ,

α : ρ_{1}, \dots, α : ρ_{h}, Γ \Rightarrow T Δ

α : ρ_{1}, \dots, α : ρ_{h}, Γ \Rightarrow T Δ

α : @_{n} ⟨ F ⟩ n, Γ \Rightarrow T Δ α : @_{n} ⟨ F ⟩ m, Γ \Rightarrow T Δ α : @_{m} ⟨ F ⟩ n, Γ \Rightarrow T Δ.

α : @_{n} ⟨ F ⟩ n, Γ \Rightarrow T Δ α : @_{n} ⟨ F ⟩ m, Γ \Rightarrow T Δ α : @_{m} ⟨ F ⟩ n, Γ \Rightarrow T Δ.

α : @_{n} □ φ, Γ \Rightarrow T Δ β : @_{n} φ, Γ \Rightarrow T Δ

α : @_{n} □ φ, Γ \Rightarrow T Δ β : @_{n} φ, Γ \Rightarrow T Δ

α : ρ_{1}, \dots, α : ρ_{h} \Rightarrow T α : ρ_{1}^{'}, \dots, α : ρ_{l}^{'} \lx@proof@logical@and α : ρ_{1}^{'} \Rightarrow T α : ρ_{1}^{'}, \dots, α : ρ_{l}^{'} \dots α : ρ_{l}^{'} \Rightarrow T α : ρ_{1}^{'}, \dots, α : ρ_{l}^{'} .

α : ρ_{1}, \dots, α : ρ_{h} \Rightarrow T α : ρ_{1}^{'}, \dots, α : ρ_{l}^{'} \lx@proof@logical@and α : ρ_{1}^{'} \Rightarrow T α : ρ_{1}^{'}, \dots, α : ρ_{l}^{'} \dots α : ρ_{l}^{'} \Rightarrow T α : ρ_{1}^{'}, \dots, α : ρ_{l}^{'} .

α : @_{n} □ φ \Rightarrow T α : @_{n} φ α : @_{n} φ \Rightarrow T α : @_{n} φ .

α : @_{n} □ φ \Rightarrow T α : @_{n} φ α : @_{n} φ \Rightarrow T α : @_{n} φ .

α : @_{n} □ φ \Rightarrow T α : @_{n} □□ φ α : @_{n} □ φ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} □ φ α : @_{n} □ φ \Rightarrow T \cup {α \cdot_{n} i, α \cdot_{n} i \cdot_{n} j} α \cdot_{n} i \cdot_{n} j : @_{n} φ α \cdot_{n} i \cdot_{n} j : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i, α \cdot_{n} i \cdot_{n} j} α \cdot_{n} i \cdot_{n} j : @_{n} φ .

α : @_{n} □ φ \Rightarrow T α : @_{n} □□ φ α : @_{n} □ φ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} □ φ α : @_{n} □ φ \Rightarrow T \cup {α \cdot_{n} i, α \cdot_{n} i \cdot_{n} j} α \cdot_{n} i \cdot_{n} j : @_{n} φ α \cdot_{n} i \cdot_{n} j : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i, α \cdot_{n} i \cdot_{n} j} α \cdot_{n} i \cdot_{n} j : @_{n} φ .

α : @_{n} φ \Rightarrow T α : @_{n} □ \neg □ \neg φ α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} \neg □ \neg φ α \cdot_{n} i : @_{n} □ \neg φ, α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α : @_{n} \neg φ, α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α : @_{n} φ .

α : @_{n} φ \Rightarrow T α : @_{n} □ \neg □ \neg φ α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α \cdot_{n} i : @_{n} \neg □ \neg φ α \cdot_{n} i : @_{n} □ \neg φ, α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α : @_{n} \neg φ, α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α : @_{n} φ \Rightarrow T \cup {α \cdot_{n} i} α : @_{n} φ .

α : @_{n} □ φ, Γ \Rightarrow T Δ β : @_{n} φ, Γ \Rightarrow T Δ

α : @_{n} □ φ, Γ \Rightarrow T Δ β : @_{n} φ, Γ \Rightarrow T Δ

Peer Reviews

No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.

Videos

No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.

Taxonomy

TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Logic, programming, and type systems

Full text

11institutetext: Department of Philosophy, Graduate School of Letters,

Hokkaido University, Sapporo, Japan

11email: [email protected]

Authors’ Instructions

Axiomatizing Epistemic Logic of Friendship

via Tree Sequent Calculus

Katsuhiko Sano

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.

Keywords:

Epistemic Logics of Friendship, Tree Sequent Calculus, Hilbert System, Completeness, Cut Elimination Theorem

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 [3, 1]. 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] added a dynamic mechanism to $\mathbf{EFL}$ for capturing public announcements [19], announcements to all the friends, and private announcements [2] and established a relative completeness result (cf. [23, 24, 12]), i.e., they provided a set of recursion axioms for dynamic operators. So once we can provide a sound and complete proof system for $\mathbf{EFL}$ , i.e., the fragment without dynamic operators, we can also establish the semantic completeness of the dynamic extension of $\mathbf{EFL}$ . Therefore, this paper focuses on an open 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 [15, 8] for modal logic and $@$ -prefixed sequent [21, 7] for hybrid logic. One of the merits of our notion of sequent is that we can still 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 systems. 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 3.1). Section 4 establishes a completeness result of a cut-free fragment of our sequent calculus (Theorem 4.1). As a corollary, we also provide a semantic proof of the cut elimination theorem of our sequent calculus (Theorems 5.1 and 5.2, 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{KT}$ , $\mathbf{S4}$ or $\mathbf{S5}$ axioms and a friendship relation satisfies a certain form of universal property (Theorems 6.1 and 6.2, Corollary 3). 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 $\to$ (the implication) and $\bot$ (the falsum), the satisfaction operators $@$ and the friendship operator $\mathsf{F}$ (read as “all my friends are …”) as well as the modal operator $\Box$ which may be regarded as the knowledge operator. 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:

[TABLE]

where $n\in\mathsf{Nom}$ and $p\in\mathsf{Prop}$ . Boolean connectives other than $\to$ or $\bot$ are introduced as ordinary abbreviations. We define the dual of $\Box$ as $\Diamond$ := $\neg\Box\neg$ and the dual of $\mathsf{F}$ as $\langle\mathsf{F}\rangle$ := $\neg\mathsf{F}\neg$ . 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}\to\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$ .

A model $\mathfrak{M}$ for our syntax $\mathcal{L}$ is a tuple

[TABLE]

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}\to\mathcal{P}(W\times A)$ such that $V(n)$ is a subset of $W\times A$ of the form $W\times\{\,{a}\,\}$ . When $V(n)$ = $W\times\{\,{a}\,\}$ , we denote such unique element $a$ by $\underline{n}$ . We note that a semantic value $\underline{n}$ of a nominal $n$ is rigid over all possible states. We do not require any property for $R_{a}$ and $\asymp_{w}$ but we will come back to this point in Section 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:

[TABLE]

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.

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 [math], $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

$\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$

where $\Gamma$ and $\Delta$ are finite sets of labelled formulas, $\mathcal{T}$ is a finite tree of labels, and all the labels in $\Gamma$ and $\Delta$ are in $\mathcal{T}$ . A tree sequent “ $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ ” is read as “if we assume all labelled formulas in $\Gamma$ , then we may conclude some labelled formulas in $\Delta$ .” A tree sequent $0:@_{n}\varphi,0\cdot_{k}2:@_{m}\rho\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}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, [math], $0\cdot_{n}1$ and $0\cdot_{k}2$ are “addresses” of the root, the left leaf, and the right leaf, respectively. Therefore, our tree sequent is a finite tree, each of which nodes has an $@$ -prefixed sequent as given in [21, 7].

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}^{-}$ . All the initial sequents and inference rules except $(\mathsf{rigid}_{=})$ , $(w\mathsf{lab})$ , $(\Box R)$ and $(\Box L)$ originate from sequent calculus for hybrid logic in terms of $@$ -prefixed sequents (cf. [21, 7] ). The inference rules $(w\mathsf{lab})$ , $(\Box R)$ and $(\Box L)$ reflect the idea of tree or nested sequent calculus for modal logic (cf. [15, 8]). Finally the rule $(\mathsf{rigid}_{=})$ encodes the semantic idea that a semantic value of a nominal is rigid, i.e., the same through all possible states.

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 $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ 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 $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ .

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}\to 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 often 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:

[TABLE]

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

Theorem 3.1 (Soundness of $\mathsf{T}\mathbf{EFL}$ )

If a tree sequent $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is provable in $\mathsf{T}\mathbf{EFL}$ then $\mathfrak{M},f\models\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ 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

$\mathrm{(i)}$

The following substitution rule $(\mathsf{sub})$ is height-preserving admissible in $\mathsf{T}\mathbf{EFL}^{-}$ and $\mathsf{T}\mathbf{EFL}$ :

[TABLE]

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

$\mathrm{(ii)}$

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}$ .

[TABLE]

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

In what follows in this section, sets $\Gamma$ , $\Delta$ , 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 $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is provable in $\mathsf{T}\mathbf{EFL}^{-}$ if there exist finite sets $\Gamma^{\prime}\subseteq\Gamma$ and $\Delta^{\prime}\subseteq\Delta$ and finite subtree $\mathcal{T}^{\prime}$ of $\mathcal{T}$ such that $\Gamma^{\prime}\stackrel{{\scriptstyle\mathcal{T}^{\prime}}}{{\Rightarrow}}\Delta^{\prime}$ is provable in $\mathsf{T}\mathbf{EFL}^{-}$ .

Definition 1 (Saturated tree sequent)

A possibly infinite tree sequent $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is saturated if it satisfies the following conditions:

(rep1)

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

(rep2)

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

(ref=)**

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

(rigid=)**

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

( $\to$ r)

If $\alpha:@_{n}(\varphi\to\psi)\in\Delta$ then $\alpha:@_{n}\varphi\in\Gamma$ and $\alpha:@_{n}\psi\in\Delta$ .

( $\to$ l)

If $\alpha:@_{n}(\varphi\to\psi)\in\Gamma$ then $\alpha:@_{n}\varphi\in\Delta$ or $\alpha:@_{n}\psi\in\Gamma$ .

( $@$ r)

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

( $@$ l)

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

( $\mathsf{F}$ r)

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

( $\mathsf{F}$ l)

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

( $\Box$ r)

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

( $\Box$ l)

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

Lemma 1 (Saturation lemma)

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

Proof

Let $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ be an unprovable tree sequent in $\mathsf{T}\mathbf{EFL}^{-}$ . Let $(\alpha_{i}:@_{{n}_{i}}\varphi_{i})_{i\in\omega}$ be an enumeration of all labelled formulas such that each labelled formula occurs infinitely often. In what follows, we inductively define a sequence $(\Gamma_{i}\stackrel{{\scriptstyle\mathcal{T}_{i}}}{{\Rightarrow}}\Delta_{i})_{i\in\omega}$ of unprovable tree sequents in $\mathsf{T}\mathbf{EFL}^{-}$ such that $\Gamma_{i}\subseteq\Gamma_{i+1}$ , $\Delta_{i}\subseteq\Delta_{i+1}$ and $\mathcal{T}_{i}\subseteq\mathcal{T}_{i+1}$ for all $i\in\omega$ . (Basis) When $i=0$ , a tree sequent $\Gamma_{0}\stackrel{{\scriptstyle\mathcal{T}_{0}}}{{\Rightarrow}}\Delta_{0}$ is defined as the tree sequent $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ which is clearly unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ .

(Inductive Step) Suppose that we have defined $(\Gamma_{i}\stackrel{{\scriptstyle\mathcal{T}_{i}}}{{\Rightarrow}}\Delta_{i})_{0\leqslant i\leqslant j}$ . We define $\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ in the following two steps.

**Step 1: **

This step expands $\Gamma_{j}$ by the rules $(\mathsf{rep}_{=1})$ , $(\mathsf{rep}_{=2})$ , $(\mathsf{ref}_{=})$ and $(\mathsf{rigid}_{=})$ while $\Delta_{j}$ and $\mathcal{T}_{j}$ are unchanged. First, we enumerate all the finite pairs of the form

$(\alpha:@_{n}m,\alpha:\varphi[n/k])$ or $(\alpha:@_{m}n,\alpha:\varphi[n/k])$

found in $\Gamma_{j}$ and for each such pair we add $\alpha:\varphi[m/k]$ to $\Gamma_{j}$ to define the expanded set as $\Gamma_{j}^{\mathsf{rep}}$ . It is easy to see that $\Gamma_{j}^{\mathsf{rep}}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by $(\mathsf{rep}_{=1})$ and $(\mathsf{rep}_{=2})$ . Second, we define

[TABLE]

It is immediate to see that $\Gamma_{j}^{\mathsf{ref}}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by $(\mathsf{ref}_{=})$ . Finally we define $\Gamma_{j}^{=}$ := $\{\,{\beta:@_{n}m}\,|\,{\alpha:@_{n}m\in\Gamma_{j}^{\mathsf{ref}}\text{ and }\beta\in\mathcal{T}_{j}}\,\}$ . Then the unprovability of $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ in $\mathsf{T}\mathbf{EFL}^{-}$ is due to $(\mathsf{rigid}_{=})$ . We note that $\Gamma_{j}^{=}$ is still finite.

**Step 2: **

This step expands the unprovable tree sequent $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ by logical rules, depending on the form of the $j$ -th element $\alpha_{j}:@_{n_{j}}\varphi_{j}$ of our enumeration of labelled formulas.

•

Let $\varphi_{j}$ be of the form $\psi_{1}\to\psi_{2}$ and $\alpha_{j}:@_{n_{j}}(\psi_{1}\to\psi_{2})\in\Gamma_{j}^{=}$ . Then either

$\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j},\alpha_{j}:@_{n_{j}}\psi_{1}$ or $\alpha_{j}:@_{n_{j}}\psi_{2},\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$

is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by $(\to L)$ . We choose an unprovable tree sequent as $\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ .

•

Let $\varphi_{j}$ be of the form $\psi_{1}\to\psi_{2}$ and $\alpha_{j}:@_{n_{j}}(\psi_{1}\to\psi_{2})\in\Delta_{j}$ . Then

$\alpha_{j}:@_{n_{j}}\psi_{1},\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j},\alpha_{j}:@_{n_{j}}\psi_{2}$

is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by $(\to R)$ and it is chosen as $\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ .

•

Let $\varphi_{j}$ be of the form $@_{m}\psi$ and $\alpha_{j}:@_{n_{j}}@_{m}\psi\in\Gamma_{j}^{=}$ . Then

$\alpha_{j}:@_{m}\psi_{1},\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$

is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by $(@L)$ and it is chosen as $\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ .

•

Let $\varphi_{j}$ be of the form $@_{m}\psi$ and $\alpha_{j}:@_{n_{j}}@_{m}\psi\in\Delta_{j}$ . Then

$\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j},\alpha_{j}:@_{m}\psi_{1}$

is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by $(@R)$ and it is chosen as $\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ .

•

Let $\varphi_{j}$ be of the form $\mathsf{F}\psi$ and $\alpha_{j}:@_{n_{j}}\mathsf{F}\psi\in\Gamma_{j}^{=}$ . Let $m_{0}$ , $\ldots$ , $m_{l}$ be all the finite agent nominals occuring in $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ . We define an increasing sequence $(\Gamma_{j}^{(i)}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}^{(i)})_{0\leqslant i\leqslant l+1}$ of unprovable tree sequent in $\mathsf{T}\mathbf{EFL}^{-}$ as follows (it is noted that $\mathcal{T}_{j}$ is unchanged in this process). We put $\Gamma_{j}^{(i)}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}^{(i)}$ := $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ . Suppose that we have constructed $(\Gamma_{j}^{(i)}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}^{(i)})_{1\leqslant i\leqslant h}$ . Then either

$\Gamma_{j}^{(h)}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}^{(h)},\alpha_{j}:@_{n_{j}}\langle\mathsf{F}\rangle m_{h}$ or $\alpha_{j}:@_{m_{h}}\psi,\Gamma_{j}^{(h)}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}^{(h)}$

is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by the rule $(\mathsf{F}L)$ . We choose an unprovable tree sequent as $\Gamma_{j}^{(h+1)}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}^{(h+1)}$ . Finally we define

$\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ := $\Gamma_{j}^{(l+1)}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}^{(l+1)}$ .

•

Let $\varphi_{j}$ be of the form $\mathsf{F}\psi$ and $\alpha_{j}:@_{n_{j}}\mathsf{F}\psi\in\Delta_{j}$ . Let $m$ be a fresh agent nominal not occuring in $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ and define

$\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ := $@_{n_{j}}\langle\mathsf{F}\rangle m,\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j},\alpha_{j}:@_{m}\psi$ ,

whose unprovability in $\mathsf{T}\mathbf{EFL}^{-}$ is assured by the rule $(\mathsf{F}R)$ .

•

Let $\varphi_{j}$ be of the form $\Box\psi$ and $\alpha_{j}:@_{n_{j}}\Box\psi\in\Gamma_{j}^{=}$ . Let us enumerate all finite $n_{j}$ -children of $\alpha_{j}$ in $\mathcal{T}_{j}$ as $\beta_{1}$ , $\ldots$ , $\beta_{h}$ and define $\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ as $\beta_{1}:@_{n_{j}}\psi,\ldots,\beta_{h}:@_{n_{j}}\psi,\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ , which is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ by the rule $(\Box L)$ .

•

Let $\varphi_{j}$ be of the form $\Box\psi$ and $\alpha_{j}:@_{n_{j}}\Box\psi\in\Delta_{j}$ . Let $\beta$ be a fresh label not occuring in $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ such that $\beta$ is an $n_{j}$ -child of $\beta$ , and define

$\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ := $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}\cup\{\,{\beta}\,\}}}{{\Rightarrow}}\Delta_{j},\beta:@_{n_{j}}\psi$ ,

whose unprovability in $\mathsf{T}\mathbf{EFL}^{-}$ is assured by the rule $(\Box R)$ .

•

Otherwise, $\Gamma_{j+1}\stackrel{{\scriptstyle\mathcal{T}_{j+1}}}{{\Rightarrow}}\Delta_{j+1}$ is defined as $\Gamma_{j}^{=}\stackrel{{\scriptstyle\mathcal{T}_{j}}}{{\Rightarrow}}\Delta_{j}$ .

We have finished defined a sequence $(\Gamma_{i}\stackrel{{\scriptstyle\mathcal{T}_{i}}}{{\Rightarrow}}\Delta_{i})_{i\in\omega}$ . We define $\Gamma^{+}$ := $\bigcup_{i\in\omega}\Gamma_{i}$ , $\mathcal{T}^{+}$ := $\bigcup_{i\in\omega}\mathcal{T}_{i}$ and $\Delta^{+}$ := $\bigcup_{i\in\omega}\Delta_{i}$ . Then it is easy to see that $\Gamma^{+}\stackrel{{\scriptstyle\mathcal{T}^{+}}}{{\Rightarrow}}\Delta^{+}$ is a saturated sequent (we note that the rule $(w\mathsf{lab})$ is needed here). ∎

Lemma 2

Let $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ 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 $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ by:

•

$A$ * $:=$ $\{\,{|n|}\,|\,{\text{$ 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\Gamma$ 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\Gamma$ .*

•

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

•

$(\alpha,|n|)\in V(p)$ * iff $\alpha:@_{n}p\in\Gamma$ $(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\Gamma$ then $\mathfrak{M},(\alpha,|n|)\models\varphi$ ;

$(\mathrm{ii})$

If $\alpha:@_{n}\varphi\in\Delta$ 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^{\prime}$ and $m\sim m^{\prime}$ then $\alpha:@_{n}\langle\mathsf{F}\rangle m\in\Gamma$ iff $\alpha:@_{n^{\prime}}\langle\mathsf{F}\rangle m^{\prime}\in\Gamma$ . 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\Gamma$ and $\alpha:@_{m}p\in\Gamma$ 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\Gamma}\,\}$ 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: $m$ , $\bot$ or $\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 $m$ . For (i), suppose that $\alpha:@_{n}m\in\Gamma$ . This means that $|n|$ = $|m|$ . Since $V(m)$ = $\mathcal{T}\times\{\,{|m|}\,\}$ , we have $\mathfrak{M},(\alpha,|n|)\models m$ , as desired. For (ii), assume that $\alpha:@_{n}m\in\Delta$ and suppose for contradiction that $\mathfrak{M},(\alpha,|n|)\models m$ , i.e., $|n|$ = $|m|$ . It follows from $|n|$ = $|m|$ and the saturation condition $(\mathbf{rigid}_{=})$ that $\alpha:@_{n}m\in\Gamma$ . This is a contradiction with the unprovability of $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ in $\mathsf{T}\mathbf{EFL}^{-}$ . Therefore, we conclude that $\mathfrak{M},(\alpha,|n|)\not\models m$ .

•

Let $\varphi$ be of the form $\bot$ . Since $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is unprovable in $\mathsf{T}\mathbf{EFL}^{-}$ , it is impossible to have $\alpha:@_{n}\bot\in\Gamma$ , (i) trivially holds. Since $\mathfrak{M},(\alpha,|n|)\not\models\bot$ always holds, (ii) also holds.

•

Let $\varphi$ be of the form $\mathsf{F}\varphi$ . For (i), assume that $\alpha:@_{n}\mathsf{F}\varphi\in\Gamma$ . 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\Gamma$ hence $\alpha:@_{n}\langle\mathsf{F}\rangle m\notin\Delta$ by the unprovability of $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ . By the condition $(\mathsf{F}\mathbf{l})$ , we obtain $\alpha:@_{m}\varphi\in\Gamma$ , which implies our goal by induction hypothesis.

For (ii), assume that $\alpha:@_{n}\mathsf{F}\varphi\in\Delta$ . By the saturation condition $(\mathsf{F}\mathbf{r})$ , we have that $\alpha:@_{n}\langle\mathsf{F}\rangle m\in\Gamma$ and $\alpha:@_{m}\varphi\in\Delta$ 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\Gamma$ . 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\Gamma$ for some label $\gamma$ . By $\alpha:@_{n}\Box\varphi\in\Gamma$ and $\gamma:@_{n}m\in\Gamma$ , the saturation condition ( $\mathbf{rep}_{1}$ ) implies that $\alpha:@_{m}\Box\varphi\in\Gamma$ . By the saturation condition ( $\Box\mathbf{l}$ ) and the fact that $\beta$ is an $m$ -child of $\alpha$ , we obtain $\beta:@_{m}\varphi\in\Gamma$ . 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\Delta$ . By the saturation condition $(\Box\mathbf{r})$ , we have that $\beta:@_{n}\varphi\in\Delta$ 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$ . ∎

Theorem 4.1 (Completeness of cut-free $\mathsf{T}\mathbf{EFL}^{-}$ )

If $\mathfrak{M},f\models\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ for all models $\mathfrak{M}$ and all assignments $f$ , then $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is provable in $\mathsf{T}\mathbf{EFL}^{-}$ .

Proof

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

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

Corollary 1

The following are all equivalent:

$\mathfrak{M},f\models\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ * for all models $\mathfrak{M}$ and all assignments $f$ .* 2. 2.

$\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ * is provable in $\mathsf{T}\mathbf{EFL}^{-}$ .* 3. 3.

$\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ * 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\to 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}\to@_{n}\Box(\psi_{1}\to@_{m}\Box(\psi_{2}\to\#))$ , then $L(\varphi)$ is $\psi_{0}\to@_{n}\Box(\psi_{1}\to@_{m}\Box(\psi_{2}\to\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 presents our Hilbert system $\mathsf{H}\mathbf{EFL}$ . The underlying idea of the system is the following. On the top of the propositional part (Taut and 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 [5, 4]) 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≠*), 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}$ . 111 By (K)-rules and (Nec)-rules for operators $\Box$ , $\mathsf{F}$ and $@_{n}$ , the replacement of equivalence holds in $\mathsf{H}\mathbf{EFL}$ . 222Given a set $\Gamma\cup\{\,{\varphi}\,\}$ of formulas, we say that $\varphi$ is deducible in $\mathsf{H}\mathbf{EFL}$ from $\Gamma$ if there exist finite formulas $\psi_{1}$ , $\ldots$ , $\psi_{n}\in\Gamma$ such that $(\psi_{1}\land\cdots\land\psi_{n})\to\varphi$ is provable in $\mathsf{H}\mathbf{EFL}$ . Then it is easy to see that the deduction theorem holds in $\mathsf{H}\mathbf{EFL}$ .

Proposition 2

Uniform substitutions are length-preserving admissible in $\mathsf{H}\mathbf{EFL}$ , i.e., if $\sigma$ is a uniform substitution and $\varphi$ has a derivation in $\mathsf{H}\mathbf{EFL}$ whose length is at most $n$ , then $\varphi\sigma$ has a derivation in $\mathsf{H}\mathbf{EFL}$ whose length is at most $n$ .

Proposition 3

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

$@_{m}@_{n}\varphi\leftrightarrow@_{n}\varphi$ . 2. 2.

$n\to(@_{n}\varphi\leftrightarrow\varphi)$ . 3. 3.

$@_{n}m\to(@_{n}\varphi\leftrightarrow@_{m}\varphi)$ . 4. 4.

$@_{n}m\leftrightarrow@_{m}n$ . 5. 5.

$@_{n}(\varphi\to\psi)\leftrightarrow(@_{n}\varphi\to@_{n}\psi)$ . 6. 6.

$@_{n}m\to(\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\to(\varphi\to@_{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$ is of the form $l\in\mathsf{Nom}$ , $\Box\psi$ and $@_{l}\psi$ . First, we consider the case where $\varphi$ is of the form $l\in\mathsf{Nom}$ . When $l\not\equiv k$ , there is nothing to prove, so we focus on the case where $l\equiv k$ . It suffices to show that $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to(n\leftrightarrow m)$ , but this is clear from items 2 and 4. Second, we move to the case where $\varphi$ is of the form $\Box\psi$ . By induction hypothesis, we obtain $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to(\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\to(\Box(\psi[n/k])\leftrightarrow\Box(\psi[m/k]))$ . It follows from the axiom $(\texttt{rigid}_{=})$ that $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to((\Box\psi)[n/k]\leftrightarrow(\Box\psi)[m/k]))$ , as desired. Third, we deal with the case where $\varphi$ is of the form $@_{l}\psi$ . When $l\equiv k$ , we show that $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to(@_{l}(\psi[n/k])\leftrightarrow@_{l}(\psi[m/k]))$ . This is easily obtained by induction hypothesis, $(\texttt{Nec}_{@})$ and items 1 and 5. When $l\not\equiv k$ , it suffices to prove that $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to(@_{n}(\psi[n/k])\leftrightarrow@_{m}(\psi[m/k]))$ . By induction hypothesis, we have $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to((\psi[n/k])\leftrightarrow(\psi[m/k]))$ . By $(\texttt{Nec}_{@})$ , we have

[TABLE]

By items 2 and 5,

[TABLE]

By items 3 and 4,

[TABLE]

This allows us to conclude $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to(@_{n}(\psi[n/k])\leftrightarrow@_{m}(\psi[m/k]))$ . ∎

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

Definition 3 (Formulaic translation)

Given a set $\Theta$ of labelled formulas and a label $\alpha$ , we define $\Theta_{\alpha}$ $:=$ $\{\,{\varphi}\,|\,{\alpha:\varphi\in\Theta}\,\}$ . Let $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ be a tree sequent. Then the formulaic translation of the sequent at $\alpha$ is defined inductively as:

[TABLE]

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 Section 3 at the root [math] is

$@_{n}\varphi\to(@_{m}\psi\lor@_{n}\Box(\top\to@_{k}\theta)\lor@_{k}\Box(@_{m}\rho\to\bot))$ .

Theorem 5.1

If a tree sequent $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is provable in $\mathsf{T}\mathbf{EFL}$ then the formulaic translation $[\![\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta]\!]_{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 $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ in $\mathsf{T}\mathbf{EFL}$ , where $i$ is the root of the tree $\mathcal{T}$ . We skip the base case where $n$ = [math]. 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 3 (6), the axiom (Ref), (Agree), or Proposition 3 (1), respectively. Here we focus on the cases where $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ 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,\Gamma^{\prime}\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is obtained by ( $\Box L$ ) from $\beta:@_{n}\varphi,\Gamma^{\prime}\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ , 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,\Gamma^{\prime}\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{i}$ . We show that $\vdash_{\mathsf{H}\mathbf{EFL}}\left[\!\!\left[\alpha:@_{n}\Box\varphi,\Gamma^{\prime}\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\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

[TABLE]

Let $h$ = [math] and so $\alpha_{l-h}$ = $\alpha$ . It suffices to show that a formula of the form

[TABLE]

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

[TABLE]

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,\Gamma^{\prime}\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{i}$ .

( $\mathsf{F}R$ )

Suppose that $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta^{\prime},\alpha:@_{n}\mathsf{F}\varphi$ is obtained by ( $\mathsf{F}R$ ) from $\alpha:@_{n}\langle\mathsf{F}\rangle m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta^{\prime},\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,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta^{\prime},\alpha:@_{m}\varphi\right]\!\!\right]_{i}$ , which is equivalent to $\vdash_{\mathsf{H}\mathbf{EFL}}L(@_{n}\langle\mathsf{F}\rangle m\to@_{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[\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta^{\prime},\alpha:@_{n}\mathsf{F}\varphi\right]\!\!\right]_{i}$ .

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

Let us suppose that $\alpha:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is obtained by $(\mathsf{rigid}_{=})$ from $\beta:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ . By induction hypothesis, we obtain $\vdash_{\mathsf{H}\mathbf{EFL}}\left[\!\!\left[\beta:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{i}$ . Our goal is to show that $\vdash_{\mathsf{H}\mathbf{EFL}}\left[\!\!\left[\alpha:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{i}$ . It suffices to show the following two cases: (i) $\beta$ is a $k$ -child of $\alpha$ or (ii) $\alpha$ is a $k$ -child of $\beta$ . We note that we will use the axioms $(\texttt{Rigid}_{=})$ in (i) and $(\texttt{Rigid}_{\neq})$ in (ii). First, we deal with the case (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}$ . Recall that we assume that $\beta$ is a $k$ -child of $\alpha$ . By induction on $0\leqslant h\leqslant l$ , we show that $\vdash_{\mathsf{H}\mathbf{EFL}}\left[\!\!\left[\beta:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{\alpha_{l-h}}\to\left[\!\!\left[\alpha:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{\alpha_{l-h}}$ . Let $h$ = [math] and so $\alpha_{l-h}$ = $\alpha$ . It suffices to show that a formula of the form:

[TABLE]

is provable in ${\mathsf{H}\mathbf{EFL}}$ . For this, it suffices to show $\vdash_{\mathsf{H}\mathbf{EFL}}@_{n}m\to@_{k}\Box@_{n}m$ , which holds by $(\texttt{Rigid}_{=})$ , the distribution of $@$ over the implication and Proposition 3 (1). 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}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{i}$ . Second, we move to the case (ii). Let $(\beta_{0},\beta_{1},\ldots,\beta_{l})$ be the unique path from $\beta$ ( $\equiv$ $\beta_{l}$ ) to the root $i$ ( $\equiv$ $\beta_{0}$ ) of tree $\mathcal{T}$ . Note that we assume that $\alpha$ is a $k$ -child of $\beta$ . By induction on $0\leqslant h\leqslant l$ , we show that $\vdash_{\mathsf{H}\mathbf{EFL}}\left[\!\!\left[\beta:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{\beta_{l-h}}\to\left[\!\!\left[\alpha:@_{n}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{\beta_{l-h}}$ . Let $h$ = [math] and so $\beta_{l-h}$ = $\beta$ . It suffices to show that a formula of the form:

[TABLE]

is provable in ${\mathsf{H}\mathbf{EFL}}$ . For this, it suffices to show $\vdash_{\mathsf{H}\mathbf{EFL}}\neg@_{n}m\to@_{k}\Box\neg@_{n}m$ , which holds by $(\texttt{Rigid}_{\neq})$ , $(\texttt{Selfdual})$ and Proposition 3 (1). 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}m,\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\right]\!\!\right]_{i}$ . ∎

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 the cut rule. The cut rule is necessary to prove the following.

Lemma 3

The rules $(\to 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 $(\to R)$ and $(\Box R)$ . First we deal with $(\to R)$ . Suppose that $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta,\alpha:@_{n}(\varphi\to\psi)$ is provable in $\mathsf{T}\mathbf{EFL}$ . This is shown as follows:

[TABLE]

where the rightmost tree sequent is provable in $\mathsf{T}\mathbf{EFL}$ by $(\to L)$ . Second we move to $(\Box R)$ . Suppose that $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta,\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:

[TABLE]

∎

Theorem 5.2

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

Proof

Suppose that there is a derivation $(\varphi_{0},\ldots,\varphi_{h})$ of $\varphi$ in $\mathsf{H}\mathbf{EFL}$ . By induction on $0\leqslant j\leqslant h$ , we show that $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi_{j}$ is provable in $\mathsf{T}\mathbf{EFL}$ for all nominals $n$ . We demonstrate some cases. Let us start with (Rigid*=*), which is shown as follows.

[TABLE]

For (Rigid*≠*), the following derivation is enough for our goal:

[TABLE]

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 derivation below, from which we can obtain the provability of $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{m}(@_{n}\Box@_{n}p\to@_{n}\Box p)$ in $\mathsf{T}\mathbf{EFL}$ :

[TABLE]

Now we deal with some inference rules below.

(Name)

Let $\varphi_{j}$ $\equiv$ $n\to\psi$ be obtained by $(\texttt{Name})$ . Fix any finite tree $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominal $k$ . Let $m\not\equiv k$ be a fresh nominal in $\mathcal{T}$ and $\psi$ . Note that $m$ is also fresh in $\alpha\in\mathcal{T}$ . By Proposition 2, $m\to\psi$ has a derivation whose length is at most $j$ . By induction hypothesis, $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}(m\to\psi)$ is provable in $\mathsf{T}\mathbf{EFL}$ . By admissibility of uniform substitution $[k/m]$ in $\mathsf{T}\mathbf{EFL}$ (by Proposition 1), $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}(k\to\psi)$ is provable in $\mathsf{T}\mathbf{EFL}$ . By Lemma 3, we obtain the provability of $\alpha:@_{k}k\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}\psi$ in $\mathsf{T}\mathbf{EFL}$ . By $(\mathsf{ref}_{=})$ , we conclude that $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}\psi$ is provable in $\mathsf{T}\mathbf{EFL}$ .

( $L$ (BG))

Let $\varphi_{j}$ $\equiv$ $\Box\psi$ be obtained by $(L(\texttt{BG}))$ . Fix any finite tree $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominal $k$ . By induction hypothesis, $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}L(@_{n}\langle\mathsf{F}\rangle m\to@_{m}\varphi)$ is provable in $\mathsf{T}\mathbf{EFL}$ , where we can assume that $m$ satisfies the freshness condition by Proposition 2. 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 $\Gamma,\beta:@_{n}\langle\mathsf{F}\rangle m\stackrel{{\scriptstyle\mathcal{T}^{\prime}}}{{\Rightarrow}}\Delta,\beta:@_{m}\varphi$ . Then we apply the right rules in a converse direction of our repeated application of Lemma 3 to conclude that $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}L(@_{n}\mathsf{F}\varphi)$ is provable in $\mathsf{T}\mathbf{EFL}$ . To illustrate this argument, let $L$ $\equiv$ $@_{n}\Box(\psi\to\#)$ . By induction hypothesis, $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}@_{n}\Box(\psi\to(@_{n}\langle\mathsf{F}\rangle m\to@_{m}\varphi))$ is provable in $\mathsf{T}\mathbf{EFL}$ , where recall that $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\stackrel{{\scriptstyle\mathcal{T}\cup\{\,{\alpha\cdot_{n}i}\,\}}}{{\Rightarrow}}\alpha\cdot_{n}i:@_{m}\varphi$ in $\mathsf{T}\mathbf{EFL}$ for some fresh label $\alpha\cdot_{n}i$ . Then we proceed as follows:

[TABLE]

as required.

(Nec*@*)

Let $\varphi_{j}$ $\equiv$ $@_{n}\psi$ be obtained by $(\texttt{Name})$ . Fix any finite tree $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominal $k$ . We show that $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{k}@_{n}\psi$ is provable in $\mathsf{T}\mathbf{EFL}$ . By the rule $(@R)$ , it suffices to establish the provability of $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\psi$ in $\mathsf{T}\mathbf{EFL}$ . This is immediate from induction hypothesis.

(Nec*□*)

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

(NecF)

Let $\varphi_{j}$ $\equiv$ $\mathsf{F}\psi$ be obtained by $(\texttt{Nec}_{\mathsf{F}})$ . Fix any finite tree $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominal $n$ . Let $m$ be a fresh nominal in $\psi$ . By induction hypothesis, $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\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\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{m}\psi$ . Since $m$ is fresh in $\psi$ , the rule $(\mathsf{F}R)$ enables us to derive the provability of $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\mathsf{F}\psi$ in $\mathsf{T}\mathbf{EFL}$ , as desired. ∎

Corollary 2 (Soudness and Completenss of $\mathsf{H}\mathbf{EFL}$ )

The following are all equivalent: for every formula $\varphi$ ,

$\varphi$ * is valid in the class of all models, *333 We do not need to assume that each of our models is named in the sense that each agent is named by an agent nominal in this statement. ** 2. 2.

$\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi$ * is provable in $\mathsf{T}\mathbf{EFL}^{-}$ for all $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominals $n$ ,* 3. 3.

$\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi$ * is provable in $\mathsf{T}\mathbf{EFL}$ for all $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominals $n$ ,* 4. 4.

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

Proof

Item 1 is equivalent to the following: $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi$ is true for all pairs $(\mathfrak{M},f)$ of models and assignments, finite trees $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominals $n$ . Then the equivalence between items 1, 2 and 3 holds by Corollary 1. The direction from item 4 to item 3 holds by Theorem 5.2. 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, $\stackrel{{\scriptstyle\{\,{0}\,\}}}{{\Rightarrow}}0:@_{n}\varphi$ is provable in $\mathsf{T}\mathbf{EFL}$ . It follows from Theorem 5.1 that $\vdash_{\mathsf{H}\mathbf{EFL}}[\![\stackrel{{\scriptstyle\{\,{0}\,\}}}{{\Rightarrow}}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\to\varphi$ hence $\vdash_{\mathsf{H}\mathbf{EFL}}\varphi$ by $(\texttt{Name})$ , as required. ∎

6 Extensions of Epistemic Logic of Friendship

This section explains 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 introduce the following sets of additional axioms:

•

$\mathbf{KT}$ $:=$ $\{\,{\Box\varphi\to\varphi}\,|\,{\varphi\in\mathsf{Form}}\,\}$ .

•

$\mathbf{S4}$ $:=$ $\mathbf{KT}\cup\{\,{\Box\varphi\to\Box\Box\varphi}\,|\,{\varphi\in\mathsf{Form}}\,\}$ .

•

$\mathbf{S5}$ $:=$ $\mathbf{S4}\cup\{\,{\varphi\to\Box\neg\Box\neg\varphi}\,|\,{\varphi\in\mathsf{Form}}\,\}$ .

Let us consider formulas of the form $@_{n}m$ or $@_{n}\langle\mathsf{F}\rangle m$ , which are denoted by $\rho_{i}$ , $\rho_{i}^{\prime}$ , etc. below. Let us consider a formula $\varphi$ of the following form:

$\left(\rho_{1}\land\cdots\land\rho_{h}\right)\to\left(\rho_{1}^{\prime}\lor\cdots\lor\rho_{l}^{\prime}\right)$ ,

where we note that $h$ and $l$ are possibly zero. We say that a formula of such form is a regular implication [17, Sec. 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

•

$\mathsf{irr}_{\asymp}$ $:=$ $@_{n}\langle\mathsf{F}\rangle n\to\bot$

•

$\mathsf{sym}_{\asymp}$ $:=$ $@_{n}\langle\mathsf{F}\rangle m\to@_{m}\langle\mathsf{F}\rangle n$ ,

respectively.

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, Sec. 6]):

$\alpha:\rho_{1},\ldots,\alpha:\rho_{h},\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\lx@proof@logical@and\alpha:\rho^{\prime}_{1},\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta\cdots\alpha:\rho^{\prime}_{l},\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$

When $l$ = [math], the rule $\mathsf{ri}(\varphi)$ is a zero premise rule of the following form:

[TABLE]

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:

[TABLE]

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

•

$\ddagger_{\mathbf{KT}}$ : $\alpha$ $\preceq_{n}$ $\beta$ , where $\preceq_{n}$ is the reflexive closure of the $n$ -children relation.

•

$\ddagger_{\mathbf{S4}}$ : $\alpha$ $\preceq_{n}^{\ast}$ $\beta$ , where $\preceq_{n}^{\ast}$ 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.

When $\Lambda$ is one of $\mathbf{KT}$ , $\mathbf{S4}$ and $\mathbf{S5}$ , we use “ $\Lambda$ ” as a subscript of the rule $(\Box L)$ as in:

[TABLE]

to indicate which side condition is considered. Second, we extend the resulting system with a finite set $\{\,{(\mathsf{ri}(\varphi))}\,|\,{\varphi\in\Theta}\,\}$ of inference rules, defined above, to finish to define the system $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)$ . We define $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)^{-}$ as the system $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)$ without the cut rule.

Definition 4

Given a set $\Psi$ 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 $\Psi$ is valid in $\mathfrak{F}$ $($ notation: $\mathfrak{F}\models\Psi$$)$ if $(\mathfrak{F},V),(w,a)\models\psi$ for all $\psi\in\Psi$ , valuations $V$ and pairs $(w,a)\in W\times A$ . We define a class $\mathbb{M}_{\Psi}$ of models as $\{\,{(\mathfrak{F},V)}\,|\,{\mathfrak{F}\models\Psi}\,\}$ .

Theorem 6.1

Let $\Lambda$ be one of $\mathbf{KT}$ , $\mathbf{S4}$ and $\mathbf{S5}$ , and let $\Theta$ be a possibly empty finite set of regular implications. The following are all equivalent:

$\mathfrak{M},f\models\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ * for all models $\mathfrak{M}\in\mathbb{M}_{\Lambda\cup\Theta}$ and all assignments $f$ .* 2. 2.

$\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ * is provable in $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)^{-}$ .* 3. 3.

$\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ * is provable in $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)$ .*

Therefore, $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)$ enjoys the cut-elimination theorem.

Proof

The direction from item 2 to item 3 is trivial and it is not difficult to establish the direction from from item 3 to item 1 (soundness result of $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)$ for the semantics). So we focus on showing the direction from item 1 to item 2 here. An outline of our proof is almost the same as in Lemma 1 and Lemma 2. First we introduce the notion of saturation of a possibly infinite tree squent as follows. As for $\varphi\equiv\left(\rho_{1}\land\cdots\land\rho_{h}\right)\to\left(\rho_{1}^{\prime}\lor\cdots\lor\rho_{l}^{\prime}\right)\in\Theta$ , we add the following saturation condition:

( $\mathbf{ri}(\varphi)$ )

If $\alpha:\rho_{1},\ldots,\alpha:\rho_{h}\in\Gamma$ then $\alpha:\rho^{\prime}_{j}\in\Gamma$ for some $1\leqslant j\leqslant l$ .

where the rule $(\mathsf{ri}(\varphi))$ in the tree sequent calculus is not a zero premise rule. Depending on our choice of $\Lambda$ , we change the condition $(\Box\mathbf{l})$ as follows:

$(\Box\mathbf{l}_{\mathbf{KT}})$

If $\alpha:@_{n}\Box\varphi\in\Gamma$ then $\beta:@_{n}\varphi\in\Gamma$ for all $\beta$ such that $\alpha$ $\preceq_{n}$ $\beta$ ,

$(\Box\mathbf{l}_{\mathbf{S4}})$

If $\alpha:@_{n}\Box\varphi\in\Gamma$ then $\beta:@_{n}\varphi\in\Gamma$ for all $\beta$ such that $\alpha$ $\preceq_{n}^{\ast}$ $\beta$ ,

$(\Box\mathbf{l}_{\mathbf{S5}})$

If $\alpha:@_{n}\Box\varphi\in\Gamma$ then $\beta:@_{n}\varphi\in\Gamma$ for all $\beta$ such that $\alpha$ $\sim_{n}$ $\beta$ .

Now we prove the corresponding saturation lemma to Lemma 1.

Our proof is almost the same as in the proof of Lemma 1. So we explain differences. For $(\textbf{Step 1})$ of the inductive step of the proof of Lemma 1, we modify our construction as follows. Before constructing $\Gamma_{j}^{\mathsf{rep}}$ , we construct $\Gamma_{j}^{\Theta}$ from $\Gamma_{j}$ as follows. We enumeate all the tuples in $\Gamma_{j}$ of the form $(\alpha:\rho_{1},\ldots,\alpha:\rho_{n})$ for some $\varphi\equiv\left(\rho_{1}\land\cdots\land\rho_{h}\right)\to\left(\rho_{1}^{\prime}\lor\cdots\lor\rho_{l}^{\prime}\right)\in\Theta$ (we note that the number of such tuples is finite). With the help of such enumeration (let $t$ be the number of such tuples), we inductively construct $(\Gamma_{j}^{(k)})_{0\leqslant k\leqslant t}$ such that $\Gamma_{j}^{(k)}\subseteq\Gamma_{j}^{(k+1)}$ as follows. Define $\Gamma_{j}^{(0)}$ = $\Gamma_{j}$ . Suppose that we have constructed $\Gamma_{j}^{(0)}\subseteq\cdots\subseteq\Gamma_{j}^{(k)}$ . Let $k$ -th tuple of the enumeration be $(\alpha:\rho_{1},\ldots,\alpha:\rho_{n})$ and the corresponding regular implication $\varphi$ is $\left(\rho_{1}\land\cdots\land\rho_{h}\right)\to\left(\rho_{1}^{\prime}\lor\cdots\lor\rho_{l}^{\prime}\right)$ . We can find some index $f$ such that $\alpha:\rho_{f}^{\prime},\Gamma_{j}^{(k)}\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ is unprovable in $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)^{-}$ by the rule $(\mathsf{ri}(\varphi))$ . Then we define $\Gamma_{j}^{(k+1)}$ as $\alpha:\rho_{f}^{\prime},\Gamma_{j}^{(k)}$ . Finally we define $\Gamma_{j}^{\Theta}$ := $\bigcup_{1\leqslant k\leqslant t}\Gamma_{j}^{(k)}$ . Then we do the same construction as in Step 1 for $\Gamma_{j}^{\Theta}$ instead of $\Gamma_{j}$ . For Step 2, there is no substantial change. This finishes to establish the corresponding saturation lemma to Lemma 1.

Next we comment on the corresponding lemma to Lemma 2. Let $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ be a saturated and unprovable tree sequent in $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)^{-}$ . As in the statement of Lemma 2, we define the derived model $\mathfrak{M}$ in the same way except $R_{|n|}$ . Depending on our choice of $\Lambda$ , we define $R_{|n|}$ as follows:

$(\mathbf{KT})$

$\alpha R_{|n|}\beta$ iff $\alpha$ $\preceq_{m}$ $\beta$ for some $m\in|n|$ .

$(\mathbf{S4})$

$\alpha R_{|n|}\beta$ iff $\alpha$ $\preceq_{m}^{\ast}$ $\beta$ for some $m\in|n|$ .

$(\mathbf{S5})$

$\alpha R_{|n|}\beta$ iff $\alpha$ $\sim_{m}$ $\beta$ for some $m\in|n|$ .

Then it is easy to see $R_{|n|}$ satisfies the corresponding properties of $\Lambda$ , i.e., $R_{|n|}$ is reflexive when $\Lambda$ is $\mathbf{KT}$ , $R_{|n|}$ is a pre-order when $\Lambda$ is $\mathbf{S4}$ , $R_{|n|}$ is an equivalence relation when $\Lambda$ is $\mathbf{S5}$ . The remaining argument is the same as in the proof of Lemma 2. Moreover, it follows from the saturation condition $\mathbf{ri}(\varphi)$ and the unprovability of $\Gamma\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\Delta$ in $\mathsf{T}\mathbf{EFL}(\Lambda;\Theta)^{-}$ that the corresponding properties of $\Theta$ are satisfied. This enables us to conclude the derived model $\mathfrak{M}$ belongs to $\mathbb{M}_{\Lambda\cup\Theta}$ . This finishes showing the direction from item 1 to item 2. ∎

Definition 5

When $\Lambda$ is one of $\mathbf{KT}$ , $\mathbf{S4}$ and $\mathbf{S5}$ and $\Theta$ is a finite set of regular implications, a Hilbert system $\mathsf{H}\mathbf{EFL}(\Lambda\cup\Theta)$ is defined as the axiomatic extension of $\mathsf{H}\mathbf{EFL}$ by new axioms $\Lambda\cup\Theta$ .

Theorem 6.2

Let $\Lambda$ be one of $\mathbf{KT}$ , $\mathbf{S4}$ and $\mathbf{S5}$ , and let $\Theta$ be a possibly empty finite set of regular implications. The following are all equivalent: for every formula $\varphi$ ,

$\varphi$ * is valid in $\mathbb{M}_{\Lambda\cup\Theta}$ .* 2. 2.

$\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi$ * is provable in $\mathsf{T}\mathbf{EFL}(\Lambda\cup\Theta)^{-}$ for all $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominals $n$ ,* 3. 3.

$\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi$ * is provable in $\mathsf{T}\mathbf{EFL}(\Lambda\cup\Theta)$ for all $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominals $n$ ,* 4. 4.

$\varphi$ * is provable in $\mathsf{H}\mathbf{EFL}(\Lambda\cup\Theta)$ .*

Proof

By Theorem 6.1, we can establish the equivalence between items 1, 2 and 3. We are going to provide our argument for a direction from item 4 to item 3 and a direction from item 3 to item 4.

From item 4 to item 3, we prove a similar statement to Theorem 5.2. But it suffices to prove the additional axioms from $\Lambda\cup\Theta$ are provable in $\mathsf{T}\mathbf{EFL}(\Lambda\cup\Theta)$ . In what folows, let us fix any tree $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominal $n$ . First of all, let $\psi\equiv\left(\rho_{1}\land\cdots\land\rho_{h}\right)\to\left(\rho_{1}^{\prime}\lor\cdots\lor\rho_{l}^{\prime}\right)\in\Theta$ . We show $\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\psi$ is provable in $\mathsf{T}\mathbf{EFL}(\Lambda\cup\Theta)$ . The crucial part of this derivation is the following:

[TABLE]

Let us move to $\Lambda$ . When $\Lambda$ is $\mathbf{KT}$ , it suffices to give the following derivation:

[TABLE]

When $\Lambda$ is $\mathbf{K4}$ , it suffices to give the following:

[TABLE]

Finally, if $\Lambda$ is $\mathbf{S5}$ , on the top of the above two derivation, it suffices to consider the following derivation:

[TABLE]

For the direction from item 3 to item 4, it suffices to establish the formulaic translation of the rules $(\mathsf{ri}(\varphi))$ for all $\varphi\in\Theta$ , $(\Box L_{\mathbf{KT}})$ , $(\Box L_{\mathbf{S4}})$ and $(\Box L_{\mathbf{S5}})$ at the root node preserves the provability in the corresponding system $\mathsf{H}\mathbf{EFL}(\Lambda\cup\Theta)$ . Since the case of $(\mathsf{ri}(\varphi))$ is not so difficult for every $\varphi\in\Theta$ , we focus on all the other rules. All the other rules have the following form:

[TABLE]

Let us suppose that $i$ be the root node of $\mathcal{T}$ . Let $(\alpha_{0},\ldots,\alpha_{l})$ be the unique path from the $\alpha$ ( $\equiv\alpha_{l}$ ) to the root node $i$ ( $\equiv\alpha_{0}$ ). Similarly as in the proof of the case of the rule $(\Box L)$ in Theorem 5.1, by induction on $h$ , that:

[TABLE]

where we often omit the subscript of $\vdash_{\mathsf{H}\mathbf{EFL}(\Lambda\cup\Theta)}$ to simply write $\vdash$ below when no confusion arises. When $\Lambda$ is $\mathbf{KT}$ , it suffice to check an application of $(\Box L_{\mathbf{KT}})$ where $\beta$ is $\alpha$ itself. We only establish the base case where $h$ = [math]. That is, we establish

[TABLE]

To show this, it suffice to show the following:

[TABLE]

which is easily obtained by $\vdash_{\mathsf{H}\mathbf{EFL}(\mathbf{KT}\cup\Theta)}\Box\varphi\to\varphi$ , $(\texttt{Nec}_{@})$ and $(\texttt{K}_{@})$ .

Let us move to the case where $\Lambda$ is $\mathbf{S4}$ . In this case, we suffice to check an application of $(\Box L_{\mathbf{S4}})$ where $\beta$ is a grand $n$ -child of $\alpha$ , i.e., $\beta$ is an $n$ -child of $\alpha^{\prime}$ and $\alpha^{\prime}$ is an $n$ -child of $\alpha^{\prime}$ for some label $\alpha^{\prime}\in\mathcal{T}$ . To show the base case where $h$ $=$ 0, it suffice to prove the following:

[TABLE]

which is provable by $\vdash_{\mathsf{H}\mathbf{EFL}(\mathbf{S4}\cup\Theta)}\Box\varphi\to\Box\Box\varphi$ , $(\texttt{Nec}_{@})$ and $(\texttt{K}_{@})$ .

Finally, if $\Lambda$ is $\mathbf{S5}$ , we suffice to check an application of $(\Box L_{\mathbf{S5}})$ where $\beta$ is an $n$ -parent of $\alpha$ , i.e., $\alpha$ is an $n$ -child of $\beta$ . In this case, our base case is $h$ = $1$ , i.e., we show the preservation of the provability of the formulaic translation at $\beta$ :

[TABLE]

To show it, it suffices to establish the following:

[TABLE]

Since this is equivalent with:

[TABLE]

we need to establish:

[TABLE]

by $\vdash\neg@_{n}\psi\leftrightarrow@_{n}\neg\psi$ . With the help of the axiom (DCom $@\Box$ ), $(\texttt{Nec}_{@})$ and $(\texttt{K}_{@})$ , the provability above is reduced to $\vdash_{\mathsf{H}\mathbf{EFL}(\mathbf{S5}\cup\Theta)}\neg\varphi\to\Box\neg\Box\varphi$ , which is easily obtained from the axiom scheme $\psi\to\Box\neg\Box\neg\psi$ . ∎

Recall that [23, 24] assume that the friendship relation $\asymp_{w}$ satisfies irreflexivity and symmetry and that $\Box$ obeys $\mathbf{S5}$ axioms. As a corollary of Theorem 6.2, the following provides a complete axiomatization of the logic studied in [23, 24], where $\mathsf{irr}_{\asymp}$ is $@_{n}\langle\mathsf{F}\rangle n\to\bot$ and $\mathsf{sym}_{\asymp}$ is $@_{n}\langle\mathsf{F}\rangle m\to@_{m}\langle\mathsf{F}\rangle n$ .

Corollary 3

The following are all equivalent: for every formula $\varphi$ ,

$\varphi$ * is valid in $\mathbb{M}_{\mathbf{S5}\cup\{\,{\mathsf{irr}_{\asymp},\mathsf{sym}_{\asymp}}\,\}}$ .* 2. 2.

$\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi$ * is provable in $\mathsf{T}\mathbf{EFL}(\mathbf{S5}\cup\{\,{\mathsf{irr}_{\asymp},\mathsf{sym}_{\asymp}}\,\})^{-}$ for all finite tree $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominals $n$ ,* 3. 3.

$\stackrel{{\scriptstyle\mathcal{T}}}{{\Rightarrow}}\alpha:@_{n}\varphi$ * is provable in $\mathsf{T}\mathbf{EFL}(\mathbf{S5}\cup\{\,{\mathsf{irr}_{\asymp},\mathsf{sym}_{\asymp}}\,\})$ for all finite tree $\mathcal{T}$ , $\alpha\in\mathcal{T}$ and nominals $n$ ,* 4. 4.

$\varphi$ * is provable in $\mathsf{H}\mathbf{EFL}(\mathbf{S5}\cup\{\,{\mathsf{irr}_{\asymp},\mathsf{sym}_{\asymp}}\,\})$ .*

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.

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

Is it possible to provide a syntactic proof of the cut elimination theorem of $\mathsf{T}\mathbf{EFL}$ ? 3. 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. 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 [18, 16]. 5. 5.

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

Can we apply our technique of this paper to obtain a Hilbert system of Term Modal Logics which is proposed in [10]? 444I would like to thank the anonymous reviewers of LORI VI for their careful reading of the manuscript and their many useful comments and suggestions. I presented the contents of this paper first at the 48th MLG meeting at Kaga, Ishikawa, Japan on 6th December 2013 and then at Kanazawa Workshop for Epistemic Logic and its Dynamic Extensions, Kanazawa, Japan on 22nd February 2014. I would like to thank Alexandru Baltag, Jeremy Seligman and Fenrong Liu for fruitful discussions of the topic. All errors, however, are mine. The work of the author was partially supported by JSPS KAKENHI Grant-in-Aid for Young Scientists (B) Grant Number 15K21025 and Grant-in-Aid for Scientific Research (B) Grant Number 17H02258, and JSPS Core-to-Core Program (A. Advanced Research Networks).

Bibliography24

The reference list from the paper itself. Each links out to its DOI / PubMed record.

1[1] C. Areces and B. ten Cate. Hybrid logics. In Patrick Blackburn, Johan van Benthem, and Frank Wolter, editors, Handbook of Modal Logic , pages 821–868. Elsevier, 2007.
2[2] A. Baltag, L. Moss, and S. Solecki. The logic of public announcements, common knowledge and private suspicions. In Proceedings of TARK , pages 43–56, Los Altos, 1989. Morgan Kaufmann Publishers.
3[3] P. Blackburn. Arthur Prior and hybrid logic. Synthese , 150(3):329–372, 2006.
4[4] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2001.
5[5] P. Blackburn and B. ten Cate. Pure extensions, proof rules, and hybrid axiomatics. Studia Logica , 84(3):277–322, 2006.
6[6] P. Blackburn and M. Tzakova. Hybrid completeness. Logic Journal of IGPL , 6(4):625–650, 1998.
7[7] T. Braüner. Hybrid Logic and Its Proof-Theory , volume 37 of Applied Logic Series . Springer, 2011.
8[8] K. Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic , 48:551â577, 2009.

TL;DR

Contribution

Findings

Abstract

Peer Reviews

Videos

Taxonomy

Axiomatizing Epistemic Logic of Friendship

Abstract

Keywords:

1 Introduction

2 Syntax and Two-dimensional Kripke Semantics

3 Tree Sequent Calculus of Epistemic Logic of Friendship

Theorem 3.1 (Soundness of TEFL\mathsf{T}\mathbf{EFL}TEFL)

Proposition 1

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

Definition 1 (Saturated tree sequent)

Lemma 1 (Saturation lemma)

Proof

Lemma 2

Proof

Theorem 4.1 (Completeness of cut-free TEFL−\mathsf{T}\mathbf{EFL}^{-}TEFL−)

Proof

Corollary 1

5 Hilbert System of Epistemic Logic of Friendship

Definition 2 (Necessity form)

Proposition 2

Proposition 3

Proof

Definition 3 (Formulaic translation)

Theorem 5.1

Proof

Lemma 3

Proof

Theorem 5.2

Proof

Corollary 2 (Soudness and Completenss of HEFL\mathsf{H}\mathbf{EFL}HEFL)

Proof

6 Extensions of Epistemic Logic of Friendship

Definition 4

Theorem 6.1

Proof

Definition 5

Theorem 6.2

Proof

Corollary 3

7 Further Directions

Theorem 3.1 (Soundness of $\mathsf{T}\mathbf{EFL}$ )

Theorem 4.1 (Completeness of cut-free $\mathsf{T}\mathbf{EFL}^{-}$ )

Corollary 2 (Soudness and Completenss of $\mathsf{H}\mathbf{EFL}$ )