# Model-checking for three-variable logics and restricted structures

Denote the $k$-variable fragment of logic $L$ by $L^{(k)}$. The model-checking problem for a logic $L$ with respect to a class of structures $C$, denoted $MC(L,C)$, is the decision problem

$MC(L,C)$
Input: formula $\phi$ of $L$, structure $S$ from $C$
Question: does $S$ satisfy $\phi$?

Is there a logic $L$, with associated class of structures $C$, and a subclass $D$ of $C$, such that
1. $MC(L^{(3)},D)$ is "easy",
2. $MC(L,D)$ is "hard", and
3. $MC(L^{(3)},C)$ is "hard"?

With "easy" vs. "hard" I mean decidable vs. undecidable, PTIME vs. NP-hard, LogCFL vs. P-complete, or similar dichotomies.

# Motivation

For many logics the three-variable fragment is enough to express "hard" properties (this is true for MSO and FO over ordered structures). So results about undecidability often carry across from the logic to its three-variable fragment. There is also often a way to reduce the arity of predicates used in formulas efficiently (for instance, SAT can be reduced to 3SAT with a linear increase in formula size). Reducing arity facilitates expressing some formulas with fewer variables.

On the other hand, there exist logics which are "easy" for some classes of structures yet "hard" in general. For instance, the model-checking problem for MSO is "easy" (linear time) on unordered graphs satisfying the property "has treewidth less than $k$" for any fixed $k$, but "hard" (NP-complete) on unordered graphs in general.

I am asking whether there are any known examples where the restriction to 3 variables interacts with the property defining the subclass $D$ in an essential way to yield tractability, yet where neither of these restrictions on their own is enough.

Apologies for the vagueness of the question: I am trying to leave this general because I can't think of any examples. As soon as I restrict $D$ enough to ensure condition 1 holds, condition 2 seems to break. I suspect there are some unnatural classes which would work, but ideally $D$ should be "nice", at least hereditary and closed under isomorphism. As a further non-example, model-checking for FO is PSPACE-complete while model-checking for $FO^{(3)}$ is PTIME-complete; here the restriction to a finite number of variables is already enough to ensure an "easy" model-checking problem and condition 3 fails.

Definitions for completeness: FO is first-order logic, MSO is monadic second-order logic, where quantification over sets of individuals is allowed, as well as quantification over individuals.

• Have you made any progress on that question, András? – Michaël Cadilhac Oct 19 '15 at 20:25
• @MichaëlCadilhac alas, no. – András Salamon Oct 20 '15 at 13:51