Branching Quantifiers (Henkin Quantifiers)

Origin. Leon Henkin, "Some remarks on infinitely long formulas" (1961), which introduced quantifier prefixes arranged in a partial rather than linear order. Ehrenfeucht showed the simplest one is not first-order expressible; Enderton and Walkoe independently settled the expressive power (1970). The construction is the historical root of the team-semantic axis: IF logic and dependence logic both exist to make its dependence pattern statable in linear notation.

Models. In a linear prefix ∀x∃y∀z∃w, the witness for w may depend on everything to its left. The branching prefix breaks that: two rows run in parallel, and each existential sees only its own row. The pattern of dependence, not the quantifiers themselves, is the content — which is why writing it needs either two dimensions or an atom.

Formalism.

The Henkin quantifier:

( ∀x  ∃y )
( ∀z  ∃w )  φ(x, y, z, w)

y depends on x only; w depends on z only.

Skolem form: ∃f ∃g ∀x ∀z φ(x, f(x), z, g(z)) Σ¹₁ by construction — the function quantifiers are the content.

Team semantics (Hodges 1997): M, X ⊨ (∀x∃y / ∀z∃w) φ iff there is a team Y extending X with x, z duplicated over the domain, y supplemented by a function of x alone, w supplemented by a function of z alone, and Y ⊨ φ. The dependence restriction is a restriction on the supplement functions.

Expressive power (Enderton, Walkoe 1970): Branching-quantifier logic ≡ Σ¹₁. Hence: not first-order (Ehrenfeucht), and equal in strength to dependence logic.

Relation to IF logic: (∀x∃y/∀z∃w)φ ≡ ∀x ∃y ∀z (∃w/{x,y}) φ The slash makes the two-dimensional prefix linear.

Natural language: Hintikka (1973) claimed English sentences require branching readings — "some relative of each villager and some relative of each townsman hate each other." Barwise (1979) disputed both the data and the analysis.

Symbols.

Symbol	Unicode	Name	Meaning
∀	U+2200	Universal	Row-local
∃	U+2203	Existential	Sees only its own row
/	—	Solidus / Slash	The IF-logic linearization
Σ¹₁	—	Sigma-1-1	Existential second-order logic; the captured class
f, g	—	Skolem functions	The dependence made explicit
X	—	Team	Set of assignments the prefix acts on
⊨	U+22A8	True / Satisfaction	Between a model-team pair and a formula
≡	U+2261	Identical to / Equi-expressive	Same definable classes

Metatheory. Ehrenfeucht showed that the simplest branching prefix is not first-order expressible: the Henkin sentence with an injectivity condition is satisfied exactly by infinite models, which no first-order sentence achieves. Enderton and Walkoe independently proved (1970) that branching-quantifier logic is expressively equivalent to Σ¹₁, so by Fagin's theorem it captures NP over finite structures; the proof is Skolemization, since the prefix is nothing but a pattern of admissible arguments for the witness functions. Compactness and downward Löwenheim–Skolem therefore hold, each Σ¹₁ sentence becoming first-order once its Skolem functions are named as new symbols. Validity does not survive the translation: the set of valid Σ¹₁ sentences is non-arithmetical — Π₂-complete in the Lévy hierarchy, by Väänänen's analysis of the equi-expressive dependence logic — so no recursive proof system is possible. Team semantics is the third option beside the two-dimensional prefix and the Skolem form: the functions become supplement operations on a team, and the dependence pattern becomes an atom.

Applies to. The foundations of IF and dependence logic. Expressive-power results between first- and second-order logic. The disputed question of quantifier scope in natural language.

Limitations. No compositional semantics in the Tarskian sense — which is the defect team semantics was invented to repair, and the reason the construction was a curiosity for thirty years. No complete proof system, since validity is non-arithmetical. The logic is not closed under negation: the complement of a branching-quantifier sentence is Π¹₁ and in general expressible by no prefix, so well-foundedness lies outside it, as does any co-NP-complete property over finite structures unless NP = co-NP. The two-dimensional notation does not compose; there is no general clause for a branching prefix occurring inside the scope of a connective, which is why the slash and the dependence atom displaced it. And the natural-language motivation is contested: Barwise's objection to Hintikka's examples has not been answered to general satisfaction, and the linguistic case for branching remains the weakest part of the tradition.