Formulating Justification Logics

We have examined a number of justification logics, each associated with a modal logic. In the next chapter it will be shown that these modal logic, justi­fication logic pairs are in fact counterparts, as defined in Section 7.2.

scheme we can use as a counterpart of the original modal formula. In a sense, it is the most general counterpart, something we will say more about later.

This does not always work. It does not work with Godel-Ldb logic, GL, for instance. It does apply to all the examples considered in this book, including the infinite family of Geach logics to be investigated in Chapter 8. In the large number of cases where it does work, it does not produce the only justification counterpart of a given modal logic, but it does produce what is, in a sense, the most general version. We illustrate this with a closer look at the most prominent and the historically first example, LP.

Other parts of the soundness proof, and the completeness proof are rather straightforward adaptations, and we omit the details.

Now here is the point. The usual formulation of LP is informally like that of LP' but with g(t) = t. In fact, in justification logics we have function sym­bols, but we do not really have a function mechanism, though one could be introduced if there were some advantage to it. But we can proceed at the meta­level. If we take the formulation of LP' and replace occurrences of g(t) with t, we get the formulation of LP. Similarly for the Fitting semantics. If we take the soundness proof for LP⁰ and make the same replacement, we get the soundness argument for LP. Similarly for the completeness argument. In short, starting with the “most general” justification counterpart of S4, we also can handle more restricted versions, and LP is such a version.

One might naturally ask why LP was formulated as it was. It was done be­cause the motivation came from the desire to create an arithmetic semantics for propositional intuitionistic logic, and the version selected was sufficient and natural for the purpose. The machinery of justification logics is rich and flexible, and this is one of its virtues.

The “most general” version has much to recommend it, because others can be derived from it with routine labor. But in general, extralogical considerations can be expected to play a role in making a choice among them.