A form of logic for a language with quantifiers, $\forall$, $\exists$, whose bound variables stand in predicate places, as in $\exists X\neg Xa$. Since predicates can have one or more places, different variables are required for different numbers of places. Thus, one might use $R$ for a second-order binary quantifier: $\forall RRab$. Classical second-order logic has no sound and complete proof procedure.