A tetrachotomy for positive equality-free logic
We consider the problem of evaluating positive equality-free sentences of first-order logic on a fixed, finite relational structure B. This may be seen as a generalisation of the Quantified Constraint Satisfaction Problem QCSP(B). We argue that our generalisation is not totally arbitrary, and that ours is the only problem in a large class - other than the CSP and QCSP - whose complexity taxonomy was unsolved. We introduce surjective hyper-endomorphisms in order to give a Galois connection that characterises definability in positive equality-free FO. Through the algebraic method we are able to characterise the complexity of our problem for all finite structures B. Specifically, the problem is either in Logspace, NP-complete, co-NP-complete or Pspacecomplete. The problem appears obtuse, but possesses a surprising elegance. Perhaps there are lessons to be learnt in the methodology of the solution of this case, for the continuing program for CSP.