The question "what are the formulas that I'm allowed to check" is answered by specifying a first-order language in which to talk about monoidal categories. The language determines the formulas that are available to you.

The most natural language is a two-sorted language with sorts $O$ (for objects) and $A$ (for arrows), with function symbols $s,t: A\to O$ (source and target), $\circ\colon O\times O\to O$ (composition), $i\colon O\to A$ (identity maps), $\otimes_O\colon O\times O\to O$ (tensor product on objects), $\otimes_A\colon A\times A\to A$ (tensor product product on arrows), and a constant symbol $I\in O$. Of course, you have to decide what to do with non-composable arrows - one possibility is to replace the binary function symbol $\circ$ with a ternary relation symbol $\circ$ defining the graph of composition ($\circ(f,g,h)$ holds iff $f$ and $g$ are composable with composition $h$), while another possibility is to include "dummy elements" $*_O$ and $*_A$ in $O$ and $A$ which are the outputs of any terms which don't make sense.

As you noted, this language allows you to write down formulas which don't satisfy the principle of equivalence. In fact, any language which is expressive enough to define the relations $X\cong Y$ and $X\neq Y$ on objects will fail the principle of equivalence. There is a standard variant of first-order logic which does not have a primitive symbol $=$ for equality (this goes by the obvious name first-order logic without equality); you could try to fix this issue by removing the ability to talk about equality, at least on the object sort. But in any reasonable first-order language for categories, the relation "$f$ and $g$ are composable" will be definable on arrows, and then equality of objects $X = Y$ can be expressed by "the identity arrows $i_X$ and $i_Y$ are composable". This seems like a real obstruction to me.

It's conceivable that there's a logic $L$ which has expressivity similar to first-order logic but is only capable of expressing formulas which satisfy the principle of equivalence. I don't know such a logic, but I'm imagining one which removes equality on objects and builds the relation on arrows "$f$ and $g$ are composable" directly into the syntax. i.e. a dependent type theory where an arrow $f$ has a type $S_f\to T_f$, and the term $f\circ g$ is only well-formed when $S_f = T_g$. In any case, based on the obstruction above, I'm convinced the logic $L$ would have to have some features not present in first-order logic.

Given such a logic $L$ (and maybe the intent of your question was really "what is the logic $L$"?), you could ask about the $L$-equivalence of monoidal categories. But it would be incorrect to call this notion of equivalence elementary equivalence, since the term *elementary* refers specifically to first-order logic.

2more comments