How to treat an isomorphism between vector spaces as an isomorphism between many sorted structures According to this PDF, p.29, a vector space is a strict many sorted structure, where strict means that the scalar set and the vector set are disjoint (the definition is here, p.23).
For any field $K$, however, $K$ is also a vector space over $K$ and the scalar set and the vector set are the same, and therefore not disjoint.
So we have to adopt a lax structure, where lax means not-strict(the definition is here, p.23), to formalize this vector space as many sorted structure.
But if we adopt a lax structure, (it seems to me) another problem arises.
Let $V$ be a one-dimensional vector space over $K$ satisfying $V \cap K = \emptyset$.
It is well known that $V$ is isomorphic to the vector space $K$ mentioned above.
But we cannot create the isomorphism between $V$ and $K$ as an isomorphism between many sorted structures(the definition is here, p.40), because if $\pi: K \cup V \to K \cup K = K$ is a isomorphism, $\pi\upharpoonright K: K \to K$ must be a bijection, but this is impossible since $\pi$ is a bijection between $K \cup V$ and $K$.
So I think we must modify or extend the definition of an isomorphism between many sorted structure to treat an isomorphism between vector spaces as an isomorphism between many sorted structures.
I would appreciate it if you could show me how to do this.
 A: My personal take is that the distinction between strict and lax structures is abstraction-breaking because we're checking equality across sorts. That being said, it seems like a good distinction to have for pragmatic purposes because it lets us know exactly how careful we have to be when building a model out of set-theoretic raw materials.
You can turn any lax many-sorted structure into a strict many-sorted structure in a straightforward, fairly brute-force way. For this reason, hypothesizing a strict model satisfying some theory is not really making a stronger claim than hypothesizing a lax one.
This is conceptually analogous to emulating a statically typed programming language in a dynamically typed programming language by tagging every value with its formerly-static type.
The definition of a many-sorted logic given on page 93 restricts us to finitely many sorts. We don't need the assumption of finitely many sorts, but it prevents us from needing to talk about ordinals explicitly.
We can define the following map $\varphi$ on each of the sorts.
If $s$ is in $M_n$, the $n$th sort, then let $\varphi(s)$ be equal to $(n, s)_K$ where $(\cdot, \cdot)_K$ denote the Kuratowski pair.
Let $\varphi$ perform similar replacements in the interpretation of every relation, function, and constant symbol.
$\varphi$ is an isomorphism when looking at each sort individually.
However, it has the nice property that we force every pair of elements of the original model that were in different sorts to have different first elements in their new interpretation.
