This is an old revision of the document!

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

presence or absence of equality in formulas
regular expression describing the sequence of quantifiers (e.g. $\exists^* \forall^*$ means formulas $\forall x_1. \ldots. \forall x_n. \exists y_1.\ldots \exists y_n. F$ )
number and arity of relation symbols
number and arity of function symbols

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