Finite entailment of Positive Horn logic

Importance: Medium ✭✭
Author(s): Martin, Barnaby
Recomm. for undergrads: no
Posted by: LucSegoufin
on: September 21st, 2012
Question   Positive Horn logic (pH) is the fragment of FO involving exactly $ \exists, \forall, \wedge, = $. Does the fragment $ pH \wedge \neg pH $ have the finite model property?

It doesn't really matter whether or not equality is allowed, as it may mostly be propagated out by substitution. The question is whether there an infinity axiom of the form $ \phi \wedge \neg \psi $, for $ \phi, \psi $ in pH?

In [CMM08] it is proved that entailment of pH sentences is decidable. I.e. input, $ \phi, \psi $ in pH and return yes if $ \phi \rightarrow \psi $ is true on all models. The question is whether this is the same as asking if entailment of pH is equivalent to finite entailment, i.e. if $ \phi \rightarrow \psi $ is true on all models iff it is true on all finite models.

For the positive equality-free fragment of FO (bigger than pH), finite entailment and general entailment do not coincide, and the latter problem is undecidable. For existential positive logic, (smaller than pH), finite entailment and general entailment do coincide, and of course both are decidable. At present, the question as to whether finite entailment of pH is decidable is also open.


[CMM08] Hubie Chen, Florent R. Madelaine, Barnaby Martin: Quantified Constraints and Containment Problems. LICS 2008: 317-328

* indicates original appearance(s) of problem.


Solved in LICS 2017 "Herbrand Property, Finite Quasi-Herbrand Models, and a Chandra-Merlin Theorem for Quantified Conjunctive Queries"

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.