Concrete models for modal logics via proof theory
| Title | Concrete models for modal logics via proof theory |
| Publication Type | Miscellaneous |
| Year of Publication | 2014 |
| Authors | López Pombo, CG, Maibaum, TSE |
| Keywords | Abstract and Concrete Model Theory, Semantics, Software specification |
| Abstract | Logic has proved essential as a formal tool for describing, and then reasoning about, different aspects of the world we perceive or wish to build. The formal modelling of software artefacts is a concrete and widely accepted example of its usefulness. Formal descriptions of software artefacts, frequently called specifications, have served not only as requirements documentation and formalisation, but also for proving desirable properties of the software systems being described. Logic is usually studied in terms of two of its inherent aspects: syntax and semantics. The latter is an integral part of logic for two ultimately important reasons. On the one hand, producing logical descriptions of real-world phenomena requires people to agree on how these descriptions must be interpreted and understood, and, on the other hand, it provides a metalogical characterization of the reach and the limitations of the tools we build and use to analyse these logical descriptions. Model theory has provided the cornerstone for the satisfaction of these needs. Firstly, a particular model provides an explicit interpretation of the so called extralogical symbols of the specification. In this way, classes of models provide the range of possible interpretations for the extralogical symbols appearing in a signature. The class of all models then provides an interpretation of the so called logical symbols, i.e., those that have an invariant behaviour across all models. Of course, different classes of models have different metalogical properties; moreover, they determine important aspects regarding the conclusions we can extract from the application of different analysis techniques. In this paper we rationalise the link between these two aspects of semantics, while providing a general approach for the practical use of models in computer science, applied to the case of modal logics. We do this by replacing the usual platonic notion of model by a purely syntactic version, formalising what we normally do in any case to describe models and to make them amenable for processing by electronic means. |
Work Package:
WP5
