Finite entailment of Positive Horn logic

Importance: Medium ✭✭
Author(s): Martin, Barnaby
Recomm. for undergrads: no
Posted by: LucSegoufin
on: September 21st, 2012

\begin{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? \end{question}

% You may use many features of TeX, such as % arbitrary math (between $...$ and $$...$$) % \begin{theorem}...\end{theorem} environment, also works for question, problem, conjecture, ... % % Our special features: % Links to wikipedia: \Def {mathematics} or \Def[coloring]{Graph_coloring} % General web links: \href [The On-Line Encyclopedia of Integer Sequences]{http://www.research.att.com/~njas/sequences/} 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.

Bibliography

% Example: %*[B] Claude Berge, Farbung von Graphen, deren samtliche bzw. deren ungerade Kreise starr sind, Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg Math.-Natur. Reihe 10 (1961), 114. % %[CRS] Maria Chudnovsky, Neil Robertson, Paul Seymour, Robin Thomas: \arxiv[The strong perfect graph theorem]{math.CO/0212070}, % Ann. of Math. (2) 164 (2006), no. 1, 51--229. \MRhref{MR2233847} % % (Put an empty line between individual entries) [CMM08] Hubie Chen, Florent R. Madelaine, Barnaby Martin: Quantified Constraints and Containment Problems. LICS 2008: 317-328


* indicates original appearance(s) of problem.