- 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
, where
are terms, and corresponds to the statement that the value of
is functionally dependent on the values of
.
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:
- A relational atom is an expression of the form
for any n-ary relation
in our signature and for any n-uple of terms
;
- An equality atom is an expression of the form
, for any two terms
and
;
- A dependence atom is an expression of the form
, for any
and for any n-uple of terms
.
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
of dependence logic and their respective sets of free variables Free(ϕ) are defined as follows:
- Any atomic formula
is a formula, and Free(ϕ) is the set of all variables occurring in it;
- If
is a formula, so is
and
;
- If
and
are formulas, so is
and
;
- If
is a formula and
is a variable,
is also a formula and
.
Nothing is a dependence logic formula unless it can be obtained through a finite number of applications of these four rules.
A formula
such that
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,
is taken as a shorthand for
, and
is taken as a shorthand for
.
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
be a first-order structure and let
be a finite set of variables. Then a team over
with domain
is a set of assignments over
with domain
, that is, a set of functions
from
to
.
It may be helpful to visualize such a team as a database relation with attributes
and with only one data type, corresponding to the domain
of the structure: for example, if the team
consists of four assignments
with domain
then one may represent it as the relation
Positive and negative satisfaction
Team semantics can be defined in terms of two relations
and
between structures, teams and formulas.
Given a structure
, a team X over it and a dependence logic formula
whose free variables are contained in the domain of
, if
we say that
is a trump for
in
, and we write that
; and analogously, if
we say that
is a cotrump for
in
, and we write that
.
If
one can also say that
is positively satisfied by
in
, and if instead
one can say that
is negatively satisfied by
in
.
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
, we say that
is true in
if and only if
, and we say that
is false in
if and only if
.
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
and
need to be performed simultaneously:
Positive satisfiability
if and only if
is a n-ary symbol in the signature of
;
- All variables occurring in the terms
are in the domain of
;
- For every assignment
, the evaluation of the tuple
according to
is in the interpretation of
in
;
if and only if
- All variables occurring in the terms
and
are in the domain of
;
- For every assignment
, the evaluations of
and
according to
are the same;
- All variables occurring in the terms
if and only if any two assignments
whose evaluations of the tuple
coincide assign the same value to
;
if and only if
;
if and only if there exist teams
and
such that
'
;
;
if and only if there exists a function
from
to the domain of
such that
, where
.
Negative satisfiability
if and only if
is a n-ary symbol in the signature of
;
- All variables occurring in the terms
are in the domain of
;
- For every assignment
, the evaluation of the tuple
according to
is not in the interpretation of
in
;
if and only if
- All variables occurring in the terms
and
are in the domain of
;
- For every assignment
, the evaluations of
and
according to
are different;
- All variables occurring in the terms
if and only if
is the empty team;
if and only if
;
if and only if
and
;
if and only if
, where
and
is the domain of
.
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
and structure
we have that
if and only if
is true in
according to the usual first order semantics. Furthemore, for any first order formula
,
if and only if all assignments
satisfy
in
according to the usual first order semantics.
However, dependence logic is strictly more expressive than first order logic:[5] for example, the sentence
is true in a model
if and only if the domain of this model is infinite, even though no first order formula
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
where
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
is equivalent to the dependence logic sentence
, 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
and all IF logic formulas
with free variables in
there exists a dependence logic formula
such that
for all structures
and for all teams
with domain
, and conversely, for every dependence logic formula
with free variables in
there exists an IF logic formula
such that
for all structures
and for all teams
with domain
. These translations cannot be compositional.[12]
Properties
Dependence logic formulas are downwards closed: if
and
then
. 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
is neither positively nor negatively satisfied by the team
. 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 bothand
hold in the same model, then there exists a first order sentence
in the common language of the two sentences such that
implies
and
is contradictory with
.[14]
As IF logic[15], Dependence logic can define its own truth operator:[16] more precisely, there exists a formulasuch that for every sentence
of dependence logic and all models
which satisfy Peano's axioms, if
is the Gödel number of
then
if and only if
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
. 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
, whose name derives from the similarity between its definition and that of the implication of intuitionistic logic, can be defined as follows[23]:
if and only if for all
such that
it holds that
.
Intuitionistic dependence logic, that is, dependence logic supplemented with the intuitionistic implication, is equivalent to second-order logic.[24]
See also
Notes
- ^ Väänänen 2007
- ^ Hodges 1997
- ^ Väänänen 2007, §3.2
- ^ Väänänen 2007, §3.2
- ^ Väänänen 2007, §4
- ^ Väänänen 2007, §6.1
- ^ Väänänen 2007, §6.3
- ^ Kontinen and Väänänen 2009
- ^ Enderton 1970
- ^ Walkoe 1970
- ^ Väänänen 2007, §3.6
- ^ Kontinen and Väänänen 2009 bis
- ^ Väänänen 2007, §3
- ^ Väänänen 2007, §6.2
- ^ Hintikka 2002
- ^ Väänänen 2007, §6.4
- ^ Väänänen 2007, §7
- ^ Väänänen 2007, §8
- ^ Kontinen and Nurmi 2009
- ^ Sevenster 2009
- ^ Väänänen 2008
- ^ Lohmann and Vollmer 2010
- ^ Abramsky and Väänänen 2009
- ^ Yang 2010
References
- Abramsky, Samson and Väänänen, Jouko (2009), 'From IF to BI'. Synthese 167(2): 207–230.
- Enderton, Herbert B. (1970), 'Finite partially-ordered quantifiers'. Z. Math. Logik Grundlagen Math., 16: 393–397.
- Hintikka, Jaakko (2002), 'The Principles of Mathematics Revisited', ISBN 978-0-521-62498-5.
- Hodges, Wilfrid (1997), 'Compositional semantics for a language of imperfect information'. Journal of the IGPL 5: 539–563.
- Kontinen, Juha and Nurmi, Ville (2009), 'Team Logic and Second-Order Logic'. In Logic, Language, Information and Computation, pp. 230–241.
- Kontinen, Juha and Väänänen, Jouko (2009), 'On definability in dependence logic'. Journal of Logic, Language and Information 18(3): 317–332.
- Kontinen, Juha and Väänänen, Jouko (2009), 'A Remark on Negation of Dependence Logic'. Institut Mittag-Leffler, report No. 22.
- Lohmann, Peter and Vollmer, Heribert (2010), 'Complexity Results for Modal Dependence Logic'. In Lecture Notes in Computer Science, pp. 411–425.
- Sevenster, Merlijn (2009), 'Model-theoretic and Computational Properties of Modal Dependence Logic'. Journal of Logic and Computation 19(6): 1157–1173.
- Väänänen, Jouko (2007), 'Dependence Logic -- A New Approach to Independence Friendly Logic', ISBN 978-0-521-87659-9.
- Väänänen, Jouko (2008), 'Modal dependence logic'. New Perspectives in Logic and Interaction, pp. 237–254.
- Walkoe, Wilbur J. (1970), 'Finite partially-ordered quantification. Journal of Symbolic Logic, 35: 535–575.
- Yang, Fan (2010), 'Expressing Second-order Sentences in Intuitionistic Dependence Logic'. Dependence and Independence in Logic proceedings, pp. 118–132.
Categories:- Systems of formal logic
- A relational atom is an expression of the form
Wikimedia Foundation. 2010.