The Internalized Disjunction Property for Intuitionistic Justification Logic

In intuitionistic justification logic, evidence terms represent intuitionistic proofs, thatis a formula r:A means r is an intuitionistic proof of A. A natural principle in thiscontext is the internalized disjunction property (IDP), which is: for each term r thereexists a term s such that r:(A or B) implies s:A or s:B.We introduce a light extension of iJT4, in which IDP is valid. Our proof relies ona model construction that enforces sharp evidence relations and a tight connectionbetween syntax and semantics. This makes it possible to switch between proofs andmodels, which will be the key to proving IDP.