Dependence logic


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 =\!\!(t_1 \ldots t_n), where t_1 \ldots t_n are terms, and corresponds to the statement that the value of \!t_n is functionally dependent on the values of t_1\ldots t_{n-1}.

Dependence logic is a logic of imperfect information, like branching quantifier logic or independence-friendly 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.

Contents

Syntax

The syntax of dependence logic is an extension of that of first-order logic. For a fixed signature σ = (Sfunc, Srel, 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 Rt_1 \ldots t_n for any n-ary relation \!R in our signature and for any n-uple of terms t_1 \ldots t_n;
  2. An equality atom is an expression of the form \!t_1 = t_2, for any two terms \!t_1 and \!t_2;
  3. A dependence atom is an expression of the form =\!\!(t_1 \ldots t_n), for any n \in \mathbb N and for any n-uple of terms 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 \!\phi of dependence logic and their respective sets of free variables Free(ϕ) are defined as follows:

  1. Any atomic formula \!\phi is a formula, and Free(ϕ) is the set of all variables occurring in it;
  2. If \!\phi is a formula, so is \lnot \phi and \mbox{Free}(\lnot\phi) = \mbox{Free}(\phi);
  3. If \!\phi and \!\psi are formulas, so is \!\phi \vee \psi and \mbox{Free}(\phi \vee \psi) = \mbox{Free}(\phi) \cup \mbox{Free}(\psi);
  4. If \!\phi is a formula and \!x is a variable, \!\exists x \phi is also a formula and \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 \!\phi such that \mbox{Free}(\phi) = \emptyset is a sentence of dependence logic.

Conjunction and universal quantification

In the above presentation of the syntax of dependence logic, conjunction and universal quantification are not treated as primitive operators; rather, they are defined in terms of disjunction and negation and existential quantification respectively, by means of De Morgan's Laws.

Therefore, \!\phi \wedge \psi is taken as a shorthand for \!\lnot (\lnot \phi \vee \lnot \psi), and \!\forall x \phi is taken as a shorthand for \!\lnot(\exists x (\lnot \phi)).

Semantics

The team semantics for dependence logic is a variant of Wilfrid Hodges' compositional semantics for IF logic.[2][3] There exist equivalent game-theoretic semantics for dependence logic, both in terms of imperfect information games and in terms of perfect information games.

Teams

Let \!\mathcal A = (A, \sigma, I) be a first-order structure and let V = \{v_1 \ldots v_n\} be a finite set of variables. Then a team over \!\mathcal A with domain \!V is a set of assignments over \!\mathcal A with domain \!V, that is, a set of functions \!\mu from \!V to \!A.

It may be helpful to visualize such a team as a database relation with attributes v_1 \ldots v_n and with only one data type, corresponding to the domain \!A of the structure: for example, if the team \!X consists of four assignments \!\mu_1 \ldots \mu_4 with domain \!\{v_1, v_2, v_3\} then one may represent it as the relation

\!v_1 \!v_2 \!v_3
\!\mu_1 \!\mu_1(v_1) \!\mu_1(v_2) \!\mu_1(v_3)
\!\mu_2 \!\mu_2(v_1) \!\mu_2(v_2) \!\mu_2(v_3)
\!\mu_3 \!\mu_3(v_1) \!\mu_3(v_2) \!\mu_3(v_3)
\!\mu_4 \!\mu_4(v_1) \!\mu_4(v_2) \!\mu_4(v_3)

Positive and negative satisfaction

Team semantics can be defined in terms of two relations \!\mathcal T and \mathcal C between structures, teams and formulas.

Given a structure \mathcal A, a team X over it and a dependence logic formula \!\phi whose free variables are contained in the domain of \!\!X, if \!(\mathcal A, X, \phi) \in \mathcal T we say that \!X is a trump for \!\phi in \!\mathcal A, and we write that \!\mathcal A \models_X^+ \phi; and analogously, if \!(\mathcal A, X, \phi) \in \mathcal C we say that \!X is a cotrump for \!\phi in \!\mathcal A, and we write that \!\mathcal A \models_X^- \phi.

If \!\mathcal A \models_X^+ \phi one can also say that \!\phi is positively satisfied by \!X in \mathcal A, and if instead \!\mathcal A \models_X^- \phi one can say that \!\phi is negatively satisfied by \!X in \mathcal A.

The necessity of considering positive and negative satisfaction separately is a consequence of the fact that in dependence logic, as in the logic of branching quantifiers or in IF logic, the law of the excluded middle does not hold; alternatively, one may assume that all formulas are in negation normal form, using De Morgan's relations in order to define universal quantification and conjunction from existential quantification and disjunction respectively, and consider positive satisfaction alone.

Given a sentence \!\phi, we say that \!\phi is true in \!\mathcal A if and only if \!\mathcal A \models_{\{\emptyset\}}^+ \phi, and we say that \!\phi is false in \!\mathcal A if and only if \!\mathcal A \models_{\{\emptyset\}}^- \phi.

Semantic rules

As for the case of Alfred Tarski's satisfiability relation for first-order formulas, the positive and negative satisfiability relations of the team semantics for dependence logic are defined by structural induction over the formulas of the language. Since the negation operator interchanges positive and negative satisfiability, the two inductions corresponding to \!\models^+ and \!\models^- need to be performed simultaneously:

Positive satisfiability

  1. \!\mathcal A \models_X^+ R t_1 \ldots t_n if and only if
    1. \!R is a n-ary symbol in the signature of \!\mathcal A;
    2. All variables occurring in the terms \!t_1 \ldots t_n are in the domain of \!X;
    3. For every assignment \!\mu \in X, the evaluation of the tuple \!(t_1 \ldots t_n) according to \!\mu is in the interpretation of \!R in \!\mathcal A;
  2. \!\mathcal A \models_X^+ t_1 = t_2 if and only if
    1. All variables occurring in the terms \!t_1 and \!t_2 are in the domain of \!X;
    2. For every assignment \!\mu \in X, the evaluations of \!t_1 and \!t_2 according to \!\mathcal A are the same;
  3. \!\mathcal A \models_X^+ =\!\!(t_1 \ldots t_n) if and only if any two assignments \!s, s' \in X whose evaluations of the tuple \!(t_1 \ldots t_{n-1}) coincide assign the same value to \!t_n;
  4. \!\mathcal A \models_X^+ \lnot \phi if and only if \!\mathcal A \models_X^- \phi;
  5. \!\mathcal A \models_X^+ \phi \vee \psi if and only if there exist teams \!Y and \!Z such that
    1. X = Y \cup Z'
    2. \!\mathcal A \models_Y^+ \phi;
    3. \!\mathcal A \models_Z^+ \psi;
  6. \!\mathcal A \models_X^+ \exists x \phi if and only if there exists a function \!F from \!X to the domain of \!\mathcal A such that \!\mathcal A \models_{X[F/x]}^+ \phi, where \!X[F/x] = \{ s[F(s)/x] : s \in X\}.

Negative satisfiability

  1. \!\mathcal A \models_X^- R t_1 \ldots t_n if and only if
    1. \!R is a n-ary symbol in the signature of \!\mathcal A;
    2. All variables occurring in the terms \!t_1 \ldots t_n are in the domain of \!X;
    3. For every assignment \!\mu \in X, the evaluation of the tuple \!(t_1 \ldots t_n) according to \!\mu is not in the interpretation of \!R in \!\mathcal A;
  2. \!\mathcal A \models_X^- t_1 = t_2 if and only if
    1. All variables occurring in the terms \!t_1 and \!t_2 are in the domain of \!X;
    2. For every assignment \!\mu \in X, the evaluations of \!t_1 and \!t_2 according to \!\mathcal A are different;
  3. \!\mathcal A \models_X^- =\!\!(t_1 \ldots t_n) if and only if \!X is the empty team;
  4. \!\mathcal A \models_X^- \lnot \phi if and only if \!\mathcal A \models_X^+ \phi;
  5. \!\mathcal A \models_X^- \phi \vee \psi if and only if \!\mathcal A \models_X^- \phi and \!\mathcal A \models_X^- \psi;
  6. \!\mathcal A \models_X^- \exists x \phi if and only if \!\mathcal A \models_{X[A/x]}^- \phi, where \!X[A/x] = \{ s[m/x] : s \in A\} and \!A is the domain of \!\mathcal A.

Dependence logic and other logics

Dependence logic and first-order logic

Dependence logic is a conservative extension of first-order logic:[4] in other words, for every first order sentence \!\phi and structure \! \mathcal A we have that \!\mathcal A \models_{\{\emptyset\}}^+ \phi if and only if \!\phi is true in \!\mathcal A according to the usual first order semantics. Furthemore, for any first order formula \!\phi, \!\mathcal A \models_{X}^+ \phi if and only if all assignments \!\mu \in X satisfy \!\phi in \!\mathcal A according to the usual first order semantics.

However, dependence logic is strictly more expressive than first order logic:[5] for example, the sentence

\!\exists z \forall x_1 \forall x_2 \exists y_1 \exists y_2 (=\!\!(x_1, y_1) \wedge =\!\!(x_2, y_2) \wedge (x_1 = x_2 \leftrightarrow y_1 = y_2) \wedge y_1 \not = z)

is true in a model \mathcal A if and only if the domain of this model is infinite, even though no first order formula \!\phi has this property.

Dependence logic and second-order logic

Every dependence logic sentence is equivalent to some sentence in the existential fragment of second order logic,[6] that is, to some second order sentence of the form

\!\exists R_1 \ldots \exists R_n \psi(R_1 \ldots R_n)

where \!\psi(R_1 \ldots R_n) does not contain second order quantifiers. Conversely, every second-order sentence in the above form is equivalent to some dependence logic sentence.[7]


As for open formulas, dependence logic corresponds to the downwards monotone fragment of existential second order logic, in the sense that a nonempty class of teams is definable by a dependence logic formula if and only if the corresponding class of relations is downwards monotone and definable by an existential second order formula.[8]

Dependence logic and branching quantifiers

Branching quantifiers are expressible in terms of dependence atoms: for example, the expression

(Q_Hx_1,x_2,y_1,y_2)\phi(x_1,x_2,y_1,y_2)\equiv\begin{pmatrix}\forall x_1 \exists y_1\\ \forall x_2 \exists y_2\end{pmatrix}\phi(x_1,x_2,y_1,y_2)

is equivalent to the dependence logic sentence \forall x_1 \exists y_1 \forall x_2 \exists y_2 (=\!\!(x_1, y_1) \wedge =\!\!(x_2, y_2) \wedge \phi), in the sense that the former expression is true in a model if and only if the latter expression is true.

Conversely, any dependence logic sentence is equivalent to some sentence in the logic of branching quantifiers, since all existential second order sentences are expressible in branching quantifier logic.[9][10]

Dependence logic and IF logic

Any dependence logic sentence is logically equivalent to some IF logic sentence, and vice versa.[11]

However, the issue is subtler when it comes to open formulas. Translations between IF logic and dependence logic formulas, and vice versa, exist as long as the domain of the team is fixed: in other words, for all sets of variables \!V = \{v_1 \ldots v_n\} and all IF logic formulas \!\phi with free variables in \!V there exists a dependence logic formula \!\phi^D such that

\mathcal A \models_X^+ \phi \Leftrightarrow \mathcal A \models_X^+ \phi^D

for all structures \mathcal A and for all teams \!X with domain \! V, and conversely, for every dependence logic formula \!\psi with free variables in \!V there exists an IF logic formula \!\psi^I such that

\mathcal A \models_X^+ \psi \Leftrightarrow \mathcal A \models_X^+ \psi^I

for all structures \mathcal A and for all teams \! X with domain \! V. These translations cannot be compositional.[12]

Properties

Dependence logic formulas are downwards closed: if \!\mathcal A \models_X \phi and \!Y \subseteq X then \!\mathcal A \models_Y \psi. Furthermore, the empty team (but not the team containing the empty assignment) satisfies all formulas of Dependence Logic, both positively and negatively.

The law of the excluded middle fails in dependence logic: for example, the formula \!\exists y (=\!\!(y) \wedge y = x) is neither positively nor negatively satisfied by the team \!X = \{(x:0), (x:1)\}. Furthermore, disjunction is not idempotent and does not distribute over conjunction.[13]


Both the compactness theorem and the Löwenheim-Skolem theorem are true for dependence logic. Craig's interpolation theorem also holds, but, due to the nature of negation in dependence logic, in a slightly modified formulation: if two dependence logic formulas ϕ and ψ are contradictory, that is, it is never the case that both \!\phi and \!\psi hold in the same model, then there exists a first order sentence \!\theta in the common language of the two sentences such that \!\phi implies \!\theta and \!\theta is contradictory with \!\psi.[14]


As IF logic[15], Dependence logic can define its own truth operator:[16] more precisely, there exists a formula \!\tau(x) such that for every sentence \!\phi of dependence logic and all models \mathcal M_\omega which satisfy Peano's axioms, if \!'\phi' is the Gödel number of \!\phi then

\mathcal M_\omega \models^+_{\{\emptyset\}} \!\phi if and only if \mathcal M_\omega \models^+_{\{\emptyset\}} \tau('\phi').

This does not contradict Tarski's undefinability theorem, since the negation of dependence logic is not the usual contradictory one.

Complexity

As a consequence of Fagin's theorem, the model checking problem for dependence logic is NP-complete. Furthermore, its inconsistency problem is semidecidable, and in fact equivalent to the inconsistency problem for first-order logic.

However, the decision problem for dependence logic is non-arithmetical, and is in fact complete with respect to the Π2 class of the Levy hierarchy.[17]

Variants and extensions

Team logic

Team logic[18] extends dependence logic with a contradictory negation \sim\!\!\phi. Its expressive power is equivalent to that of full second order logic.[19]

Modal dependence logic

The dependence atom, or a suitable variant thereof, can be added to the language of modal logic, thus obtaining modal dependence logic.[20][21][22]

Intuitionistic dependence logic

As it is, dependence logic lacks an implication. The intuitionistic implication \phi \rightarrow \psi, whose name derives from the similarity between its definition and that of the implication of intuitionistic logic, can be defined as follows[23]:

\!\mathcal A \models_X \phi \rightarrow \psi if and only if for all \!Y \subseteq X such that \!\mathcal A \models_Y \phi it holds that \!\mathcal A \models_Y \psi.

Intuitionistic dependence logic, that is, dependence logic supplemented with the intuitionistic implication, is equivalent to second-order logic.[24]

See also

Notes

References


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Independence-friendly logic — (IF logic), proposed by Jaakko Hintikka and Gabriel Sandu, aims at being a more natural and intuitive alternative to classical first order logic (FOL). IF logic is characterized by branching quantifiers. It is more expressive than FOL because it… …   Wikipedia

  • Quantum logic — In mathematical physics and quantum mechanics, quantum logic is a set of rules for reasoning about propositions which takes the principles of quantum theory into account. This research area and its name originated in the 1936 paper by Garrett… …   Wikipedia

  • History of logic — Philosophy ( …   Wikipedia

  • Outline of logic — The following outline is provided as an overview of and topical guide to logic: Logic – formal science of using reason, considered a branch of both philosophy and mathematics. Logic investigates and classifies the structure of statements and… …   Wikipedia

  • Aristotle’s logic and metaphysics — Alan Code PART 1: LOGICAL WORKS OVERVIEW OF ARISTOTLE’S LOGIC The Aristotelian logical works are referred to collectively using the Greek term ‘Organon’. This is a reflection of the idea that logic is a tool or instrument of, though not… …   History of philosophy

  • Institutional logic — is a core concept in sociological theory and organizational studies that focuses on how broader belief systems shape the cognition and behavior of actors (see Friedland Alford, 1991; Lounsbury, 2007; Thornton, 2004). Friedland and Alford (1991:… …   Wikipedia

  • Buddhist logic — This article presents the formal background to Buddhist logic which started at about 500 CE in ancient India and still has a living tradition in the Tibetan Gelug order. Like the logic of Aristotle, ancient Indian logic is a highly formal system… …   Wikipedia

  • Game semantics — (German: dialogische Logik) is an approach to formal semantics that grounds the concepts of truth or validity on game theoretic concepts, such as the existence of a winning strategy for a player, somewhat resembling Socratic dialogues or medieval …   Wikipedia

  • nature, law of — ▪ logic       in logic, a stated regularity in the relations or order of phenomena in the world that holds, under a stipulated set of conditions, either universally or in a stated proportion of instances. For the philosophical law of nature, see… …   Universalium

  • Memory disambiguation — is a set of techniques employed by high performance out of order execution microprocessors that execute memory access instructions (loads and stores) out of program order. The mechanisms for performing memory disambiguation, implemented using… …   Wikipedia