pith. sign in

arxiv: 2511.10966 · v4 · submitted 2025-11-14 · 🧮 math.LO

Neighborhood and algebraic models for predicate modal logics with ω-rules

Yoshihito Tanaka This is my paper

Pith reviewed 2026-05-17 22:45 UTC · model grok-4.3

classification 🧮 math.LO
keywords predicate modal logicneighborhood modelω-ruleconstant domaincompletenessnon-normal modal logicGL logiccommon knowledge logic
0
0 comments X

The pith

Sufficient conditions allow predicate modal logics with ω-rules to have complete neighborhood models with constant domains.

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

This paper establishes sufficient conditions for predicate modal logics that incorporate ω-rules to admit neighborhood models with constant domains. When these conditions hold, the logics are complete with respect to the corresponding class of neighborhood frames. The results apply to both normal and non-normal modal logics and build on earlier work that treated normal logics with ω-rules or non-normal logics without such rules. Applications include a soundness and completeness proof for a predicate extension of GL with respect to neighborhood frames with constant domains, along with a demonstration that a predicate common knowledge logic is incomplete for Kripke semantics but complete for neighborhood semantics.

Core claim

We establish sufficient conditions under which such logics have neighborhood models with constant domains and satisfy the completeness theorem with respect to neighborhood frames with constant domains. Related results for normal modal logics with ω-rules were obtained previously, while similar results for non-normal modal logics without ω-rules were presented elsewhere. The results extend these works. As applications, a predicate extension of GL is sound and complete with respect to a class of neighborhood frames with constant domains, and a predicate common knowledge logic is Kripke incomplete but neighborhood complete.

What carries the argument

The sufficient conditions derived from the ω-rules and predicate extensions that enable the construction of neighborhood models with constant domains and the proof of completeness.

If this is right

  • The predicate extension of GL is sound and complete with respect to neighborhood frames with constant domains.
  • A predicate common knowledge logic is Kripke incomplete but complete with respect to neighborhood frames with constant domains.
  • Neighborhood semantics provides completeness where Kripke semantics may fail for certain predicate modal logics with ω-rules.

Where Pith is reading between the lines

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

  • This method could extend to other infinitary modal logics or systems with similar rule sets.
  • Neighborhood models with constant domains may offer advantages for analyzing common knowledge in predicate settings where standard Kripke frames fall short.

Load-bearing premise

The logics must meet the specific properties required to build neighborhood models with constant domains out of the ω-rules and the predicate extensions as described.

What would settle it

A predicate modal logic equipped with ω-rules that fulfills the sufficient conditions but does not possess a neighborhood model with constant domains or fails to be complete for such frames.

read the original abstract

This paper investigates neighborhood and algebraic models for predicate modal logics with $\omega$-rules, including non-normal cases. We establish sufficient conditions under which such logics have neighborhood models with constant domains and satisfy the completeness theorem with respect to neighborhood frames with constant domains. Related results for normal modal logics with $\omega$-rules were obtained by Tanaka, while similar results for non-normal modal logics without $\omega$-rules were presented by Arl\'{o}-Costa and Pacuit and by Tanaka. The results presented here extend these works. As applications, we prove that a predicate extension of GL is sound and complete with respect to a class of neighborhood frames with constant domains, and that a predicate common knowledge logic is Kripke incomplete but neighborhood complete.

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

Summary. The paper investigates neighborhood and algebraic models for predicate modal logics with ω-rules, including non-normal cases. It establishes sufficient conditions under which such logics have neighborhood models with constant domains and satisfy the completeness theorem with respect to neighborhood frames with constant domains. The results extend Tanaka's work on normal modal logics with ω-rules and Arló-Costa/Pacuit/Tanaka results on non-normal modal logics without ω-rules. Applications include soundness and completeness of a predicate extension of GL w.r.t. a class of neighborhood frames with constant domains, and neighborhood completeness (but Kripke incompleteness) for a predicate common knowledge logic.

Significance. If the sufficient conditions hold and the proofs are correct, this provides a useful extension of neighborhood semantics to predicate modal logics with infinitary ω-rules in both normal and non-normal settings. It supplies frame conditions, verifies preservation of the ω-rule, and demonstrates utility via the GL and common-knowledge applications, addressing cases where Kripke semantics may be incomplete.

minor comments (2)
  1. The introduction would benefit from an explicit outline of how the sufficient conditions are used to construct the canonical neighborhood models in the main theorems.
  2. In the applications section, ensure that the verification that the specific frame conditions hold for the predicate GL axioms is cross-referenced to the general sufficient conditions theorem.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our manuscript, their accurate summary of its contributions, and their recommendation for minor revision. The report correctly identifies the extension of prior results by Tanaka and by Arló-Costa, Pacuit, and Tanaka to the setting of predicate modal logics with ω-rules in both normal and non-normal cases. As the report lists no specific major comments, we have no individual points requiring detailed rebuttal or clarification at this stage.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper extends prior results on neighborhood and algebraic models for modal logics by establishing new sufficient conditions for constant-domain neighborhood frames and completeness in the presence of ω-rules for both normal and non-normal predicate cases. The central steps involve defining frame conditions, proving preservation of the ω-rule under neighborhood semantics, and verifying the conditions for applications such as predicate GL and predicate common-knowledge logic. These proofs supply independent content beyond the cited extensions of Tanaka's normal-case results and Arló-Costa/Pacuit/Tanaka non-normal results without ω-rules. No self-definitional reductions, fitted parameters renamed as predictions, or load-bearing self-citations that collapse the new claims appear in the derivation chain.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claims rest on standard modal logic axioms, properties of neighborhood frames, and the extension to ω-rules and predicates; no free parameters or invented entities are indicated in the abstract.

axioms (2)
  • standard math Standard axioms and rules of modal logics including those for non-normal cases
    Invoked as the base for extending to ω-rules and predicate versions.
  • domain assumption Existence of neighborhood frames with constant domains satisfying the sufficient conditions
    Central to the completeness theorem stated in the abstract.

pith-pipeline@v0.9.0 · 5413 in / 1285 out tokens · 30090 ms · 2026-05-17T22:45:13.123351+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

18 extracted references · 18 canonical work pages

  1. [1]

    First-order classical modal logic.Studia Logica, 84(2):171–210, 2006

    Horacio Arl´ o-Costa and Eric Pacuit. First-order classical modal logic.Studia Logica, 84(2):171–210, 2006

    work page 2006

  2. [2]

    Cambridge, third edition, 2001

    Patrick Blackburn, Maarten de Rijke, and Yde Venema.Modal Logic. Cambridge, third edition, 2001

    work page 2001

  3. [3]

    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

  4. [4]

    Gabbay, Dimitrij Skvortsov, and Valentin Shehtman.Quantification in Nonclassical Logic

    Dov M. Gabbay, Dimitrij Skvortsov, and Valentin Shehtman.Quantification in Nonclassical Logic. Elsevier, 2012

    work page 2012

  5. [5]

    CSLI Publi- cations, 1993

    Robert Goldblatt.Mathematics of Modality, volume 43 ofCSLI Lecture Notes. CSLI Publi- cations, 1993

    work page 1993

  6. [6]

    Halpern and Yoram Moses

    Joseph Y. Halpern and Yoram Moses. A guide to completeness and complexity for modal logics of knowledge and beliefs.Artificial Intelligence, 54:319–379, 1992

    work page 1992

  7. [7]

    Map of common knowledge logics.Studia Logica, 71:57–86, 2002

    Mamoru Kaneko, Takashi Nagashima, Nobu-Yuki Suzuki, and Yoshihito Tanaka. Map of common knowledge logics.Studia Logica, 71:57–86, 2002

    work page 2002

  8. [8]

    Meyer and Wiebe van der Hoek.Epistemic Logic for AI and Computer Sci- ence

    John-Jules Ch. Meyer and Wiebe van der Hoek.Epistemic Logic for AI and Computer Sci- ence. Cambridge Tracts in Theoretical Computer Science. Cambridge, 1995

    work page 1995

  9. [9]

    Some remarks on the proof-theory and the semantics of infinitary logic

    Pierluigi Minari. Some remarks on the proof-theory and the semantics of infinitary logic. In Reinhard Kahle, Thomas Strahm, and Thomas Studer, editors,Advances in Proof Theory, pages 291–318. Springer, 2016

    work page 2016

  10. [10]

    PWN-Polish Scientific Publishers, 1963

    Helena Rasiowa and Roman Sikorski.The Mathematics of Metamathematics. PWN-Polish Scientific Publishers, 1963

    work page 1963

  11. [11]

    Enumerability of modal predicate logics and the condition of non-existence of infinite ascending chains.Logical Investigation, 9:155–167, 2002

    Mikhail Rybakov. Enumerability of modal predicate logics and the condition of non-existence of infinite ascending chains.Logical Investigation, 9:155–167, 2002

    work page 2002

  12. [12]

    A model existence theorem in infinitary propositional modal logic.Journal of Philosophical Logic, 23:337–367, 1994

    Krister Segerberg. A model existence theorem in infinitary propositional modal logic.Journal of Philosophical Logic, 23:337–367, 1994

    work page 1994

  13. [13]

    Model existence in non-compact modal logic.Studia Logica, 67:61–73, 2001

    Yoshihito Tanaka. Model existence in non-compact modal logic.Studia Logica, 67:61–73, 2001

    work page 2001

  14. [14]

    Some proof systems for predicate common knowledge logic.Reports on Mathematical Logic, 37:79–100, 2003

    Yoshihito Tanaka. Some proof systems for predicate common knowledge logic.Reports on Mathematical Logic, 37:79–100, 2003

    work page 2003

  15. [15]

    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

    work page 2018

  16. [16]

    Duality forκ-additive complete atomic modal algebras.Algebra Univer- salis, 82:1–20, 2021

    Yoshihito Tanaka. Duality forκ-additive complete atomic modal algebras.Algebra Univer- salis, 82:1–20, 2021

    work page 2021

  17. [17]

    An extension of J´ osson-Tarski representation and model existence in pred- icate non-normal modal logics.Mathematical Logic Quarterly, 68(2):189–201, 2022

    Yoshihito Tanaka. An extension of J´ osson-Tarski representation and model existence in pred- icate non-normal modal logics.Mathematical Logic Quarterly, 68(2):189–201, 2022

    work page 2022

  18. [18]

    First order common knowledge logics

    Frank Wolter. First order common knowledge logics. to appear in Studia Logica, 1999

    work page 1999