Publication details

Saarland University Computer Science

Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic

Christian Hagemeier, Dominik Kirst

Logical Foundations of Computer Science (LFCS), January 10-13, 2022, Deerfield Beach, Florida, U.S.A., Springer, 2022

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

Project page

Download PDF        Show BibTeX               

Login to edit

Legal notice, Privacy policy