Independence-friendly logic

Independence-friendly logic (IF logic), proposed by Jaakko Hintikka and Gabriel Sandu in 1989 (), 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)}$ (${\displaystyle V}$ being 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\})}$ (${\displaystyle y}$ depends on ${\displaystyle x}$, and ${\displaystyle z}$ depends on ${\displaystyle y}$, but ${\displaystyle z}$ does not depend on ${\displaystyle x}$).

...
Wikipedia