• README ⤓ .txt 2026-10-22T165042.936 000000000000624
  Logics whose semantics evaluates a formula not at a single assignment but at a set of them—a team. The shift is not to the truth values, not to an accessibility relation, not to the structural rules, and not to the typing judgment: it is a change in what a formula is evaluated at, and it is what makes dependence, independence, inclusion, and exclusion expressible as atoms rather than as second-order paraphrases.
• Anonymity Logic ⤓ .md 2026-10-22T180154.561 000000000000688
  Jouko Väänänen, "An atom's worth of anonymity" (Logic Journal of the IGPL 31, 2023, 1078–1083, written for John Crossley's birthday), which named the atom, read it as data anonymity, and axiomatized it. The atom itself is Pietro Galliani's non-dependence atom ("The dynamics of imperfect information", PhD thesis, Amsterdam 2012), and it is the afunctional dependency of database theory (Paredaens, De Bra, Gyssens and Van Gucht, The Structure of the Relational Database Model, 1989).
• Branching Quantifiers ⤓ .md 2026-08-20T065006.000 000000000038976
  Leon Henkin, "Some remarks on infinitely long formulas" (1961), which introduced quantifier prefixes arranged in a partial rather than linear order. Ehrenfeucht showed the simplest one is not first-order expressible; Enderton and Walkoe independently settled the expressive power (1970). The construction is the historical root of the team-semantic axis: IF logic and dependence logic both exist to make its dependence pattern statable in linear notation.
• Dependence Logic ⤓ .md 2026-08-20T064918.000 000000000050656
  Jouko Väänänen introduced dependence logic (2007), building on Hintikka's IF logic. Uses team semantics: formulas evaluated on sets of assignments, not single assignments. The dependence atom =(x,y) expresses "y is functionally determined by x." Clean semantics while capturing IF logic's expressiveness. Foundation for a family of logics: independence, inclusion, exclusion.
• Exclusion Logic ⤓ .md 2026-10-22T161354.000 000000000034008
  Pietro Galliani, "Inclusion and exclusion dependencies in team semantics" (Annals of Pure and Applied Logic, 2012), which introduced the exclusion atom alongside the inclusion atom and settled its expressive power in the same paper.
• Inclusion Logic ⤓ .md 2026-10-22T090936.000 000000000038480
  Pietro Galliani, "Inclusion and exclusion dependencies in team semantics" (Annals of Pure and Applied Logic, 2012). First-order logic extended with the inclusion atom, borrowed from the inclusion dependencies of database theory. Its expressive power was settled by Galliani and Hella (2013).
• Independence Logic ⤓ .md 2026-08-20T065157.000 000000000040616
  Erich Grädel and Jouko Väänänen, "Dependence and independence" (Studia Logica, 2013). First-order logic with the independence atom, proposed because dependence logic's downward closure was an artifact of the dependence atom rather than of team semantics — independence is the notion that team semantics was reaching for and could not express.
• Independence-Friendly Logic ⤓ .md 2026-08-20T065043.000 000000000040632
  Jaakko Hintikka and Gabriel Sandu introduced Independence-Friendly (IF) logic (1989, 1996). Extends first-order logic with informationally independent quantifiers. Motivated by game-theoretic semantics: quantifiers as moves in a game where some moves may be made without knowledge of others. Equivalent to existential second-order logic in expressive power.
• Intuitionistic Dependence Logic ⤓ .md 2026-10-22T090631.000 000000000036360
  Samson Abramsky and Jouko Väänänen, "From IF to BI" (Synthese, 2009), which introduced the implication and named the connection it exposes; Fan Yang, "Expressing second-order sentences in intuitionistic dependence logic" (2010), proved the expressive power. The second of the two routes from dependence logic to full second-order logic, and the one nobody expected.
• Modal Dependence Logic ⤓ .md 2026-08-20T022201.000 000000000039064
  Jouko Väänänen, "Modal dependence logic" (in New Perspectives on Games and Interaction, 2008), transposing his 2007 first-order dependence logic to the modal setting. Sevenster (2009) settled the complexity; Ebbing, Lohmann, Hella, Kontinen, Müller, and Vollmer mapped the fragments (2011–2013); Yang and Väänänen (2016) gave the propositional theory.
• Multiteam Semantics ⤓ .md 2026-10-22T180154.561 000000000000720
  Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier and Jonni Virtema, "Approximation and dependence via multiteam semantics" (FoIKS 2016, pp. 271–291; journal version Annals of Mathematics and Artificial Intelligence 83, 2018, pp. 297–320), which defined lax and strict multiteam semantics and the probabilistic inclusion and independence atoms, and the same five authors' "Probabilistic team semantics" (FoIKS 2018, Lecture Notes in Computer Science 10833, pp. 186–206), which replaced multisets by distributions. Teams with measure predate the names: Tapani Hyttinen, Gianluca Paolini and Jouko Väänänen, "Quantum team logic and Bell's inequalities" (Review of Symbolic Logic 8, 2015, pp. 722–742) reasoned about probabilities of first-order formulas in measure teams, and probabilistic variants of dependence and IF logic had been studied by Galliani, Mann, Sevenster and Sandu. Erich Grädel and Richard Wilke, "Logics with multiteam semantics" (ACM Transactions on Computational Logic 23(2), 2022) is the systematic development on the multiset side.
• Team Logic ⤓ .md 2026-10-22T180154.561 000000000000648
  Jouko Väänänen, Dependence Logic (2007), §8, where it appears as the closure of dependence logic under a genuine negation; Juha Kontinen and Ville Nurmi, "Team logic and second-order logic" (2009), settled its expressive power. The system exists to answer an obvious question: dependence logic's negation is the game-theoretic dual, so what happens if you add the contradictory one?
• CRITERIA ⤓ .txt 2026-07-16T000538.000 000000000013728
  Not sufficient: A Kripke semantics, in which a formula is evaluated at a world and the set of worlds is the model rather than the object of evaluation (that belongs in Modal). The test is where the formula is evaluated, not what the elements are: a modal logic whose formulas are evaluated at a *set* of worlds, with atoms constraining that set, is a team-semantic logic whose elements happen to be worlds, and belongs here cross-listed with Modal. A many-valued or degree semantics (Algebraic). Branching quantifiers presented only as an abbreviation in existential second-order logic, without a team-semantic evaluation.