1
$\begingroup$

I'm trying to formalize vectorspaces in a proof checker (Coq), and that means one does not get away with forgetting to state assumptions, etc.

Many proofs of $a{\bf 0} = {\bf 0}$, for instance here and here assume without any explicit justification that $$a {\bf 0} = a({\bf 0} + {\bf 0} )$$ How is this derived purely from the vectorspace axioms?

In more techical terms, I have a function $scal : R\rightarrow V \rightarrow V$ and an equivalence relation $equ : V \rightarrow V \rightarrow Prop$ with infix notation $==$. I want to prove that $$\forall a, {\bf u}\ == {\bf v} \implies a{\bf u} == a{\bf v}$$ i.e. that one can "rewrite" in the arguments of the scalar multiplication. However, this is usually not stated as an axiom, and seems to be silently assumed in many pen-and-paper proofs. So do I have to add some more assumption about $scal$ than is usually given in the vectorspace axioms, or can $a {\bf 0} = a({\bf 0} + {\bf 0} )$ be proved purely from the axioms?

To moderators: I asked a related question about this earlier, and got some comments (which had the same problem as above) but the question was removed by the moderators. If you are again removing this question, please let me know why this is an irrelevant question for math.stackexchange.com as I'm new to this forum.

Update: (Sorry if my use of the word "respectful" below is not the standard name, it is what the property happens to be called in the software I'm using) @Hagen von Eitzen says that the unstated assumption is that scalar multiplication is "respectful" of the equivalence; $\forall P x y, x == y \implies P(x) == P(y)$. I wonder if it is not a more complicated assumption than necessary, as "respectfulness" with respect to scalar multiplication is implied by $$ {\bf v} == {\bf 0} \implies a \cdot {\bf v} == {\bf 0} \qquad (1)$$ If that is the case, I think it would make more sense to say (1) explicitly rather than silently assuming "respectfulness". As this is not usually stated, I still wonder if there is a proof of the above that does not rest upon "respectfulness" (making it circular).

$\endgroup$
2
  • 4
    $\begingroup$ The mentioned property of "$==$" is "silently assumed" by using "$=$" instead, whereby $a=b\to (\phi(a)\leftrightarrow \phi(b))$ for any predicate $\phi$ $\endgroup$ Commented Sep 15, 2020 at 21:13
  • $\begingroup$ That is what I below called being ”respectful” of the equivalence relation. I was hoping to be able to avoid that assumption. A similar adsumption is necessary for vector addition but not for negation so I was hoping it wasnt necessary. And also, a(0+0)==a(0) seems to imply it. $\endgroup$
    – larsr
    Commented Sep 15, 2020 at 21:35

2 Answers 2

2
$\begingroup$

From the axioms, $0+b=b$ for all $b$ (recall that a vector space is in particlar an abelian group with addition where $0$ is the neutral element), so in particular, setting $b=0$ we have $0+0=0$. Therefore $a0=a(0+0)$.

$\endgroup$
7
  • $\begingroup$ No, it is that last step that requires some unstated assumption to be valid. Ie that scalar multiplication is respectful to the equivalence relation - which is what I wanted to prove in the first place. $\endgroup$
    – larsr
    Commented Sep 15, 2020 at 21:27
  • 1
    $\begingroup$ @larsr It seemed to me that you only needed to show what I wrote. The fact that $au=av$ if $v=u$ is set-theoretic. $av$ is the image of a map $k\times V\to V$. For this map to be well-defined as a map of sets, it needs to satisfy $au=av$ whenever $u=v$. $\endgroup$
    – Javi
    Commented Sep 16, 2020 at 11:38
  • $\begingroup$ It can also be seen as an assumption of mathematical logic as Hagen von Eitzen commented. $\endgroup$
    – Javi
    Commented Sep 16, 2020 at 11:44
  • 1
    $\begingroup$ If you're not going to assume classical logic, then you should specify which system of logic you're operating in and post this as a separate logic qusetion. $\endgroup$
    – Thorgott
    Commented Sep 16, 2020 at 16:06
  • 1
    $\begingroup$ This is a correct answer. The axiom in Coq that lets you multiply both sides by a is called f_equal. $\endgroup$
    – user581023
    Commented Sep 17, 2020 at 12:34
0
$\begingroup$

Using the axioms from wikipedia.

Let us call a vector $\bf z$ a zero if $\forall \mathbf{v}, \mathbf{v} + \mathbf{z} = \mathbf{z}$.

Lemma All zeros are equal.

proof: Let $\mathbf{z}, \mathbf{z'}$ be zeros. Then using commutativity of vector addition we have $\mathbf{z} = \mathbf{z} + \mathbf{z'} = \mathbf{z'} + \mathbf{z} = \mathbf{z'}$.

Proposition For any $\mathbf{v}$, $\mathbf{v} = 1 \cdot \mathbf{v} = (0 + 1) \cdot \mathbf{v} = 0 \cdot \mathbf{v} + 1 \cdot \mathbf{v} = 0 \cdot \mathbf{v} + \mathbf{v}$.

Theorem $0 \cdot \mathbf v = \mathbf 0$.

proof: By the proposition we have that $0 \cdot \mathbf v$ is a zero. And by definition $\mathbf 0$ is a zero, so by the lemma they are equal.


Edit: To prove that $c \cdot (\mathbf{0} + \mathbf{0}) = c \cdot \mathbf{0}$ start with $\mathbf{0} + \mathbf{0} = \mathbf{0}$ from "Identity element" axiom and the apply the function $\lambda \mathbf{v}. (c \cdot \mathbf{v})$ to both sides of the equation.

$\endgroup$
7
  • $\begingroup$ Again, this proof is circular in that it assumes the thing I wanted to prove, i.e. that you can change the vector on the right side of the scalar multiplication under the given equivalence relation. BTW, 1 is not a vector but a scalar, and ${\bf 0}$ is a vector $\endgroup$
    – larsr
    Commented Sep 16, 2020 at 9:06
  • $\begingroup$ In the context of the OP, $0$ means the $0$ vector, so you can't do that because there might no be a $1$ vector. $\endgroup$
    – Javi
    Commented Sep 16, 2020 at 11:40
  • 1
    $\begingroup$ @larsr please state your axioms. i.e. paste your Coq code $\endgroup$
    – user581023
    Commented Sep 16, 2020 at 14:26
  • $\begingroup$ @rain1 I'm using the 8 axioms from Wikipedia Vectorspace $\endgroup$
    – larsr
    Commented Sep 16, 2020 at 14:43
  • $\begingroup$ @larsr cool, hows this? $\endgroup$
    – user581023
    Commented Sep 16, 2020 at 15:52

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .