Possible World Semantics for First Order LP

In [1] an elegant formulation of the first-order logic of proofs was given, FOLP. That report also proved an arithmetic completeness theorem, and a realization theorem for the logic. In this report we provide a possible-world semantics for FOLP, based on the propositional semantics of [2]. Motivation and intuition for the logic itself can be found in [1], and are not discussed here. We also give an Mkrtychev semantics for FOLP. This report was essentially completed June 10, 2011. 1 The Language and the Axioms This is directly from a technical report of Artemov and Yavorskaya, [1]. The language definition is not repeated here, but the axiomatization is, for reference purposes. A1 classical axioms of first order logic A2 t:XyA → t:XA, y / ∈ FVar(A) A3 t:X → t:XyA B1 t:XA → A B2 s:X(A → B) → (t:X → (s · t):XA) B3 t:XA → (t+ s):XA, s:XA → (t+ s):X