This question looks at the same intuition as, but expressed via a different formal notion than, a couple earlier questions of mine (1, 2). Basically, I'm playing around with using model theory to provide a precise meaning of "bijective proof" in combinatorics. Below, all formulas/sentences are first-order.
Given a sentence $\varphi$ in the language of a single binary relation symbol $R$ and a natural number $n$, let $[\varphi]_n$ be the set of isomorphism types of models of $\varphi$ with size $n$. This question is about a (seeming) refinement of the equivalence relation $$\varphi\sim\psi:\quad\forall n([\varphi]_n=[\psi]_n).$$
Roughly speaking - the details are tedious, so I've put them below the fold - suppose $\varphi\sim\psi$. A concrete bijection between $\varphi$ and $\psi$ is a pair $(\lambda,\theta)$ with $\lambda$ a sentence (in an arbitrary language) and $\theta$ a formula (in a language related to that of $\lambda$), such that the following hold for each $n>0$:
There is at least one model of $\lambda$ with size $n$ up to isomorphism.
If $\mathcal{A}$ is a structure consisting of $(i)$ the set $\{1,...,n\}$ expanded to be a model of $\lambda$, $(ii)$ a further set of objects $U$ representing each element of $[\varphi]_n$, and $(iii)$ a further set of objects $V$ representing each element of $[\psi]_n$, then $\theta^{\mathcal{A}}$ is a bijection between $U$ and $V$. (This part is vague; see below for details.)
The motivating example is the following: there is a concrete bijection between "$R$ partitions the universe into $\le 2$ classes" and "$R$ partitions the universe into pairs-or-singletons" using the linear order axioms for $\lambda$, since we can say when an instance of the former type "turns into" an instance of the latter by "rotating the Young diagram."
Write $\varphi\approx\psi$ if there is a concrete bijection between $\varphi$ and $\psi$. While trivially symmetric (compare with the second above-linked question), transitivity is not obvious to me:
Question 1: Is $\approx$ transitive?
Separately, I'm curious if it actually refines $\sim$ at all:
Question 2: Do $\sim$ and $\approx$ coincide?
Obviously an affirmative answer to 2 gives the same for 1, but rather sadly.
Concrete bijections, rigorously
The only aspect of the description of "concrete bijection" given above that wasn't rigorous was the nature of the structures $\mathcal{A}$ considered in the second bulletpoint. Precisely, we're looking at all structures $\mathcal{A}$ such that:
The underlying set of $\mathcal{A}$ is broken into three pieces named by unary predicates, $X\sqcup U\sqcup V$, with $\vert X\vert=n$, $\vert U\vert=\vert[\varphi]_n\vert$, and $\vert V\vert=\vert[\psi]_n\vert$. (And remember that $\vert[\varphi]_n\vert=\vert[\psi]_n\vert$.)
On the $X$-part, we have relations turning it into a model of $\lambda$. These relations do not hold anywhere else.
Additionally, we have two ternary relation symbols $E\subseteq U\times X^2$ and $F\subseteq V\times X^2$ such that (conflating structures and isomorphism types) $$[\varphi]_n=\{(X; E(u,-,-): u\in U\}\quad\mbox{and}\quad [\psi]_n=\{(X; F(v,-,-): v\in V)\}.$$
The second bulletpoint in the definition of concrete bijections, then, says: "For every $\mathcal{A}$ of the above type, $\theta$ defines a bijection between the $U$- and $V$-parts." (And this is required to hold for all $n$, with $\lambda$ and $\theta$ not depending on $n$.)
Intuitively, a concrete bijection between $\varphi$ and $\psi$ is a way to, given any finite set $X$ and any set of representatives of $\varphi$ and $\psi$ on $X$, build in a first-order way a bijection between those sets of representatives ... possibly using some "auxiliary" structure on $X$ itself (e.g. a linear order). There are various natural tweaks we could further consider - most obviously, it's tempting to demand that $\theta^\mathcal{A}$'s behavior on $[\varphi]_n,[\psi]_n$ be independent of the choice of representatives - but for now I'll stick to the rather weak notion above.
