• README ⤓ .txt 2026-07-17T121634.146 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.
• Branching Quantifiers ⤓ .md 2026-07-15T230335.000 000000000028184
  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-07-16T004347.000 000000000034960
  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-07-15T230256.000 000000000021552
  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-07-15T230256.000 000000000025904
  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-07-15T230335.000 000000000026656
  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-07-15T054955.000 000000000026128
  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-07-16T004347.000 000000000033240
  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-07-17T120407.600 000000000000744
  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.
• Team Logic ⤓ .md 2026-07-16T004347.000 000000000030480
  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-17T120407.600 000000000000640
  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.