On one decidable generalized quantifier logic corresponding to a decidable
fragment of firstorder logic
Natasha Alechina
Van Lambalgen (1990) proposed a translation from a language containing a
generalized quantifier Q into a firstorder language enriched with a family
of predicates R_i , for every arity i (or an infinitary predicate R) which
takes $Qx\phi(x, y_1, ..., y_n)$ to $\forall x (R(x, y_1, ..., y_n) \implies
\phi(x, y_1, ..., y_n) )$ ($y_1, ..., y_n$ are precisely the free variables of
$Qx\phi$). The logic of Q (without ordinary quantifiers) corresponds therefore
to the fragment of firstorder logic which contains only specially restricted
quantification. We prove that it is decidable using the method of semantic
tableaux. Similar results were obtained by Andreka and Nemeti (1994) using
the methods of algebraic logic.