In this paper, we propose Point-set Neighborhood Logic (PSNL) to reason about neighborhood structures. The bimodal language of PSNL is defined via a mutual induction of point-formulas and set-formulas. We show that this simple language is equally expressive as the language of Instantial Neighborhood Logic (INL). As the main results, we first give two complete proof systems, one in Hilbert-style and one in Gentzen sequent-style, each featuring two intertwined $\mathsf{K}$-like systems. The proof of strong completeness of the Hilbert-style system is based on a direct canonical model construction without relying on a normal form. Based on the sequent calculus, we establish the uniform interpolation property of PSNL, from which that of INL follows.
Leave a Reply