Is this type of "definable bijective solution" of combinatorial identities symmetric? Say that a combinatorial problem is a pair of first-order sentences $\langle\varphi,\psi\rangle$ in (disjoint and relational, for simplicity) finite languages $\Sigma=\{R_1,...,R_l\},\Pi=\{S_1,...,S_m\}$ respectively such that for each finite set $X$, the sets $Mod_X(\varphi),Mod_X(\psi)$ of isomorphism types of models of $\varphi,\psi$ respectively with domain $X$ have the same cardinality. (The components of a combinatorial problem are just particularly simple combinatorial species.)
I'm interested in the class of combinatorial problems $\langle\varphi,\psi\rangle$ for which we can, in a first-order-definable way, establish a bijection between $\varphi$-models and $\psi$-models (on a fixed finite set) possibly with the additional help of some auxiliary structure on that set. Formally, say that $\langle\varphi,\psi\rangle$ is definably solvable iff there is a language $\Gamma=\{T_1,...,T_n\}$ disjoint from both $\Sigma$ and $\Pi$, a first-order $\Gamma$-sentence $\lambda$, and a tuple of $\mathsf{FOL}[\Sigma\cup\Gamma]$-formulas $(\theta_i)_{1\le i\le m}$ such that the following hold for every finite set $X$:

*

*Whenever $Mod_X(\varphi)\not=\emptyset$ we also have $Mod_X(\lambda)\not=\emptyset$.


*For each $1\le i\le m$, $\theta_i$ is a formula with the same arity (in terms of free variables) as the symbol $S_i$.


*If $Mod_X(\varphi)\not=\emptyset$, $\mathcal{X}$ is a $\Sigma\cup\Gamma$-structure with domain $X$ such that $\mathcal{X}\models\lambda\wedge\varphi$, then:

*

*The structure $(X;(\theta_i^\mathcal{X})_{1\le i\le m})$ is a model of $\psi$.


*For every $\Sigma\cup\Gamma$-structure $\mathcal{Y}\models\lambda\wedge\varphi$ with domain $\mathcal{X}$, we have $$\mathcal{X}\upharpoonright\Sigma\cong\mathcal{Y}\upharpoonright\Sigma\quad\iff\quad(X;(\theta_i^\mathcal{X})_{1\le i\le m})\cong (X;(\theta_i^\mathcal{Y})_{1\le i\le m}).$$
For example, with $E$ a binary relation symbol let $\pi_2$ = "$E$ is a partition of the domain into pairs or singletons" and let $\pi^2$ = "$E$ is a partition of the domain into two pieces." This question sketches why the combinatorial problem $\langle\pi_2,\pi^2\rangle$ is definably solvable. With a bit of tedium, one can show that $\langle\pi^2,\pi_2\rangle$ is also definably solvable. I'm curious whether this always holds:

If $\langle\varphi,\psi\rangle$ is a definably solvable combinatorial problem, must $\langle\psi,\varphi\rangle$ also be definably solvable?

(I would also be interested in results for the analogous notion defined with some not-too-strong logic $\mathcal{L}$ in place of first-order logic. Even second-order logic isn't so strong, at first glance, as to trivialize the situation! But my main focus is on $\mathsf{FOL}$.)
 A: It’s not symmetric. Here are two examples. The idea is to take $\Sigma,\phi$ to be $\Pi,\psi$ augmented with hard-to-compute but uniquely determined structure.
I’ll make use of results for $AC^0/\text{poly}$ circuits. A first-order formula can be implemented as $AC^0$ circuits by replacing quantifiers by conjunctions or disjunctions over the domain. Details are given in Immerman’s Descriptive Complexity Theorem 5.22 (and Meta-Proposition 11.19).
No use is made of the assumption that $\lambda$ is first-order.
First example:
$\Sigma,\phi$: a total order $<$ and a compatible BIT predicate, and a 1-ary relation $R_1$ that is an initial segment of $<$
$\Pi,\psi$: no axioms, just a 1-ary relation $S_1$
The BIT predicate can be axiomatized by specifying that the least element has all zero bits, and the bits of the successor of $n$ are calculated by flipping the least significant bits of $n$ up to and including the least significant zero.
There are $|X|+1$ models of each theory. $\langle \phi_1,\psi_1\rangle$ is definably solvable by taking $\theta_1(x)=R_1(x).$
Suppose that $\langle \psi,\phi\rangle$ were definably solvable.Then there would be quasipolynomial size constant depth circuits for computing the parity function, contradicting Håstad's switching lemma bound.
Fix $X$ and a $\Gamma$-structure satisfying $\lambda.$ Let $N_{X}$ be the set of $\lfloor n/2\rfloor$ possible values of $|R_1|$ that you get from inputs with $|S_1|$ odd. (More precisely: values of $|\theta_1^{\mathcal X}|$ where $\mathcal X$ is a $\Pi\cup\Gamma$ structure with the chosen $\Gamma$ structure as a reduct, and with $|S_1^{\mathcal X}|$ odd.) The circuit takes (the characteristic function of an interpretation of) $S_1$ as input, and can apply circuits for the $\theta_i$ formulas to compute $<,$ BIT, and $R_1$ as polynomial-size, constant depth subcircuits. It guesses the $<$-first $\log n$ elements, trying all $n^{\log n}$ options in parallel, verifying using circuits for $<.$ It then tests the BIT representation of the $<$-first element $x$ satisfying $\neg R_1(x)$ (if any) against each of the values in $N_X.$ The circuit outputs $1$ if any of these values is hit, or if $|X|\in N_X$ and $\forall x.R_1(x)$ holds.
Second example:
$\Sigma,\phi$: a total order, and a 1-ary relation $R_1,$ and a deterministic  easily-verifiable derivation of the output of the function $h$ in Sampling Lower Bounds: Boolean Average-Case and Permutations, Emanuele Viola, Theorem 2, applied to the characteristic function of $R_1$
$\Pi,\psi$: a total order, and a 1-ary relation $S_1$
For example, the derivation could be an encoding of a complete record of every step taken by a fixed polynomial-time Turing machine computing $h,$ including the entire tape at each step as a polynomial-sized bitstring, together with basic arithmetic operations to make all this data verifiable by a first-order predicate.
There are $2^{|X|}$ models of each theory. $\langle \phi,\psi\rangle$ is definably solvable by taking $\theta_1(x)=R_1(x).$  Suppose that $\langle \psi,\phi\rangle$ were definably solvable. Then there would be polynomial size constant depth circuits giving the correct distribution on $(R_1,h(R_1))$ when given a uniformly chosen bitstring $S_1$ as input. Viola’s Theorem 2 says that such a small circuit cannot give anything like the correct distribution.
