logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premise ...

a branching quantifier, also called a Henkin quantifier, finite partially ordered quantifier or even nonlinear quantifier, is a partial ordering :

\langle Qx_1\dots Qx_n\rangle

of quantifiers for ''Q'' ∈ . It is a special case of

generalized quantifier In formal semantics, a generalized quantifier (GQ) is an expression that denotes a set of sets. This is the standard semantics assigned to quantified noun phrases. For example, the generalized quantifier ''every boy'' denotes the set of sets of ...

. 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 : ''y''₁, ..., ''y''_''m''−1 bound by quantifiers : ''Qy''₁, ..., ''Qy''_''m''−1 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 Leon Albert Henkin (April 19, 1921, Brooklyn, New York - November 1, 2006, Oakland, California) was an American logician, whose works played a strong role in the development of logic, particularly in the theory of types. He was an active scholar ...

. Systems of partially ordered quantification are intermediate in strength between

first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...

and

second-order logic In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies on ...

. They are being used as a basis for Hintikka's and Gabriel Sandu's

independence-friendly logic Independence-friendly logic (IF logic; proposed by Jaakko Hintikka and in 1989) is an extension of classical first-order logic (FOL) by means of slashed quantifiers of the form (\exists v/V) and (\forall v/V), where V is a finite set of variables. ...

Defin