A First-Order Expansion of Artemov and Protopopescu's Intuitionistic Epistemic Logic

Intuitionistic epistemic logic by Artemov and Protopopescu (Rev Symb Log 9:266-298, 2016) accepts the axiom "if A, then A is known" (written A superset of KA) in terms of the Brouwer-Heyting-Kolmogorov interpretation. There are two variants of intuitionistic epistemic logic: one with the axiom "KA superset of (sic)(sic)A" and one without it. The former is called IEL, and the latter is called IEL-. The aim of this paper is to study first-order expansions (with equality and function symbols) of these two intuitionistic epistemic logics. We define Hilbert systems with additional axioms called geometric axioms and sequent calculi with the corresponding rules to geometric axioms and prove that they are sound and complete for the intended semantics. We also prove the cut-elimination theorems for both sequent calculi. As a consequence, the disjunction property and existence property are established for the sequent calculi without geometric implications. Finally, we establish that our sequent calculi can also be formulated with admissible structural rules (i.e., in terms of a G3-style sequent calculus).