To page body
university of tampere: sis/luo-coms: research: cis - the tampere research center for information and systems: research groups: logic group: research:
Faculties of Natural and Communication SciencesUniversity of TampereFaculties of Natural and Communication Sciences
CIS - The Tampere Research Center for Information and Systems

Dependence Logic and Independence-Friendly Logic at UTA

Dependence logic and independence-friendly (IF) logic are both conservative extensions of first-order logic that have the same expressive power as existential second-order logic. The syntax of IF logic can be viewed as a linearization of Henkin's partially ordered quantifiers. However, the semantics for IF logic is obtained by generalizing Hintikka's evaluation games for first-order sentences.

Game-Theoretical Semantics

Abelard and Eloise are two lovers who can never seem to agree about anything. Whenever Eloise makes an assertion, Abelard immediately tries to refute it. If Eloise asserts a disjunction, Abelard insists she verify one of the disjuncts. If Eloise makes an existential claim, Abelard demands that she identify an individual satisfying it. When Eloise asserts a negated formula the lovers switch roles: Abelard attempts to verify the formula, whilst Eloise tries to refute it.

When Eloise asserts an ordinary first-order sentence, the ensuing dispute is a game of perfect information. If the sentence is true, Eloise will always win. If it is false, Abelard will always win. When Eloise asserts an IF sentence, the dispute becomes a game of imperfect information. Thus, we are no longer guaranteed that one of the lovers will have a winning strategy. If Eloise has a winning strategy we say the sentence is true. If Abelard has a winning strategy we say the sentence is false. If neither player has a winning strategy we say the formula is undetermined.

Thus an IF sentence can have one of three possible truth-values. One can show that the propositional logic underlying IF logic is Kleene's strong three-valued logic.


Skolemization is the process of eliminating the existential quantifiers from a formula by introducing fresh function symbols. A first-order sentence is true in a model if and only if its Skolemization is true in some expansion of the model obtained by interpreting the fresh function symbols. The interpretations of the fresh function symbols are called Skolem functions.

A Skolem function produces a witness for an existential claim. Taken together, a set of Skolem functions for a sentence can be seen as encoding a strategy for Eloise in the associated semantic game. If the sentence is true, the Skolem functions can be assumed to encode a winning strategy.

The same process can be applied to IF sentences. The difference is that in the Skolemization of an IF sentence, the Skolem functions may depend on just some – rather than all – of the universally quantified variables bound superordinate to the original existential quantifier.

Team Semantics

Originally, it was thought that IF logic did not have a compositional semantics because the game-theoretical definition of truth applied only to sentences, not to formulas. Also, during a semantic game, play proceeds from "outside-in" rather than "inside-out" as with Tarski's semantics for first-order logic.

Nontheless, Wilfrid Hodges discovered a way to assign a meaning to IF formulas using sets of assignments called teams. A team satisfies an IF formula if Eloise has a winning strategy for the formula, assuming she knows the initial assignment belongs to the team.

Dependence Logic

Recently, Väänänen proposed a new approach to IF logic based on teams. He observed that the basic notion involved in the definition of team semantics is that of the dependence of one term on another. So why not add the notion of dependence to first-order logic as a primitive concept? The new atomic formula = (t_1,...,t_n) has the intended meaning: "the value of t_n is determined by the values of t_1,...,t_(n-1)."

Maintained by:
Last update: 24.12.2011 22.24 Muokkaa

University of Tampere
+358 3 355 111

FINEEC Audited HR Excellence in Research

Cooperation and Services
About Us

Research & Study

Career Services
Finnish Social Science Data Archive
Centre for International Education
IT services
Language Centre
Language Services
Registrar's Office
Sports Activities
» more

Teaching schedules
Curricula guides
Student's Desktop

Andor search
Renew your loans
UTA intranet
Office 365 webmail
Uta webmail
Electronic exam service
Examination results