Throughout I'm only interested in the standard semantics for second-order logic, and all structures/languages are relational for simplicity.
If defined naively, second-order logic without equality is equivalent to second-order logic, since $x=y$ is equivalent to $\forall A(x\in A\leftrightarrow y\in A)$. However, there is a natural detrivialization of this. Say that a quasi-isomorphism between two structures $\mathfrak{A},\mathfrak{B}$ in the same language $\Sigma$ is a binary relation $I\subseteq\mathfrak{A}\times\mathfrak{B}$ such that:
$dom(I)=\mathfrak{A}$ and $ran(I)=\mathfrak{B}$.
$I$ preserves-and-reflects all basic relations: for each $n$-ary $R\in\Sigma$, each $a_1,...,a_n\in \mathfrak{A}$, and each $b_1,...,b_n\in\mathfrak{B}$ with $a_iIb_i$ for all $1\le i\le n$, we have $$(a_1,...,a_n)\in R^\mathfrak{A}\quad\iff\quad (b_1,...,b_n)\in R^\mathfrak{B}.$$
Write $\mathfrak{A}\cong^q\mathfrak{B}$ if there is a quasi-isomorphism between $\mathfrak{A}$ and $\mathfrak{B}$. Quasi-isomorphisms arise as a natural tool for showing non-expressibility in equality-free $\mathsf{FOL}$ or even $\mathcal{L}_{\infty,\infty}$. This motivates the following "strongly-without-equality" fragment of second-order logic:
Let $\mathsf{SOL}_*$ be the set of second-order formulas such that for every pair of structures $\mathfrak{A},\mathfrak{B}$, every quasi-isomorphism $I:\mathfrak{A}\cong^q\mathfrak{B}$, and every pair of appropriate-arity tuples of elements $a_1,...,a_n\in\mathfrak{A}$ and $b_1,...,b_n\in\mathfrak{B}$ with $a_iIb_i$ for all $1\le i\le n$, we have $$\mathfrak{A}\models\varphi(a_1,...,a_n)\quad\iff\quad\mathfrak{B}\models\varphi(b_1,...,b_n).$$
In some notes on abstract model theory I'm writing I plan to include a few challenge exercises about $\mathsf{SOL}_*$ (e.g. "give a not-too-terrible syntax for it"), but I have a strong suspicion that it's already present in the literature. So my question is: what's a good source on this logic?
