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 , for in pH?

In [CMM08] it is proved that entailment of pH sentences is decidable. I.e. input, in pH and return yes if 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 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.