Say a set of sentences in first-order logic has the finite countermodel property if any sentence in the set that is falsifiable is falsifiable on a finite domain. (Two examples: the set of sentences with only unary predicates; the dual class to the Bernays–Schönfinkel class, i.e., those sentences in prenex form whose universal quantifiers, if any, precede existential quantifiers.) It's obvious that logical validity for any such set is decidable.

But is the converse true? Or are there decidable fragments of first-order logic that lack the finite countermodel property? (I think there ought to be: I'm imagining sentences that may be false only on infinite domains -- i.e. which admit only infinite countermodels -- but which nevertheless permit the computation of an upper bound on finite countermodel size. Though I suppose my question amounts to asking whether that's possible.)

Say a set of sentences in first-order logic has the finite countermodel property if any sentence in the set that is falsifiable is falsifiable on a finite domain. (Two examples: the set of sentences with only unary predicates; the dual class to the Bernays–Schönfinkel class, i.e., those sentences in prenex form whose universal quantifiers, if any, precede existential quantifiers.) It's obvious that logical validity for any such set is decidable.

But is the converse true? Or are there decidable fragments of first-order logic that lack the finite countermodel property? (I think there ought to be: I'm imagining sentences that may be false only on infinite domains -- i.e. which admit only infinite countermodels -- but which nevertheless permit the computation of an upper bound on the time it takes some semidecision procedure to finish. Though I suppose my question amounts to asking whether that's possible.)

Say a set of sentences in first-order logic has the finite model property if any sentence in the set that is falsifiable is falsifiable on a finite domain. (Two examples: the set of sentences with only monadic predicates; the Bernays–Schönfinkel class, i.e., those sentences in prenex form whose existential quantifiers, if any, precede universal quantifiers.) I believe it's a fact that logical validity for any such set is decidable.

But is the converse true? Or are there decidable fragments of first-order logic that lack the finite model property? (I think there ought to be: I'm imagining sentences that may be true only on infinite domains but which nevertheless permit the computation of an upper bound on model size. Though I suppose my question amounts to asking whether that's possible.)

Say a set of sentences in first-order logic has the finite countermodel property if any sentence in the set that is falsifiable is falsifiable on a finite domain. (Two examples: the set of sentences with only unary predicates; the dual class to the Bernays–Schönfinkel class, i.e., those sentences in prenex form whose universal quantifiers, if any, precede existential quantifiers.) It's obvious that logical validity for any such set is decidable.

But is the converse true? Or are there decidable fragments of first-order logic that lack the finite countermodel property? (I think there ought to be: I'm imagining sentences that may be false only on infinite domains -- i.e. which admit only infinite countermodels -- but which nevertheless permit the computation of an upper bound on finite countermodel size. Though I suppose my question amounts to asking whether that's possible.)