pith. sign in

arxiv: 2605.18043 · v1 · pith:5GBHF2GHnew · submitted 2026-05-18 · 💻 cs.LO

A Proof-Theoretic Study of Modal Logic

Hirohiko Kushida This is my paper

Pith reviewed 2026-05-20 00:38 UTC · model grok-4.3

classification 💻 cs.LO
keywords modal logichypersequent calculuscut eliminationsequent calculusproof theorymodal axiomsS5
0
0 comments X

The pith

A hypersequent calculus framework generates the standard sequent calculi for modal logics K, T, D, S4 and S5 and establishes cut-elimination for most of them.

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

The paper sets out a basic framework using hypersequent calculus to handle major modal logics such as S5 and its subsystems based on K with axioms T, D, 4, B, 5. It provides an account of how the usual sequent and hypersequent systems for K, T, D, S4, S5 come out of this framework. A syntactic proof of cut-elimination is given for these logics except KB, KDB and KTB. Quantified extensions are also considered. Readers interested in proof theory would see value in having a single setup that explains multiple known systems and their properties.

Core claim

The central discovery is a hypersequent calculus framework for the modal logics K and its extensions with T, D, 4, B, 5, from which the standard sequent calculi for K, T, D, S4, S5 emerge, with a syntactic proof of cut-elimination for all except KB, KDB, KTB, and discussion of quantified versions.

What carries the argument

The version of hypersequent calculus that serves as the basic system, with rules added for the modal axioms to generate the target logics.

If this is right

  • Standard sequent calculi for K, T, D, S4, S5 arise directly from the hypersequent framework.
  • Cut-elimination theorems hold for the modal logics except KB, KDB, KTB.
  • Quantified versions of these modal systems can be formulated and studied within the same framework.

Where Pith is reading between the lines

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

  • The framework could be tested for its ability to handle additional modal axioms or other non-classical logics.
  • Success in syntactic cut-elimination might facilitate the development of proof search algorithms for these modal logics.

Load-bearing premise

The proposed hypersequent rules for the modal axioms T, D, 4, B, 5 correctly represent their logical properties without introducing any mismatches or incomplete proofs.

What would settle it

Finding a specific modal formula that has a proof in one of the standard calculi for KB but cannot be derived without cuts in the proposed framework would challenge the cut-elimination result.

read the original abstract

This paper proposes a basic proof theoretic framework for major modal logics: {\sf S5} and some of its subsystems. The framework is based on a version of hypersequent calculus, and the basic modal systems we handle here are the system {\sf K} and its standard extensions with combinations of axioms: $T, D, 4, B, 5$. First we propose a reasonable explanation of how the standard sequent and hypersequent calculi for some of those modal logics such as {\sf K, T, D, S4, S5} emerge on the basis of the framework. Then, by a syntactic method, we prove the cut-elimination theorem for the modal logics except for the modal logics {\sf KB, KDB, KTB}. Quantified versions of the systems of the framework are also discussed.

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

1 major / 3 minor

Summary. The paper proposes a hypersequent calculus framework for the modal logic K and its extensions by the axioms T, D, 4, B and 5. It shows how the standard sequent and hypersequent calculi for K, T, D, S4 and S5 emerge from this basic framework via explicit derivations, then gives syntactic cut-elimination proofs for these systems (excluding KB, KDB and KTB) by induction on derivation height. Quantified versions of the systems are also discussed.

Significance. If the derivations and syntactic cut-elimination arguments hold, the work supplies a unified proof-theoretic account that explains the origin of several standard modal calculi from a single hypersequent base and avoids semantic arguments for cut-elimination. This is useful for comparing modal proof systems and for applications that rely on purely syntactic properties such as consistency or automated search.

major comments (1)
  1. The exclusion of KB, KDB and KTB from the cut-elimination theorem is stated in the abstract and introduction without an explicit account of where the induction fails for the B axiom; this limits assessment of the framework's scope even though the claim is only made for the covered systems.
minor comments (3)
  1. The derivations showing how standard rules for S4 and S5 arise from the basic framework (around the relevant sections on rule emergence) would benefit from one or two fully worked example derivations to make the translation steps fully explicit.
  2. Notation for hypersequent components and the precise form of the modal rules for 4 and 5 should be cross-referenced consistently between the framework definition and the cut-elimination proof to avoid minor ambiguity.
  3. The quantified extension is mentioned only briefly; adding a short remark on how the hypersequent structure interacts with quantifier rules would improve completeness without altering the central claims.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive evaluation and the recommendation of minor revision. The single major comment is addressed point by point below.

read point-by-point responses

  1. Referee: The exclusion of KB, KDB and KTB from the cut-elimination theorem is stated in the abstract and introduction without an explicit account of where the induction fails for the B axiom; this limits assessment of the framework's scope even though the claim is only made for the covered systems.

    Authors: We agree that the manuscript would benefit from greater transparency regarding the boundaries of the result. While the abstract and introduction correctly limit the cut-elimination claim to the systems for which a syntactic proof is supplied, we do not currently provide an explicit diagnosis of the obstruction that arises when the B rule is added. In the revised version we will insert a concise paragraph (in the introduction and cross-referenced from the cut-elimination section) that identifies the step in the induction on derivation height at which the argument breaks down for the B axiom. This addition will clarify the scope of the framework without altering the positive results already obtained. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper defines a basic hypersequent framework for K and its extensions with T, D, 4, B, 5, then derives standard sequent and hypersequent calculi for K, T, D, S4, S5 by explicit rule translations and admissibility arguments that remain internal to the hypersequent language. Cut-elimination is established by a standard syntactic induction on derivation height that handles the modal rules without semantic assumptions or external parameters. These steps constitute independent syntactic constructions; no load-bearing claim reduces by definition, fitted input, or self-citation chain to the paper's own inputs. The derivation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract provides insufficient detail on specific assumptions or parameters; framework appears to rest on standard modal axiom interpretations via hypersequents.

axioms (1)
  • domain assumption Hypersequent rules correctly encode the modal axioms T, D, 4, B, 5 and allow emergence of standard calculi
    Invoked when proposing the basic framework and explaining standard systems

pith-pipeline@v0.9.0 · 5660 in / 1210 out tokens · 39485 ms · 2026-05-20T00:38:30.563622+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

11 extracted references · 11 canonical work pages

  1. [1]

    Br\"unnler, Deep sequent systems for modal logic, Archive for Mathematical Logic, 48, pp.551-577, 2009

    K. Br\"unnler, Deep sequent systems for modal logic, Archive for Mathematical Logic, 48, pp.551-577, 2009

    work page 2009

  2. [2]

    Bednarska and A

    K. Bednarska and A. Indrzejczak, Hypersequent Calculi for S5: The Methods of Cut Elimination, Logic and Logical Philosophy , vol. 24 no. 3, pp.277-311, 2015

    work page 2015

  3. [3]

    Buss, An Introduction to Proof Theory

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

    work page 1998

  4. [4]

    Gentzen, Untersuchungen \"uber das logische Schlie en

    G. Gentzen, Untersuchungen \"uber das logische Schlie en. Mathematische Zeitschrift 39, pp. 176-210, pp. 405-431, 1935 (English translation in Gentzen gentzen1969 )

    work page 1935

  5. [5]

    Gentzen, The Collected Papers of Gerhard Gentzen, Szabo, M.E

    G. Gentzen, The Collected Papers of Gerhard Gentzen, Szabo, M.E. (ed.), North Holland, 1969

    work page 1969

  6. [6]

    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

  7. [7]

    Mints, Cut Elimination for S4C: A Case Study, Studia Logica , vol

    G. Mints, Cut Elimination for S4C: A Case Study, Studia Logica , vol. 82 no. 1, Cut-Elimination in Classical and Nonclassical Logic, pp. 121-132, 2006

    work page 2006

  8. [8]

    Ohnishi and K

    M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi. Osaka mathematical journal, vol. 9 no. 2, pp.113-130, 1957

    work page 1957

  9. [9]

    Ohnishi and K

    M. Ohnishi and K. Matsumoto. Gentzen method in modal calculi. II, Osaka mathematical journal, vol. 11 no. 2,, pp.115-120, 1959

    work page 1959

  10. [10]

    Pottinger, Uniform Cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic, vol

    G. Pottinger, Uniform Cut-free formulations of T, S4 and S5 (abstract), Journal of Symbolic Logic, vol. 48, p.900, 1983

    work page 1983

  11. [11]

    Valentini, The sequent calculus for the modal logic D, Bollettinodell’Unione Matematica Italiana 7, pp.455-460, 1993

    S. Valentini, The sequent calculus for the modal logic D, Bollettinodell’Unione Matematica Italiana 7, pp.455-460, 1993

    work page 1993