On First Order Logic of Proofs
Sergei Nikolaevich Artemov, Tatiana Yavorskaya · Moscow Mathematical Journal · 2001
The propositional logic of proofs LP revealed an explicit provability reading of modal logic S4 which provided an indented provability semantics for the propositional intuitionistic logic IPC and led to a new area, Justification Logic. In this paper, we find the first-order logic of proofs FOLP capable of realizing first-order modal logic S4 and, therefore, the first-order intuitionistic logic HPC. FOLP enjoys a natural provability interpretation; this provides a semantics of explicit proofs for first-order S4 and HPC compliant with Brouwer-Heyting-Kolmogorov requirements. FOLP opens the door to a general theory of first-order justification. 1