In what sense do isomorphisms "preserve all logical properties"? My background in mathematical logic, model theory, etc. is patchy, so I'm looking for a clearer way to think about this. (Edit: I'm not asking what an isomorphism is, I'm asking how to formalize the idea of "preserving all logical properties" in order to state the principle described below in its full power.)
Motivating example: we know that $\Bbb N$ and $\Bbb Z$ are not order-isomorphic, because $\Bbb N$ has a least element whereas $\Bbb Z$ does not. The principle underlying this argument seems to be that an order isomorphism preserves the truth values of (first-order) sentences: if $(A,<_A)\cong(B,<_B)$ then $\operatorname{Th}(A,<_A)=\operatorname{Th}(B,<_B)$. Since the property "there is a least element" corresponds to the sentence $\exists x\forall y. x\le y$, the principle applies. The principle also seems to apply to higher-order properties. For example, we can conclude that $(\Bbb R\setminus\{0\},<)\not\cong(\Bbb R,<)$ by checking the least-upper-bound property, which is second-order.
More generally (if we think of set theory as modeling higher-order logic in first-order logic), I'm tempted to claim that the whole "set theory of <" (I'm not sure what this is exactly - a two-sorted first-order logic with relation symbols $<,\in$, maybe?) is preserved by isomorphisms. I think I can convince myself of this fact by observing that when $f:A\to B$ is an isomorphism, certain substitution rules involving $f$ in various syntactic contexts are valid, allowing us to prove equivalences between propositions about $<_A$ and the corresponding propositions about $<_B$.
I'm calling this a "principle" instead of a "theorem" because it seems easier to apply in specific cases (by reasoning directly about the elements and the isomorphism, without formalizing the notion of sentences) than to express in its full generality. My claim that "the set theory of $<$ is preserved" seems closely related to the fact that set theory is my metatheory (if that's the right word), so some kind of circularity or self-reference is appearing when I attempt to state the principle, and I wonder whether any formal version of the principle can fully eliminate the need to apply the principle directly.
So I guess my questions are:

*

*In what sense (if any) is there a most general version of this principle, applying to all properties preserved by order isomorphisms?

*Can it be expressed as a theorem in the deductive system where we want to apply it, or is there a theoretical obstacle to this?

*Am I getting anything wrong? Or missing a clarifying perspective?

Thanks!
 A: Here is an outline of a theorem which, I think, addresses the situation pretty well (incidentally, this MO question is related):
Most logic books will include a proof that first-order logic is isomorphism-invariant. But what about non-first-order properties? For example, the isomorphism-invariance of (say) Archimedeanness in the context of ordered fields is not a mere case of the isomorphism-invariance of first-order logic, even though "obviously" it holds for exactly the same reason.
There is in fact a framework for extending isomorphism-invariance from first-order logic to all "reasonable" logics, in a precise sense. The logics beyond first-order logic that we actually consider are really just "first-order logic in a superstructure." E.g. saying that a relation $R$ is definable over a structure $\mathcal{A}$ in monadic second-order logic is the same as saying that it is definable over $\mathcal{A}\sqcup\mathcal{P}(\mathcal{A})$ (being a bit vague about what that is, in the interest of brevity) in first-order logic.
This motivates the following idea. Working in $\mathsf{ZFC}$, let $V$ as usual denote the whole set-theoretic universe. There is a standard machinery for developing, first-order-definably inside $V$, a "version of $V$ with urelements" where the urelements correspond to elements of a given structure; the details are a bit tedious, but see e.g. Barwise's book. Call the resulting object "$V_\mathcal{A}$." Being a bit sloppy about set/class issues, we can prove in $\mathsf{ZFC}$ that $\mathcal{A}\cong\mathcal{B}$ implies $V_\mathcal{A}\cong V_\mathcal{B}$. This, together with the fact that isomorphism preserves first-order truth, gives the following result:

Isomorphisms preserve truth with respect to every "set-theoretically-definable" logic.

Here the idea is that each sentence $\varphi$ in a set-theoretically-definable logic should correspond to a first-order sentence $\hat{\varphi}$ such that $$\mathcal{A}\models\varphi\quad\iff\quad V_\mathcal{A}\models\hat{\varphi}$$ (or at worst, a first-order sentence $\hat{\varphi}$ with a parameter from $V$ - note that $V$ sits inside $V_\mathcal{A}$ in a canonical way, so a single $V$-parameter makes sense across all $V_\mathcal{A}$s independently of $\mathcal{A}$; we need to allow parameters to handle logics with "too many sentences," such as infinitary logic).
So what we have here is a way to "bootstrap" the isomorphism-invariance of first-order truth to all logics which are set-theoretically definable in a precise sense.
I'm skipping a lot of detail in the above, since quite frankly it's rather tedious. If you're interested, let me know and I'll expand on this. But I think it is worth mentioning, even if only very briefly, the existence of a precise theorem of the above type.
A: If $\mathbf{M_1}$ and $\mathbf{M_2}$ are structures for some signature $\Sigma$ (so $\Sigma = (<)$) in your example. Then, by definition, $\mathbf{M_1}$ and $\mathbf{M_2}$ are isomorphic iff there are functions $f : M_1 \to M_2$ and $g : M_2 \to M_1$ (where $M_i$ is the universe of discourse of $\mathbf{M_i}$), such that $g \circ f = 1_{M_1}$ and $g \circ f = 1_{M_2}$ and such that $f$ and $g$ are homomorphisms for the relations and functions in $\Sigma$ (so, in your example, $x < y$ iff $f(x) < g(y)$ and $u < v$ iff $g(u) < g(v)$). So if $\mathbf{M_1}$ and $\mathbf{M_2}$ are isomorphic, a logical language $\cal L$ (first-order or higher-order) over the signature $\Sigma$ cannot distinguish between $\mathbf{M_1}$ and $\mathbf{M_2}$, since $f$ induces a truth-preserving mapping from interpretations of $\cal L$ in  $\mathbf{M_1}$ and interpretations of $\cal L$ in $\mathbf{M_2}$ (and vice versa for $g$).
