An Arithmetically Complete Predicate Modal Logic

This paper investigates a first-order extension of GL called \(\textup{ML}^3\). We outline briefly the history that led to \(\textup{ML}^3\), its key properties and some of its toolbox: the \emph{conservation theorem}, its cut-free Gentzenisation, the ``formulators'' tool. Its semantic completeness (with respect to finite reverse well-founded Kripke models) is fully stated in the current paper and the proof is retold here. Applying the Solovay technique to those models the present paper establishes its main result, namely, that \(\textup{ML}^3\) is arithmetically complete. As expanded below, \(\textup{ML}^3\) is a first-order modal logic that along with its built-in ability to simulate general classical first-order provability―"\(\Box\)" simulating the the informal classical "\(\vdash\)"―is also arithmetically complete in the Solovay sense.

EVERYONE KNOWS THAT SOMEONE KNOWS: QUANTIFIERS OVER EPISTEMIC AGENTS

Modal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics.

Implementing Connection Calculi for First-order Modal Logics

An implementation of an automated theorem prover for first-order modal logic is presented that works for the constant, cumulative and varying domains of the modal logics D, T, S4 and S5. It is based on the (classical) connection calculus and uses prefixes (or world paths) and a prefix unification algorithm to capture the restrictions given by the Kripke semantics of the standard modal logics. This permits a modular and elegant treatment of the considered modal logics and yields an efficient implementation. Details of the calculus, the implementation and performance results on the QMLTP problem library are presented.

Categories and Modalities

Category theory provides various guiding principles for modal logic and its semantic modeling. In particular, Stone duality, or “syntax-semantics duality”, has been a prominent theme in semantics of modal logic since the early days of modern modal logic. This chapter focuses on duality and a few other categorical principles, and brings to light how they underlie a variety of concepts, constructions, and facts in philosophical applications as well as the model theory of modal logic. In the first half of the chapter, I review the syntax-semantics duality and illustrate some of its functions in Kripke semantics and topological semantics for propositional modal logic. In the second half, taking Kripke’s semantics for quantified modal logic and David Lewis’s counterpart theory as examples, I demonstrate how we can dissect and analyze assumptions behind different semantics for first-order modal logic from a structural and unifying perspective of category theory. (As an example, I give an analysis of the import of the converse Barcan formula that goes farther than just “increasing domains”.) It will be made clear that categorical principles play essential roles behind the interaction between logic, semantics, and ontology, and that category theory provides powerful methods that help us both mathematically and philosophically in the investigation of modal logic.

First-order modal logic in the necessary framework of objects

I consider the first-order modal logic which counts as valid those sentences which are true on every interpretation of the non-logical constants. Based on the assumptions that it is necessary what individuals there are and that it is necessary which propositions are necessary, Timothy Williamson has tentatively suggested an argument for the claim that this logic is determined by a possible world structure consisting of an infinite set of individuals and an infinite set of worlds. He notes that only the cardinalities of these sets matters, and that not all pairs of infinite sets determine the same logic. I use so-called two-cardinal theorems from model theory to investigate the space of logics and consequence relations determined by pairs of infinite sets, and show how to eliminate the assumption that worlds are individuals from Williamson's argument.