A Tableau System for Instantial Neighborhood Logic

  • Junhua YuEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10703)


Extending classical propositional logic, instantial neighborhood logic (\(\mathsf {INL}\)) employs formulas like \(\Box (\alpha _1,...,\alpha _j;\alpha _0)\). The intended meaning of such a formula is: there is a neighborhood (of the current point) in which \(\alpha _0\) universally holds and none of \(\alpha _1,...,\alpha _j\) universally fails. This paper offers to \(\mathsf {INL}\) a tableau system that supports mechanical proof/counter-model search.


Neighborhood logic Tableau 



The tableau system introduced in this paper was invented by the author during his January 2015 visit to University of Amsterdam, where he was led by Johan van Benthem and Nick Bezhanishvili to the field of neighborhood logic. Four anonymous referees have offered helpful suggestions to the initial submission of this paper.


  1. 1.
    Beth, E.W.: Semantic Entailment and Formal Derivability. Mededelingen van de Koninklijke Nederlandske Akademie van Wetenschappen, vol. 18, no. 13, pp. 309–342 (1955)Google Scholar
  2. 2.
    ten Cate, B., Gabelaia, D., Sustretov, D.: Modal languages for topology: expressivity and definability. Ann. Pure Appl. Log. 159(1), 146–170 (2006)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Chagrov, A., Zakharyashche, M.: Modal Logic. Oxford Science Publications, Oxford (1997)Google Scholar
  4. 4.
    Chellas, B.F.: Modal Logic - An Introduction. Cambridge University Press, Cambridge (1980)CrossRefzbMATHGoogle Scholar
  5. 5.
    D’Agostino, M.: Tableau methods for classical propositional logic. In: [6]Google Scholar
  6. 6.
    D’Agostino, M., Gabbay, D.M., Hähnle, R., Posegga, J. (eds.): Handbook of Tableau Methods. Kluwer Academic Publisher, Dordrecht (1999)zbMATHGoogle Scholar
  7. 7.
    Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. D. Reidel, Dordrecht (1983)CrossRefzbMATHGoogle Scholar
  8. 8.
    Fitting, M.: Introduction. In: [6]Google Scholar
  9. 9.
    Fitting, M.: Types, Tableaus, and Gödel’s God. Kluwer Academic Publisher, Dordrecht (2002)CrossRefzbMATHGoogle Scholar
  10. 10.
    Hintikka, J.: Two papers on symbolic logic: form and content in quanlification thoery. Acta Philos. Fenn. 8, 8–55 (1955)Google Scholar
  11. 11.
    Lis, Z.: Wynikanie semantyczne a wynikanie fonnalne. Stud. Log. 10, 39–60 (1960). (in Polish)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Pacuit, E.: Neighborhood semantics for modal logic - An introduction. ESSLLI 2007 course notes (2007)Google Scholar
  13. 13.
    Smullyan, R.: First-Order Logic. Springer, Heidelberg (1968)CrossRefzbMATHGoogle Scholar
  14. 14.
    van Benthem, J., Bezhanishvili, N., Enqvist, S., Yu, J.: Instantial neighbourhood logic. Rev. Symb. Log. 10(1), 116–144 (2017)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Yu, J.: Lyndon interpolation theorem of instantial neighborhood logic - constructively via a sequent calculus (submitted)Google Scholar

Copyright information

© Springer International Publishing AG 2018

Authors and Affiliations

  1. 1.Department of PhilosophyTsinghua UniversityBeijingChina

Personalised recommendations