pith. sign in

arxiv: 2604.25780 · v1 · submitted 2026-04-28 · 🧮 math.LO

Finite Kripke models and provability interpretations in quantified modal logic

Haruka Kogure , Taishi Kurahashi This is my paper

Pith reviewed 2026-05-07 13:45 UTC · model grok-4.3

classification 🧮 math.LO
keywords quantified modal logicKripke modelsprovability predicatearithmetical interpretationfinite modelsarithmetical completenessFefermanian provability
0
0 comments X

The pith

Finite Kripke models of quantified modal logic embed into arithmetic via tailored provability predicates.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper constructs explicit arithmetical interpretations that realize finite Kripke models inside arithmetic for quantified modal logic. For conversely well-founded finite models it builds a Σ₂ Fefermanian provability predicate together with an embedding that preserves the modal accessibility relation and quantifier behavior. For finite constant-domain models it uses a Σ₁ provability predicate satisfying D2^G to achieve a similar embedding. A sympathetic reader would care because the constructions show that the truth of modal formulas at worlds in these models can be mirrored by statements about provability in arithmetic, extending earlier completeness techniques from the propositional case.

Core claim

For conversely well-founded finite Kripke models of quantified modal logic, the paper constructs a Σ₂ Fefermanian provability predicate together with an arithmetical interpretation that embeds the model into arithmetic. For finite constant domain Kripke models it constructs a Σ₁ provability predicate satisfying D2^G and an arithmetical interpretation that likewise embeds the model.

What carries the argument

Specially constructed provability predicates (a Σ₂ Fefermanian predicate in the conversely well-founded case and a Σ₁ predicate satisfying D2^G in the constant-domain case) that serve as the basis for arithmetical interpretations embedding the accessibility relation and domains of the Kripke models into arithmetic.

If this is right

  • Modal formulas true at a world in the Kripke model translate to arithmetic sentences that are provable under the constructed interpretation.
  • The embeddings establish a concrete form of arithmetical completeness for the two specified classes of finite models in quantified modal logic.
  • The constructions separate the conversely well-founded case, which requires Σ₂ complexity, from the constant-domain case, which admits Σ₁ complexity with the D2^G property.
  • Truth preservation holds for both the accessibility relation between worlds and the quantifier behavior over domains.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The separation of syntactic complexity between the two model classes suggests that further model restrictions might allow even simpler predicates.
  • If the embeddings are faithful, consistency statements for the modal theory can be read off from the corresponding arithmetic statements about the provability predicate.
  • The method supplies an explicit bridge that could be used to transfer questions about decidability of the modal logic to questions about the arithmetic theory generated by the predicate.

Load-bearing premise

The embedding techniques previously used for finite models in propositional modal logic can be adapted to the quantified setting while preserving the needed syntactic complexity and modal properties of the predicates.

What would settle it

Existence of a finite conversely well-founded Kripke model for which no Σ₂ Fefermanian provability predicate yields an arithmetical interpretation that correctly embeds the model's modal truths would falsify the central claim.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript adapts the finite-model embedding techniques of Artemov and Japaridze to quantified modal logic. For conversely well-founded finite Kripke models it constructs a Σ₂ Fefermanian provability predicate together with an arithmetical interpretation that embeds the model into arithmetic; for finite constant-domain Kripke models it constructs a Σ₁ provability predicate satisfying D2^G together with a corresponding arithmetical interpretation.

Significance. If the constructions are correct, the work extends arithmetical completeness results to two classes of finite Kripke models in the quantified setting while controlling the syntactic complexity of the provability predicates. This supplies explicit embeddings that realize the modal structures inside arithmetic and thereby strengthens the bridge between provability logic and quantified modal logic.

minor comments (2)
  1. The abstract asserts the existence of the constructions but supplies no outline of the key inductive steps or verification that the adapted predicates retain the required modal axioms and complexity bounds; a short paragraph sketching the main technical moves would improve readability.
  2. Notation for the arithmetical interpretations and the precise definition of the Fefermanian predicate should be introduced with a dedicated preliminary subsection to avoid forward references in the main constructions.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the concise summary of our results on arithmetical embeddings for finite Kripke models in quantified modal logic and for the recommendation of minor revision. No specific major comments appear in the report, so there are no individual points requiring point-by-point rebuttal or clarification at present.

Circularity Check

0 steps flagged

No significant circularity in the derivation chain

full rationale

The paper presents explicit constructions adapting the finite-model embedding techniques of Artemov and Japaridze (external authors) to two classes of finite Kripke models in quantified modal logic, yielding Σ₂ Fefermanian and Σ₁ (D2^G-satisfying) provability predicates together with arithmetical interpretations. No equations, definitions, or steps in the abstract or described results reduce these predicates or embeddings to fitted parameters, self-referential inputs, or self-citation chains by construction. The cited techniques supply independent support, rendering the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on the successful adaptation of prior embedding techniques; no free parameters, invented entities, or additional axioms are introduced in the abstract.

axioms (1)
  • domain assumption Finite-model embedding techniques of Artemov and Japaridze transfer to quantified modal logic while preserving the required predicate complexity and modal axioms.
    Invoked to justify the existence of the constructed predicates.

pith-pipeline@v0.9.0 · 5410 in / 1199 out tokens · 66595 ms · 2026-05-07T13:45:48.584802+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

27 extracted references · 27 canonical work pages

  1. [1]

    Artemov, Sergei N. (1985). Nonarithmeticity of truth predicate logics of provability.Doklady Akademii Nauk SSSR, 284(2), 270–271

    work page 1985

  2. [2]

    Artemov, Sergei N. (1986). Numerically correct logics of provability.Dok- lady Akademii Nauk SSSR, 290(6), 1289–1292

    work page 1986

  3. [3]

    and Beklemishev, Lev D

    Artemov, Sergei N. and Beklemishev, Lev D. (2005). Provability Logic. In: D. Gabbay and F. Guenthner (eds.),Handbook of Philosophical Logic, 2nd edition, vol.13, Springer, Dordrecht, 189–360

    work page 2005

  4. [4]

    and Dzhaparidze, Giorgie

    Artemov, Sergei N. and Dzhaparidze, Giorgie. (1990). Finite Kripke mod- els and predicate logics of provability.The Journal of Symbolic Logic, 55(3), 1090–1098

    work page 1990

  5. [5]

    Beklemishev, Lev D. (1990). On the classification of propositional prov- ability logics.Mathematics of the USSR. Izvestiya, 35(2), 247–275

    work page 1990

  6. [6]

    Berarducci, Alessandro. (1989). Σ 0 n-interpretations of modal logic.Bollet- tino dell’Unione Matematica Italiana. Serie VII. A, 3(2), 177–184

    work page 1989

  7. [7]

    Boolos, George and McGee, Vann. (1987). The degree of the set of sen- tences of predicate provability logic that are true under every interpreta- tion.The Journal of Symbolic Logic, 52(1), 165–171

    work page 1987

  8. [8]

    Dzhaparidze, Giorgie. (1990). Decidable and enumerable predicate logics of provability.Studia Logica, 49(1), 7–21

    work page 1990

  9. [9]

    (2001).A mathematical introduction to logic, 2nd edition, Harcourt/Academic Press, San Diego

    Enderton, Herbert B. (2001).A mathematical introduction to logic, 2nd edition, Harcourt/Academic Press, San Diego

    work page 2001

  10. [10]

    Feferman, Solomon. (1960). Arithmetization of metamathematics in a gen- eral setting.Fundamenta Mathematicae, 49, 35–92

    work page 1960

  11. [11]

    (1998).First-order modal logic, Synthese Library, 277, Dordrecht: Kluwer Academic Publishers Group

    Fitting, Melvin and Mendelsohn, Richard L. (1998).First-order modal logic, Synthese Library, 277, Dordrecht: Kluwer Academic Publishers Group

    work page 1998

  12. [12]

    Guaspari, David and Solovay, Robert M. (1979). Rosser sentences.Annals of Mathematical Logic, 16, 81–99

    work page 1979

  13. [13]

    Japaridze, Giorgi and de Jongh, Dick. (1998). The logic of provability. In: Handbook of proof theory, Elsevier, Amsterdam, 475–546

    work page 1998

  14. [14]

    Kogure, Haruka and Kurahashi, Taishi. (2025). Modal logical aspects of provability predicates and consistency statements. arXiv preprint, arXiv:2511.15531

    work page arXiv 2025

  15. [15]

    Kurahashi, Taishi. (2013). On predicate provability logics and binumera- tions of fragments of Peano arithmetic.Archive for Mathematical Logic, 52(7-8), 871–880. 21

    work page 2013

  16. [16]

    Kurahashi, Taishi. (2018). Arithmetical completeness theorem for modal logicK.Studia Logica, 106(2), 219–235

    work page 2018

  17. [17]

    Kurahashi, Taishi. (2020). A note on derivability conditions.The Journal of Symbolic Logic, 85(3), 1224–1253

    work page 2020

  18. [18]

    Kurahashi, Taishi. (2021). Rosser provability and the second incomplete- ness theorem. In: T. Arai, M. Kikuchi, S. Kuroda, M. Okada, T. Yorioka (eds),Advances in Mathematical Logic. SAML 2018, Springer Proceedings in Mathematics & Statistics, vol.369, Springer, Singapore, 77–97

    work page 2021

  19. [19]

    Kurahashi, Taishi. (2022). On inclusions between quantified provability logics.Studia Logica, 110(1), 165–188

    work page 2022

  20. [20]

    Kurahashi, Taishi. (2024). The provability logic of all provability predi- cates.Journal of Logic and Computation, 34(6), 1108–1135

    work page 2024

  21. [21]

    Kurahashi, Taishi. (2025). Refinements of provability and consistency principles for the second incompleteness theorem. arXiv preprint, arXiv:2507.00955

    work page arXiv 2025

  22. [22]

    McGee, Vann. (1994). On the degrees of unsolvability of modal predicate logics of provability.The Journal of Symbolic Logic, 59(1), 253–261

    work page 1994

  23. [23]

    Montagna, Franco. (1984). The predicate modal logic of provability.Notre Dame Journal of Formal Logic, 25(2), 179–189

    work page 1984

  24. [24]

    Solovay, Robert M. (1976). Provability interpretations of modal logic.Is- rael Journal of Mathematics, 25(3-4), 287–304

    work page 1976

  25. [25]

    Vardanyan, V. A. (1986). Arithmetic complexity of provability predicate logics and their fragments.Doklady Akademii Nauk SSSR, 288(1), 11–14

    work page 1986

  26. [26]

    j 22 is activated at stagel

    Wolter, Frank and Zakharyaschev, Michael (2001). Decidable fragments of first-order modal logics.The Journal of Symbolic Logic, 66(3), 1415–1438. Appendix: The primitive recursiveness of the func- tionh In this appendix, we prove the primitive recursiveness of the functionh(Propo- sition 4.5), whose proof was postponed in Section 4. We first show that whe...

    work page 2001

  27. [27]

    There are only finitely many equivalence relations onX, and their number is effectively bounded in terms ofl

    There exists a good equivalence relation∼onXsuch that ∀α, β∈X(α∼β⇐ ⇒α∼ ∗ β) . There are only finitely many equivalence relations onX, and their number is effectively bounded in terms ofl. Moreover, for each such equivalence relation, whether it is good can be decided in a primitive recursive way. Indeed, for a fixed equivalence relation∼, the formula in q...

    work page