Independence-Friendly Logic

Origin. Jaakko Hintikka and Gabriel Sandu introduced Independence-Friendly (IF) logic (1989, 1996). Extends first-order logic with informationally independent quantifiers. Motivated by game-theoretic semantics: quantifiers as moves in a game where some moves may be made without knowledge of others. Equivalent to existential second-order logic in expressive power.

Models. Quantifier independence and imperfect information. In classical ∀x∃y.φ(x,y), the choice of y can depend on x. In IF logic, (∀x)(∃y/x).φ(x,y) means y must be chosen independently of x — you pick y without knowing which x was chosen. Models situations with hidden information, simultaneous choice, or signaling constraints.

Formalism.

Syntax: First-order logic extended with slashed quantifiers:

(∃y/W)φ — choose y without knowing values of variables in W
(∀x/W)φ — universal quantifier independent of W

Examples:

∀x(∃y/x).R(x,y) — for all x, there exists y (chosen blindly) such that R(x,y)
This differs from ∀x∃y.R(x,y) — where y can depend on x

Game-theoretic semantics: Two players: Verifier (∃loise) and Falsifier (∀belard).

∃ moves: Verifier picks witness
∀ moves: Falsifier picks counterexample
Independence: at move (∃y/x), Verifier doesn't see Falsifier's choice of x

Formula is true iff Verifier has a winning strategy.

Uniformity: (∀x)(∃y/x).R(x,y) requires a uniform witness function: one y that works for all x simultaneously. Equivalent to: ∃f∀x.R(x, f) — existential second-order!

Branching quantifiers (Henkin): (∀x)(∃y) φ(x,y,z,w) (∀z)(∃w)

y independent of z, w independent of x.

Signaling: Information can be passed through term structure. (∀x)(∃y/x).P(x,y) ∧ Q(y,z) — z can depend on y, indirectly on x.

Symbols.

Symbol	Unicode	Name	Meaning
/	—	Solidus / Slash	Marks the variables a quantifier is independent of
∃	U+2203	Existential quantifier	Verifier's move
∀	U+2200	Universal quantifier	Falsifier's move
(∃y/x)	—	Independent existential	Choose y without seeing x
(∀x/W)	—	Independent universal	Choose x without seeing the variables in W
W	—	Slash set	The variables hidden from the quantifier
∃loise	—	Verifier	The player who tries to make the formula true
∀belard	—	Falsifier	The player who tries to make it false
f	—	Skolem function	Strategy, with arguments restricted by the slash
Σ¹₁	—	Sigma-1-1	Existential second-order logic; the captured class

Metatheory. Truth is the existence of a winning strategy for the Verifier, and since strategies are Skolem functions whose admissible arguments are exactly what the slashes leave visible, every IF sentence translates effectively into an equivalent Σ¹₁ sentence and every Σ¹₁ sentence back — the equivalence Enderton and Walkoe established for branching prefixes in 1970. Over finite structures this is NP by Fagin's theorem, and the data complexity of model checking is NP-complete. Compactness and downward Löwenheim–Skolem hold, because a Σ¹₁ sentence becomes first-order once its Skolem functions are named. Validity does not: by the translation it coincides with the validity problem for dependence logic, which Väänänen showed to be Π₂-complete in the Lévy hierarchy and hence non-arithmetical, so no recursive axiomatization exists. The games are of imperfect information and so need not be determined: ∀x(∃y/x) x = y is neither true nor false in any model with at least two elements. Hodges (1997) supplied the compositional semantics on sets of assignments that Hintikka had declared impossible, and that construction is the origin of team semantics.

Applies to. Game theory (imperfect information games). Semantics of natural language (branching readings). Database theory (query languages with independence). Security (information flow). Philosophy of logic (challenging compositionality).

Limitations. The negation is the game-theoretic dual, not the contradictory one, so excluded middle fails and sentences may be neither true nor false; the logic is not closed under contradictory negation, and extended IF logic, which is, has the strength of full second-order logic and forfeits compactness and Löwenheim–Skolem. The slash does not reliably deliver the independence it declares: a value can be signalled through a term or through an intervening quantifier, so (∃y/x) may still be effectively informed about x, and the syntactic notation therefore underdetermines the game. Truth is not compositional at the level of single assignments, which is what forced Hodges' move to teams. Validity admits no recursive axiomatization. Expressive power is capped at Σ¹₁: well-foundedness, which is Π¹₁, is not definable, and no co-NP-complete property is definable over finite structures unless NP = co-NP.