Artemov and Protopopescu proposed intuitionistic epistemic logic (IEL) to capture an intuitionistic conception of knowledge.
By establishing completeness, they provided the base for a meta-theoretic investigation of IEL, which was continued by Krupski with a proof of cut-elimination, and Su and Sano establishing semantic cut-elimination and the finite model property.
However, to the best of our knowledge, no analysis of these results in a constructive meta-logic has been conducted.
We aim to close this gap and investigate IEL in the constructive type theory of the Coq proof assistant.
Concretely, we present a constructive and mechanised completeness proof for IEL, employing a syntactic decidability proof based on cut-elimination to constructivise the ideas from the literature.
Following Su and Sano, we then also give constructive versions of semantic cut-elimination and the finite model property.
Given our constructive and mechanised setting, all these results now bear executable algorithms.
We expect that our methods used for mechanising cut-elimination and decidability also extend to other modal logics (and have verified this observation for the classical modal logic K).