Independence-friendly logic


Independence-friendly logic is an extension of classical first-order logic by means of slashed quantifiers of the form and, where is a finite set of variables. The intended reading of is "there is a which is functionally independent from the variables in ". IF logic allows one to express more general patterns of dependence between variables than those which are implicit in first-order logic. This greater level of generality leads to an actual increase in expressive power; the set of [|IF sentences] can characterize the same classes of structures as existential second-order logic.
For example, it can express branching quantifier sentences, such as the formula which expresses infinity in the empty signature; this cannot be done in FOL. Therefore, first-order logic cannot, in general, express this pattern of dependency, in which depends only on and, and depends only on and. IF logic is more general than branching quantifiers, for example in that it can express dependencies that are not transitive, such as in the quantifier prefix, which expresses that depends on, and depends on, but does not depend on.
The introduction of IF logic was partly motivated by the attempt of extending the game semantics of first-order logic to games of imperfect information. Indeed, a semantics for IF sentences can be given in terms of these kinds of games. A semantics for open formulas cannot be given in the form of a Tarskian semantics; an adequate semantics must specify what it means for a formula to be satisfied by a set of assignments of common variable domain rather than satisfaction by a single assignment. Such a team semantics was developed by Hodges.
Independence-friendly logic is translation equivalent, at the level of sentences, with a number of other logical systems based on team semantics, such as dependence logic, dependence-friendly logic, exclusion logic and independence logic; with the exception of the latter, IF logic is known to be equiexpressive to these logics also at the level of open formulas. However, IF logic differs from all the above-mentioned systems in that it lacks locality: the meaning of an open formula cannot be described just in terms of the free variables of the formula; it is instead dependent on the context in which the formula occurs.
Independence-friendly logic shares a number of metalogical properties with first-order logic, but there are some differences, including lack of closure under negation and higher complexity for deciding the validity of formulas. Extended IF logic addresses the closure problem, but its game-theoretical semantics is more complicated, and such logic corresponds to a larger fragment of second-order logic, a proper subset of Analytical hierarchy|.
Hintikka argued that IF and extended IF logic should be used as a basis for the foundations of mathematics; this proposal was met in some cases with skepticism.

Syntax

A number of slightly different presentations of independence-friendly logic have appeared in the literature; here we follow Mann et al.

Terms and atomic formulas

For a fixed signature σ, terms and atomic formulas are defined exactly as in first-order logic with equality.

IF formulas

Formulas of IF logic are defined as follows:
  1. Any atomic formula is an IF formula.
  2. If is an IF formula, then is an IF formula.
  3. If and are IF formulas, then and are IF formulas.
  4. If is a formula, is a variable, and is a finite set of variables, then and are also IF formulas.

    Free variables

The set of the free variables of an IF formula is defined inductively as follows:
  1. If is an atomic formula, then is the set of all variables occurring in it.
  2. ;
  3. ;
  4. .
The last clause is the only one that differs from the clauses for first-order logic, the difference being that also the variables in the slash set are counted as free variables.

IF Sentences

An IF formula such that is an IF sentence.

Semantics

Three main approaches have been proposed for the definition of the semantics of IF logic. The first two, based respectively on games of imperfect information and on Skolemization, are mainly used in the definition of IF sentences only. The former generalizes a similar approach, for first-order logic, which was based instead on games of perfect information.
The third approach, team semantics, is a compositional semantics in the spirit of Tarskian semantics. However, this semantics does not define what it means for a formula to be satisfied by an assignment.
The first two approaches were developed in earlier publications on if logic; the third one by Hodges in 1997.
In this section, we differentiate the three approaches by writing distinct pedices, as in. Since the three approaches are fundamentally equivalent, only the symbol will be used in the rest of the article.

Game-Theoretical Semantics

Game-Theoretical Semantics assigns truth values to IF sentences according to the properties of some 2-player games of imperfect information.
For ease of presentation, it is convenient to associate games not only to sentences, but also to formulas. More precisely, one defines games for each triple formed by an IF formula, a structure, and an assignment.

Players

The semantic game has two players, called Eloise and Abelard.

Game rules

The allowed moves in the semantic game are determined by the synctactical structure of the formula under consideration.
For simplicity, we first assume that is in negation normal form, with negations symbols occurring only in front of atomic subformulas.
  1. If is a literal, the game ends, and, if is true in , then Eloise wins; otherwise, Abelard wins.
  2. If, then Abelard chooses one of the subformulas, and the corresponding game is played.
  3. If, then Eloises chooses one of the subformulas, and the corresponding game is played.
  4. If, then Abelard chooses an element of, and game is played.
  5. If, then Eloise chooses an element of, and game is played.
More generally, if is not in negation normal form, we can state, as a rule for negation, that, when a game is reached, the players begin playing a dual game in which the roles of Verifiers and Falsifier are switched.

Histories

Informally, a sequence of moves in a game is a history. At the end of each history, some subgame is played; we call the assignment associated to, and the subformula occurrence associated to. The player associated to is Eloise in case the most external logical operator in is or, and Abelard in case it is or.
The set of allowed moves in a history is if the most external operator of is or ; it is in case the most external operator of is or.
Given two assignments of same domain, and we write if on any variable.
Imperfect information is introduced in the games by stipulating that certain histories are indistinguishable for the associated player; indistinguishable histories are said to form an 'information set'. Intuitively, if the history is in the information set, the player associated to does not know whether he is in or in some other history of.
Consider two histories such that the associated are identical subformula occurrences of the form ; if furthermore, we write or , in order to specify that the two histories are indistinguishable for Eloise, resp. for Abelard. We also stipulate, in general, reflexivity of this relation: if, then ; and if, then.

Strategies

For a fixed game, write for the set of histories to which Eloise is associated, and similarly for the set of histories of Abelard.
A strategy for Eloise in the game is any function that assigns, to any possible history in which it is Eloise's turn to play, a legal move; more precisely, any function such that for every history. One can define dually the strategies of Abelard.
A strategy for Eloise is uniform if, whenever, ; for Abelard, if implies.
A strategy for Eloise is winning if Eloise wins in each terminal history that can be reached by playing according to. Similarly for Abelard.

Truth, falsity, indeterminacy

An IF sentence is true in a structure if Eloise has a uniform winning strategy in the game.
It is false if Abelard has a winning strategy.
It is undetermined if neither Eloise nor Abelard has a winning strategy.

Conservativity

The semantics of IF logic thus defined is a conservative extension of first-order semantics, in the following sense. If is an IF sentence with empty slash sets, associate to it the first-order formula which is identical to it, except in that each IF quantifier is replaced by the corresponding first-order quantifier. Then iff in the Tarskian sense; and iff in the Tarskian sense.

Open formulas

More general games can be used to assign a meaning to IF formulas; more exactly, it is possible to define what it means for an IF formula to be satisfied, on a structure, by a team .
The associated games begin with the random choice of an assignment ; after this initial move, the game
is played. The existence of a winning strategy for Eloise defines positive satisfaction, and existence of a winning strategy for Abelard defines negative satisfaction.
At this level of generality, Game-theoretical Semantics can be replaced by an algebraic approach, team semantics.

Skolem Semantics

A definition of truth for IF sentences can be given, alternatively, by means of a translation into existential second-order logic. The translation generalizes the Skolemization procedure of first-order logic. Falsity is defined by a dual procedure called Kreiselization.

Skolemization

Given an IF formula, we first define its skolemization relativized to a finite set of variables. For every existential quantifier occurring in, let be a new function symbol. We write for the formula which is obtained substituting, in, all free occurrences of the variable with the term. The Skolemization of relative to, denoted, is defined by the following inductive clauses:
  1. if is a literal.
  2. .
  3. .
  4. .
  5. , where is a list of the variables in.
If is an IF sentence, its Skolemization is defined as.