I'm attempting to come up with a first order language $L$ that is able to describe vector spaces over fields. I came up with a few sets of nonlogical symbols.

$Rs_L=\{Scal,Vec\}$ where $Scal,Vec$ are unary relation symbols which I interpret to be true or false depending on whether $x$ is a scalar or vector.

Also, $Fs_L=\{+,\cdot,\}$ which are the usual addition and multiplication for both vectors and scalars.

For constant symbols, $Cs_L=\{0,1,0_V\}$, where $0$ and $1$ are regular field scalars for the additive and multiplicative identities, respectively, and $0_V$ is the additive identity for vectors.

Using these, I was able to formulate axioms for scalar multiplication on a given structure, and I define addition between a scalar and a vector to simply always give the 0 vector and define multiplication between two vectors to always be the 0 vector. This gives a theory such that a structure models it if and only if it is a vector space in the regular algebraic sense. It is easy to see that all linear transformations in the algebraic sense are included in the class of homomorphisms (in the logical sense), but I am having difficulty proving they are the only ones in this class.

I suppose I want to show that for any $L$-homomorphism $T$, $T(av+w)=aTv+Tw$ for $a$ a scalar and $v,w$ vectors. Since $T$ is a homomorphism, I see that $T(av+w)=Tav+Tw=TaTv+Tw$, so it would be enough to show that all homomorphisms act as the identity on all scalars? Is there a way to show this, or an extra axiom to include?


2 Answers 2


If you work in two-sorted first-order logic, it is possible to formalize vector spaces by using one sort for the field of scalars and another sort for the vectors, just as you describe. But there is no way, within the theory itself, to force an embedding of models to act as the identity on the scalars. For example, if you take a structure for your theory, every automorphism of the field will give a homomorphism from the structure to itself. And every proper subfield of the field of scalars gives rise to a proper substructure in which the vectors remain the same and the scalars are cut down. This is the motivation for the usual method in which the field is fixed through the addition of a lot of constant symbols to the language.

One response is to simply refuse to consider such things when you work on your proofs. That is, you could simply limit your attention to those homomorphisms that do preserve the field, and those substructures that do not change the field. It depends on what you are trying to get out of the formalization.


It's not clear what your motivations are but, in any case, I thought it would be worthwhile to point out that usually the most convenient way to specify a vector space is to view it as a "group with operators", i.e. for each scalar $c\:$ introduce a unary operation $\ c(v) = c\:v\:$.

  • $\begingroup$ You are exactly right if one is trying to devise a language for vector spaces over some fixed field $K$, but I am trying to find a language for any vector space over any field. Since there exist fields for any infinite cardinal number, I must resort to fitting the field into the structure, and somehow making axioms that give me the notion of a vector space and give $L$-homomorphisms that coincide with the linear algebraic notion of linear map. I have been trying a sorting method with limited success. $\endgroup$
    – anonymous
    Oct 20, 2010 at 4:57
  • $\begingroup$ I think simply adding operator would create uncountable function symbols. Making it became uncountable language.... $\endgroup$
    – Shore
    Jan 15 at 2:54

You must log in to answer this question.