Intuitionistic Epistemic Logic IEL with Justification

Studies in Logic, Vol. 19, No. 3 (2026): 92–105                                  PII: 1674-3202(2026)-03-0092-14

Youan Su

Abstract. In Artemov and Protopopescu (2016), an intuitionistic epistemic logic IEL is introduced, in which the axiom A → KA is accepted whereas the axiom KA → A is rejected. This paper explores the relation between knowledge and justification on the basis of IEL. The expressions for the knowledge of a proposition "A" denoted as "KA" and the justification "t" of a proposition "A" denoted as "t:A" are included. The proposed systems contain the axioms of IEL and the axioms of the logic of proof LP (or JT4). It also includes a connection axiom t:A → KA. This paper gives Hilbert systems and Kripke-Fitting semantics for the newly introduced systems and shows that they are sound and complete for the intended semantics.