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

Recognition: no theorem link

Proof Theory for Bimodal Provability Logics

Borja Sierra Miranda, Thomas Studer

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

classification 🧮 math.LO MSC 03F0503B45

keywords provability logicbimodal logicsequent calculuscut-eliminationLyndon interpolationCSCSMER

0 comments

The pith

Bimodal provability logics CS, CSM and ER now have non-labelled sequent calculi that prove uniform Lyndon interpolation.

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

The paper introduces the first sequent calculi for the bimodal provability logics CS, CSM, and ER that rely on usual provability predicates. Non-wellfounded extensions of these calculi are constructed specifically to establish cut-elimination. The work then proves that each of these logics satisfies the uniform Lyndon interpolation property. A sympathetic reader cares because the results supply concrete syntactic tools for reasoning about provability statements involving two modalities, rather than relying solely on semantic definitions.

Core claim

We provide the first non-labelled sequent calculi for the bimodal provability logics CS, CSM and ER. We present non-wellfounded versions of our calculi to establish a cut-elimination procedure. Finally, we prove that these logics enjoy the uniform Lyndon interpolation property.

What carries the argument

Non-labelled sequent calculi for bimodal provability logics with usual provability predicates, together with their non-wellfounded extensions that support cut-elimination.

If this is right

The logics CS, CSM and ER admit cut-free proofs through their non-wellfounded sequent calculi.
Uniform Lyndon interpolation holds for all three logics, preserving variable polarities in interpolants.
These calculi give a syntactic basis for studying proof properties in bimodal provability logics.
Cut-elimination and interpolation results apply uniformly across CS, CSM and ER.

Where Pith is reading between the lines

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

The calculi could be adapted to support proof search or decision procedures for statements involving two provability predicates.
Non-wellfounded techniques for cut-elimination may transfer to other modal logics that lack ordinary wellfounded derivations.
The interpolation property might imply further structural results, such as variable dependencies in arithmetic realizations of the logics.

Load-bearing premise

The sequent rules correctly encode the semantics of the usual provability predicates in CS, CSM and ER, and the non-wellfounded rules do not create new inconsistencies.

What would settle it

A sequent that is valid under the intended semantics of one of the logics but is not derivable in the corresponding calculus, or a counterexample to uniform Lyndon interpolation in CS, CSM or ER.

Figures

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

**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: 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 obtained by deleting repetitions from Γ. If Σ is a multiset {𝜙1, . . . , 𝜙𝑛}, then◻𝑖 Σ stands for {◻𝑖 𝜙1, . . . ,◻𝑖 𝜙𝑛} where 𝑖 ∈ {0, 1}. Mor… view at source ↗

**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: 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: 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: 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: 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 nonwellfounded 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: 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.

Desk Editor's Note private letter to a colleague

The paper supplies the first non-labelled sequent calculi for CS, CSM, and ER, plus cut-elimination via non-wellfounded proofs and uniform Lyndon interpolation.

read the letter

The main takeaway is that this paper introduces the first non-labelled sequent calculi for the three bimodal provability logics CS, CSM, and ER. It uses non-wellfounded versions of these calculi to prove cut-elimination and then establishes the uniform Lyndon interpolation property for each of them. The authors do a straightforward job laying out the rules for the calculi. They focus on capturing the standard provability predicates in a syntactic way, which avoids the complications that come with labelled systems in this domain. The non-wellfounded approach for cut-elimination is a solid choice here, as it allows them to handle the interactions between the two modalities without getting stuck on termination issues. The interpolation results build on that foundation and are presented as the first such theorems for these logics. The paper stays true to its claims without overreaching. The constructions are new and not reductions to prior systems. The proofs seem to rely on explicit rule applications and induction or similar methods adapted for the non-wellfounded case. No major gaps appear in the logic of the argument from what is described. A possible soft spot is verifying that every rule is semantically sound for the intended models of these logics, but the cut-elimination procedure likely serves as part of that justification. The work does not introduce any self-referential definitions that could lead to circularity. This paper is for researchers in proof theory, particularly those dealing with modal and provability logics. It provides practical syntactic tools and new theorems that could be built upon. If you work in sequent calculi or interpolation in logic, it is worth examining. It deserves a serious referee because it fills a documented gap with concrete, checkable contributions rather than vague semantic assertions.

Referee Report

2 major / 2 minor

Summary. The paper introduces the first non-labelled sequent calculi for the bimodal provability logics CS, CSM, and ER (with usual provability predicates). It defines non-wellfounded extensions of these calculi and uses them to prove cut-elimination. It further establishes the first interpolation theorems for these logics, specifically that they satisfy the uniform Lyndon interpolation property.

Significance. If the syntactic rules are shown to be sound and complete for the intended semantics and the cut-elimination and interpolation arguments go through, this constitutes a solid advance in the proof theory of provability logics. The explicit construction of non-labelled systems (rather than labelled ones) and the uniform Lyndon interpolation results are the main contributions; the non-wellfounded technique is a recognized tool in the field and is applied here to obtain cut-elimination without additional semantic machinery.

major comments (2)

§3 (sequent rules for CS/CSM/ER): the paper must explicitly verify that each modal rule preserves the intended fixed-point semantics of the usual provability predicates; without a direct soundness lemma relating the rules to the bimodal Kripke models or arithmetical interpretations, the claim that these are the 'first' adequate calculi remains provisional.
§4 (non-wellfounded cut-elimination): the argument that every infinite branch is 'progressing' (and therefore admissible) needs a precise measure or ordinal assignment; if the progress condition is only stated informally, the cut-elimination theorem does not yet follow from the standard non-wellfounded proof theory results cited.

minor comments (2)

Notation for the two modalities is introduced without a dedicated table; a small table listing the rules for □ and ◇ (or their bimodal counterparts) would improve readability.
The statement of uniform Lyndon interpolation in §5 should include an explicit definition of the polarity condition on the interpolant, as the term 'uniform' is used in several non-equivalent ways in the interpolation literature.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thorough review and valuable suggestions. We address the two major comments point by point below, indicating the revisions we will make to strengthen the manuscript.

read point-by-point responses

Referee: §3 (sequent rules for CS/CSM/ER): the paper must explicitly verify that each modal rule preserves the intended fixed-point semantics of the usual provability predicates; without a direct soundness lemma relating the rules to the bimodal Kripke models or arithmetical interpretations, the claim that these are the 'first' adequate calculi remains provisional.

Authors: We agree that an explicit soundness argument is required to substantiate the adequacy of the calculi. In the revised manuscript we will insert a new subsection in §3 that states and proves a direct soundness lemma for each modal rule. The lemma will relate the rules to the fixed-point semantics of the provability predicates and to the corresponding bimodal Kripke models, thereby confirming that the systems are sound for the intended interpretations. This addition will also support the claim that the calculi are the first non-labelled ones for CS, CSM and ER. revision: yes
Referee: §4 (non-wellfounded cut-elimination): the argument that every infinite branch is 'progressing' (and therefore admissible) needs a precise measure or ordinal assignment; if the progress condition is only stated informally, the cut-elimination theorem does not yet follow from the standard non-wellfounded proof theory results cited.

Authors: The referee correctly identifies that the progress condition must be made fully precise. Although the manuscript defines progressing branches via a decrease in a modal-depth measure, we will revise §4 to introduce an explicit ordinal assignment (based on the lexicographic order of formula complexity and modal nesting along each branch). We will then prove that every infinite branch is progressing if and only if the associated ordinal sequence is strictly decreasing, allowing a direct appeal to the cited non-wellfounded cut-elimination theorems. This formalization will be added without altering the overall proof strategy. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper defines new non-labelled sequent calculi for CS, CSM and ER from explicit syntactic rules, then proves cut-elimination via non-wellfounded extensions and uniform Lyndon interpolation directly from those rules. No step reduces a claimed result to a fitted parameter, self-referential definition, or load-bearing self-citation whose content is presupposed; the derivations are self-contained syntactic constructions whose adequacy is established by independent semantic and proof-theoretic arguments.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard background axioms of provability logic (such as the Hilbert-Bernays-Löb derivability conditions) and classical sequent calculus rules; no new free parameters or invented entities are introduced in the abstract. Full details of any additional assumptions would appear in the definitions of CS, CSM, and ER.

axioms (2)

domain assumption Standard Hilbert-Bernays-Löb conditions for provability predicates
Invoked implicitly when defining the 'usual' provability predicates for the bimodal logics.
standard math Classical sequent calculus rules for propositional connectives
Base system on which the modal rules are added.

pith-pipeline@v0.9.0 · 5355 in / 1361 out tokens · 47931 ms · 2026-05-13T02:42:14.952248+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

45 extracted references · 45 canonical work pages

[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]

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]

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]

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]

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]

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]

Beklemishev

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

work page 1994
[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]

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

work page 2008
[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]

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]

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]

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]

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

work page 1986
[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]

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]

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]

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]

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]

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]

Springer International Publishing. 41

work page
[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]

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]

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]

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]

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]

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

work page 2020
[28]

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
[29]

Springer, 1955

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

work page 1955
[30]

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
[31]

Elsevier, 1997

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

work page 1997
[32]

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
[33]

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
[34]

Springer, 1960

Kurt Schütte.Beweistheorie. Springer, 1960

work page 1960
[35]

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
[36]

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
[37]

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
[38]

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
[39]

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

work page 2024
[40]

Universitext

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

work page 1985
[41]

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

work page 1976
[42]

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
[43]

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
[44]

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
[45]

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