Foundations for team semantics: Meaning in an enriched framework
The project aims to develop new semantics for a variety of logics including temporal logics used for program verification. The goal is to provide a classification of principles that guide team semantics, a relatively new perspective of formal language which greatly enlarges applicability of formal methods to reasoning about meaning and interpretation. The findings of the investigation will in turn be utilised to shed light on the most basic question of all in logic: What is logic and which operators should be considered as part of the logical language?
Team semantics generalizes the standard Tarskian model theoretic semantics for formal languages. Lifting the semantics from the level of single assignments to that of sets of assignments, or teams, it offers a unified framework for a broad class of semantical intuitions that manifest database theory, semantics of questions, program specification and verification, uncertainty, probabilities, and quantum physics.
In the fast-growing literature on team semantics, a basic foundational conservativeness principle, called flatness, is often taken as a guiding principle. Some have argued for the naturalness and correctness of this principle. Recently, however, emergence of several non-flat semantics raised the question of whether flatness is indeed forced.
In this project we will develop new non-flat team semantics for a variety of logics including temporal logics used for program verification. This will be the starting point for a critical and open-minded investigation of the arguments for, and against, flatness. Our goal is to provide a classification of principles that guide team semantics. We will further use our findings to shed light on the most basic question of all: What is logic and which operators should be considered as part of the logical language?