Finite Kripke models and provability interpretations in quantified modal logic

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 $Σ_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 $Σ_1$ provability predicate satisfying $\mathbf{D2^G}$ and an arithmetical interpretation yielding such an embedding.