CLASSIFICATION O F QUANTlFIER PREFIXES OVER EXPONER'TIAL DIOPHANTINE EQUATIONS J. P. J o s ~s in Calgary, Alberta (Canada), H. LEVITZ in Tallahassee, Florida (U.S.A.) and A. J . WILKIE in Manchester (England)
S 1. Introduction
In 1 9 i l P. V. MATIJASEVI~: [15] undertook the project of attempting to classify first order arithmetical formulas in prenex normal form, according to their solvability or unsolvability. According to this classification scheme, a prefix class is to be considered solvable if formulas with that prefix type can define only general recursive sets. A prefix sufficient for the definition of some (at least one) non-recursive relation, is to be considered unsolvable. In his paper [13], Y. V. MATIJASEVI~: considered only prefixes with bounded V quantifiers. The reason for that was probably because arithmetic formulas with such prefixes define only recursively enumerable sets.
The project of classifying quantifier prefixes over diophantine equations was continued in the paper of JONES [9]. "here further results were obtained for prefixes with bounded Y quantifiers. Prefixes with unbounded V quantifiers were also classified.
Here in the present paper we take up the problem of classification of quantifier prefixes over exponential diophantine equations. I n the exponential case we are able to give a very satisfying, nearly complete classification. From the paper of JONES and MATIJASEVI~: [lo], it follows that several prefixes with only three quantifiers, e.g.
3V3 and VV3, are already unsolvable. So there are not so many undecided prefixes (open problems) as in the polynomial case, Theorems of H. LEVITZ [ l l ] and A. MACMTYRE [12] dispose of most of the remaining prefixes.