# On Courcelle's question about Monadic second-order logic with cardinality predicates

I have found the following question at openproblemgarden.org:

The problem concerns the extension of Monadic Second Order Logic (over a binary relation representing the edge relation) with the following atomic formulas:

• $$\text{}\,\mathrm{Card}(X) = \mathrm{Card}(Y)\,\text{''}$$

• $$\text{}\,\mathrm{Card}(X) \text{ belongs to } A\,\text{''}$$

where $$A$$ is a fixed recursive set of integers.

Let us fix $$k$$ and a closed formula $$F$$ in this language.

Conjecture Is it true that the validity of $$F$$ for a graph $$G$$ of tree-width at most $$k$$ can be tested in polynomial time in the size of $$G$$?

I think that this conjecture of course false:

Consider some set $$A$$ such that $$A$$ recursive but $$A$$ is EEXP-hard.
Consider the formula $$\text{}\,\mathrm{Card}(V) \text{ belongs to } A\,\text{''}$$, where $$V$$ is the set of vertices.

Now assume that the conjecture is true. I claim that in this case $$A$$ belongs to EXP that contradict to Time-hierarchy theorem. Consider the following algorithm deciding $$A$$:

On input $$n$$ construct a tree with $$n$$ vertices. By the conjecture we can decides does $$n$$ belongs to $$A$$ in time $$\text{poly}(n)$$ that is $$2^{\text{poly}(\text{the size of the input})}$$.

Am I wrong?

• This may well be a mistake in the Open Problem Garden. Unfortunately, they do not give a reference to the original. – Emil Jeřábek Oct 9 at 14:20
• The author of the Open Problem Garden question (dberwanger) should be Dietmar Berwanger from CNRS; lsv.fr/~dwb . You could contact him by email. – Gamow Oct 9 at 15:25
• I believe that the autor meant the version of the problem where have an oracle in A, i.e., you can check whether card(V) belongs to A in a single step. – Bartosz Bednarczyk Oct 9 at 17:04
• I tried to post a comment at the OPG page. – Emil Jeřábek Oct 10 at 9:43
• Might be interesting: arxiv.org/abs/1703.00544 – Bartosz Bednarczyk Oct 10 at 12:26