Logics with Multiteam SemanticsCopyright: Stefan Hense
Classical logics model queries on structures such as graphs, groups, databases and so on. They are usually evaluated via so called Tarski-style semantics. That means during the evaluation process we use an assignment, that is a function mapping each free variable of the current subformula to its value, an element of the target structure. There might be multiple assignments one can use in this process, and there is no way of letting these communicate with each other, as the evaluation processes are independent of each other. In the game semantical sense one can think of such an assignment as a play in the model-checking game, that is the path taken by both players when they choose which value a variable should be assigned in order to prove that the formula is satisfied, or not, depending on the player. Classically one is only interested in the question if there exists a winning strategy for one of the players, because this shows whether the given formula is satisfied by the structure at hand. Analysing these games one can find dependencies between variables, that cannot be expressed in classical logics. For example we could find out that one player can only win if she adapts her move depending on the previous move by her opponent. As said before, a move can be thought of as selecting a value for a variable. Historically many attempts to define logics that are able to speak about dependencies between variables have been made. Such logics are sometimes called logics of imperfect information, and (besides others) originated in the work of Henkin, Enderton and Walkoe. Initially the semantics of these logics were defined in a top down manner, meaning that one cannot infer anything about the formula just from looking at its subformulae. One example is independence friendly logic (IF), proposed by Hintikka and Sandu, where quantifiers are restricted in such a way that only the knowledge about certain variables can be used to determine next value. In the model-checking game this means a player must be able to choose a value without knowing which values the other player has picked for certain variables. Another example are Henkin quantifiers, which can be interpreted as parallel classical quantifiers. It was conjectured that the semantics of these logics cannot be defined in a compositional fashion, but 1997 Hodges has disproven this informal conjecture by providing a model-theoretic semantics for IF-logic in terms of what he called trumps. Today this semantics is called team semantics and it enabled Väänänen to propose a new logic called dependence logic. The main idea is that dependencies are treated as atomic properties. Therefore one has to collect all information about the variables, resulting in a set of assignments, in contrast to the classical case. Such a set is called a team. On the atomic level we can evaluate a dependence or independence statement by looking at the team arriving at it, whence giving us a bottom up semantics. A quantifier no longer provides a single value to a variable, but rather induces a set of values. Grädel and Väänänen introduced independence logic which interestingly corresponds precisely to the complexity class NP in terms of expressive power (over finite structures), that is existential second order logic. There have been many extensions of logics with team semantics, most of which share a single weakness: A team is viewed as a set of assignments, hence ignoring the number of occurrences of each assignment. While this is appealing in many theoretical settings, it fails to give a good description of real-world scenarios. One can easily think of examples where not only the existence, but rather the number of assignments matters, e.g. in voting. The goal of this project is to augment dependence logics with the ability to handle multiplicities. Our approach is to consider multisets instead of set of assignments, resulting in logics with multiteam semantics. These will for example be able to express statistical dependencies between data. One can also think of a multiteam as a way to incorporate uncertainty in logic, since it allows us to make statements on which portion of the (input) multiteam satisfies a certain criterion.