Branching quantifier

In logic a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering of quantifiers for Q ∈ {∀,∃}. It is a special case of generalized quantifier. In classical logic, quantifier prefixes are linearly ordered such that the value of a variable ym bound by a quantifier Qm depends on the value of the variables y1, ..., ym−1 bound by quantifiers Qy1, ..., Qym−1 preceding Qm. In a logic with (finite) partially ordered quantification this is not in general the case. Branching quantification first appeared in a 1959 conference paper of Leon Henkin. Systems of partially ordered quantification are intermediate in strength between first-order logic and second-order logic. They are being used as a basis for Hintikka's and Gabriel Sandu's independence-friendly logic. The simplest Henkin quantifier is It (in fact every formula with a Henkin prefix, not just the simplest one) is equivalent to its second-order Skolemization, i.e. It is also powerful enough to define the quantifier (i.e. "there are infinitely many") defined as Several things follow from this, including the nonaxiomatizability of first-order logic with (first observed by Ehrenfeucht), and its equivalence to the -fragment of second-order logic (existential second-order logic)—the latter result published independently in 1970 by Herbert Enderton and W. Walkoe. The following quantifiers are also definable by . Rescher: "The number of φs is less than or equal to the number of ψs" Härtig: "The φs are equinumerous with the ψs" Chang: "The number of φs is equinumerous with the domain of the model" The Henkin quantifier can itself be expressed as a type (4) Lindström quantifier. Hintikka in a 1973 paper 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: which is known to have no first-order logic equivalent.