Linear Depth Deduction with Subformula Property for Intuitionistic Epistemic Logic

TL;DR

This paper introduces sequent calculi with the subformula property and linear depth for intuitionistic epistemic logic, enabling minimal-depth Kripke model construction and refutational proof procedures.

Contribution

It develops new sequent calculi with the subformula property and linear depth for intuitionistic epistemic logic, facilitating minimal-depth model construction and refutational methods.

Findings

Sequent calculi with subformula property and linear depth are established.

A procedure for constructing minimal-depth Kripke models for invalid formulas is designed.

Discussion of refutational sequent calculi for proving invalidity.

Abstract

In their seminal paper Artemov and Protopopescu provide Hilbert formal systems, Brower-Heyting-Kolmogorov and Kripke semantics for the logics of intuitionistic belief and knowledge. Subsequently Krupski has proved that the logic of intuitionistic knowledge is PSPACE-complete and Su and Sano have provided calculi enjoying the subformula property. This paper continues the investigations around to sequent calculi for Intuitionistic Epistemic Logics by providing sequent calculi that have the subformula property and that are terminating in linear depth. Our calculi allow us to design a procedure that for invalid formulas returns a Kripke model of minimal depth. Finally we also discuss refutational sequent calculi, that is sequent calculi to prove the invalidity.