Program

Jouko Väänänen, Team semantics—an introduction

I will review some of the basic ideas and concepts of team semantics and logics based on it, as well as problems they give rise to.

Samson Abramsky, The Logic of Quantum Paradoxes

Quantum “paradoxes” - features which defy classical explanation - occur in a bewildering variety of forms: probabilistic arguments such as Bell’s theorem and Bell inequalities, “possibilistic” arguments such as the Hardy paradox and the GHZ construction, the Kochen-Specker theorem and Kochen-Specker paradoxes - classical tautologies which can be falsified in quantum structures - and more. It is these very paradoxical and non-classical features which lie at the heart of quantum advantage in information processing and computational tasks.

A first task for a systematic theory is to unify these phenomena in a single coherent framework.

This is achieved in the sheaf-theoretic approach to contextuality, introduced by Abamsky and Brandenburger in 2011. The common pattern is that we have a locally consistent family of data which is not globally consistent - there is an obstruction to forming a global section. This subsumes traditional hidden variable theories or ontolgogical models, and by varying the underlying presheaf - in particular the distributions functor - the various probabilistic and possibilistic forms of contextuality are recovered.

This analysis also reveals a hierarchy of contextuality: there are different levels of contextuality,

probabilistic < logical < strong.

Moreover, if algebraic structure on the outcomes is taken into account, then a further level of “All-versus-Nothing” contextuality can be distinguished. If furthermore algebraic structure is considered on the observables/measurements themselves, we get a structural account of state-independent contextuality.

At this level, we can also systematically relate paradoxes based on algebraic structure, the paradigmatic example being the Peres-Mermin magic square, to logical Kochen-Specker paradoxes. This leads to a further distinction, between linear and non-linear (more orecisely affine and non-affine) Kochen-Specker paradoxes. The mod-2 affine part of Boolean algebra (generated by exclusive or and True) already suffices to express Kochen-Specker paradoxes over Hilbert spaces of dimension 4 and higher. The three dimensional case is special, and needs non-linear connectives.

Fausto Barbero, Indeterministic counterfactuals on causal teams

Interventionist counterfactuals are expressions of the form “If such and such variables had been set to such and such values, then condition phi would hold”. Their importance stems from the fact that many causal concepts are definable in terms of them.

Halpern (2000) briefly suggested extending causal models so that they may represent also indeterministic (or possibilistic) causal laws, such as the fact that a tossed coin will (typically) land on heads on tails. Developing a concrete semantics for counterfactuals in this context presents some new challenges, some of which I will point out. I will propose a notion of model based on the causal team semantics of Barbero and Sandu (2020) and present complete axiomatizations for languages of unnested and right-nested counterfactuals in a number of significant classes of model. I will then compare these proof systems to the classical complete systems for the deterministic case.

Miika Hannula, Dependencies in K-relations

K-relations (or K-teams) are ordinary relations whose tuples are associated with values from some algebraic structure, such as a semiring. Such K-relations provide a uniform way to model e.g. ordinary relations,  probability distributions, and more generally annotated data, where the annotations capture multiplicity, provenance, uncertainty, or cost. In team semantics, K-relations offer a unifying perspective to team semantics, multiteam semantics, and probabilistic team semantics. In this talk we consider dependency notions such as inclusion dependencies and conditional independence. In particular, we investigate how the axiomatic properties extend from the relational and probabilistic settings to K-relations, and how these properties depend on the underlying algebraic structure of K.

Nicolas Fröhlich, Complexity of Logics with Semiring Semantics

We study the expressive power and computational properties of first-order logic and its extensions under the semiring semantics originating from the seminal work of Green, Karvounarakis, and Tannen. While semiring semantics is currently extensively used, e.g., in the study of provenance in database theory and description logic, a comprehensive computational analysis of these logics acting over general semirings is still lacking. The expressivity and complexity of model-checking of first-order formulae in this framework are analysed, providing characterizations in terms of generalized Blum–Shub–Smale machines over semirings. A variant of Fagin's theorem is also shown, i.e., a logical characterization of nondeterministic polynomial time over semirings using a version of existential second-order logic. Furthermore, Cook's theorem is generalized for the semiring framework, showing that propositional satisfiability in the semiring semantics is complete for this notion of NP.

Minna Hirvonen, Independence Under Incomplete Information

We initiate an investigation how the fundamental concept of independence can be represented effectively in the presence of incomplete information in relational databases. The concepts of possible and certain independence are proposed, and first results regarding the axiomatisability and computational complexity of implication problems associated with these concepts are established. In addition, several results for the data and the combined complexity of model checking are presented. The findings help reduce computational overheads associated with the processing of updates and answering of queries.

Jonni Virtema, Negative probabilities, locally consistent families, axioms of FDs, and all that

Local consistency arises in diverse areas, including Bayesian statistics, relational databases, and quantum foundations, and so does the notion of functional dependence. In this talk, I give a short recap how previous generalisations of team semantics lead to (locally consistent) families of K-relations, where K is a positive commutative monoid. I then show how functional dependencies (FDs) behave in this setting. In particular, I consider how Amstrong's axioms of FDs need to be adapted, and consider the complexity of the related entailment problem. Notably, the transitivity rule for FDs is no longer sound, but can be replaced by two novel axiom schemas.  I present a complete axiomatisation for the entailment of unary FDs and discuss it's complexity. I conclude with open problems and directions for future work.

Fan Yang, Possible and impossible conditionals in team semantics

Logics based on team semantics are typically extensions of classical logic and thus inherit classical implication over classical formulas. However, the earliest versions of team-based logic, such as independence-friendly logic and dependence logic, do not include a conditional connective for arbitrary formulas. An adequate conditional, known as intuitionistic implication, was proposed for dependence logic by Abramsky and Väänänen (2009). This connective is also part of the syntax of inquisitive logic. Intuitionistic implication behaves well in these downward closed logics, in the sene that it preserves downward closure and satisfies both Modus Ponens and the Deduction Theorem.

In recent years, team logics with different closure properties have received increasing attention, including union closed and convex logics. In these settings, the intuitionistic implication no longer behaves well, as it either fails to preserve the relevant closure property or fails to satisfy the Deduction Theorem. In this talk, we show that this failure is unavoidable: these logics cannot be enriched with any conditional connective that simultaneously preserves the closure property and satisfies both Modus Ponens and the Deduction Theorem.

This is joint work with Fausto Barbero.

Pietro Galliani, Looking for Strongly First Order Dependencies

Some dependencies do not increase the expressive power of First Order Logic with Team Semantics when added to it, while others do. In this talk, I will discuss a number of results that characterize the class of "safe" dependencies for First Order Logic modulo various restrictions, and I will argue that studying this question (as well as similar ones starting from different choices of "base logics") provide a natural and still largely open avenue for studying the expressive capabilities of Team Semantics. 

Aleksi Anttila, Bisimulations and Expressive Completeness for Strict Inclusion Logics

Modal inclusion logic is a logic with team semantics that extends standard modal logic with inclusion atoms—team-based atoms which correspond to the inclusion dependencies of relational database theory. Propositional inclusion logic similarly extends classical propositional logic with inclusion atoms. There are two variants of each of these logics in the literature, with distinct semantics for the disjunction and the diamond: lax and strict (modal/propositional) inclusion logic. We develop notions of bisimulation and simulation that characterize the expressive power of strict modal and propositional inclusion logic, and use these notions to prove Ehrenfeucht-Fraïssé and expressive completeness theorems for these logics.

Joni Puljujärvi, On Infinite Model Theory of Team Semantics

One might argue that most research on team semantics has been finite model theory flavoured. However, independence logic, having the expressive power of existential second-order logic, is an interesting extension of first-order logic and many good questions in the realm of infinite model theory can be asked about it. We introduce a framework for studying team semantics in a way that is reminiscent of abstract elementary classes of Shelah. The basis for our study is the notion of an elementary team map that maps teams of one structure to teams of another. This is joint-work with Tapani Hyttinen and Davide Quadrellaro.

Matilda Häggblom, We might be upward closed

We examine upwards closed variants of propositional team-based logics in relation to their expressive power. Our main tool to reach the desired expressivity is to use might modalities. In the upward closed setting, a curious equivalence between connectives can be observed, namely that the split disjunction coincides with the conjunction. This reflects the free-choice inference from 'You may have coffee or tea' to 'You may have coffee, and you may have tea'. By relaxing the upward closure condition and modifying the might modalities slightly, we obtain a quasi upward closed logic with the empty team property. In this setting, it is instead the split disjunction and global disjunction that coincide. 

Kerkko Luosto, Dimensions as logical resources

Dimensions are a relatively new tool, compared to some more traditional logical resources such as quantifier rank or the number of variables, to study the expressive power of logics. The idea is that, both in variants of modal team logic and of dependence logic, the teams satisfying a given formula in a given structure gives rise to a family of teams, the complexity of which can be studied by combinatorial means. In this context, the upper dimension, the dual upper dimension, and the cylindrical dimension are measures of the complexity of such a family of teams.

I shall survey some results with this theme. The presentation is mainly based on my works with Lauri Hella, Katsuhiko Sano and Jonni Virtema, on one hand, and with Lauri Hella and Jouko Väänänen, on the other hand.

Arne Meier, Synchronous Team Semantics for Temporal Logics

We present team semantics for two of the most important linear and branching time specification languages, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). With team semantics, LTL is able to express hyperproperties, which have in the last decade been identified as a key concept in the verification of information flow properties. We study basic properties of the logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of the basic logic react to adding additional atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL with team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties. For CTL with team semantics, we investigate the computational complexity of the satisfiability and model checking problem. The satisfiability problem is shown to be EXPTIME-complete while we show that model checking is PSPACE-complete.

This is joint work with Andreas Krebs, Jonni Virtema, and Martin Zimmermann

Phokion Kolaitis, On Disjunctions of Two Dependence Atoms

On finite structures, it is well known that dependence logic captures NP, hence there are sentences of dependence logic whose model-checking problem is NP-complete. In fact, it is known that there are disjunctions of three dependence atoms whose model-checking problem is NP-complete. Motivated from considerations in database theory, we study the model-checking problem for disjunctions of two unary dependence atoms and establish a trichotomy theorem, namely, for every such formula, one of the following is true for its model-checking problem: (i) it is NLOGSPACE-complete; (ii) it is LOGSPACE-complete; (iii) it is first-order definable (hence, in AC0). Furthermore, we classify the complexity of the model-checking problem for disjunctions of two arbitrary dependence atoms, and also characterize when such a disjunction is coherent,  i.e., when it satisfies a certain small-model property. 

This is joint work with Nicolas Fröhlich and Arne Meier at the Leibniz University of Hannover.

Åsa Hirvonen, Continuous dependence logic

When the data in a team comes with a metric (as for, e.g., real valued outcomes of physical measurements), dependence alone may say too little. If you only know position depends on time, but not how, and your team contains a row for some given time t, dependence alone cannot tell you what the position will be a fraction of a second later. This motivates for the study of continuous or even uniformly continuous dependences.

Baltag and van Benthem have studied continuous and uniformly continuous dependences from an epistemic point of view, and built logics for dependences and knowability modalities stemming from the dependences. I investigate the same dependences, but take another approach to the logic, using the [0,1]-valued continuous logic developed by Ben Yaacov and Usvyatsov in the beginning of this century, and based on Chang's and Keisler's more general continuous model theory from the 60's.

Since continuous logic allows for any continuous connectives, there is not a canonical generalisation of team semantics to a continuous setting. I present a suggestion for continuous dependence logic that captures the idea of dependence logic as a positive logic, and show how, over suitable models, it can be viewed as a fragment of continuous existential second order logic.

Fredrik Engström, Substitutional Logics of Teams

Standard team semantics, as used in Dependence and Independence Logic, is inherently non-substitutional due to the mismatch between the denotations of atomic formulas and complex formulas. This limits the applicability of algebraic methods.

A general framework for constructing substitutional logics of teams via algebraic semantics is developed. In the propositional case, formulas are interpreted as elements of powerset algebras over Boolean algebras, equipped with both external (set-theoretic) and internal (pointwise) operations. This yields a substitutional entailment relation defined via homomorphisms, together with a sound and complete labelled natural deduction system. Moreover, standard dependence-based propositional team logics can be recovered and axiomatized as fragments of this framework.

At the first-order level, where the connection to algebraic semantics is less direct, predicate symbols are instead interpreted as sets of relations, aligning the denotations of atomic and complex formulas. This restores substitutionality while preserving the expressive power of team semantics, allowing standard logics such as Dependence Logic to be recovered as definable fragments.