First-order justification logic with constant domain semantics

TL;DR

This paper develops a constant domain semantics for first-order justification logic with the Barcan Formula, establishing soundness and completeness, and extends the approach to related logics, offering new tools for modal-justification frameworks.

Contribution

It introduces a novel constant domain semantics for first-order justification logic with the Barcan Formula, including proofs of soundness and completeness, and suggests generalizations to other justification logics.

Findings

Established soundness and completeness for the logic

Developed new machinery for constant domain semantics

Outlined generalization to other justification systems

Abstract

Justification logic is a term used to identify a relatively new family of modal-like logics. There is an established literature about propositional justification logic, but incursions on the first-order case are scarce. In this paper we present a constant domain semantics for the first-order logic of proofs with the Barcan Formula (FOLPb); then we prove Soundness and Completeness Theorems. A monotonic semantics for a version of this logic without the Barcan Formula is already in the literature, but constant domains requires substantial new machinery, which may prove useful in other contexts as well. Although we work mainly with one system, we also indicate how to generalize these results for the quantified version of JT45, the justification counterpart of the modal logic S5. We believe our methods are more generally applicable, but initially examining specific cases should make the work easier to follow.