Propositional justification logic went through a historical process of development taking over twenty years from its beginnings to the stage represented in this book.
Quantified justification logic is much more recent and has been in development for less than half that time. Interestingly, it seems to be passing through stages analogous to the propositional version.
The initial quantified justification logic is a first-order version of LP and is presented in this chapter. Its intended goal is to connect quantified intuitionistic logic to an arithmetic semantics, and this is also presented here. Its first (and so far only) realization proof is constructive, using a sequent calculus for first-order S4. So far, other quantified justification logics have been confined to those connected with well- known sublogics of S4. A possible world semantics has been created. And that's where things are now. Propositionally, the range of modal logics with justification counterparts was gradually extended. That has yet to happen in the quantificational setting, but it seems likely that it will.Quantificational modal logic brings complexities that do not exist propo- sitionally, or purely classically. With possible world semantics, each possible world can have its own domain of quantification, or they can all share the same one. Other possibilities exist. So for each propositional modal logic there is generally more than one quantified version. So far all development for quantified LP has been connected with the so-called monotonic version of quantified S4. This is just beginning to broaden, and a semantics for a constant domain version now exists (Fitting and Salvatore, 2018). Clearly there is much here that awaits exploration.
The initial paper on the first-order Logic of Proofs was Artemov and Yavorskaya (2001), cf. also a short discussion in Artemov (2001), in which it was shown that, unlike LP, the first-order Logic of Proofs cannot be completely ax- iomatized. In Artemov and Yavorskaya (Sidon) (2011), the First-Order Logic of Proofs, FOLP, was introduced as an explicit counterpart of first-order S4, the realization theorem was established, and several natural versions of arithmetical semantics for FOLP were outlined. Because first-order intuitionistic logic HPC can be faithfully embedded in FOS4 via Godel’s translation, this also provided HPC with a BHK-style semantics in FOLP.
In this chapter we present the current state of the subject. The only modal logic considered is S4 with a first-order semantics that is monotonic. There are no general results of the kind we saw propositionally. We hope the work presented here serves to motivate a larger community of people to continue our investigations in first-order justification logic.
10.1