A proof system for the positive fragment of GL
Source: arXiv:2605.19349 · Published 2026-05-19 · By Yoshihito Tanaka
TL;DR
This paper introduces a novel proof system, named GL_+^{\top\bot}, for the positive fragment of the modal provability logic GL. Unlike previous work that covered various modal logics' positive fragments, GL had no dedicated proof system specifically for its positive fragment—formulas without negation or implication but using connectives ∨, ∧, ◇, □, ⊥, ⊤. The system is based on Dunn's K_+^{\top\bot} sequent system, augmented with GL-specific ω-rules reflecting Löb's axiom's modal fixed point nature. By employing algebraic techniques involving GLD-lattices and embeddings into GL-algebras, the author proves soundness and completeness of the new system, establishing an exact correspondence between provability in GL and derivability in GL_+^{\top\bot} for positive formulas. The ω-rule introduction and the use of modal distributive lattice theory constitute key innovations. As a result, this work fills an important gap in positive modal logic and modal provability logic literature, providing a well-founded calculus for reasoning about the positive fragment of GL.
Key findings
- The proof system GL_+^{\top\bot} is sound and complete for the positive fragment of GL, i.e., a sequent ϕ ⊢ ψ is derivable in GL_+^{\top\bot} if and only if the implication ϕ → ψ is provable in GL (Theorem 5.8).
- GL_+^{\top\bot} extends Dunn's K_+^{\top\bot} sequent system for positive modal logic with additional ω-rules capturing GL's Löb formula behavior (Definition 5.5).
- The class DGLD of GLD-lattices is introduced as an algebraic semantics for GL_+^{\top\bot}, and the system is shown sound and complete with respect to DGLD (Theorem 5.7).
- Every GLD-lattice can be embedded into a GL-algebra, establishing a strong algebraic link between the positive fragment and full GL modal algebra semantics (Theorem 3.4, Corollary 3.5).
- The ω-rules require countably many premises and are crucial for completeness, reflecting infinite derivations characteristic of provability logics (Definition 5.5, GLD-rules).
- A translation map ρ injects positive formulas into terms of modal distributive lattices preserving provability equivalence, connecting syntactic and algebraic frameworks (Theorem 5.4).
- Quasi-identities and quasi-sequents of modal distributive lattices are characterized by equivalences between classes of GL-algebras and GLD-lattices, via Birkhoff and Mal'cev theorems (Theorem 4.7).
- The positive fragment of GL properly extends the positive fragment of K4, capturing a strictly richer class of formulas (Introduction, citing Dashkov [3]).
Threat model
n/a — this is a mathematical logic and proof theory paper focused on formal proof systems and algebraic semantics rather than adversarial or security settings.
Methodology — deep read
Threat Model & Assumptions: The problem considered is purely formal proof theory and algebraic semantics of the positive fragment of the modal logic GL, so no adversarial threat model applies; rather, the 'adversary' is missing a suitable proof system for positive GL fragment. The logic GL extends the basic normal modal logic K with Löb's axiom, representing provability logic.
Data: The data are well-formed modal formulas constructed from propositional variables and connectives {∨, ∧, ◇, □, ⊥, ⊤}, restricted to exclude negation and implication. The positive fragment subset forms the domain of interest. No external datasets; proofs and algebraic classes serve as the semantic structures.
Architecture/Algorithm: The new proof system GL_+^{\top\bot} is a sequent calculus extending Dunn's K_+^{\top\bot} calculus with additional ω-rule inference rules that have countably infinite premises, reflecting the fixed point nature of Löb's axiom (□(□p→p)→□p). Sequents are expressions ϕ ⊢ψ where ϕ, ψ are positive modal formulas. The system includes axioms and rules for reflexivity, transitivity, conjunction/disjunction introduction/elimination, modal Becker's rules, linearity, interactions between □ and ◇ operators, and crucially the ω-rules.
Algebraically, the work introduces GLD-lattices as modal distributive lattices satisfying certain GL-inspired identities, including fixpoint-like conditions and infinite meet/join conditions. The modal algebraic semantics uses GL-algebras and GLD-lattices. A representation theorem constructs embeddings from any GLD-lattice into a GL-algebra, providing completeness.
Training Regime: N/A for this logic paper; however, proofs are deployed stepwise, building definitions and lemmas culminating in the main completeness theorem (Theorem 5.8).
Evaluation Protocol: Soundness is established by induction on derivations in GL_+^{\top\bot}. Completeness is shown via construction of countermodels in the algebraic semantics (GLD-lattices) when a sequent is not derivable. Theorems relating semantic validity in MGL and DGLD classes underpin correctness. The equivalence between sequent derivability and GL-provability is rigorously shown by reduction through several equivalences and algebraic embeddings.
Reproducibility: All definitions, rules, and theorems are fully spelled out with proofs. The logical calculus is formal and self-contained. No code or datasets involved, but the algebraic methods and proof rules are clearly given. The infinite-premise ω-rules imply proofs may require infinitary reasoning, making mechanical reproduction nontrivial but conceptually well-defined.
Concrete walkthrough example: Given positive formulas ϕ and ψ, to decide if ϕ → ψ is provable in GL, translate them into sequent ϕ ⊢ ψ. Check if this sequent is derivable in GL_+^{\top\bot} using its finitary axioms plus ω-rules. If not derivable, build a GLD-lattice counterexample by embedding ϕ, ψ and their valuations showing v(ϕ) ≤ v(ψ) fails. The key is that the calculus and algebraic structures align bidirectionally, closing the soundness-completeness loop.
Technical innovations
- Introduction of GLD-lattices as modal distributive lattices capturing essential properties of GL’s positive fragment, including infinite meets/joins reflecting Löb modality fixpoints.
- Development of the proof system GL_+^{\top\bot}, extending Dunn’s positive modal logic calculus with ω-rules that have countably many premises to handle provability logic’s fixed-point phenomena.
- Representation theorem embedding any GLD-lattice into a GL-algebra, bridging positive fragment algebraic semantics with classical GL modal algebras and establishing completeness.
- Use of quasi-identities and quasi-sequents framework to characterize logical consequences beyond single sequents, enhancing algebraic proof theory for positive modal logics.
Limitations
- The proof system requires ω-rules with infinitely many premises, which may render practical proof search non-terminating and difficult to mechanize fully.
- The positive fragment excludes negation and implication, limiting expressiveness compared to full GL logic; result does not directly address full GL proof complexity.
- The algebraic semantics and embeddings rely on technical modal lattice theory that may not generalize easily to other modal logics or fragments without modification.
- No explicit constructive proof search algorithm or complexity analysis is provided for the GL_+^{\top\bot} system.
- The paper does not discuss automated proof tool support or empirical evaluation of proof lengths or efficiency compared to other calculi.
- Completeness proofs depend significantly on infinite lattice-theoretic constructs; the intuition behind these algebraic constructs may be challenging for non-specialists.
Open questions / follow-ons
- Can the ω-rules in GL_+^{\top\bot} be replaced or approximated by finitary rules to improve mechanizability?
- Is there a useful proof system for quasi-sequents (conditional sequents) that is sound and complete for DGLD, as hinted in the conclusion?
- How can these algebraic and proof-theoretic insights extend to positive fragments of other well-known modal provability logics, such as GLP?
- What is the computational complexity of proof search or decision problems within GL_+^{\top\bot} given the ω-rules?
Why it matters for bot defense
While this paper is deeply theoretical and focused on modal provability logic proof systems, its contributions indirectly benefit bot-defense and CAPTCHA researchers working on logic-based challenge-response protocols or formal verification of security protocols involving modalities. The soundness and completeness of a proof system for positive modal fragments ensures that reasoning about certain monotone modal properties (absence of negation) can be done rigorously and potentially mechanized.
In particular, understanding how infinite-premise inference rules (ω-rules) are necessary to capture fixed-point properties typical of provability modalities may inform designs of resilience against automated attacks that exploit incomplete logical inference methods. However, the paper's focus is not directly on CAPTCHAs or bot defenses, so application would require significant adaptation from modal provability contexts to computational complexity or user-interaction settings typical in bot-defense. The algebraic frameworks developed could inspire new ways to specify and verify positive monotone modal conditions relevant for interactive proof systems in CAPTCHA design.
Cite
@article{arxiv2605_19349,
title={ A proof system for the positive fragment of GL },
author={ Yoshihito Tanaka },
journal={arXiv preprint arXiv:2605.19349},
year={ 2026 },
url={https://arxiv.org/abs/2605.19349}
}