pith. sign in

arxiv: 2605.19349 · v1 · pith:2NQUYRAAnew · submitted 2026-05-19 · 🧮 math.LO

A proof system for the positive fragment of GL

Yoshihito Tanaka This is my paper

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

classification 🧮 math.LO
keywords GLmodal logicpositive fragmentsequent calculusLöb axiomproof systemprovability logic
0
0 comments X

The pith

A sequent system for positive modal formulas proves φ ⊢ ψ exactly when GL proves φ ⊃ ψ.

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

The paper constructs a sequent calculus GL₊^{⊤⊥} for modal formulas that use only disjunction, conjunction, diamond, box, top, bottom, and propositional variables. It establishes that this calculus derives the sequent φ ⊢ ψ if and only if the full modal logic GL derives the implication φ ⊃ ψ. A reader would care because the construction lets one reason directly about implications in provability logic while staying inside the positive fragment, avoiding negation and implication connectives in the premises and conclusions. The system starts from an earlier positive sequent calculus for the basic modal logic K and adds rules that incorporate the Löb axiom while preserving the correspondence for positive formulas.

Core claim

The sequent system GL₊^{⊤⊥} is defined by extending the positive sequent rules for K with additional rules that capture the Löb axiom; the resulting system satisfies the property that, for any positive modal formulas φ and ψ, the sequent φ ⊢ ψ is derivable in GL₊^{⊤⊥} precisely when the implication φ ⊃ ψ is a theorem of GL.

What carries the argument

The sequent calculus GL₊^{⊤⊥}, which augments Dunn's positive sequent system for K with rules enforcing the Löb axiom on positive formulas.

If this is right

  • Derivability of sequents in the positive system directly corresponds to theoremhood of implications in GL.
  • Proofs of positive implications in GL can be carried out entirely within sequent derivations that avoid negation and implication symbols.
  • The positive fragment of GL admits a sequent-style presentation that inherits soundness and completeness from the underlying K system plus the Löb rules.
  • Any theorem of GL that can be written as an implication between positive formulas becomes provable via the sequent calculus.

Where Pith is reading between the lines

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

  • The same pattern of extending a positive base system with axiom-specific rules could be tried for other modal logics whose axioms are expressible in positive form.
  • This sequent system might serve as a foundation for automated search procedures restricted to positive statements in provability logic.
  • Connections between sequent derivations in the positive fragment and fixed-point properties of GL could be explored by examining how the Löb rules interact with box and diamond in derivations.

Load-bearing premise

The positive sequent system for the basic modal logic K is sound and complete for positive formulas, and the added Löb rules extend the equivalence to GL without creating new gaps or mismatches for positive formulas.

What would settle it

A concrete counterexample would be a pair of positive modal formulas φ and ψ for which either the sequent φ ⊢ ψ is derivable in GL₊^{⊤⊥} yet φ ⊃ ψ is not a theorem of GL, or the sequent is underivable yet the implication is a theorem of GL.

read the original abstract

In this paper, we present a proof system $\mathsf{GL}_{+}^{\top\bot}$, which is based on a sequent system $\mathsf{K}_{+}^{\top\bot}$ given by Dunn, for the positive fragment of $\mathsf{GL}$. Positive modal formulas are modal formulas that contain neither negation symbols nor implication symbols. More precisely, they are modal formulas constructed from the connectives $\lor$, $\land$, $\Diamond$, $\Box$, $\bot$, $\top$, and propositional variables. The logic $\mathsf{GL}$ is the least normal modal logic that contains $\mathsf{K}$ and the L\"{o}b formula $\Box(\Box p\supset p)\supset\Box p$. Following Dunn, a sequent is an expression of the form $\phi\vdash\psi$, where $\phi$ and $\psi$ are positive modal formulas. We present a proof system $\mathsf{GL}_{+}^{\top\bot}$ for sequents with the property that a sequent $\phi\vdash\psi$ is provable in $\mathsf{GL}_{+}^{\top\bot}$, if and only if $\phi\supset\psi$ is provable in $\mathsf{GL}$.

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

2 major / 2 minor

Summary. The paper presents a sequent calculus GL₊^{⊤⊥} extending Dunn's K₊^{⊤⊥} with rules for the Löb axiom, for positive modal formulas (built from ∧, ∨, □, ◇, ⊤, ⊥, and variables, without ¬ or ⊃). It claims that for such φ and ψ, the sequent φ ⊢ ψ is derivable in GL₊^{⊤⊥} if and only if GL ⊢ φ ⊃ ψ.

Significance. If the equivalence is established, the result supplies a sequent system for the positive fragment of GL. This is useful for proof-theoretic investigations of modal logics, as the positive fragment avoids negation and implication while still capturing key modal behavior; it may support further work on cut-elimination or decidability restricted to this fragment. The construction reuses Dunn's base system and adds Löb-specific rules, which is a standard proof-theoretic strategy.

major comments (2)
  1. [§5] §5 (Completeness direction): The argument that every positive sequent valid in GL is derivable in GL₊^{⊤⊥} relies on the claim that the added Löb rules suffice to simulate all positive consequences of the Löb axiom. However, the manuscript does not exhibit an explicit derivation or inductive argument showing how nested □ applications on positive formulas are captured without cut or an external semantic embedding; this leaves the completeness claim under-supported for formulas with multiple modalities.
  2. [§3.2] §3.2, Löb rule schema: The sequent rule(s) introduced for the Löb axiom are stated, but it is not shown that they are sufficient to derive the positive instances of □(□p ⊃ p) ⊃ □p (or their sequent equivalents) in a way that matches GL's fixed-point behavior restricted to the positive language. A concrete example derivation for a simple positive Löb instance would be needed to confirm no gaps are introduced.
minor comments (2)
  1. [§3] The manuscript would benefit from an explicit list or table of all rules in GL₊^{⊤⊥} (including the inherited Dunn rules and the new Löb rules) for easy reference.
  2. [§2] Notation for positive formulas and sequents is mostly clear, but a short example derivation in the preliminaries would help readers unfamiliar with Dunn's system.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and valuable suggestions regarding the completeness argument and the presentation of the Löb rules. We address each major comment below and will incorporate revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: [§5] §5 (Completeness direction): The argument that every positive sequent valid in GL is derivable in GL₊^{⊤⊥} relies on the claim that the added Löb rules suffice to simulate all positive consequences of the Löb axiom. However, the manuscript does not exhibit an explicit derivation or inductive argument showing how nested □ applications on positive formulas are captured without cut or an external semantic embedding; this leaves the completeness claim under-supported for formulas with multiple modalities.

    Authors: We agree that the completeness direction in §5 would benefit from greater explicitness. We will revise the section to include a detailed inductive argument on the structure of positive formulas, showing step by step how the added Löb rules simulate the positive consequences of the Löb axiom for nested □ applications. The induction will proceed directly on the sequent derivations and avoid any appeal to cut or semantic embeddings. revision: yes

  2. Referee: [§3.2] §3.2, Löb rule schema: The sequent rule(s) introduced for the Löb axiom are stated, but it is not shown that they are sufficient to derive the positive instances of □(□p ⊃ p) ⊃ □p (or their sequent equivalents) in a way that matches GL's fixed-point behavior restricted to the positive language. A concrete example derivation for a simple positive Löb instance would be needed to confirm no gaps are introduced.

    Authors: We accept that a concrete example would improve clarity. In the revised manuscript we will insert, in §3.2, an explicit derivation of a simple positive sequent equivalent to a Löb instance (for instance, the sequent □(□p ∧ p) ⊢ □p, which is expressible in the positive language). This derivation will illustrate how the rules capture the relevant fixed-point behavior without introducing gaps. revision: yes

Circularity Check

0 steps flagged

No circularity: equivalence to external GL is a proven theorem, not a self-definition

full rationale

The paper constructs GL₊^{⊤⊥} by extending Dunn's independent base system K₊^{⊤⊥} with explicit sequent rules for the Löb axiom. The central claim is an iff theorem relating provability in the new system to provability of the corresponding implication in the external logic GL. This is established via soundness and completeness arguments that rely on the prior base system and standard modal logic properties, without any reduction of the target result to a fitted parameter, self-citation chain, or definitional renaming. The derivation remains self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper rests on standard definitions of normal modal logics and the specific prior sequent system by Dunn; no free parameters or invented entities are introduced.

axioms (2)
  • domain assumption GL is the least normal modal logic containing K and the Löb formula □(□p ⊃ p) ⊃ □p
    Explicitly stated in the abstract as the definition of GL.
  • domain assumption The sequent system K₊^{⊤⊥} by Dunn is appropriate for the positive fragment of K
    The new system is presented as based on this prior system.

pith-pipeline@v0.9.0 · 5729 in / 1350 out tokens · 49373 ms · 2026-05-20T02:47:10.272883+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

10 extracted references · 10 canonical work pages

  1. [1]

    On the structure of abstract algebras.Proceedings of the Cambridge Philo- sophical Society, 31(4):433–454, 1935

    Garrett Birkhoff. On the structure of abstract algebras.Proceedings of the Cambridge Philo- sophical Society, 31(4):433–454, 1935

    work page 1935

  2. [2]

    Celani and Ramon Jansana

    Sergio A. Celani and Ramon Jansana. A new semantics for positive modal logic.Notre Dame Journal of Formal Logic, 38(1):1–19, 1997

    work page 1997

  3. [3]

    Evgenij V. Dashkov. On the positive fragment of the polymodal provability logic GLP.Math- ematical Notes, 91(3):318–333, 2012

    work page 2012

  4. [4]

    Duality between modal algebras and neighbourhood frames.Studia Logica, 48:219–234, 1989

    Kosta Doˇ sen. Duality between modal algebras and neighbourhood frames.Studia Logica, 48:219–234, 1989

    work page 1989

  5. [5]

    Positive modal logic.Studia Logica, 55:301–317, 1995

    Jon Michael Dunn. Positive modal logic.Studia Logica, 55:301–317, 1995

    work page 1995

  6. [6]

    Kripke completeness of strictly positive modal logics over meet-semilattices with operators

    Stanislav Kikot, Agi Kurucz, Yoshihito Tanaka, Frank Wolter, and Michael Zakharyaschev. Kripke completeness of strictly positive modal logics over meet-semilattices with operators. The Journal of Symbolic Logic, 84:533–588, 2019

    work page 2019

  7. [7]

    Several remarks on quasivarieties of algebraic systems.Algebra i Logika, 5:3–9, 1966

    Anatoly Ivanovich Mal’cev. Several remarks on quasivarieties of algebraic systems.Algebra i Logika, 5:3–9, 1966

    work page 1966

  8. [8]

    Anω-rule for the logic of provability and its models

    Katsumi Sasaki and Yoshihito Tanaka. Anω-rule for the logic of provability and its models. Studia Logica, 112:1163–1180, 2024

    work page 2024

  9. [9]

    Locality and subsumption testing inELand some of its exten- sions

    Viorica Sofronie-Stokkermans. Locality and subsumption testing inELand some of its exten- sions. In Carlos Areces and Robert Goldblatt, editors,Advances in Modal Logic, volume 7, pages 315–339. College Publications, 2008

    work page 2008

  10. [10]

    A cut-free proof system for a predicate extension of the logic of provability

    Yoshihito Tanaka. A cut-free proof system for a predicate extension of the logic of provability. Reports on Mathematical Logic, 53:97–109, 2018. Kyushu Sangyo University

    work page 2018