Finite Kripke models and predicate logics of provability
Sergei Nikolaevich Artemov, Giorgie Dzhaparidze · Journal of Symbolic Logic · 1990
Abstract The paper proves a predicate version of Solovay's well-known theorem on provability interpretations of modal logic: If a closed modal predicate-logical formula R is not valid in some finite Kripke model, then there exists an arithmetical interpretation f such that PA ⊬ fR. This result implies the arithmetical completeness of arithmetically correct modal predicate logics with the finite model property (including the one-variable fragments of QGL and QS). The proof was obtained by adding “the predicate part” as a specific addition to the standard Solovay construction.