Dependence logic

Dependence logic is a logical formalism, created by Jouko Väänänen,^[1] which adds dependence atoms to the language of first-order logic. A dependence atom is an expression of the form ${\displaystyle =\!\!(t_{1}\ldots t_{n})}$, where ${\displaystyle t_{1}\ldots t_{n}}$ are terms, and corresponds to the statement that the value of ${\displaystyle t_{n}}$ is functionally dependent on the values of ${\displaystyle t_{1},\ldots ,t_{n-1}}$.

Dependence logic is a logic of imperfect information, like branching quantifier logic or independence-friendly logic (IF logic): in other words, its game-theoretic semantics can be obtained from that of first-order logic by restricting the availability of information to the players, thus allowing for non-linearly ordered patterns of dependence and independence between variables. However, dependence logic differs from these logics in that it separates the notions of dependence and independence from the notion of quantification.