Logics for context-free languages

We define matchings, and show that they capture the essence of context-freeness. More precisely, we show that the class of context-free languages coincides with the class of those sets of strings which call be defined by sentences of the form There Exists b phi, where phi is first order, b is a binary predicate symbol, and the range of the second order quantifier is restricted to the class of matchings. Several variations and extensions are discussed.