8
$\begingroup$

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.)

Improve this question
$\endgroup$
3
  • $\begingroup$ The Bernays–Schönfinkel class $\exists^\*\forall^\*$ has FMP for satisfiability. Validity of $\exists^\*\forall^\*$-sentences is in fact undecidable. If you want FMP for validity (or falsifiability), you need to define the class dually: $\forall^\*\exists^\*$. $\endgroup$
    – Emil Jeřábek
    Commented Dec 14, 2011 at 12:51
  • $\begingroup$ Also, it’s important that the Bernays–Schönfinkel class does not allow any function symbols. $\endgroup$
    – Emil Jeřábek
    Commented Dec 14, 2011 at 12:53
  • $\begingroup$ Revised the question question in light of your first comment. $\endgroup$
    – symplectomorphic
    Commented Dec 20, 2011 at 18:26

1 Answer 1

Reset to default
7
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thanks Emil. I realized, though, that I wanted to ask something slightly different---about the tree method, rather than about FMP. One especially intuitive way to prove that validity is decidable for both (1) unary FOL & (2) the B-S dual class, is to show their negation trees must be finite. (For (2) this is almost obvious; for (1) one can use the fact that every sentence is equivalent to one in 'pure form', as Quine put it.) Clearly negation tree finiteness guarantees decidability, but are there decidable sets of FO sentences whose negation trees aren't necessarily finite? $\endgroup$
    – symplectomorphic
    Commented Dec 20, 2011 at 1:30
  • $\begingroup$ I am not familiar with this terminology. What is a negation tree? $\endgroup$
    – Emil Jeřábek
    Commented Dec 20, 2011 at 12:33
  • $\begingroup$ I know the terminology is non-standard, but I don't know of any that is standard. I was referring to a routine method taught in intro logic: to test a FO sentence for validity, take its negation & use the tree method to see if it's satisfiable. So by a sentence's 'negation tree' I just mean the tree one constructs to test satisfiability of its negation. With this, we get an obvious fact: the set of FO sentences with finite negation trees (which includes as subsets unary FO sentences in pure form & the B-S dual class) is decidable. Can one admit infinite neg. trees but preserve decidability? $\endgroup$
    – symplectomorphic
    Commented Dec 20, 2011 at 17:52
  • $\begingroup$ Is “tree method” another name for Hintikka/Smullyan analytic tableaux? As far as I can see, any non-tautology starting with $\exists\forall$ (such as $\exists x\,\forall y\,R(x,y)$) will have an infinite tree. In particular, the class $\forall^∗\exists\forall^∗$ without nonunary functions I mentioned above (or already its subclass $\exists\forall$ in a purely relational language) is your counterexample. $\endgroup$
    – Emil Jeřábek
    Commented Dec 20, 2011 at 18:26
  • $\begingroup$ What you are calling the ``negation tree" is commonly referred to in the literature as the dual. $\endgroup$
    – Michael McGrady
    Commented May 27, 2017 at 16:47

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .