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
/	—	Slash	Independence
(∃y/x)	—	Independent ∃	Choose y without seeing x
(∀x/W)	—	Independent ∀	Universal, ignoring W
∀x∃y	—	Dependent	Standard: y sees x
↓	U+2193	Signaling	Information flow

Metatheory. IF logic = existential fragment of second-order logic (Σ₁¹) over vocabulary. Strictly more expressive than first-order. Can define: infinity, evenness, connectivity — impossible in FOL. Truth is not compositional: truth of compound formula not determined by truth of parts. Negation is problematic: game-theoretic dual (¬φ true iff Falsifier wins) differs from contradictory negation. Decidability: generally undecidable (includes SOL fragment).

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. Breaks compositionality — can't evaluate subformulas independently. Two negations (dual, contradictory) with different properties. Model checking is harder than FOL. Equivalence to Σ₁¹ limits practical decidability. The syntax is unusual; learning curve is steep. Not widely implemented in tools.