2017/04/24 by Katsuhiko Sano, Sano, Katsuhiko
Computer Science · Mathematics · #Advanced Algebra and Logic #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #cs.LO #math.LO
paper · pdf · doi:10.48550/arxiv.1704.07149
24 pages, 1 figure
openalex publication_date 2017/04/24 · arxiv created 2019/07/10 · arxiv updated 2019/07/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.