Dependence logic

Dependence logic is a logical formalism, created by Jouko Väänänen, 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.

The syntax of dependence logic is an extension of that of first-order logic. For a fixed signature σ = (S_func, S_rel, ar), the set of all well-formed dependence logic formulas is defined according to the following rules:

Terms in dependence logic are defined precisely as in first-order logic.

There are three types of atomic formulas in dependence logic:

Nothing else is an atomic formula of dependence logic.

Relational and equality atoms are also called first-order atoms.

For a fixed signature σ, the set of all formulas ${\displaystyle \phi }$ of dependence logic and their respective sets of free variables ${\displaystyle {\mbox{Free}}(\phi )}$ are defined as follows: