Independence-friendly logic

Independence-friendly logic (IF logic; proposed by Jaakko Hintikka and Gabriel Sandu [fr] in 1989)^[1] is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form ${\displaystyle (\exists v/V)}$ and ${\displaystyle (\forall v/V)}$, where ${\displaystyle V}$ is a finite set of variables. The intended reading of ${\displaystyle (\exists v/V)}$ is "there is a ${\displaystyle v}$ which is functionally independent from the variables in ${\displaystyle V}$". 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 (${\displaystyle \Sigma _{1}^{1}}$).

For example, it can express branching quantifier sentences, such as the formula ${\displaystyle \exists c\forall x\exists y\forall z(\exists w/\{x,y\})((x=z\leftrightarrow y=w)\land y\neq c)}$ 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 ${\displaystyle y}$ depends only on ${\displaystyle x}$ and ${\displaystyle c}$, and ${\displaystyle w}$ depends only on ${\displaystyle z}$ and ${\displaystyle c}$. 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 ${\displaystyle \forall x\exists y(\exists z/\{x\})}$, which expresses that ${\displaystyle y}$ depends on ${\displaystyle x}$, and ${\displaystyle z}$ depends on ${\displaystyle y}$, but ${\displaystyle z}$ does not depend on ${\displaystyle x}$.

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;^[2] 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.^[3]

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 ${\displaystyle \Delta _{2}^{1}}$.^[4]

Hintikka argued^[5] 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.^[6]