Formal specification of vector space. The declaration of a field as a triplet $(\mathbb{K},\oplus,\odot)$ is canonical and in every book I've read, the definition of field is written using it. I can use this notation to describe any field in a strict and technical way. For example, this is how I can describe the finite field $\Bbb{Z}_2$:
$(\Bbb{Z}_2:=\{0,1\},\\\ \oplus:\Bbb{Z}_2^2\to\Bbb{Z}_2:=(x+y)\mod2,\\\
\odot:\Bbb{Z}_2^2\to\Bbb{Z}_2:=(x\cdot y)\mod2)$
I'm looking for a likewise technically strict way to describe a vector space over a field, since I've only found verbose specifications in common language (e.g., "a vector space $\mathbb{V}$ with operations $\oplus$ and $\odot$ over a field $\mathbb{k}$ with operations $+$ and $\cdot$").
There is any formal notation in which I can specify a vector space in few words (actually, in no words at all) as I do with fields?
 A: Formally, I don't see any additional challenge (of course, it gets more verbose, because you have more things to ask).

Given a field $(\Bbb F,\oplus,\odot)$ a triple $(V,+,\cdot)$ is a $(\Bbb F,\oplus,\odot)$-vector space if and only if:
  
  
*
  
*$(V,+)$ is an abelian group (= verbose subdefinition)
  
*$\cdot:\Bbb F\times V\to V$ and $+:V\times V\to V$ satisfy:
  
  
*
  
*$\forall \alpha,\beta\in\Bbb K,\forall x\in V,\ (a\odot b)\cdot v=a\cdot(b\cdot v)$ or, if you want to be more formal, $\cdot(\odot(a,b),x)=\cdot(a,\cdot(b,x))$
  
*$\forall \alpha,\beta\in\Bbb K,\forall x\in V,\ (a\oplus b)\cdot x=(a\cdot x)+(b\cdot x)$ or, if you want to be more formal, $\cdot(\oplus(a,b),x)=+(\cdot(a,x),\cdot(b,x))$
  
*$\forall x\in V,\ 1_{\Bbb F}\cdot x=x$
  
*$\forall \alpha\in\Bbb K,\forall x,y\in V,\ \alpha\cdot(x+y)=(\alpha\cdot x)+(\beta\cdot y)$ or, if you want to be more formal, $\cdot(\alpha,+(x,y))=+(\cdot(\alpha,x),\cdot(\alpha,y))$
  
  

Typically, mathematicians (and anyone who has clear in mind what is what) swiftly adopt the big boys' notation $+:=\oplus$, $\text{nothing}:=\cdot:=\odot$, $0:=0_V$ and $0:= 0_{\Bbb F}$. This, basically because the aforementioned formal properties have the consequence of making such identifications harmless, as long as you have a way to distinguish vectors from scalars. This is acheived by noticing that, as long as multiplication by scalar acts on the left and you don't introduce a "dot product of two vectors", the only way to make sense of a "monomial" such as $abcd\in V$ is by assuming $a,b,c\in \Bbb F$ and $d\in V$, thus reading it $(a\odot b\odot c)\cdot d$. Similarly for $x(a+b)(c+d)=(x\odot(a\oplus b))\cdot (c+d)$
A: I think one thing you're missing is that the term "vector space" doesn't really have a definition.  What has a definition is the term "vector space over $(K,+,\cdot)$", where $(K,+,\cdot)$ is some field.  So, if $(K,+,\cdot)$ is a field, then a vector space over $(K,+,\cdot)$ is defined as a triple $(V,\oplus,\odot)$ where $V$ is a set, $\oplus:V\times V\to V$, $\odot:K\times V\to V$, and a certain long list of axioms are satified.  This is really a separate definition for every single field $(K,+,\cdot)$.
If you really want to have a definition of "vector space" without specifying the field beforehand (and this is not how people normally talk about vector spaces), you could define it as a tuple $(V,\oplus,\odot,K,+,\cdot)$ where $V$ and $K$ are sets, $\oplus:V\times V\to V$, $\odot:K\times V\to V$, $+:K\times K\to K$, $\cdot:K\times K\to K$, and an even longer list of axioms are satisfied.
