15 August 2024, Joint NihiL/LIRa session, Yanjing Wang

Abstract:
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) proposed by van Benthem et al. (2017). 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 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 constructively the uniform interpolation property of PSNL, from which that of INL follows. (Joint work with Junhua Yu)