DECIDABILITY PROBLEMS IN LANGUAGES WITH HENKIN QUANTIFIERS

We consider the language L(H(omega)) with all Henkin quantifiers H(n) defined as follows: H(n)x1...x(n)y1...y(n) phi(x1,...,x(n), y1,...,y(n)) iff there exists f1...f(n) for-all x1...x(n) phi(x1,...,x(n), f1(x1), ..., f(n)(x(n))). We show that the theory of equality in L(H(omega)) is undecidable. The proof of this result goes by interpretation of the word problem for semigroups. Henkin quantifiers are strictly related to the function quantifiers F(n) defined as follows: F(n)x1...x(n)y1...y(n) phi(x1,...,x(n), y1,...,y(n)) iff there exists f for-all x1...x(n) phi(x1,...,x(n), f(x1),...,f(x(n)). In contrast with the first result we show that the theory of equality with all quantifiers F(n) is decidable. We also consider decidability problems for other theories in languages L(F2) and L(H-2).