Classical Decision Problem

Consider satisfiability problem for sentences in first-order logic.

Without loss of generality, assume that formulas are in prenex form.

Classify formulas according to

regular expression describing the sequence of quantifiers (e.g. $\exists^* \forall^*$ means formulas $\exists x_1. \ldots. \exists x_n. \forall y_1.\ldots \forall y_m. F$ where $F$ is quantifier-free)
sequence of numbers of relation symbols for each arity
sequence of numbers of function symbols for each arity
presence or absence of equality in formulas

For each such description, determine whether the subsets of formulas that satisfy it are decidable or not.

Example: the exists-forall class that we will look at shortly is denoted $[\exists^* \forall^*,all,(0)]_{=}$ .

References