Trustworthy Systems

Mechanised modal model theory

Authors

Michael Norrish and Yiming Xu

DATA61

ANU

Australian National University

Abstract

In this paper, we discuss the formalisation of some fundamental propositional modal model theory. The focus on models is novel: previous work in formalisations of modal logic have centered on proof systems and applications in model-checking. We have formalised a number of fundamental results from the first two chapters of a standard textbook (Blackburn et al.). Among others, one important result, the Van Benthem characterisation theorem, characterizes the connection between modal logic and first order logic. This latter captures the desired saturation property of ultraproduct models on countably incomplete ultrafilters.

BibTeX Entry

  @inproceedings{Norrish_Xu_20,
    address          = {Paris},
    author           = {Norrish, Michael and Xu, Yiming},
    booktitle        = {International Joint Conference on Automated Reasoning},
    date             = {2020-7-1},
    doi              = {https://doi.org/10.1007/978-3-030-51074-9\_30},
    month            = jul,
    pages            = {518-533},
    publisher        = {Springer},
    title            = {Mechanised Modal Model Theory},
    year             = {2020}
  }

Download