Independence-friendly logic

Independence-friendly logic (IF logic; proposed by Jaakko Hintikka and in 1989) is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form formula_1 and formula_2, where formula_3 is a finite set of variables. The intended reading of formula_1 is "there is a formula_5 which is functionally independent from the variables in formula_3". 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 (formula_7). For example, it can express branching quantifier sentences, such as the formula formula_8 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 formula_9 depends "only" on formula_10 and formula_11, and formula_12 depends "only" on formula_13 and formula_11. 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 formula_15, which expresses that formula_9 depends on formula_10, and formula_13 depends on formula_9, but formula_13 does not depend on formula_10.
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 (or, alternatively, by means of a translation procedure to existential second-order logic). 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 (a "team") 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 (classical, contradictory) 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 formula_22.
Hintikka has argued that IF and extended IF logic should be used as a basis for the foundations of mathematics; this proposal has been 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 (2011).
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:
Free variables.
The set formula_35 of the free variables of an IF formula formula_23 is defined inductively as follows:
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 formula_3 are counted as free variables.
IF Sentences.
An IF formula formula_23 such that formula_44 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 (rather, by a "set" of assignments).
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 formula_45. Since the three approaches are fundamentally equivalent, only the symbol formula_46 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 formula_47 for each triple formed by an IF formula formula_23, a structure formula_49, and an assignment formula_50.
Players.
The semantic game formula_47 has two players, called Eloise (or Verifier) and Abelard (or Falsifier).
Game rules.
The allowed moves in the semantic game formula_52 are determined by the synctactical structure of the formula under consideration.
For simplicity, we first assume that formula_23 is in negation normal form, with negations symbols occurring only in front of atomic subformulas.
More generally, if formula_23 is not in negation normal form, we can state, as a rule for negation, that, when a game formula_72 is reached, the players begin playing a dual game formula_73 in which the roles of Verifiers and Falsifier are switched.
Histories.
Informally, a sequence of moves in a game formula_52 is a history. At the end of each history formula_75, some subgame formula_76 is played; we call formula_77 the "assignment associated to" formula_75, and formula_79 the "subformula occurrence associated to" formula_75. The "player associated to" formula_75 is Eloise in case the most external logical operator in formula_79 is formula_83 or formula_84, and Abelard in case it is formula_85 or formula_86.
The set formula_75 of "allowed moves" in a history formula_75 is formula_49 if the most external operator of formula_79 is formula_84 or formula_86; it is formula_93 (formula_94 being any two distinct objects, symbolizing 'left' and 'right') in case the most external operator of formula_79 is formula_83 or formula_85.
Given two assignments formula_98 of same domain, and formula_99 we write formula_100 if formula_101 on any variable formula_102.
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 formula_75 is in the information set formula_104, the player associated to formula_75 does not know whether he is in formula_75 or in some other history of formula_104.
Consider two histories formula_108 such that the associated formula_109 are identical subformula occurrences of the form formula_110 (formula_111 or formula_86); if furthermore formula_113, we write formula_114 (in case formula_111) or formula_116 (in case formula_117), 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 formula_118, then formula_114; and if formula_120, then formula_116.
Strategies.
For a fixed game formula_52, write formula_123 for the set of histories to which Eloise is associated, and similarly formula_124 for the set of histories of Abelard.
A "strategy" for Eloise in the game formula_52 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 formula_126 such that formula_127 for every history formula_128. One can define dually the strategies of Abelard.
A strategy for Eloise is "uniform" if, whenever formula_114, formula_130; for Abelard, if formula_116 implies formula_130.
A strategy formula_133 for Eloise is "winning" if Eloise wins in each terminal history that can be reached by playing according to formula_133. Similarly for Abelard.
Truth, falsity, indeterminacy.
An IF sentence formula_23 is "true" in a structure formula_49 (formula_137) if Eloise has a uniform winning strategy in the game formula_138. 
It is "false" (formula_139) 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 formula_23 is an IF sentence with empty slash sets, associate to it the first-order formula formula_141 which is identical to it, except in that each IF quantifier formula_142 is replaced by the corresponding first-order quantifier formula_143. Then formula_137 iff formula_145 in the Tarskian sense; and formula_139 iff formula_147 in the Tarskian sense.
Open formulas.
More general games can be used to assign a meaning to (possibly open) IF formulas; more exactly, it is possible to define what it means for an IF formula formula_23 to be satisfied, on a structure formula_49, by a "team" formula_150 (a set of assignments of common variable domain formula_151 and codomain formula_49).
The associated games formula_153 begin with the random choice of an assignment formula_154; after this initial move, the game 
formula_155 is played. The existence of a winning strategy for Eloise defines "positive satisfaction" (formula_156), and existence of a winning strategy for Abelard defines "negative satisfaction" (formula_157).
At this level of generality, Game-theoretical Semantics can be replaced by an algebraic approach, "team semantics" (defined below).
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 formula_23, we first define its skolemization relativized to a finite set formula_159 of variables. For every existential quantifier formula_1 occurring in formula_23, let formula_162 be a new function symbol (a "Skolem function"). We write formula_163 for the formula which is obtained substituting, in formula_23, all free occurrences of the variable formula_5 with the term formula_166. The Skolemization of formula_23 relative to formula_168, denoted formula_169, is defined by the following inductive clauses:
If formula_23 is an IF sentence, its (unrelativized) Skolemization is defined as formula_179.
Kreiselization.
Given an IF formula formula_23, associate, to each universal quantifier formula_2 occurring in it, a new function symbol formula_182 (a "Kreisel function"). Then, the Kreiselization formula_183 of formula_23 relative to a finite set of variables formula_185, is defined by the following inductive clauses:
If formula_23 is an IF sentence, its (unrelativized) Kreiselization is defined as formula_195.
Truth, falsity, indeterminacy.
Given an IF sentence formula_23 with formula_197 existential quantifiers, a structure formula_49, and a list formula_199of formula_197 functions of appropriate arities, we denote as formula_201 the expansion of formula_49 which assigns the functions formula_199 as interpretations for the Skolem functions of formula_23.
An IF sentence is true on a structure formula_49, written formula_206, if there is a tuple formula_199 of functions such that formula_208.
Similarly, formula_209 if there is a tuple formula_199 of functions such that formula_211; and formula_212 iff neither of the previous conditions holds.
For any IF sentence, Skolem Semantics returns the same values as Game-theoretical Semantics.
Team Semantics.
By means of team semantics, it is possible to give a compositional account of the semantics of IF logic. Truth and falsity are grounded on the notion of 'satisfiability of a formula by a team'.
Teams.
Let formula_213 be a structure and let formula_214 be a finite set of variables. Then a team over formula_49 with domain formula_3 is a set of assignments over formula_49 with domain formula_3, that is, a set of functions formula_219 from formula_3 to formula_49.
Duplicating and supplementing teams.
Duplicating and supplementing are two operations on teams which are related to the semantics of universal and existential quantification.
It is customary to replace repeated applications of these two operation with more succinct notations, such as formula_233 for formula_234.
Uniform functions on teams.
As above, given two assignments formula_98 with same variable domain, we write formula_100 if formula_101 for every variable formula_102.
Given a team formula_150 on a structure formula_49 and a finite set formula_3 of variables, we say that a function formula_229 is formula_3-uniform if formula_244 whenever formula_245.
Semantic clauses.
Team semantics is three-valued, in the sense that a formula may happen to be positively satisfied by a team on a given structure, or negatively satisfied by it, or neither. The semantics clauses for positive and negative satisfaction are defined by simultaneous induction on the synctactical structure of IF formulas.
Positive satisfaction:
Negative satisfaction:
Truth, falsity, indeterminacy.
According to team semantics, an IF sentence formula_23 is said to be true (formula_299) on a structure formula_49 if it is satisfied on formula_49 by the singleton team formula_302, in symbols: formula_303. 
Similarly, formula_23 is said to be false (formula_305) on formula_49 if formula_307; it is said to be undetermined (formula_308) if formula_309 and formula_310.
Relationship with Game-Theoretical Semantics.
For any team formula_150 on a structure formula_49, and any IF formula formula_23, we have:
formula_314 iff formula_315
and
formula_316 iff formula_317.
From this it immediately follows that, for sentences formula_23, formula_319, formula_320 and formula_321.
Notions of equivalence.
Since IF logic is, in its usual acception, three-valued, multiple notions of formula equivalence are of interest.
Equivalence of formulas.
Let formula_322 be two IF formulas.
formula_323 (formula_23 "truth entails" formula_27) if formula_326 for any structure formula_49 and any team formula_150 such that formula_329.
formula_330 (formula_23 is "truth equivalent" to formula_27) if formula_323 and formula_334.
formula_335 (formula_23 "falsity entails" formula_27) if formula_338 for any structure formula_49 and any team formula_150 such that formula_329.
formula_342 (formula_23 is "falsity equivalent" to formula_27) if formula_335 and formula_346.
formula_347 (formula_23 "strongly entails" to formula_27) if formula_323 and formula_335.
formula_352 (formula_23 is "strongly equivalent" to formula_27) if formula_330 and formula_342.
Equivalence of sentences.
The definitions above specialize for IF sentences as follows.
Two IF sentences formula_322 are "truth equivalent" if they are true in the same structures; they are "falsity equivalent" if they are false in the same structures; they are "strongly equivalent" if they are both truth and falsity equivalent.
Intuitively, using strong equivalence amounts to considering IF logic as 3-valued (true/undetermined/false), while truth equivalence treats IF sentences as if they were 2-valued (true/untrue).
Equivalence relative to a context.
Many logical rules of IF logic can be adequately expressed only in terms of more restricted notions of equivalence, which take into account the context in which a formula might appear.
For example, if formula_168 is a finite set of variables and formula_359, one can state that formula_23 is "truth equivalent to" formula_27 "relative to" formula_168 (formula_363) in case formula_364 for any structure formula_49 and any team formula_150 "of domain" formula_168.
Model-theoretic properties.
Sentence level.
IF sentences can be translated in a truth-preserving fashion into sentences of (functional) existential second-order logic (formula_368) by means of the Skolemization procedure (see above). Vice versa, every formula_368 can be translated into an IF sentence by means of a variant of the Walkoe-Enderton translation procedure for partially-ordered quantifiers (). In other words, IF logic and formula_368 are expressively equivalent at the level of sentences. This equivalence can be used to prove many of the properties that follow; they are inherited from formula_368 and in many cases similar to properties of FOL.
We denote by formula_372 a (possibly infinite) set of IF sentences.
Formula level.
The notion of satisfiability by a team has the following properties:
Since IF formulas are satisfied by teams and formulas of classical logics are satisfied by assignments, there is no obvious intertranslation between IF formulas and formulas of some classical logic system. However, there is a translation procedure of IF formulas into "sentences" of "relational" formula_368 (actually, one distinct translation formula_401 for each finite formula_159 and for each choice of a predicate symbol formula_251 of arity formula_404). In this kind of translation, an extra n-ary predicate symbol formula_251 is used to represent an n-variable team formula_150. This is motivated by the fact that, once an ordering formula_407 of the variables of formula_151 has been fixed, it is possible to associate a relation formula_409 to the team formula_150. With this conventions, an IF formula is related to its translation thus:
where formula_412 is the expansion of formula_49 that assigns formula_414 as interpretation for the predicate formula_251.
Through this correlation, it is possible to say that, on a structure formula_49, an IF formula formula_23 of n free variables "defines" a family of n-ary relations over formula_49 (the family of the relations formula_414 such that formula_420).
In 2009, Kontinen and Väänänen, showed, by means of a partial inverse translation procedure, that the families of relations that are definable by IF logic are exactly those that are nonempty, downward closed and definable in relational formula_368 with an extra predicate formula_251 (or, equivalently, nonempty and definable by a formula_368 sentence in which formula_251 occurs only negatively).
Extended IF logic.
IF logic is not closed under classical negation. The boolean closure of IF logic is known as extended IF logic and it is equivalent to a proper fragment of formula_22 (Figueira et al. 2011). Hintikka (1996, p. 196) claimed that "virtually all of classical mathematics can in principle be done in extended IF first-order logic".
Properties and critique.
A number of properties of IF logic follow from logical equivalence with formula_7 and bring it closer to first-order logic including a compactness theorem, a Löwenheim–Skolem theorem, and a Craig interpolation theorem. (Väänänen, 2007, p. 86). However, Väänänen (2001) proved that the set of Gödel numbers of valid sentences of IF logic with at least one binary
predicate symbol (set denoted by "ValIF") is recursively isomorphic with the corresponding set of Gödel numbers of valid (full) second-order sentences in a vocabulary that contains one binary predicate symbol (set denoted by "Val2"). Furthermore, Väänänen showed that "Val2" is the complete Π2-definable set of integers, and that it is "Val2" not in formula_427 for any finite "m" and "n". Väänänen (2007, pp. 136–139) summarizes the complexity results as follows:
Feferman (2006) cites Väänänen's 2001 result to argue (contra Hintikka) that while satisfiability might be a first-order matter, the question of whether there is a winning strategy for Verifier over all structures in general "lands us squarely in "full second order logic"" (emphasis Feferman's). Feferman also attacked the claimed usefulness of the extended IF logic, because the sentences in formula_428 do not admit a game-theoretic interpretation.