Can one define second-order equinumerosity in MSO via first-order cardinality quantifiers?

Question

Let $L$ be MSO (Monadic Second Order Logic) extended with an $n$-ary second-order cardinality predicate (i.e., a first-order cardinality quantifier) $C_R$ for every $n$-ary relation $R$ on the naturals and two additional unary second-order predicates $F$ and $G$. Say that a model $M$ is admissible provided that it is finite and interprets $C_R$ as follows: $(A_1,...,A_n) \in C_R^M$ iff $(|A_1|,...,|A_n|) \in R$ for sets $A_1,...,A_n$ of elements of $M$.

The cardinality predicates $C_R$ let one define arbitrarily complicated counting of elements of sets, allowing one to express things like "$|X|+3^{|Y|}=\operatorname{BusyBeaver}(|Z|)$" for monadic second-order variables $X$, $Y$ and $Z$. I am wondering if this is enough to let one define "The number of sets $X$ such that $\phi(X)$ is equal to the number of sets $Y$ such that $\psi(Y)$". In other words, can we go from counting elements to counting sets, or more precisely:

Question: Is there a sentence of $\phi$ of $L$ such that $M\vDash \phi$ iff $|F^M|=|G^M|$ for all admissible models $M$?

I conjecture that the answer is negative, but can't prove it. I also suspect that the question is still negative if all we want to do is define the parity of $|F^M|$.

FO rephrasing: Say that an admissible model $M=({\cal P}A,\sigma,I)$ has the powerset of a finite set $A$ as its objects, a signature $\sigma$ consisting of $\subseteq$, unary predicates $F$ and $G$, and an $n$-ary predicate $C_R$ for every $n$-ary relation on the naturals, and an interpretation $I$ such that $\subseteq^I$ is the standard subset relation and $C_R^I = \{ (a_1,...,a_n) \in ({\cal P}A)^n : (|a_1|,...,|a_n|)\in R \}$. Then the question is whether there is a sentence $\phi$ of $\sigma$ such that $M\vDash \phi$ iff $|F^I|=|G^I|$ for every admissible $M=({\cal P}A,\sigma,I)$.

Note: If the only predicate $C_R$ we had was equinumerosity (i.e., $R$ had to be identity on the naturals), I think the answer would be negative since van Benthem and Icard recently showed that in MSO with equinumerosity the only relations one could define between cardinalities are semi-linear, while the possibility of defining $|F^M|=|G^M|$ would allow one to define power-of-two relations.

Answer 1

The answer is negative even for nonmonadic second-order logic by complexity considerations.

Assume for contradiction that such a sentence $\phi$ exists.

First, let us see how difficult it is to check that a given finite structure satisfies $\phi$. It is a standard fact that if $\phi$ were just an ordinary SO sentence (with only first-order relations and functions), then checking its truth in a structure $\mathcal M=([n],\dots)$ presented by the tables of the relations and functions can be done in the polynomial hierarchy PH, i.e., in $\Sigma^P_k$ for some constant $k$; in particular, an existential SO quantifier can be evaluated by nondeterministically guessing a witness (which takes $n^{O(1)}$ bits to write down), and dually for universal quantifiers.

Here we have to be more careful because we have more complex atomic formulas:

• $C_R$: Counting the number of elements in a set can be done in polynomial time, but checking whether $(n_1,\dots,n_k)\in R$ may not be even computable for arbitrary $R$. However, the finitely many $R$’s that occur in $\phi$ are fixed, and we are only interested in $R$ restricted to $\vec n\in[n]^k$: this is altogether $n^{O(1)}$ many bits that only depend on $n$ rather than the whole structure, hence they can be supplied as nonuniform advice.

• $F(X)$ and $G(X)$: We cannot afford to include the full table of $F$ and $G$ in the description of $\mathcal M$ in the first place, as this would take exponential size. Thus, we will assume that $F$ and $G$ are given to us as oracles that we can query at a given (polynomial-size) argument $X$.

All in all, in this representation, $\mathcal M\models\phi$ can be checked in $(\Sigma^P_k)^{F,G}/\def\poly{\mathrm{poly}}\poly$ for some $k\ge1$. (Note that here the input proper is just $n$ written in unary; the rest of the structure is supplied by the oracles $F$ and $G$. The polynomial advice is independent of $F$ and $G$.)

To assess what can be computed in $(\Sigma^P_k)^{F,G}/\poly$ by means of $\phi$, let me recall (a relativized version of) the somewhat uncommon counting class $\def\cep{\mathrm{C_=P}}\cep$, which can be defined in several equivalent ways:

• $X\in\cep^A$ if there is $R\in\mathrm P^A$ and a polynomial $p(n)$ such that for all $x$, $$x\in X\iff|\{y:|y|=p(|x|)\land R(x,y)\}|=|\{y:|y|=p(|x|)\land\neg R(x,y)\}|.$$

• $X\in\cep^A$ if there are $R,S\in\mathrm P^A$ and a polynomial $p(n)$ such that for all $x$, $$x\in X\iff|\{y:|y|=p(|x|)\land R(x,y)\}|=|\{y:|y|=p(|x|)\land S(x,y)\}|.$$

• $X\in\cep$ if there is $R\in\mathrm P^A$, a polynomial $p(n)$, and $F\in\mathrm{FP}$ such that for all $x$, $$x\in X\iff|\{y:|y|=p(|x|)\land R(x,y)\}|=F(x).$$

Now, the existence of $\phi$ implies that for all oracles $A$, $$\tag1\cep^A\subseteq(\Sigma^P_k)^A/\poly.$$ Indeed, fix, say, $R$ and $S$ as in the second definition of $\cep^A$ above. Then we can decide whether a given input $x$ of length $n$ belongs to $X$ by checking whether $\phi$ holds in the structure $\mathcal M=([p(n)],F,G)$, where $F$ and $G$ consist of sets $Y\subseteq[p(n)]$ such that the corresponding binary strings $y$ satisfy $R(x,y)$, resp. $S(x,y)$. Since a query to $F$ or $G$ can be evaluated in polynomial time with oracle $A$ using the input $x$, we can still check this in $(\Sigma^P_k)^A/\poly$. (Note that even though the simulated oracles for $F$ and $G$ depend on the input $x$, the polynomial advice still depends only on $n=|x|$—as it should—because it was independent of $F$ and $G$.)

Now, we just reap the consequences of (1) using a few results from complexity theory. To get from $\cep^A$ to more conventional classes such as PP and #P, (1) implies $$\def\A{\mathit A}\mathrm{P^{\#P^\A}=P^{PP^\A}\subseteq NP^{\cep^\A}}\subseteq(\Sigma^P_{k+1})^A/\poly:$$ an oracle call to a $\mathrm{\#P}^A$ oracle (i.e., given $x$, count the number of $y$, $|y|=p(|x|)$, satisfying a poly-time predicate $R^A(x,y)$ with oracle $A$) can be simulated by nondeterministically guessing the result, and verifying it with a $\cep^A$ oracle (using the third definition of $\cep$).

Then, (the relativized version of) Toda’s theorem gives $$\mathrm{PH^\A\subseteq P^{PP^\A}}\subseteq(\Sigma^P_{k+1})^A/\poly,$$ and a relativized version of the Karp–Lipton theorem gives $$\tag2\mathrm{PH}^A=(\Sigma^P_{k+3})^A.$$ (In fact, with a bit more effort you can show that even $\mathrm{P^{PP}}^A=(\Sigma^P_{k+3})^A$, which then implies by induction that the whole relativized counting hierarchy $\mathrm{CH}^A$ collapses to $(\Sigma^P_{k+3})^A$, but we will not need this.)

All of this is supposed to hold for all oracles $A$. But this is impossible, as it is known that there exist oracles $A$ relative to which the polynomial hierarchy does not collapse, in particular, $(\Sigma^P_{k+3})^A\subsetneq(\Sigma^P_{k+4})^A$.

---

Concerning the latest edit: the parity of $F$ cannot be defined in this way either, by much the same argument—if it could, we would obtain $$\tag{1'}\oplus\mathrm P^A\subseteq(\Sigma^P_k)^A/\poly$$ (see $\oplus$P), which again yields (2) by means of another version of Toda’s theorem (and relativized Adleman’s theorem): $$\mathrm{PH^\A\subseteq BP\cdot\oplus P^\A\subseteq\oplus P^\A/\poly}.$$