On the semantics of the Henkin quantifier

In [5] Henkin defined a quantifier, which we shall denote by Q H : linking four variables in one formula. This quantifier is related to the notion of formulas in which the usual universal and existential quantifiers occur but are not linearly ordered. The original definition of Q H was Here ( Q H x 1 x 2 y 1 y 2 )φ is true if for every x 1 there exists y 1 such that for every x 2 there exists y 2 , whose choice depends only on x 2 not on x 1 and y 1 such that φ( x 14 , x 2 , y 1 , y 2 ). Another way of writing this is In [5] it was observed that the logic L(Q H ) obtained by adjoining Q H defined as in (1) is more powerful than first-order logic. In particular, it turned out that the quantifier “there exist infinitely many” denoted Q 0 was definable from Q H because