# Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus

## 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.

## Key findings

- The sequent calculus is sound and complete for EFL.
- The Hilbert system derived is sound and complete.
- 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.