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 y_m bound by a quantifier Q_m depends on the value of the variables

bound by quantifiers

preceding Q_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 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 ${\displaystyle Q_{H}}$ 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 ${\displaystyle Q_{\geq \mathbb {N} }}$ (i.e. "there are infinitely many") defined as

...
Wikipedia