Yes, there are known examples satisfying the conditions. One such example involves monadic second-order logic (MSO), with the class of finite trees as the subclass ( D ) and all finite graphs as the superclass ( C ).

Details:

1. Logic ( L ): Monadic Second-Order Logic (MSO), which allows quantification over individual elements and sets (monadic predicates) of elements.
2. **Clas...

Yes. A clean way to see this is via quantified constraint satisfaction (QCSP), i.e., the positive Horn fragment of first-order logic (prenex ∀/∃, matrix a conjunction of atomic predicates). Let

• L be the positive Horn fragment of FO over a fixed binary relation symbol (so sentences are prenex, with only ∀ and ∃, and the quantifier-free part is a conjunction of atoms R(x,y)).
• C be the class of ...

No “off‐the‐shelf’’ example is known in the literature. In fact every time one looks at a familiar logic (FO, MSO, FO+TC, LFP, etc.) one of two things happens:

1. Restricting to 3 variables alone never tames the combined‐complexity.
   For almost all Horn‐and‐trivial extensions of first‐order (FO^3, MSO^3, FO[TC]^3, LFP^3, …) the model‐checking problem
   “Given φ in the 3-v...

Yes – by combining a very standard “padding’’ trick that forces every vertex of a graph to be represented by four elements of the structure we obtain a perfectly elementary (although admittedly not very beautiful) example that satisfies the three requirements.

Notation

• FO  = ordinary first–order logic
• FO³ = its three–variable fragment
• Graphs are represented by a single bina...

Model-checking for Three-Variable Logics and Restricted Structures

This question asks for a logic L where model checking exhibits a specific complexity pattern when restricted to three variables (L^(3)) and when operating on different classes of structures.

The goal is to find a logic L, a class of structures C, and a subclass D ⊂ C such that:

1. MC(L^(3), D) is "easy" (tractable)
2. MC(L, D) ...

This is an excellent question that hits on a core theme in descriptive complexity and finite model theory: the interplay between logical resources (like the number of variables) and structural properties of models.

The answer is yes, such a logic , class , and subclass exist. We can construct an example using Monadic Second-Order Logic (MSO) and well-known results about its expressi...

This is a fascinating question about the interaction between variable restrictions and structural restrictions in model-checking complexity. Let me analyze what we're looking for and provide some insights.

What We're Looking For

We need a logic and classes such that:

1. is easy (e.g., in P)
2. is hard (e.g., NP-hard)
3. is hard ...

First, I need to recall that model-checking (MC) is...

Short answer. No convincing example is known. With all “standard’’ logics that have been studied (FO, FO + TC, (E)MSO, fixed-point logics, guarded fragments, …) every natural way of choosing a subclass D that makes model checking of the 3–variable fragment tractable also makes model checking of the whole logic tractable – or at least no one has managed to separate the two. Conversely, wheneve...