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.

Syntax

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

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

Atomic formulas

There are three types of atomic formulas in dependence logic:

1. A relational atom is an expression of the form ${\displaystyle Rt_{1}\ldots t_{n}}$ for any n-ary relation ${\displaystyle R}$ in our signature and for any n-tuple of terms ${\displaystyle (t_{1},\ldots ,t_{n})}$;
2. An equality atom is an expression of the form ${\displaystyle t_{1}=t_{2}}$, for any two terms ${\displaystyle t_{1}}$ and ${\displaystyle t_{2}}$;
3. A dependence atom is an expression of the form ${\displaystyle =\!\!(t_{1}\ldots t_{n})}$, for any ${\displaystyle n\in \mathbb {N} }$ and for any n-tuple of terms ${\displaystyle (t_{1},\ldots ,t_{n})}$.

Nothing else is an atomic formula of dependence logic.

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

Complex formulas and sentences

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:

1. Any atomic formula ${\displaystyle \phi }$ is a formula, and ${\displaystyle {\mbox{Free}}(\phi )}$ is the set of all variables occurring in it;
2. If ${\displaystyle \phi }$ is a formula, so is ${\displaystyle \lnot \phi }$ and ${\displaystyle {\mbox{Free}}(\lnot \phi )={\mbox{Free}}(\phi )}$;
3. If ${\displaystyle \phi }$ and ${\displaystyle \psi }$ are formulas, so is ${\displaystyle \phi \vee \psi }$ and ${\displaystyle {\mbox{Free}}(\phi \vee \psi )={\mbox{Free}}(\phi )\cup {\mbox{Free}}(\psi )}$;
4. If ${\displaystyle \phi }$ is a formula and ${\displaystyle x}$ is a variable, ${\displaystyle \exists x\phi }$ is also a formula and ${\displaystyle {\mbox{Free}}(\exists v\phi )={\mbox{Free}}(\phi )\backslash \{v\}}$.

Nothing is a dependence logic formula unless it can be obtained through a finite number of applications of these four rules.

A formula ${\displaystyle \mathrm{\varphi <!--\; \varphi \; -->}}$Zdroj:https://en.wikipedia.org?pojem=Dependence_logic
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.