4月1日，杨帆教授作了题为《A complete logic for first-order team properties》的报告。

　　In this talk, Prof. Fan Yang introduce a complete logic for first-order team properties. First, Prof. Yang introduces the history and definition of team semantics. Historically, team semantics was related with the characterization of dependencies among quantified variables. It also has connection with database theory as a team can be viewed as a relational database. Formally speaking, a team is a set of assignment w.r.t the domain of a given model $M$, and is essentially . Under this definition, the team semantics according to teams of first-order logic is given. Instead of focusing on single assignment, the satisfaction of a formula is considered over a set of assignment under team semantics, for example, given an atom , a model satisfies the atom (under team semantics) iff  atom is satisfied by the model for every assignment in the team under the usual first-order semantics. It can be observe that a team X of an first-order model over a finite domain of variables (which contains k variables)can  be viewed as a k-ary relation. A set of teams is called a (local) team property. We call a team property first-order if there is a first-order sentence that defines it. In this sense, Prof. Yang introduce the core part of the lecture, a logic based on team semantics and defines all first-order team properties, called FOT, which contains first-order atoms,  weakened negation, weakened disjunction and quantifiers defined for team semantics. Then Prof. Yang shows  that FOT characterized exactly the first-order team properties. A complete axiomatization of FOT is also given in sequent style. Finally, Prof. Yang gives several application for FOT:

　　1.Database theory: Data dependency notions, such as Armstrong's axioms for functional dependencies, can be formalized in FOT;

　　2. Social choice: Arrow's Theorem can be formalized and derived in FOT.

——唐闻