Return to Answer

If you restrict attention to the traditional prefix–vocabulary classes, validity in the following fragments is decidable without having the finite model property (note that it is customary in the literature to discuss satisfiability rather than validity, hence you will find there the dual classes):

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

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

• Any prefix class with a finite prefix in a fixed language with 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. A comprehensive reference is: E. Börger, E. Grädel, Y. Gurevich, The Classical Decision Problem, Springer, 1997 (reprinted 2001), MR1482227.

If you restrict attention to the traditional prefix–vocabulary classes, validity in the following fragments is decidable without having the finite model property (note that it is customary in the literature to discuss satisfiability rather than validity, hence you will find there the dual classes):

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

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

• Any prefix class with a finite prefix in a fixed language with 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. A comprehensive reference is: E. Börger, E. Grädel, Y. Gurevich, The Classical Decision Problem, Springer, 1997 (reprinted 2001), MR1482227.

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. A comprehensive reference is: E. Börger, E. Grädel, Y. Gurevich, The Classical Decision Problem, Springer, 1997 (reprinted 2001), MR1482227.

If you restrict attention to the traditional prefix–vocabulary classes, validity in the following fragments is decidable without having the finite model property (note that it is customary in the literature to discuss satisfiability rather than validity, hence you will find there the dual classes):

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

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

• Any prefix class with a finite prefix in a fixed language with 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. A comprehensive reference is: E. Börger, E. Grädel, Y. Gurevich, The Classical Decision Problem, Springer, 1997 (reprinted 2001), MR1482227.

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.

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. A comprehensive reference is: E. Börger, E. Grädel, Y. Gurevich, The Classical Decision Problem, Springer, 1997 (reprinted 2001), MR1482227.