Possible world semantics for first-order logic of proofs

In the tech report Artemov and Yavorskaya (Sidon) (2011) 4] an elegant formulation of the first-order logic of proofs was given, FOLP. This logic plays a fundamental role in providing an arithmetic semantics for first-order intuitionistic logic, as was shown. In particular, the tech report proved an arithmetic completeness theorem, and a realization theorem for FOLP. In this paper we provide a possible-world semantics for FOLP, based on the propositional semantics of Fitting (2005) 5]. We also give an Mkrtychev semantics. Motivation and intuition for FOLP can be found in Artemov and Yavorskaya (Sidon) (2011) 4], and are not fully discussed here.