Finite Kripke models and provability interpretations in quantified modal logic

TL;DR

This paper explores arithmetical completeness of quantified modal logic using finite Kripke models, adapting embedding techniques to construct provability predicates and interpretations for specific model classes.

Contribution

It introduces novel methods for embedding finite Kripke models into arithmetic via provability predicates, extending existing techniques to new model settings.

Findings

Constructed a $ ext{Sigma}_2$ Fefermanian provability predicate for well-founded models.

Developed a $ ext{Sigma}_1$ provability predicate satisfying $ ext{D2}^G$ for constant domain models.

Established arithmetical interpretations embedding finite Kripke models into arithmetic.

Abstract

In this paper, we investigate arithmetical completeness with respect to finite Kripke models of quantified modal logic. We adapt the finite-model embedding techniques of Artemov and Japaridze to two settings involving finite Kripke models. First, for conversely well-founded finite Kripke models of quantified modal logic, we construct a $\Sigma_2$ Fefermanian provability predicate together with an arithmetical interpretation that embeds the model into arithmetic. Second, for finite constant domain Kripke models of quantified modal logic, we construct a $\Sigma_1$ provability predicate satisfying $\mathbf{D2^G}$ and an arithmetical interpretation yielding such an embedding.