PaperlayerView exact revision on arXiv

Source-linked AI summary

Inclusion and Exclusion Dependencies in Team Semantics: On Some Logics of Imperfect Information

Pietro Galliani

arXiv:1106.1323v2math.LO

TL;DR

The paper addresses the open problem of characterizing independence logic’s expressive power over open formulas. It develops inclusion and exclusion logics with game-theoretic semantics and shows that dependence logic and exclusion logic are equally expressive, with broader dependency expressibility in independence logic.

  • Problem

    The expressive power of independence logic over open formulas remained an open problem, limiting its characterization as a logic of imperfect information.

  • Method

    The paper adds inclusion and exclusion dependency atoms to first-order logic, studies the resulting logics, and develops game-theoretic semantics for them.

  • Results

    Dependence logic is precisely as expressive as exclusion logic for both team definability and sentence definability.

  • Takeaways & Limitations

    The results suggest that independence logic provides a theoretical framework for expressing general dependency forms studied in database theory.

  • Takeaways & Limitations

    The paper notes that relatively little is known about the expressive properties of inclusion logic.

Abstract

from arXiv · show

We introduce some new logics of imperfect information by adding atomic formulas corresponding to inclusion and exclusion dependencies to the language of first order logic. The properties of these logics and their relationships with other logics of imperfect information are then studied. Furthermore, a game theoretic semantics for these logics is developed. As a corollary of these results, we characterize the expressive power of independence logic, thus answering an open problem posed in (Grädel and Väänänen, 2010).

1. Introduction

The paper extends first-order logic with inclusion and exclusion atoms to study additional dependency patterns in logics of imperfect information. It develops corresponding team- and game-semantic frameworks and uses them to characterize the expressive power of independence logic.

  • Motivation: Logics of imperfect information address dependence and independence patterns that first-order logic cannot represent, extending the language with specialized atoms.Dependence logic isolates functional dependence through dependence atoms, while independence logic represents informational independence through atoms y ⊥x z [15].
  • Expressive power: The results show that some of the most general dependency forms studied in database theory are expressible in independence logic, addressing an open problem about its expressive power over open formulas.The introduction identifies this expressive-power question as an open problem and presents the database-dependency consequence as a final result.
  • Contributions: The paper introduces inclusion and exclusion dependencies as additional relational constraints and develops the corresponding logics.It recalls their definitions and basic properties before studying inclusion and exclusion logic; equiextension dependencies are treated as equivalent to inclusion dependencies for these purposes.
  • Contributions: Exclusion logic is equivalent in a strong sense to dependence logic, linking the new dependency formalism to an established logic of imperfect information.This equivalence is presented as one of the paper’s principal structural results.
  • Semantics: The paper develops a game-theoretic semantics for inclusion and exclusion logic alongside team semantics.The semantics assigns truth through semantic games, often via the existence of winning strategies, while team semantics remains a useful complementary formalism.

2. Dependence and independence logic

Dependence logic extends first-order logic with atoms expressing functional dependence, interpreted over teams and closely matching database-theoretic dependencies. The section also introduces independence logic and frames the paper’s answer to its open expressive-power problem.

  • Dependence logic: Dependence logic extends first-order logic with dependence atoms asserting that the final term is functionally determined by preceding terms.This separates dependency patterns from quantification and supports dependence relations not expressible in first-order logic.
  • Dependence logic: Under team semantics, a team represents an information state, and satisfaction means that the Verifier has a strategy winning from every assignment in the team.This semantics adapts Hodges’ compositional semantics for IF logic.
  • Dependence logic: Dependence-atom satisfaction is equivalent to the database dependency {t1 . . . tn−1} →tn on the relation induced by the team.Thus, the value of tn is a function of the values of t1 . . . tn−1.
  • Independence logic: Independence logic replaces dependence atoms with independence atoms, introducing a distinct logic of imperfect information.The section positions this logic in relation to the open problem of characterizing its NP properties of teams.
  • Independence logic: The paper answers the open problem of characterizing the NP properties of teams definable in independence logic, as a corollary of an analogous result for a new logic.This result is presented as a consequence of the paper’s broader development of new logics of imperfect information.

3. Team semantics

Section 3 introduces team semantics for first-order and dependence-related logics, defining teams, their relational interpretation, and the satisfaction rules for logical operators. It establishes agreement with Tarski semantics on singleton teams, flatness for first-order formulas, and the greater expressive complexity introduced by dependency atoms and alternative semantic rules.

  • 3.1 Team semantics: A team is a set of assignments over a model, with restrictions and associated relations providing the basic objects for team semantics.The section defines teams as sets of assignments with a common variable domain and introduces notation for extracting relations from teams and restricting assignments.
  • 3.1 Team semantics: Team semantics for first-order logic uses pointwise literals, team-splitting disjunction, shared conjunction, supplemented existential quantification, and duplicated universal quantification.Formulas are assumed to be in negation normal form because negation is not a semantic operation in dependence logic.
  • 3.1 Team semantics: On singleton teams, first-order team semantics coincides with ordinary Tarski semantics, and on arbitrary teams first-order formulas hold exactly when they hold for every assignment.This establishes both agreement with classical semantics and the flatness property of first-order formulas.
  • 3.1 Team semantics: Dependency atoms make teams semantically indispensable because conditions such as constancy can require comparing multiple assignments rather than evaluating assignments independently.The section identifies dependence logic as the result of adding dependence atoms and notes that team satisfaction is no longer reducible to singleton satisfaction.
  • 3.1 Team semantics: Alternative strict rules for disjunction and existential quantification are introduced because rules equivalent in dependence logic may differ in the new logics, although lax and strict semantics coincide for first-order and dependence logic.Strict disjunction requires disjoint subteams, while strict existential quantification uses single-valued supplementation.
  • 3.2 Constancy logic: Constancy logic is contained in dependence logic, is more expressive than first-order logic on open formulas, but is exactly as expressive as first-order logic on sentences and therefore strictly weaker than dependence logic.The section also notes a sentence-level versus formula-level discrepancy in expressive comparisons between these logics.

4. Inclusion and exclusion in logic

The section develops inclusion, exclusion, and equiextension logics within team semantics, establishing their semantic properties and expressive relationships. It shows that exclusion logic matches dependence logic, while inclusion/exclusion logic matches independence logic, under specified semantics.

  • Motivation and dependency theory: The section motivates replacing dependence atoms with other database-theoretic dependencies, drawing on established dependency theory and proving soundness and completeness for inclusion, exclusion, and their implication system.The authors present non-functional dependencies as relevant to knowledge states and expect database results to inform the corresponding logics.
  • Inclusion logic: Inclusion logic with lax semantics is local and union closed, but it is not downward closed; strict semantics fails locality.The choice between strict and lax disjunction and existential quantification is therefore essential for inclusion logic.
  • Inclusion logic: Inclusion logic is strictly more expressive than first-order logic over sentences, while remaining properly contained in independence logic.It can define parity on finite linear orders, a property not expressible in first-order logic; inclusion atoms are expressible in independence logic.
  • Equiextension logic: Inclusion logic and equiextension logic have exactly the same expressive power, with each formula equivalent to a formula in the other logic.Equiextension logic is first shown to be contained in inclusion logic, and inclusion atoms are then translated into equiextension formulas.
  • Exclusion logic: Exclusion logic is precisely as expressive as dependence logic, both for definability of teams and for sentences.Dependence atoms can be expressed using exclusion logic, and exclusion atoms can be translated into dependence-logic formulas.

5. Game theoretic semantics

The section develops a game-theoretic semantics for inclusion/exclusion logic, with uniform strategies connecting inclusion and exclusion atoms to team semantics. It proves equivalence with lax semantics and, for inclusion logic, with strict semantics under deterministic strategies, supporting nondeterministic/lax semantics as the natural choice for imperfect-information logics.

  • Semantic games: The game starts from assignments in the team, moves through subformulas according to logical connectives and quantifiers, and declares terminal literals and dependency atoms winning for Player II under specified conditions.Players I and II occupy positions (ψ,s); disjunction and existential quantification are controlled by II, conjunction and universal quantification by I, while inclusion and exclusion atoms are always locally winning for II.
  • Uniform strategies: Uniformity restricts Player II’s strategies so inclusion atoms require matching values from another compatible play, while exclusion atoms require unequal term values across relevant plays.Although these atoms are locally winning for II, they constrain the set of admissible strategies; inclusion uniformity also explains why nondeterministic and deterministic strategies differ.
  • Equivalence with team semantics: Uniform winning strategies in the semantic game characterize lax team semantics for inclusion logic.Theorem 5.10 states that Player II has a uniform winning strategy exactly when M |=X φ under lax semantics; the game semantics for inclusion and exclusion logic restrict accordingly.
  • Equivalence with team semantics: Uniform deterministic winning strategies characterize strict team semantics for inclusion logic.Theorem 5.11 establishes the corresponding equivalence between deterministic game strategies and strict semantics.
  • Interpretive consequences: For inclusion logic and its extensions, lax and strict semantics are not equivalent, so the results support adopting nondeterministic, equivalently lax, semantics as the natural imperfect-information semantics.The distinction persists even with the Axiom of Choice, whereas lax semantics satisfies Locality in the cited results.

6. Definability in I/E logic (and in independence logic)

This section establishes that I/E logic is exactly as expressive as existential second-order logic over team relations, and transfers the characterization to independence logic. Consequently, all NP properties of teams are expressible in independence logic, making it the most expressive imperfect-information logic within the existential-second-order fragment.

  • 6. Definability in I/E logic (and in independence logic): I/E logic formulas translate into existential second-order formulas over the relation represented by a team.The translation is proved by induction on the I/E formula.
  • 6. Definability in I/E logic (and in independence logic): Conversely, every existential second-order formula with one free relation variable is definable by an I/E logic formula over teams.The construction replaces existentially quantified functions with dependence conditions and uses inclusion/exclusion atoms to encode membership in the team relation.
  • 6. Definability in I/E logic (and in independence logic): Because I/E logic and independence logic have the same expressive power, every existential second-order team property is expressible in independence logic.The result follows directly from the preceding characterization and Corollary 4.23.
  • 6. Definability in I/E logic (and in independence logic): All NP properties of teams are expressible in independence logic.This follows from the existential-second-order characterization and Fagin’s Theorem [10].
  • 6. Definability in I/E logic (and in independence logic): Independence logic, equivalently I/E logic, is the most expressive imperfect-information logic whose properties remain within existential second-order logic.Extensions surpass this boundary only if they express properties that are not existential second order.

7. Equality generating dependencies, tuple generating dependencies and independence logic

The section connects database-theoretic tuple-generating and equality-generating dependencies with dependence and independence atoms, then shows that I/E logic—and therefore independence logic—can express all such dependencies. This expressive coverage supports using independence logic for knowledge-base reasoning, despite its high computational cost.

  • Database dependencies: Tuple-generating dependencies have the form ∀x1 . . . xn(φ(x1 . . . xn) →∃z1 . . . zkψ(x1 . . . xn, z1 . . . zk)), with φ and ψ conjunctions of relational or equality atoms.The relation symbol A has arity equal to that of the database relation R, and the terms use the empty vocabulary with free variables among x1 . . . xn.
  • Database dependencies: Equality-generating dependencies differ by requiring ψ to be a single equality atom, and satisfaction is evaluated in the usual first-order sense over a relation R.These are presented as two general database-theoretic notions of dependence.
  • Atom correspondences: Dependence atoms correspond to equality-generating dependencies, while independence atoms correspond to tuple-generating dependencies.The section gives these correspondences as examples of the expressive power of tuple-generating and equality-generating dependencies.
  • Expressive power: I/E logic, and consequently independence logic, expresses every tuple-generating and equality-generating dependency.Proposition 7.1 states that each such dependency has an equivalent I/E-logic formula, and the proof derives independence-logic expressibility via Theorem 6.2 and Corollary 4.23.
  • Implications: This expressive power enables independence logic to represent many database-theoretic properties and potentially support general knowledge-base reasoning, although computational costs are very high.The author presents this application as a motivation for studying independence logic and, more generally, logics of imperfect information.
Loading 1106.1323v2…