Skip to main content
1 of 4
Emil Jeřábek
  • 47.1k
  • 4
  • 147
  • 208

If you restrict attention to the traditional prefix classes, the following fragments are decidable without having the finite model property:

  • Full FO in a language with equality, unary predicates, and a single unary function.

  • The prefix class $\exists^\*\forall\exists^\*$ (i.e., sentences in prenex normal form with only one universal quantifier) in a language with equality, arbitrary predicates, and a single unary function.

  • Any prefix class with a finite prefix, finitely many relations, and no functions. (This is a trivial case: if you further normalize the matrix to CNF, there are only finitely many formulas in the class.)

A nice survey is in this lecture by Erich Grädel.

Emil Jeřábek
  • 47.1k
  • 4
  • 147
  • 208