pith. sign in

arxiv: 1907.03849 · v1 · pith:JLS4PS7Qnew · submitted 2019-07-08 · 🧮 math.LO

Interpretability logics and generalized Veltman semantics

Luka Mikec , Mladen Vukovi\'c This is my paper

Pith reviewed 2026-05-25 00:27 UTC · model grok-4.3

classification 🧮 math.LO
keywords interpretability logicsgeneralized Veltman semanticsmodal completenessILP0ILRsmart labelsdecidabilityfinite model property
0
0 comments X

The pith

ILP0 and ILR are modally complete with respect to generalized Veltman semantics.

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

The paper proves that the interpretability logics ILP0 and ILR are complete for generalized Veltman semantics, meaning a formula is provable in the logic exactly when it holds in every generalized Veltman model. The argument proceeds by showing how to build a countermodel from any unprovable formula using a labeling technique. The same method shortens existing completeness proofs for many other interpretability logics. As direct consequences the logics are decidable and enjoy the finite model property under the generalized semantics.

Core claim

The interpretability logics ILP_0 and ILR are modally complete with respect to generalized Veltman semantics. Proofs rely on smart (full) labels to construct models from consistent sets of formulas while preserving the required frame conditions. The same technique supplies shorter completeness arguments for many classical interpretability logics. Decidability and the finite model property follow immediately for ILP_0 and ILR, and a new construction is introduced that may support future completeness results for extensions of ILW.

What carries the argument

Smart (full) labels, which assign sets of formulas to nodes so that the generalized Veltman accessibility and interpretability relations are satisfied exactly when the labeling conditions hold.

If this is right

  • Validity in ILP0 and ILR is decidable under generalized Veltman semantics.
  • Both logics possess the finite model property with respect to generalized Veltman frames.
  • Several other interpretability logics receive shorter completeness proofs via the same labeling method.
  • A model-construction technique is available that may be applied to extensions of ILW in future work.

Where Pith is reading between the lines

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

  • Generalized Veltman semantics could serve as a common setting in which further interpretability logics receive uniform completeness and decidability results.
  • The smart-label construction might transfer to related modal systems whose frames involve multiple accessibility relations.
  • If the construction shown for ILW* succeeds more broadly, it could shorten proofs for additional members of the ILW family.

Load-bearing premise

The smart full labels method encodes precisely the conditions of generalized Veltman semantics and introduces no extra constraints that would block the completeness direction.

What would settle it

An explicit formula that is true in every generalized Veltman model yet unprovable in ILP0 would refute the completeness claim.

Figures

Figures reproduced from arXiv: 1907.03849 by Luka Mikec, Mladen Vukovi\'c.

Figure 1
Figure 1. Figure 1: Left: extending an ordinary Veltman model. Right: extend [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
read the original abstract

We obtain modal completeness of the interpretability logics ILP_0 and ILR w.r.t. generalized Veltman semantics. Our proofs are based on the notion of smart (full) labels. We also give shorter proofs of completeness w.r.t. generalized semantics for many classical interpretability logics. We obtain decidability and finite model property w.r.t. generalized semantics for ILP_0 and ILR. Finally, we develop a construction that might be useful for proofs of completeness of extensions of ILW w.r.t. generalized semantics in the future, and demonstrate its usage with ILW* = ILM_0W.

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 paper proves modal completeness of interpretability logics ILP_0 and ILR with respect to generalized Veltman semantics, using the technique of smart (full) labels. It also supplies shorter completeness proofs for many classical interpretability logics, establishes decidability and the finite model property for ILP_0 and ILR under generalized semantics, and introduces a construction (demonstrated on ILW* = ILM_0W) intended to support future completeness results for extensions of ILW.

Significance. If the completeness proofs hold, the results advance the model theory of interpretability logics by extending known completeness theorems to generalized Veltman frames and by supplying a reusable labeling technique. The decidability and finite-model-property corollaries are of independent computational interest, while the new construction for ILW-extensions may streamline subsequent work in the area.

minor comments (2)
  1. [Abstract and §1] The abstract and introduction use both “ILP0” and “ILP_0”; a uniform subscript notation should be adopted throughout.
  2. [Section on smart labels] The definition of “smart (full) labels” is introduced without an explicit comparison table to ordinary labels; adding such a table would clarify the technical innovation.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment and the recommendation to accept the manuscript. The report accurately summarizes the main contributions.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper presents modal completeness results for ILP0 and ILR with respect to generalized Veltman semantics via the introduction of smart (full) labels as a proof technique. No equations or derivations reduce results to self-defined quantities, fitted inputs, or renamings of prior outputs. Self-citations, if present, are not load-bearing for the central completeness claims, which rely on explicit semantic constructions and standard modal logic methods rather than imported uniqueness theorems or ansatzes from overlapping prior work. The proofs are self-contained against the target semantics without internal reduction to inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Pure logic paper; no numerical free parameters. Relies on standard modal axioms and the definition of generalized Veltman semantics (domain assumption). No invented entities.

axioms (2)
  • standard math Standard axioms and rules of interpretability logics (IL, ILM, etc.) as background
    Invoked throughout as the base systems whose extensions are studied.
  • domain assumption Generalized Veltman semantics correctly models interpretability
    Central to all completeness claims; assumed as the target semantics.

pith-pipeline@v0.9.0 · 5627 in / 1247 out tokens · 15347 ms · 2026-05-25T00:27:09.491479+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

  1. [1]

    Berarducci, The Interpretability Logic of Peano Arithmetic, Journal of Symbolic Logic , 55 (1990), 1059–1089

    A. Berarducci, The Interpretability Logic of Peano Arithmetic, Journal of Symbolic Logic , 55 (1990), 1059–1089

    work page 1990

  2. [2]

    Bilkova, E

    M. Bilkova, E. Goris, J. J. Joosten, Smart labels, In Liber Amicorum for Dick de Jongh , J. van Benthem et al. eds., Institute for Logic, Language and Computatio n, 2004

    work page 2004

  3. [3]

    D. H. J. de Jongh, F. Veltman, Provability logics for relative interp retability, In P. P. Petkov (ed.), Mathematical Logic, Proceedings of the 1988 Heyting Confer ence, pp. 31–42, Plenum Press, 1990

    work page 1988

  4. [4]

    D. H. J. de Jongh, F. Veltman, Modal completeness of ILW, In Essays dedicated to Johan van Benthem on the occasion of his 50th birthday , J. Gerbrandy et al. eds., Amsterdam University Press, 1999

    work page 1999

  5. [5]

    Goris, J

    E. Goris, J. J. Joosten, Modal matters in interpretability logics, Logic Journal of the IGPL , 16 (2008), 371–412

    work page 2008

  6. [6]

    Goris, J

    E. Goris, J. J. Joosten, A new principle in the interpretability logic o f all reasonable arith- metical theories, Logic Journal of the IGPL , 19 (2011), 1–17

    work page 2011

  7. [7]

    Mikec, T

    L. Mikec, T. Perkov, M. Vukovi´ c, Decidability of interpretability logics ILM0 and ILW∗ , Logic Journal of the IGPL , 25 (2017), 758–772

    work page 2017

  8. [8]

    Perkov, M

    T. Perkov, M. Vukovi´ c, Filtrations of generalized Veltman mode ls, Mathematical Logic Quar- terly, 62 (2016), 412–419 19

    work page 2016

  9. [9]

    V. Y. Shavrukov, The logic of relative interpretability over Peano arithmetic, Preprint, Steklov Mathematical Institute, Moscow , 1988. In Russian

    work page 1988

  10. [10]

    Visser, Interpretability logic, In Mathematical Logic, Proceedings of the 1988 Heyting Conference, P

    A. Visser, Interpretability logic, In Mathematical Logic, Proceedings of the 1988 Heyting Conference, P. P. Petkov (ed.), pp. 175–210. Plenum Press, 1990

    work page 1988

  11. [11]

    Visser, An overview of interpretability logic, In Advances in modal logic 1, M

    A. Visser, An overview of interpretability logic, In Advances in modal logic 1, M. Kracht et al. eds., pp. 307–359. CSLI Publications, 1998

    work page 1998

  12. [12]

    Vrgoˇ c, M

    D. Vrgoˇ c, M. Vukovi´ c, Bisimulations and bisimulation quotientsof generalized Veltman models, Logic Journal of the IGPL , 18 (2010), 870–880

    work page 2010

  13. [13]

    Vukovi´ c, The principles of interpretability,Notre Dame Journal of Formal Logic , 40 (1999), 227–235

    M. Vukovi´ c, The principles of interpretability,Notre Dame Journal of Formal Logic , 40 (1999), 227–235

    work page 1999

  14. [14]

    Vukovi´ c, Bisimulations between generalized Veltman models a nd Veltman models, Mathe- matical Logic Quarterly , 54 (2008), 368–373

    M. Vukovi´ c, Bisimulations between generalized Veltman models a nd Veltman models, Mathe- matical Logic Quarterly , 54 (2008), 368–373. 20

    work page 2008