Sequent Calculus for Intuitionistic Epistemic Logic

TL;DR

This paper develops a cut-free sequent calculus for intuitionistic epistemic logic IEL, demonstrating that proof search is feasible within polynomial space and establishing IEL as PSPACE-complete.

Contribution

It introduces a novel sequent calculus for IEL and proves its computational complexity as PSPACE-complete.

Findings

Constructed a cut-free sequent calculus for IEL

Proved polynomial space sufficiency for proof search

Established IEL as PSPACE-complete

Abstract

The formal system of intuitionistic epistemic logic IEL was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer-Hayting-Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. So, we prove that IEL is PSPACE-complete.