Inlogic abranching quantifier,^[1] also called aHenkin quantifier,finite partially ordered quantifier or evennonlinear quantifier, is a partial ordering^[2]

${\displaystyle ⟨Q{x}_1\dots Q{x}_n⟩}$

ofquantifiers forQ ∈ {∀,∃}. It is a special case ofgeneralized quantifier. Inclassical logic, quantifier prefixes are linearly ordered such that the value of a variabley_m bound by a quantifierQ_m depends on the value of the variables

y₁, ...,y_m−1

bound by quantifiers

Qy₁, ...,Qy_m−1

precedingQ_m. In a logic with (finite) partially ordered quantification this is not in general the case.

Branching quantification first appeared in a 1959 conference paper ofLeon Henkin.^[3] Systems of partially ordered quantification are intermediate in strength betweenfirst-order logic andsecond-order logic. They are being used as a basis forHintikka's and Gabriel Sandu'sindependence-friendly logic.

The simplest Henkin quantifier${\displaystyle Q_H}$ is

${\displaystyle (Q_H{x}_1,x_2,y_1,y_2)\phi (x_1,x_2,y_1,y_2)\equiv \left(\begin{array}{c}\mathrm{\forall }{x}_1\mathrm{\exists }{y}_1\\ \mathrm{\forall }{x}_2\mathrm{\exists }{y}_2\end{array}\right)\phi (x_1,x_2,y_1,y_2).}$

It (in fact every formula with a Henkin prefix, not just the simplest one) is equivalent to its second-orderSkolemization, i.e.

${\displaystyle \mathrm{\exists }f\mathrm{\exists }g\mathrm{\forall }{x}_1\mathrm{\forall }{x}_2\phi (x_1,x_2,f(x_1),g(x_2)).}$

It is also powerful enough to define the quantifier${\displaystyle Q_{\ge \mathbb{N}}}$ (i.e. "there are infinitely many") defined as

${\displaystyle (Q_{\ge \mathbb{N}}x)\phi (x)\equiv (\mathrm{\exists }a)(Q_H{x}_1,x_2,y_1,y_2)[\phi (a)\wedge (x_1=x_2\leftrightarrow y_1=y_2)\wedge (\phi (x_1)\to (\phi (y_1)\wedge y_1\ne a))].}$

Several things follow from this, including the nonaxiomatizability of first-order logic with${\displaystyle Q_H}$ (first observed byEhrenfeucht), and its equivalence to the${\displaystyle {\mathrm{\Sigma }}_1^1}$-fragment ofsecond-order logic (existential second-order logic)—the latter result published independently in 1970 byHerbert Enderton^[4] and W. Walkoe.^[5]

The following quantifiers are also definable by${\displaystyle Q_H}$.^[2]

• Rescher: "The number ofφs is less than or equal to the number ofψs"

${\displaystyle (Q_{L}x)(\phi x,\psi x)\equiv \mathrm{Card}(\{x:\phi x\})\le \mathrm{Card}(\{x:\psi x\})\equiv (Q_H{x}_1{x}_2{y}_1{y}_2)[(x_1=x_2\leftrightarrow y_1=y_2)\wedge (\phi x_1\to \psi y_1)]}$

• Härtig: "Theφs are equinumerous with theψs"

${\displaystyle (Q_{I}x)(\phi x,\psi x)\equiv (Q_{L}x)(\phi x,\psi x)\wedge (Q_{L}x)(\psi x,\phi x)}$

• Chang: "The number ofφs is equinumerous with the domain of the model"

${\displaystyle (Q_{C}x)(\phi x)\equiv (Q_{L}x)(x=x,\phi x)}$

The Henkin quantifier${\displaystyle Q_H}$ can itself be expressed as a type (4)Lindström quantifier.^[2]

Hintikka in a 1973 paper^[6] advanced the hypothesis that some sentences in natural languages are best understood in terms of branching quantifiers, for example: "some relative of each villager and some relative of each townsman hate each other" is supposed to be interpreted, according to Hintikka, as:^[7][8]

${\displaystyle \left(\begin{array}{c}\mathrm{\forall }{x}_1\mathrm{\exists }{y}_1\\ \mathrm{\forall }{x}_2\mathrm{\exists }{y}_2\end{array}\right)[(V(x_1)\wedge T(x_2))\to (R(x_1,y_1)\wedge R(x_2,y_2)\wedge H(y_1,y_2)\wedge H(y_2,y_1))].}$

which is known to have no first-order logic equivalent.^[7]

The idea of branching is not necessarily restricted to using the classical quantifiers as leaves. In a 1979 paper,^[9]Jon Barwise proposed variations of Hintikka sentences (as the above is sometimes called) in which the inner quantifiers are themselvesgeneralized quantifiers, for example: "Most villagers and most townsmen hate each other."^[7] Observing that${\displaystyle {\mathrm{\Sigma }}_1^1}$ is not closed under negation, Barwise also proposed a practical test to determine whether natural language sentences really involve branching quantifiers, namely to test whether their natural-language negation involves universal quantification over a set variable (a${\displaystyle {\mathrm{\Pi }}_1^1}$ sentence).^[10]

Hintikka's proposal was met with skepticism by a number of logicians because some first-order sentences like the one below appear to capture well enough the natural language Hintikka sentence.

${\displaystyle [\mathrm{\forall }{x}_1\mathrm{\exists }{y}_1\mathrm{\forall }{x}_2\mathrm{\exists }{y}_2\phi (x_1,x_2,y_1,y_2)]\wedge [\mathrm{\forall }{x}_2\mathrm{\exists }{y}_2\mathrm{\forall }{x}_1\mathrm{\exists }{y}_1\phi (x_1,x_2,y_1,y_2)]}$

where

${\displaystyle \phi (x_1,x_2,y_1,y_2)}$

denotes

${\displaystyle (V(x_1)\wedge T(x_2))\to (R(x_1,y_1)\wedge R(x_2,y_2)\wedge H(y_1,y_2)\wedge H(y_2,y_1))}$

Although much purely theoretical debate followed, it wasn't until 2009 that some empirical tests with students trained in logic found that they are more likely to assign models matching the "bidirectional" first-order sentence rather than branching-quantifier sentence to several natural-language constructs derived from the Hintikka sentence. For instance students were shown undirectedbipartite graphs—with squares and circles as vertices—and asked to say whether sentences like "more than 3 circles and more than 3 squares are connected by lines" were correctly describing the diagrams.^[7]

• Game semantics
• Dependence logic
• Independence-friendly logic (IF logic)
• Mostowski quantifier
• Lindström quantifier
• Nonfirstorderizability

• Game-theoretical quantifier at PlanetMath.

• Quantifier (logic)