The complexity of positive first-order logic without equality

TL;DR

This paper classifies the computational complexity of evaluating positive first-order logic sentences without equality over small structures, revealing a range from Logspace to Pspace-complete problems.

Contribution

It introduces surjective hyper-endomorphisms and a Galois connection to characterize definability, providing a complete complexity classification for structures of size up to three.

Findings

Problems range from Logspace to Pspace-complete.

A new algebraic method using surjective hyper-endomorphisms was developed.

Complete classification for structures of size at most three.

Abstract

We study the complexity of evaluating positive equality-free sentences of first-order (FO) logic over a fixed, finite structure B. This may be seen as a natural generalisation of the non-uniform quantified constraint satisfaction problem QCSP(B). We introduce surjective hyper-endomorphisms and use them in proving a Galois connection that characterises definability in positive equality-free FO. Through an algebraic method, we derive a complete complexity classification for our problems as B ranges over structures of size at most three. Specifically, each problem is either in Logspace, is NP-complete, is co-NP-complete or is Pspace-complete.