university of tampere:
sis/luo-coms:
research:
cis - the tampere research center for information and systems:
research groups:
logic group:
research:

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.

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.

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.

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)."

**THE UNIVERSITY**

Research

Admissions

Studies

News

Cooperation and Services

About Us

**CURRENT ISSUES**

Research & Study

Tampere3

Vacancies