First order logic of proofs

The propositional logic of proofs LP (S. Artemov, 1995) revealed an explicit provability reading of modal logic S4 and thereby provided a provability semantics for the propositional intuitionistic logic. In the first-order case it was established that the most natural axiomatizability questions for the first-order logic of proofs have negative answers (S. Artemov, T. Yavorskaya, 2001). The questions of provability reading for first-order S4 and the first-order intuitionistic logic HPC remained open until 2011. In my talk I am going present the first-order logic of proofs FOLP and its exact interpretation in formal systems (e.g., in Peano Arithmetic). FOLP is capable of realizing first-order S4 and, therefore, HPC. This provides a semantics of explicit proofs for first-order S4 and HPC compliant with Brouwer-Heyting-Kolmogorov requirements.
(Joint work with S. Artemov.)