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
/	—	Slash	The IF-logic linearization
Σ¹₁	—	Sigma-1-1	The captured class
f, g	—	Skolem functions	The dependence made explicit

Metatheory. Σ¹₁-completeness makes branching quantifiers a second-order construction wearing first-order notation, and that is the reason the whole axis exists: the Skolem form is honest about the functions and unusable as a logic, while the branching prefix is usable and opaque. Team semantics is the third option — the functions become supplement operations on a team, and the dependence pattern becomes an atom. Validity is not axiomatizable, since Σ¹₁ validity is Π¹₁-complete.

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, by Π¹₁-completeness of validity. 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.