Speaker: Fan Yang (University of Helsinki)
Date and Time: Thursday, May 9th 2019, 16:30-18:00
Venue: ILLC Seminar Room F1.15, Science Park 107.
Title: Logics for first-order team properties.
Abstract. Team semantics is a semantical framework originally introduced by Hodges [1997] for the study of various dependence and independence concepts, and later systematically developed by Väänänen [2007] with the introduction of dependence logic (D). Other prominent logics based on team semantics include independence logic (Ind) [Grädel, Väänänen 2013], inclusion logic [Galliani 2012], etc. In team semantics formulas are evaluated in a model over sets of assignments (called teams) rather than single assignments as in the usual first-order logic. Teams are essentially relations, and thus open formulas define team properties. In general, knowing the expressive power of a logic for sentences (with no free variables) does not automatically give a characterization for the expressive power of open formulas of the same logic. Such a peculiar phenomenon has sparked several studies on the expressive power of logics based on team semantics. In particular, while D and Ind are both equivalent to existential second-order logic (ESO) on the level of sentences, it turns out that open formulas of Ind characterize all ESO team properties [Galliani 2012], whereas the former characterize only downward closed ESO team properties [Kontinen, Väänänen 2009]. In this talk, we introduce a logic, denoted by FOT, whose expressive power coincides with first-order logic both on the level of sentences and on the level of open formulas (in the sense that open formulas of FOT characterize exactly first-order definable team properties). We also show, as an application of Lyndon’s Interpolation Theorem, that a natural fragment of FOT captures downward closed first-order definable team properties.
In the second part of the talk, we define a system of natural deduction for FOT, and show that it is sound and complete. We also discuss some applications of our logic. In particular, we demonstrate that Arrow’s Theorem in social choice can be formalized in FOT, and Armstrong’s axioms for functional dependencies in database theory can be derived in our system of FOT.
(This talk is based on joint work with Juha Kontinen.)