Positive Instantial Neighbourhood logic

Anupam Khanra; Litan Kumar Das; Sujit Kumar Sardar

arxiv: 2606.08083 · v1 · pith:U3PEXHMFnew · submitted 2026-06-06 · 💻 cs.LO

Positive Instantial Neighbourhood logic

Litan Kumar Das , Anupam Khanra , Sujit Kumar Sardar This is my paper

Pith reviewed 2026-06-27 19:20 UTC · model grok-4.3

classification 💻 cs.LO

keywords instantial neighbourhood logicpositive modal logiccompletenesstruth lemmaalgebraic semanticsbitopological spacesneighbourhood modelsdistributive lattices

0 comments

The pith

Positive instantial neighbourhood logic is complete over persistent two-sided neighbourhood models via a typed auxiliary semantics and admits a canonical bitopological representation.

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

The paper introduces PINL, a negation-free modal language with independent box-type and diamond-type instantial modalities for expressing information about worlds inside neighbourhoods. It interprets the logic on persistent two-sided neighbourhood models and defines a typed persistent neighbourhood semantics to manage witness and co-witness conditions. This auxiliary semantics produces a truth lemma that yields completeness for the proof system. Algebraically the paper defines 2-DLIOs as bounded distributive lattices equipped with two families of instantial operations and establishes soundness and completeness through the Lindenbaum 2-DLIO. It then builds a canonical bitopological PINL-space in which the algebra of admissible positive opens is shown isomorphic to the Lindenbaum algebra.

Core claim

PINL is complete with respect to persistent two-sided neighbourhood models because the typed persistent neighbourhood semantics delivers the required truth lemma, algebraic soundness and completeness hold via the Lindenbaum 2-DLIO, and the algebra of admissible positive opens in the constructed canonical bitopological PINL-space is isomorphic to that Lindenbaum algebra.

What carries the argument

Typed persistent neighbourhood semantics on persistent two-sided neighbourhood models, used to control witness and co-witness conditions and thereby obtain the truth lemma.

If this is right

Every consistent PINL theory corresponds to a persistent two-sided neighbourhood model in which it is satisfied.
The Lindenbaum 2-DLIO supplies a canonical algebraic model for any consistent set of PINL formulas.
The admissible positive opens of the canonical bitopological PINL-space provide a concrete topological model isomorphic to the Lindenbaum algebra.
The representation supplies the first concrete step toward a duality theory linking the logic to bitopological spaces.

Where Pith is reading between the lines

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

The bitopological representation could be used to transfer separation or compactness properties from topology back into logical completeness or finite model properties.
Similar typed auxiliary semantics might be adapted to obtain completeness for other negation-free neighbourhood or modal logics that lack classical negation.
If the canonical spaces admit finite approximations, the representation might yield decision procedures for PINL satisfiability.

Load-bearing premise

The typed persistent neighbourhood semantics controls witness and co-witness conditions sufficiently to deliver the truth lemma for the persistent two-sided neighbourhood models.

What would settle it

A PINL formula that holds in every persistent two-sided neighbourhood model yet fails to be derivable in the PINL proof system, or a failure of the stated isomorphism between the Lindenbaum 2-DLIO and the algebra of admissible positive opens of the canonical bitopological PINL-space.

read the original abstract

Instantial neighbourhood logic is a modal language for neighbourhood frames in which formulas can express information about the kinds of worlds occurring inside a neighbourhood of a given world. In this paper, we study a positive, negation-free version of instantial neighbourhood logic with two primitive instantial modalities, one of box-type and one of diamond-type. Since classical negation is not available, the two modalities are treated independently. We introduce the language and proof system of positive instantial neighbourhood logic (PINL) and interpret it over persistent two-sided neighbourhood models. We then define a typed persistent neighbourhood semantics, used as an auxiliary canonical semantics to control witness and co-witness conditions. This yields a truth lemma and the corresponding completeness result of PINL. On the algebraic side, we introduce $2$-$\mathrm{DLIO}$s, bounded distributive lattices equipped with two families of instantial operations, as the algebraic semantics of PINL. We prove algebraic soundness and completeness via the Lindenbaum $2$-$\mathrm{DLIO}$. Finally, we construct the canonical bitopological PINL-space and show that the algebra of its admissible positive opens is isomorphic to the Lindenbaum $2$-$\mathrm{DLIO}$. Thus the paper gives a canonical admissible-open representation of positive instantial neighbourhood logic, providing a first step toward a future duality theory.

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

PINL defines a negation-free instantial neighbourhood logic with independent box and diamond modalities, then gives completeness via typed persistent semantics and a 2-DLIO algebraic representation.

read the letter

The paper introduces PINL, a positive fragment of instantial neighbourhood logic that keeps the two instantial modalities separate because negation is absent. It supplies a Hilbert-style proof system, interprets the language on persistent two-sided neighbourhood models, and uses an auxiliary typed persistent semantics to secure a truth lemma. Algebraically it defines 2-DLIOs as bounded distributive lattices with two families of instantial operations, proves soundness and completeness via the Lindenbaum algebra, and constructs a canonical bitopological space whose admissible positive opens are isomorphic to that algebra.

What stands out is the clean separation of the modalities and the move to a typed auxiliary semantics to handle witness and co-witness conditions. The bitopological representation is presented as a first step toward duality, and the constructions do not collapse into earlier results on standard neighbourhood or positive modal logics. The setup is self-contained and the citation pattern stays within the relevant subfield without obvious self-referential shortcuts.

The main limitation is that the abstract supplies no proof steps or lemmas, so the critical claim that the typed semantics actually controls the witness conditions rests on unexamined derivations. If the full text follows the usual pattern for these logics the argument should go through, but that remains to be checked. No internal contradictions or hidden fitting assumptions appear in the given description.

This work is aimed at researchers already working on neighbourhood semantics, positive modal logics, or algebraic duality for modal systems. A reader who needs a concrete completeness result and representation theorem for this specific language will find it useful. It is coherent on its own terms and formally grounded enough to merit referee time even if the proofs require tightening.

Referee Report

0 major / 3 minor

Summary. The paper introduces Positive Instantial Neighbourhood Logic (PINL), a negation-free modal logic with independent box-type and diamond-type instantial modalities. It interprets the logic over persistent two-sided neighbourhood models, introduces an auxiliary typed persistent neighbourhood semantics to obtain a truth lemma and completeness, defines 2-DLIOs as algebraic semantics, proves algebraic soundness and completeness via the Lindenbaum 2-DLIO, and constructs a canonical bitopological PINL-space whose algebra of admissible positive opens is isomorphic to the Lindenbaum algebra, yielding a canonical representation.

Significance. If the derivations hold, the work supplies a completeness theorem and admissible-open representation for a positive fragment of instantial neighbourhood logic, treating the two modalities independently in the absence of negation. This constitutes a first step toward duality theory for such logics. The use of an auxiliary typed semantics to secure the truth lemma and the explicit Lindenbaum-algebra isomorphism are concrete technical contributions.

minor comments (3)

§2 (Language and proof system): the syntax for the two instantial modalities is introduced without an explicit comparison table to the classical instantial neighbourhood logic operators; adding such a table would clarify the negation-free treatment.
§4 (Typed persistent neighbourhood semantics): the definition of the witness and co-witness conditions is given in prose; a displayed list of the four conditions with their formal clauses would improve readability of the truth-lemma argument.
The paper cites prior work on instantial neighbourhood logic but does not include a short paragraph contrasting the positive case with the classical one; such a paragraph would help situate the contribution.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the paper, recognition of its technical contributions, and recommendation of minor revision. No specific major comments were raised in the report.

Circularity Check

0 steps flagged

No significant circularity; standard completeness construction

full rationale

The paper defines PINL syntax, persistent two-sided neighbourhood models, typed auxiliary semantics, proof system, 2-DLIO algebras, Lindenbaum algebra, and canonical bitopological space from scratch. Completeness follows the usual pattern: truth lemma via auxiliary semantics, algebraic soundness/completeness via Lindenbaum 2-DLIO, and admissible-open isomorphism. No equations reduce a target result to a fitted parameter, no self-citation chain bears the central claim, and no ansatz or renaming is smuggled in. The derivation is self-contained against external model-theoretic and algebraic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

No free parameters or invented entities are introduced; the work relies on standard background assumptions of lattice theory and modal semantics.

axioms (2)

standard math Bounded distributive lattices satisfy the standard equational axioms of bounded lattices and distributivity
Invoked when defining 2-DLIOs as the algebraic semantics
domain assumption Neighbourhood frames admit persistent two-sided models
Used as the base interpretation for PINL formulas

pith-pipeline@v0.9.1-grok · 5769 in / 1392 out tokens · 22718 ms · 2026-06-27T19:20:55.814508+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

16 extracted references

[1]

The Review of Symbolic Logic, CUP, 10(1), 116- 144, 2017

Van Benthem, Johan., Bezhanishvili, Nick.,Enqvist, Sebastian., Yu, Junhua.: Instantial neighbourhood logic. The Review of Symbolic Logic, CUP, 10(1), 116- 144, 2017

2017
[2]

International Workshop on Coalgebraic Methods in Computer Science, Springer, 32-54, 2020

Bezhanishvili, Nick., Enqvist, Sebastian., De Groot, Jim.:Duality for instan- tial neighbourhood logic via coalgebra. International Workshop on Coalgebraic Methods in Computer Science, Springer, 32-54, 2020

2020
[3]

Dunn, J Michael.:Positive modal logic, Studia Logica, 55(2), 301-317, 1995

1995
[4]

Priestley, Hilary A.:Representation of distributive lattices by means of ordered Stone spaces, Bulletin of the London Mathematical Society, 2(2), 186-190, 1970

1970
[5]

Celani, Sergio., Jansana, Ramon.:Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic, Logic Journal of the IGPL, OUP, 7(6), 683-715, 1999. 53

1999
[6]

Jakl, Tomáš.:d-Frames as algebraic duals of bitopological spaces, PhD thesis, Univerzita Karlova, Matematicko-fyzikální fakulta., 2018

2018
[7]

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

1997
[8]

Celani, Sergio., Jansana, Ramon.:A note on the model theory for positive modal logic, Fundamenta Informaticae, 114(1), 31-54, 2012

2012
[9]

Gehrke, Mai., Nagahashi, Hideo., Venema, Yde.:A Sahlqvist theorem for distributive modal logic, Annals of pure and applied logic, 131(1-3), 65-102, 2005

2005
[10]

3 Frames., Advances in Modal Logic, 12, 399-418, 2018

Kikot, Stanislav., Kurucz, Agi., Wolter, Frank., Zakharyaschev, Michael.:On Strictly Positive Modal Logics with S4. 3 Frames., Advances in Modal Logic, 12, 399-418, 2018

2018
[11]

Palmigiano, Alessandra.:A coalgebraic view on positive modal logic, 327(1-2), 175-195, 2004

2004
[12]

Sadrzadeh, Mehrnoosh., Dyckhoff, Roy.:Positive logic with adjoint modali- ties: Proof theory, semantics, and reasoning about information, The Review of Symbolic Logic, 3(3), 351-373, 2010

2010
[13]

De Groot, Jim.:Positive monotone modal logic, Studia Logica, 109(4), 829-857, 2021

2021
[14]

Bezhanishvili, Nick., De Groot, Jim., Venema, Yde.:Coalgebraic geometric logic: basic theory, Logical Methods in Computer Science, 18, 2022

2022
[15]

Vickers, Steven.:The double powerlocale and exponentiation: a case study in geometric logic, Theory and Applications of Categories, 12(13), 372-422, 2004

2004
[16]

Vickers, Steven.:Topology via logic, Cambridge University Press, 1989. 54

1989

[1] [1]

The Review of Symbolic Logic, CUP, 10(1), 116- 144, 2017

Van Benthem, Johan., Bezhanishvili, Nick.,Enqvist, Sebastian., Yu, Junhua.: Instantial neighbourhood logic. The Review of Symbolic Logic, CUP, 10(1), 116- 144, 2017

2017

[2] [2]

International Workshop on Coalgebraic Methods in Computer Science, Springer, 32-54, 2020

Bezhanishvili, Nick., Enqvist, Sebastian., De Groot, Jim.:Duality for instan- tial neighbourhood logic via coalgebra. International Workshop on Coalgebraic Methods in Computer Science, Springer, 32-54, 2020

2020

[3] [3]

Dunn, J Michael.:Positive modal logic, Studia Logica, 55(2), 301-317, 1995

1995

[4] [4]

Priestley, Hilary A.:Representation of distributive lattices by means of ordered Stone spaces, Bulletin of the London Mathematical Society, 2(2), 186-190, 1970

1970

[5] [5]

Celani, Sergio., Jansana, Ramon.:Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic, Logic Journal of the IGPL, OUP, 7(6), 683-715, 1999. 53

1999

[6] [6]

Jakl, Tomáš.:d-Frames as algebraic duals of bitopological spaces, PhD thesis, Univerzita Karlova, Matematicko-fyzikální fakulta., 2018

2018

[7] [7]

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

1997

[8] [8]

Celani, Sergio., Jansana, Ramon.:A note on the model theory for positive modal logic, Fundamenta Informaticae, 114(1), 31-54, 2012

2012

[9] [9]

Gehrke, Mai., Nagahashi, Hideo., Venema, Yde.:A Sahlqvist theorem for distributive modal logic, Annals of pure and applied logic, 131(1-3), 65-102, 2005

2005

[10] [10]

3 Frames., Advances in Modal Logic, 12, 399-418, 2018

Kikot, Stanislav., Kurucz, Agi., Wolter, Frank., Zakharyaschev, Michael.:On Strictly Positive Modal Logics with S4. 3 Frames., Advances in Modal Logic, 12, 399-418, 2018

2018

[11] [11]

Palmigiano, Alessandra.:A coalgebraic view on positive modal logic, 327(1-2), 175-195, 2004

2004

[12] [12]

Sadrzadeh, Mehrnoosh., Dyckhoff, Roy.:Positive logic with adjoint modali- ties: Proof theory, semantics, and reasoning about information, The Review of Symbolic Logic, 3(3), 351-373, 2010

2010

[13] [13]

De Groot, Jim.:Positive monotone modal logic, Studia Logica, 109(4), 829-857, 2021

2021

[14] [14]

Bezhanishvili, Nick., De Groot, Jim., Venema, Yde.:Coalgebraic geometric logic: basic theory, Logical Methods in Computer Science, 18, 2022

2022

[15] [15]

Vickers, Steven.:The double powerlocale and exponentiation: a case study in geometric logic, Theory and Applications of Categories, 12(13), 372-422, 2004

2004

[16] [16]

Vickers, Steven.:Topology via logic, Cambridge University Press, 1989. 54

1989