pith. sign in

arxiv: 2605.15732 · v1 · pith:ARN4Z42Dnew · submitted 2026-05-15 · 💻 cs.LO

Cut-Elimination for the Bimodal Logic GR

Hirohiko Kushida This is my paper

Pith reviewed 2026-05-19 19:03 UTC · model grok-4.3

classification 💻 cs.LO
keywords hypersequent calculusbimodal logiccut-eliminationprovability logicGödel predicateRosser predicateGR logic
0
0 comments X

The pith

A hypersequent calculus for the bimodal logic GR admits cut-elimination.

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

The paper introduces a hypersequent calculus designed specifically for the bimodal logic GR. One modality captures Gödel's provability predicate and the other captures Rosser's. The authors establish that this calculus satisfies the cut-elimination theorem, so every derivable sequent possesses a proof that avoids the cut rule. A reader would care because cut-free systems in provability logics often yield clearer connections to arithmetic and support more effective proof search. The work therefore supplies a proof-theoretic framework that directly encodes the interaction of these two predicates.

Core claim

The paper presents a hypersequent calculus for bimodal logic GR, where the two modalities represent the arithmetic provability predicates of Gödel and Rosser, respectively, and proves the cut-elimination theorem for the calculus.

What carries the argument

The hypersequent calculus with dedicated rules for the Gödel and Rosser modalities that together encode the axioms of GR.

If this is right

  • Every theorem of GR possesses a cut-free hypersequent derivation.
  • The calculus supplies a syntactic method for establishing properties of combined provability predicates.
  • Cut-free proofs become available for analyzing the interaction between Gödel and Rosser modalities in arithmetic.
  • The system offers a basis for studying interpolation or other structural properties in this bimodal setting.

Where Pith is reading between the lines

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

  • The same hypersequent style might be adapted to other pairs of provability predicates that satisfy similar interaction axioms.
  • Cut-free derivations could be used to extract explicit realizers or bounds when the logic is interpreted back in arithmetic.
  • The framework may help compare the proof-theoretic strength of GR with single-modality provability logics.

Load-bearing premise

The hypersequent rules correctly capture the axioms and semantics of the bimodal logic GR without introducing extraneous theorems or failing to derive the intended provability statements.

What would settle it

A concrete counterexample would be a sequent that is provable in GR yet possesses no cut-free derivation in the given hypersequent calculus.

read the original abstract

In this paper, we present a hypersequent calculus for bimodal logic GR, where the two modalities represent the arithmetic provability predicates of Goedel and Rosser, respectively. We prove the cut-elimination theorem for the calculus.

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 presents a hypersequent calculus for the bimodal logic GR, with modalities corresponding to the Gödel and Rosser provability predicates from arithmetic. The main result is a syntactic proof of the cut-elimination theorem for this calculus.

Significance. If the cut-elimination result holds, the work supplies a proof-theoretic tool for analyzing the bimodal logic GR without appeal to semantic completeness. The purely syntactic induction on derivation height and cut-rank aligns with standard methods for hypersequent modal systems and avoids circularity with the logic's axioms.

minor comments (2)
  1. The definition of the hypersequent rules for the Rosser modality (likely in §3) would benefit from an explicit example derivation showing how the rules capture the intended arithmetic interpretation without overgeneration.
  2. In the cut-elimination proof, the base case for atomic cuts could be expanded with a short diagram or case breakdown to improve readability for readers unfamiliar with hypersequent calculi.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our work on the hypersequent calculus for bimodal logic GR and the syntactic cut-elimination proof, as well as for the recommendation of minor revision. The assessment of significance aligns with our goals of providing a proof-theoretic tool without semantic completeness.

Circularity Check

0 steps flagged

No circularity: syntactic cut-elimination stands independently of rule choice

full rationale

The paper introduces a hypersequent calculus whose rules are explicitly designed to encode the axioms of bimodal GR (Gödel-Rosser provability), then proves cut-elimination separately by induction on derivation height and cut-rank. This induction is a standard syntactic argument that does not presuppose the target theorem, invoke self-citations for uniqueness, or reduce the result to a fitted parameter or renamed input. No load-bearing step collapses by construction; the calculus definition and the cut-elimination theorem remain distinct.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper relies on background notions of hypersequent calculi and the standard interpretation of Gödel and Rosser predicates; without the full text the precise axioms and any free parameters remain unspecified.

axioms (1)
  • standard math Standard definition and properties of hypersequent calculi for modal logics
    Invoked as the framework into which the new rules for GR are placed.

pith-pipeline@v0.9.0 · 5541 in / 1224 out tokens · 58640 ms · 2026-05-19T19:03:59.400725+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

18 extracted references · 18 canonical work pages

  1. [1]

    Artemov and L.D

    S.N. Artemov and L.D. Beklemishev, PROVABILITY LOGIC, Handbook of Philosophical Logic, D. Gabbay and F. Guenthner (eds.), Volume 10, pp. 189-360, 2002, Kluwer Academic Publishers

    work page 2002

  2. [2]

    Boolos,The Logic of Provability, Cambridge University Press, 1993

    G. Boolos,The Logic of Provability, Cambridge University Press, 1993

    work page 1993

  3. [3]

    Buss, An Introduction to Proof Theory.Handbook of Proof Theory, Elsevier Science, pp

    S. Buss, An Introduction to Proof Theory.Handbook of Proof Theory, Elsevier Science, pp. 1-78, 1998

    work page 1998

  4. [4]

    Guaspari, and R

    D. Guaspari, and R. M. Solovay, Rosser sentences,Annals of Mathematical Logic, vol. 16 (1979), pp. 81-99

    work page 1979

  5. [5]

    Kashima, T

    R. Kashima, T. Kurahashi, S. Iwata, and S. Morioka, Cut-free Sequent Calculi for the Provability Logic D,The Review of Symbolic Logic.Published online 2025:1-22. doi:10.1017/S1755020325000036 42

    work page doi:10.1017/s1755020325000036 2025

  6. [6]

    Kogure and T

    H. Kogure and T. Kurahashi, Interpolation properties for the bimodal provability logic, to appear inStudia Logica

    work page

  7. [7]

    G. Kreisel, Ordinal logics and the characterization of informal concept of proof,Proceedings of the International Congress of Mathematicians, 14-21 August 1958, Cambridge at the University Press, 1960, pp. 289-299

    work page 1958

  8. [8]

    Kurahashi, Rosser Provability and Normal Modal Logics.Studia Logica 108, 597-617 (2020)

    T. Kurahashi, Rosser Provability and Normal Modal Logics.Studia Logica 108, 597-617 (2020)

    work page 2020

  9. [9]

    Kurahashi, Rosser provability and the second incompleteness theorem In: Arai T., Kikuchi M., Kuroda S., Okada M., Yorioka T

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

    work page 2018

  10. [10]

    Kushida, A Proof Theory for the Logic of Provability in True Arithmetic

    H. Kushida, A Proof Theory for the Logic of Provability in True Arithmetic. Studia Logica, 108 (4):857-875

    work page

  11. [11]

    Kushida, Topdown Cut-Elimination,Report of Japan Coast Guard Academy, vol.66, no.1 and 2 (Consecutive no

    H. Kushida, Topdown Cut-Elimination,Report of Japan Coast Guard Academy, vol.66, no.1 and 2 (Consecutive no. 89), Part II (The Science and Engineering Section), Japan Coast Guard Academy, pp. 1-8, 2024

    work page 2024

  12. [12]

    Kushida, A Proof-Theoretic Study of Modal Logic,submitted, 2025

    H. Kushida, A Proof-Theoretic Study of Modal Logic,submitted, 2025

    work page 2025

  13. [13]

    Rosser, Extensions of some theorems of G¨odel and Church.The Journal of Symbolic Logic, 1(3):87-91, 1936

    J.B. Rosser, Extensions of some theorems of G¨odel and Church.The Journal of Symbolic Logic, 1(3):87-91, 1936

    work page 1936

  14. [14]

    Shavrukov, On Rosser’s Provability Predicate,Mathematical Logic Quarterly, vol

    V .Y. Shavrukov, On Rosser’s Provability Predicate,Mathematical Logic Quarterly, vol. 37(4), pp. 317-330, 1991

    work page 1991

  15. [15]

    Sidon, Craig interpolation property in modal logics with provability interpretation, inLogical Foundations of Computer Science (St

    T. Sidon, Craig interpolation property in modal logics with provability interpretation, inLogical Foundations of Computer Science (St. Petersburg, 1994), vol. 813 of Lecture Notes in Computer Science, Springer, Berlin, 1994, pp. 329-340

    work page 1994

  16. [16]

    Smorynski,Self-Reference and Modal Logic, Springer-Verlag, Berlin, 1985

    C. Smorynski,Self-Reference and Modal Logic, Springer-Verlag, Berlin, 1985

    work page 1985

  17. [17]

    R. M. Solovay, Provability interpretation of modal logic,Israel Journal of Mathematics, vol. 25 pp. 287-304, 1976

    work page 1976

  18. [18]

    A. Visser. Peano’s smart children: A provability logical study of systems with built-in consistency.Notre Dame Journal of Formal Logic, 30(2):161-196, 1989. 43

    work page 1989