# 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. means formulas where 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 .