pith. sign in

arxiv: 2605.12351 · v2 · submitted 2026-05-12 · 🧮 math.LO

Proof Theory for Bimodal Provability Logics

Borja Sierra Miranda , Thomas Studer This is my paper

Pith reviewed 2026-05-15 05:02 UTC · model grok-4.3

classification 🧮 math.LO
keywords sequent calculusbimodal provability logiccut-eliminationinterpolationnon-wellfounded proofsmodal logicprovability logic
0
0 comments X

The pith

Non-labelled sequent calculi are defined for the bimodal provability logics CS, CSM and ER.

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

The paper supplies the first sequent calculi for these logics that operate without labels while using ordinary provability predicates. It introduces concrete systems for CS, CSM and ER, then supplies non-wellfounded variants of the calculi to obtain cut-elimination. The same calculi are used to prove that each logic satisfies the uniform Lyndon interpolation property. A reader would care because these results give direct syntactic access to properties of provability that previously required labelled or semantic methods.

Core claim

We introduce the first non-labelled sequent calculi for the bimodal provability logics CS, CSM and ER with usual provability predicates. We also present non-wellfounded versions of the calculi and use them to establish cut-elimination. Finally we prove that the logics enjoy the uniform Lyndon interpolation property.

What carries the argument

Non-labelled sequent calculi whose rules directly encode the interaction of two provability predicates without external annotations.

If this is right

  • Cut-elimination holds for the calculi once their non-wellfounded versions are admitted.
  • Uniform Lyndon interpolation is established for CS, CSM and ER.
  • The calculi supply a syntactic basis for further investigations of provability interactions in these logics.

Where Pith is reading between the lines

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

  • The same non-labelled style may extend to other multimodal provability logics.
  • The calculi could support the design of proof-search or decision procedures for the logics.
  • Comparisons with labelled systems might yield translations that preserve cut-free derivations.

Load-bearing premise

That the standard sequent-calculus rules can be adapted directly to these bimodal systems without labels while still capturing the intended provability predicates.

What would settle it

A concrete sequent that is valid in one of the logics CS, CSM or ER but not derivable in the corresponding calculus, or a cut that cannot be eliminated in the non-wellfounded system.

Figures

Figures reproduced from arXiv: 2605.12351 by Borja Sierra Miranda, Thomas Studer.

Figure 1
Figure 1. Figure 1: Structure of proofs in local progress calculi [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Propositional rules ⊡𝑖 Σ𝑖 ,◻𝑖 Σ𝑖 ,◻𝑖 𝜙 ⇒ 𝜙 ◻CS ◻ 𝑖 𝑖 Σ𝑖 ,◻𝑖 Σ𝑖 , Γ ⇒ ◻𝑖 𝜙, Δ ⊡0 Σ0,◻1 Σ1,◻0 𝜙 ⇒ 𝜙 ◻CSM ◻ 0 0 Σ0,◻1 Σ1, Γ ⇒ ◻𝑖 𝜙, Δ ⊡0 Σ0,⊡1 Σ1,◻1 𝜙 ⇒ 𝜙 ◻CSM ◻ 1 0 Σ0,◻1 Σ1, Γ ⇒ ◻𝑖 𝜙, Δ [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Modal rules for GCS and GCSM 3.1 CS and CSM A sequent is a pair (Γ, Δ) of finite multisets of formulas, usually denoted by Γ ⇒ Δ. Γ is called the left side of the sequent while Δ is called the right side. Given a multisets of formulas Γ, we write Γ 𝑠 to mean the set ob￾tained by deleting repetitions from Γ. If Σ is a multiset {𝜙1, . . . , 𝜙𝑛}, then◻𝑖 Σ stands for {◻𝑖 𝜙1, . . . ,◻𝑖 𝜙𝑛} where 𝑖 ∈ {0, 1}. Mor… view at source ↗
Figure 4
Figure 4. Figure 4: Structural rules together the structural properties of GCS and GCSM which are easy to show, all of them by induction on the height of the proof (using Theorem 2.16 when necessary). Lemma 3.3. In GCS, GCSM, GCS + Cut and GCSM + Cut we have the following. 1. (Wk) is eliminable and admissible preserving height and rules. 2. (⊥R), (→L) and (→R) are invertible preserving height and rules. 3. (Ctr) is eliminable… view at source ↗
Figure 5
Figure 5. Figure 5: Propositional rules for ER ⊡𝑖 Σ𝑖 ,◻𝑖 Σ𝑖 ,◻𝑖 𝜙 ⇒𝑖 𝜙 ◻ER ◻ 𝑖 𝑖 Σ𝑖 ,◻𝑖 Σ𝑖 , Γ ≫ ◻𝑖 𝜙, Δ ⊡0 𝜙, Γ ⇒1 Δ ER1,0 ◻0 𝜙, Γ ⇒1 Δ [PITH_FULL_IMAGE:figures/full_fig_p011_5.png] view at source ↗
Figure 7
Figure 7. Figure 7: Structural rules In the following lemma, we put together some structural properties of GER (see [PITH_FULL_IMAGE:figures/full_fig_p012_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Non-wellfounded rules 4 Cut elimination The methodology that we will use to show cut elimination for GCS, GCSM and GER will be local progress proof theory. The advantage of this approach is that the calculi do not have diagonal formulas, which greatly simplifies the inductive measure needed in the cut elimination procedure. In particular, contrary to the original proof [43], this cut elimination does not n… view at source ↗
Figure 9
Figure 9. Figure 9: Interpolation template rules for CS 5.1 Uniform Lyndon Interpolation for CS and CSM We start by defining the notion of interpolation template for CS. Notice that, even if it is based on an non￾wellfounded system, we need the interpolation template to be a finite object, i.e., a cyclic proof and not any non-wellfounded proof. Otherwise, the construction of the interpolant would be hard if not impossible. De… view at source ↗
Figure 10
Figure 10. Figure 10: Interpolation template rules for ER A sequent Γ ⇒𝑖 Δ is said to be saturated if every 𝜙 ∈ Γ is left-saturated in Γ ⇒𝑖 Δ and every 𝜓 ∈ Δ is right-saturated in Γ ⇒𝑖 Δ. We define the saturation complexity of a sequent Γ ⇒𝑖 Δ, denoted |Γ ⇒𝑖 Δ|Sat, as the number ∑︁ ({|𝜙| | 𝜙 ∈ Γ, 𝜙 not left-saturated in Γ ⇒𝑖 Δ} ∪ {|𝜙| | 𝜙 ∈ Δ, 𝜙 not right-saturated in Γ ⇒𝑖 Δ}) . ■ Notice that if (𝑆0, . . . , 𝑆𝑛−1, 𝑆) is an ins… view at source ↗
read the original abstract

We provide the first (non-labelled) sequent calculi for bimodal provability logics with "usual" provability predicates. In particular, we introduce calculi for the logics CS, CSM and ER. Additionally, we present non-wellfounded versions of our calculi, and use them to establish a cut-elimination procedure. Finally, we prove the first interpolation results for these logics showing that they all enjoy the uniform Lyndon interpolation property.

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 / 1 minor

Summary. The paper constructs the first non-labelled sequent calculi for the bimodal provability logics CS, CSM and ER by adapting standard sequent rules to the usual provability predicates. It develops non-wellfounded variants of these calculi to obtain a cut-elimination theorem and proves that all three logics satisfy the uniform Lyndon interpolation property.

Significance. If the constructions and proofs are correct, the results supply the first standard (non-labelled) proof systems for these logics together with cut-elimination and interpolation, which are foundational metatheoretic tools. These contributions are likely to support further work on automated reasoning, proof search and model-theoretic investigations in provability logic.

minor comments (1)
  1. [Abstract] The abstract states the main results but does not indicate the key technical devices (e.g., the precise form of the modal rules or the side conditions used in the non-wellfounded calculi); a single sentence summarising these devices would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive assessment and recommendation to accept the manuscript. The referee's summary accurately captures the main contributions regarding the first non-labelled sequent calculi for CS, CSM, and ER, along with cut-elimination via non-wellfounded variants and the uniform Lyndon interpolation results.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper constructs non-labelled sequent calculi for the bimodal logics CS, CSM and ER by direct adaptation of standard sequent rules to the bimodal modalities with usual provability predicates. Cut-elimination is obtained via separate non-wellfounded variants of those calculi, and uniform Lyndon interpolation is proved independently. None of these steps reduce by definition, by fitted parameters renamed as predictions, or by load-bearing self-citation chains; each component is an independent construction whose soundness and completeness rest on explicit inductive arguments rather than re-deriving the input assumptions. The manuscript is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard background from proof theory and modal logic; no free parameters or invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard sequent calculus rules and properties of modal provability predicates hold as in prior literature
    The constructions build directly on established techniques for sequent systems in modal logic.

pith-pipeline@v0.9.0 · 5355 in / 1275 out tokens · 47379 ms · 2026-05-15T05:02:46.808821+00:00 · methodology

Review history (2 revisions) →

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

46 extracted references · 46 canonical work pages

  1. [1]

    Afshari, G

    B. Afshari, G. E. Leigh, and G. Menéndez Turata. Uniform interpolation from cyclic proofs: The case of modal mu-calculus. InAutomated Reasoning with Analytic Tableaux and Related Methods: 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6–9, 2021, Proceedings, Berlin, Heidelberg, 2021. Springer-Verlag

    work page 2021

  2. [2]

    Afshari, G

    B. Afshari, G. E. Leigh, and G. Menéndez Turata. A cyclic proof system for full computation tree logic. In B. Klin and E. Pimentel, editors,31st EACSL Annual Conference on Computer Science Logic (CSL 2023), volume 252 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl – Leibniz-Zentrum fü...

    work page 2023

  3. [3]

    Afshari, L

    B. Afshari, L. Grotenhuis G. E. Leigh, and L. Zenger. Ill-founded proof systems for intuitionistic linear- time temporal logic. In R. Ramanayake and J. Urban, editors,Automated Reasoning with Analytic Tableaux and Related Methods, pages 223–241, Cham, 2023. Springer Nature Switzerland

    work page 2023

  4. [4]

    Baelde, A

    D. Baelde, A. Doumane, and A. Saurin. Infinitary proof theory: the multiplicative additive case. In Annual Conference for Computer Science Logic, 2016

    work page 2016

  5. [5]

    A non-wellfounded and labelled sequent calculus for bimodal provability logic, 2025

    Justus Becker. A non-wellfounded and labelled sequent calculus for bimodal provability logic, 2025

    work page 2025

  6. [6]

    Springer Berlin Heidelberg, Berlin, Heidelberg, 1984

    Hans Bekić.Definable operations in general algebras, and the theory of automata and flowcharts, pages 30–55. Springer Berlin Heidelberg, Berlin, Heidelberg, 1984

    work page 1984

  7. [7]

    Beklemishev

    Lev D. Beklemishev. On bimodal logics of provability.Annals of Pure and Applied Logic, 68(2):115–159, 1994

    work page 1994

  8. [8]

    Beklemishev

    Lev D. Beklemishev. Bimodal logics for extensions of arithmetical theories.Journal of Symbolic Logic, 61(1):91–124, 1996

    work page 1996

  9. [9]

    G. Boolos. On systems of modal logic with provability interpretations.Theoria, 46:7–18, 2008

    work page 2008

  10. [10]

    Borzechowski, M

    M. Borzechowski, M. Gattinger, H. H. Hansen, R. Ramanayake, V. Trucco Dalmas, and Y. Venema. Propositional dynamic logic has Craig interpolation: a tableau-based proof, 2025

    work page 2025

  11. [11]

    Cut elimination for GLS using the terminability of its regress process.Journal of Philosophical Logic, 45, 03 2015

    Jude Brighton. Cut elimination for GLS using the terminability of its regress process.Journal of Philosophical Logic, 45, 03 2015

    work page 2015

  12. [12]

    Brotherston and A

    J. Brotherston and A. Simpson. Complete sequent calculi for induction and infinite descent. In22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pages 51–62, 2007

    work page 2007

  13. [13]

    Bucheli, R

    S. Bucheli, R. Kuznets, and Thomas Studer. Two ways to common knowledge.Electronic Notes in Theoretical Computer Science, 262:83–98, 2010. Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)

    work page 2010

  14. [14]

    Timothy J. Carlson. Modal logics with several operators and provability interpretations.Israel Journal of Mathematics, 54:14–24, 1986

    work page 1986

  15. [15]

    Beklemishev

    Lev D. Beklemishev. Normalization of deductions and interpolation for some logics of provability. Russian Math. Surveys, 42(6):223–224, 1987

    work page 1987

  16. [16]

    Das and D

    A. Das and D. Pous. Non-wellfounded proof theory for (kleene+action)(algebras+lattices). In D. R. Ghica and A. Jung, editors,27th EACSL Annual Conference on Computer Science Logic, CSL 2018, Birmingham, UK, September 4-7, 2018, volume 119 ofLIPIcs, pages 19:1–19:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018

    work page 2018

  17. [17]

    On the proof of solovay’s theorem.Studia Logica: An International Journal for Symbolic Logic, 50(1):51–69, 1991

    Dick de Jongh, Marc Jumelet, and Franco Montagna. On the proof of solovay’s theorem.Studia Logica: An International Journal for Symbolic Logic, 50(1):51–69, 1991

    work page 1991

  18. [18]

    Cam- bridge Tracts in Theoretical Computer Science

    Stéphane Demri, Valentin Goranko, and Martin Lange.The Modal Mu-Calculus, page 271–328. Cam- bridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016

    work page 2016

  19. [19]

    Untersuchungen über das logische Schließen I.Mathematische Zeitschrift, 39:176– 210, 1935

    Gerhard Gentzen. Untersuchungen über das logische Schließen I.Mathematische Zeitschrift, 39:176– 210, 1935

    work page 1935

  20. [20]

    Cut-elimination for provability logic by ter- minating proof-search: Formalised and deconstructed using Coq

    Rajeev Goré, Revantha Ramanayake, and Ian Shillito. Cut-elimination for provability logic by ter- minating proof-search: Formalised and deconstructed using Coq. In Anupam Das and Sara Negri, editors,Automated Reasoning with Analytic Tableaux and Related Methods, pages 299–313, Cham,

    work page

  21. [21]

    Springer International Publishing. 41

    work page

  22. [22]

    Non-wellfounded proof theory for inter- pretability logic

    Sebastijan Horvat, Borja Sierra Miranda, and Thomas Studer. Non-wellfounded proof theory for inter- pretability logic. InAutomated Reasoning with Analytic Tableaux and Related Methods: 34th Interna- tional Conference, TABLEAUX 2025, Reykjavik, Iceland, September 27–29, 2025, Proceedings, Berlin, Heidelberg, 2025. Springer-Verlag

    work page 2025

  23. [23]

    Uniform interpolation for interpretabil- ity logic, 2025

    Sebastijan Horvat, Borja Sierra Miranda, and Thomas Studer. Uniform interpolation for interpretabil- ity logic, 2025. arXiv:2511.01428

    work page arXiv 2025

  24. [24]

    The logic of provability

    Giorgi Japaridze and Dick de Jongh. The logic of provability. In Samuel R. Buss, editor,Handbook of Proof Theory, volume 137 ofStudies in Logic and the Foundations of Mathematics, pages 475–546. Elsevier, 1998

    work page 1998

  25. [25]

    Kloibhofer, V

    J. Kloibhofer, V. Trucco Dalmas, and Y. Venema. Interpolation for converse PDL. In G. L. Pozzato and T. Uustalu, editors,Automated Reasoning with Analytic Tableaux and Related Methods, pages 258–277, Cham, 2026. Springer Nature Switzerland

    work page 2026

  26. [26]

    Cyclic proofs for linear temporal logic

    Ioannis Kokkinis and Thomas Studer. Cyclic proofs for linear temporal logic. In Dieter Probst and Peter Schuster, editors,Concepts of Proof in Mathematics, Philosophy, and Computer Science, pages 171–192, Berlin, Boston, 2016. De Gruyter

    work page 2016

  27. [27]

    Uniform Lyndon interpolation property in propositional modal logics.Arch

    Taishi Kurahashi. Uniform Lyndon interpolation property in propositional modal logics.Arch. Math. Log., 59(5-6):659–678, 2020

    work page 2020

  28. [28]

    H. Kushida. A proof theory for the logic of provability in true arithmetic.Studia Logica, 108, 2020

    work page 2020

  29. [29]

    Note on some fixed point constructions in provability logic.J Philos Logic, 35:225–230, 2006

    Per Lindström. Note on some fixed point constructions in provability logic.J Philos Logic, 35:225–230, 2006

    work page 2006

  30. [30]

    Springer, 1955

    Paul Lorenzen.Einführung in die operative Logik und Mathematik. Springer, 1955

    work page 1955

  31. [31]

    Provability in finite subtheories of PA and relative interpretability: A modal inves- tigation.The Journal of Symbolic Logic, 52(2):494–511, 1987

    Franco Montagna. Provability in finite subtheories of PA and relative interpretability: A modal inves- tigation.The Journal of Symbolic Logic, 52(2):494–511, 1987

    work page 1987

  32. [32]

    Elsevier, 1997

    Vladimir Rybakov.Admissibility of Logical Inference Rules. Elsevier, 1997

    work page 1997

  33. [33]

    Non-well-founded proofs for the Grzegorczyk modal logic.The Review of Symbolic Logic, 14(1), 2021

    Yuri Savateev and Daniyar Shamkanov. Non-well-founded proofs for the Grzegorczyk modal logic.The Review of Symbolic Logic, 14(1), 2021

    work page 2021

  34. [34]

    Cut elimination for the weak modal Grzegorczyk logic via non-well-founded proofs

    Yury Savateev and Daniyar Shamkanov. Cut elimination for the weak modal Grzegorczyk logic via non-well-founded proofs. In Rosalie Iemhoff, Michael Moortgat, and Ruy de Queiroz, editors,Logic, Language, Information, and Computation, pages 569–583. Springer, 2019

    work page 2019

  35. [35]

    Springer, 1960

    Kurt Schütte.Beweistheorie. Springer, 1960

    work page 1960

  36. [36]

    Circular proofs for the Gödel-Löb provability logic.Mathematical Notes, 96, 2014

    Daniyar Shamkanov. Circular proofs for the Gödel-Löb provability logic.Mathematical Notes, 96, 2014

    work page 2014

  37. [37]

    Nested sequents for provability logic GLP.Logic Journal of the IGPL, 23(5):789– 815, 2015

    Daniyar Shamkanov. Nested sequents for provability logic GLP.Logic Journal of the IGPL, 23(5):789– 815, 2015

    work page 2015

  38. [38]

    Cut elimination for a non-wellfounded system for the master modality.Journal of Symbolic Logic, to appear

    Borja Sierra Miranda and Thomas Studer. Cut elimination for a non-wellfounded system for the master modality.Journal of Symbolic Logic, to appear. arXiv:2505.02700

    work page arXiv

  39. [39]

    Uniform Lyndon interpolation via non-wellfounded proofs

    Borja Sierra Miranda and Thomas Studer. Uniform Lyndon interpolation via non-wellfounded proofs. InAdvances in Modal Logic 2026, to appear

    work page 2026

  40. [40]

    Coalgebraic proof translations for non- wellfounded proofs

    Borja Sierra Miranda, Thomas Studer, and Lukas Zenger. Coalgebraic proof translations for non- wellfounded proofs. In A. Ciabattoni, D. Gabelaia, and I. Sedlár, editors,Advances in Modal Logic 2024, pages 527–548, 2024. 42

    work page 2024

  41. [41]

    Universitext

    Craig Smoryński.Self-Reference and Modal Logic. Universitext. Springer New York, NY, 1985

    work page 1985

  42. [42]

    R. M. Solovay. Provability interpretations of modal logic.Israel Journal of Mathematics, 25, 1976

    work page 1976

  43. [43]

    W. W. Tait. A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic.Bulletin of the American Mathematical Society, 72(6):980–983, 1966

    work page 1966

  44. [44]

    A proof of cut-elimination theorem in simple type-theory.Journal of the Mathe- matical Society of Japan, 19(4):399–410, 1967

    Moto-o Takahashi. A proof of cut-elimination theorem in simple type-theory.Journal of the Mathe- matical Society of Japan, 19(4):399–410, 1967

    work page 1967

  45. [45]

    The modal logic of provability: Cut-elimination.Journal of Philosophical Logic, 12(4):471–476, 1983

    Silvio Valentini. The modal logic of provability: Cut-elimination.Journal of Philosophical Logic, 12(4):471–476, 1983

    work page 1983

  46. [46]

    A course on bimodal provability logic.Annals of Pure and Applied Logic, 73(1):109–142, 1995

    Albert Visser. A course on bimodal provability logic.Annals of Pure and Applied Logic, 73(1):109–142, 1995. 43

    work page 1995